Step
*
1
1
2
4
2
of Lemma
new_23_sig_votes_consistent
1. Cmd : Type
2. valueall-type(Cmd)
3. cmdeq : EqDecider(Cmd)
4. reps : bag(Id)
5. clients : bag(Id)
6. coeff : ℤ
7. flrs : ℤ
8. notify : Atom List
9. propose : Atom List
10. slots : set-sig{i:l}(ℤ)
11. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)
12. (f propose) = (ℤ × Cmd) ∈ Type
13. (f notify) = (ℤ × Cmd) ∈ Type
14. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
15. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
16. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
17. f ∈ Name ─→ Type
18. es : EO+(Message(f))
19. new_23_sig_message-constraint{i:l}(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f)@i'
20. e1 : E@i
21. e2 : E@i
22. n : ℤ@i
23. r : ℤ@i
24. sender : Id@i
25. l1 : Id@i
26. l2 : Id@i
27. c1 : Cmd@i
28. c2 : Cmd@i
29. d1 : ℤ@i
30. d2 : ℤ@i
31. loc(e1) ↓∈ reps
32. e3 : E
33. e3 ≤loc e1
34. z3 : Cmd
35. ((header(e3) = propose ∈ Name) ∧ has-es-info-type(es;e3;f;ℤ × Cmd) ∧ (<n, z3> = msgval(e3) ∈ (ℤ × Cmd)))
∨ ((header(e3) = ``new_23_sig vote`` ∈ Name)
∧ has-es-info-type(es;e3;f;ℤ × ℤ × Cmd × Id)
∧ (n = (fst(fst(fst(msgval(e3))))) ∈ ℤ)
∧ (z3 = (snd(fst(msgval(e3)))) ∈ Cmd))
36. ¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e3))
37. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) n between e3 and e1)
38. l1 ↓∈ reps
39. d1 = 0 ∈ ℤ
40. ff = ff
41. sender = loc(e1) ∈ Id
42. new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e3;e1) < r
43. ((header(e1) = ``new_23_sig retry`` ∈ Name)
∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd)
∧ (<<n, r>, c1> = msgval(e1) ∈ (ℤ × ℤ × Cmd)))
∨ ((header(e1) = ``new_23_sig vote`` ∈ Name)
∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
∧ (<<n, r>, c1> = (fst(msgval(e1))) ∈ (ℤ × ℤ × Cmd)))
44. loc(e2) ↓∈ reps
45. e' : E
46. e' ≤loc e2
47. z2 : Cmd
48. ((header(e') = propose ∈ Name) ∧ has-es-info-type(es;e';f;ℤ × Cmd) ∧ (<n, z2> = msgval(e') ∈ (ℤ × Cmd)))
∨ ((header(e') = ``new_23_sig vote`` ∈ Name)
∧ has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
∧ (n = (fst(fst(fst(msgval(e'))))) ∈ ℤ)
∧ (z2 = (snd(fst(msgval(e')))) ∈ Cmd))
49. ¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))
50. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) n between e' and e2)
51. l2 ↓∈ reps
52. d2 = 0 ∈ ℤ
53. ff = ff
54. sender = loc(e2) ∈ Id
55. new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e';e2) < r
56. ((header(e2) = ``new_23_sig retry`` ∈ Name)
∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd)
∧ (<<n, r>, c2> = msgval(e2) ∈ (ℤ × ℤ × Cmd)))
∨ ((header(e2) = ``new_23_sig vote`` ∈ Name)
∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd × Id)
∧ (<<n, r>, c2> = (fst(msgval(e2))) ∈ (ℤ × ℤ × Cmd)))
57. e' = e3 ∈ E
58. e2 = e1 ∈ E
⊢ c1 = c2 ∈ Cmd
BY
{ (D 43
THEN D 56
THEN Auto
THEN Try (Complete ((Assert ⌈msgval(e1) = msgval(e2) ∈ (ℤ × ℤ × Cmd × Id)⌉⋅ THEN Auto)))
THEN Assert ⌈``new_23_sig retry`` = ``new_23_sig vote`` ∈ Name⌉⋅
THEN Auto
THEN DiffHeaders) }
Latex:
Latex:
1. Cmd : Type
2. valueall-type(Cmd)
3. cmdeq : EqDecider(Cmd)
4. reps : bag(Id)
5. clients : bag(Id)
6. coeff : \mBbbZ{}
7. flrs : \mBbbZ{}
8. notify : Atom List
9. propose : Atom List
10. slots : set-sig\{i:l\}(\mBbbZ{})
11. f : new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose)
12. (f propose) = (\mBbbZ{} \mtimes{} Cmd)
13. (f notify) = (\mBbbZ{} \mtimes{} Cmd)
14. (f ``new\_23\_sig decided``) = (\mBbbZ{} \mtimes{} Cmd)
15. (f ``new\_23\_sig retry``) = (\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)
16. (f ``new\_23\_sig vote``) = (\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)
17. f \mmember{} Name {}\mrightarrow{} Type
18. es : EO+(Message(f))
19. new\_23\_sig\_message-constraint\{i:l\}(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f)@i'
20. e1 : E@i
21. e2 : E@i
22. n : \mBbbZ{}@i
23. r : \mBbbZ{}@i
24. sender : Id@i
25. l1 : Id@i
26. l2 : Id@i
27. c1 : Cmd@i
28. c2 : Cmd@i
29. d1 : \mBbbZ{}@i
30. d2 : \mBbbZ{}@i
31. loc(e1) \mdownarrow{}\mmember{} reps
32. e3 : E
33. e3 \mleq{}loc e1
34. z3 : Cmd
35. ((header(e3) = propose) \mwedge{} has-es-info-type(es;e3;f;\mBbbZ{} \mtimes{} Cmd) \mwedge{} (<n, z3> = msgval(e3)))
\mvee{} ((header(e3) = ``new\_23\_sig vote``)
\mwedge{} has-es-info-type(es;e3;f;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)
\mwedge{} (n = (fst(fst(fst(msgval(e3))))))
\mwedge{} (z3 = (snd(fst(msgval(e3))))))
36. \mneg{}\muparrow{}(set-sig-member(slots) n new\_23\_sig\_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e3))
37. (no new\_23\_sig\_Notify(Cmd;clients;notify;propose;f) n between e3 and e1)
38. l1 \mdownarrow{}\mmember{} reps
39. d1 = 0
40. ff = ff
41. sender = loc(e1)
42. new\_23\_sig\_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e3;e1) < r
43. ((header(e1) = ``new\_23\_sig retry``)
\mwedge{} has-es-info-type(es;e1;f;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)
\mwedge{} (<<n, r>, c1> = msgval(e1)))
\mvee{} ((header(e1) = ``new\_23\_sig vote``)
\mwedge{} has-es-info-type(es;e1;f;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)
\mwedge{} (<<n, r>, c1> = (fst(msgval(e1)))))
44. loc(e2) \mdownarrow{}\mmember{} reps
45. e' : E
46. e' \mleq{}loc e2
47. z2 : Cmd
48. ((header(e') = propose) \mwedge{} has-es-info-type(es;e';f;\mBbbZ{} \mtimes{} Cmd) \mwedge{} (<n, z2> = msgval(e')))
\mvee{} ((header(e') = ``new\_23\_sig vote``)
\mwedge{} has-es-info-type(es;e';f;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)
\mwedge{} (n = (fst(fst(fst(msgval(e'))))))
\mwedge{} (z2 = (snd(fst(msgval(e'))))))
49. \mneg{}\muparrow{}(set-sig-member(slots) n new\_23\_sig\_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))
50. (no new\_23\_sig\_Notify(Cmd;clients;notify;propose;f) n between e' and e2)
51. l2 \mdownarrow{}\mmember{} reps
52. d2 = 0
53. ff = ff
54. sender = loc(e2)
55. new\_23\_sig\_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e';e2) < r
56. ((header(e2) = ``new\_23\_sig retry``)
\mwedge{} has-es-info-type(es;e2;f;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)
\mwedge{} (<<n, r>, c2> = msgval(e2)))
\mvee{} ((header(e2) = ``new\_23\_sig vote``)
\mwedge{} has-es-info-type(es;e2;f;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)
\mwedge{} (<<n, r>, c2> = (fst(msgval(e2)))))
57. e' = e3
58. e2 = e1
\mvdash{} c1 = c2
By
Latex:
(D 43
THEN D 56
THEN Auto
THEN Try (Complete ((Assert \mkleeneopen{}msgval(e1) = msgval(e2)\mkleeneclose{}\mcdot{} THEN Auto)))
THEN Assert \mkleeneopen{}``new\_23\_sig retry`` = ``new\_23\_sig vote``\mkleeneclose{}\mcdot{}
THEN Auto
THEN DiffHeaders)
Home
Index