Step
*
1
1
2
1
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. (r = 0 ∈ ℤ) ∧ (c1 = z3 ∈ Cmd) ∧ (e1 = e3 ∈ E)
43. loc(e2) ↓∈ reps
44. e' : E
45. e' ≤loc e2
46. z2 : Cmd
47. ((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))
48. ¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))
49. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) n between e' and e2)
50. l2 ↓∈ reps
51. d2 = 0 ∈ ℤ
52. ff = ff
53. sender = loc(e2) ∈ Id
54. (r = 0 ∈ ℤ) ∧ (c2 = z2 ∈ Cmd) ∧ (e2 = e' ∈ E)
55. e' = e3 ∈ E
⊢ c1 = c2 ∈ Cmd
BY
{ (DProdsAndUnions
THEN Try (Complete ((Assert ⌈<n, z3> = <n, z2> ∈ (ℤ × Cmd)⌉⋅ THEN Auto)))
THEN Try (Complete (((Assert ⌈propose = ``new_23_sig vote`` ∈ Name⌉⋅ THENA Auto) THEN DiffHeaders)))
THEN Try (Complete ((Assert ⌈msgval(e') = msgval(e3) ∈ (ℤ × ℤ × Cmd × Id)⌉⋅ THEN Auto)))) }
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. (r = 0) \mwedge{} (c1 = z3) \mwedge{} (e1 = e3)
43. loc(e2) \mdownarrow{}\mmember{} reps
44. e' : E
45. e' \mleq{}loc e2
46. z2 : Cmd
47. ((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'))))))
48. \mneg{}\muparrow{}(set-sig-member(slots) n new\_23\_sig\_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))
49. (no new\_23\_sig\_Notify(Cmd;clients;notify;propose;f) n between e' and e2)
50. l2 \mdownarrow{}\mmember{} reps
51. d2 = 0
52. ff = ff
53. sender = loc(e2)
54. (r = 0) \mwedge{} (c2 = z2) \mwedge{} (e2 = e')
55. e' = e3
\mvdash{} c1 = c2
By
Latex:
(DProdsAndUnions
THEN Try (Complete ((Assert \mkleeneopen{}<n, z3> = <n, z2>\mkleeneclose{}\mcdot{} THEN Auto)))
THEN Try (Complete (((Assert \mkleeneopen{}propose = ``new\_23\_sig vote``\mkleeneclose{}\mcdot{} THENA Auto) THEN DiffHeaders)))
THEN Try (Complete ((Assert \mkleeneopen{}msgval(e') = msgval(e3)\mkleeneclose{}\mcdot{} THEN Auto))))
Home
Index