Step
*
2
1
of Lemma
new_23_sig_quorum_mem
1. Cmd : {T:Type| valueall-type(T)} @i'
2. notify : Atom List@i
3. propose : Atom List@i
4. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)@i'
5. (f propose) = (ℤ × Cmd) ∈ Type
6. (f notify) = (ℤ × Cmd) ∈ Type
7. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
8. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
9. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
10. f ∈ Name ─→ Type
11. es : EO+(Message(f))@i'
12. e1 : E@i
13. e2 : E@i
14. ni : ℤ × ℤ@i
15. s1 : Cmd List × (Id List)@i
16. s2 : Cmd List × (Id List)@i
17. v : ℤ × ℤ × Cmd × Id@i
18. (e1 <loc e2)@i
19. v ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e1)@i
20. s1 ∈ Memory-loc-class(new_23_sig_add_to_quorum(Cmd) ni;λloc.{<[], []>};new_23_sig_vote'base(Cmd;notify;propose;f))(
e1)
21. s2 ∈ Memory-loc-class(new_23_sig_add_to_quorum(Cmd) ni;λloc.{<[], []>};new_23_sig_vote'base(Cmd;notify;propose;f))(
e2)
22. a1 : ℤ × ℤ × Cmd × Id@i
23. a2 : ℤ × ℤ × Cmd × Id@i
24. s3 : Cmd List × (Id List)@i
25. s4 : Cmd List × (Id List)@i
26. e : E@i
27. e' : E@i
28. e1 ≤loc e @i
29. (e <loc e')@i
30. (e' <loc e2)@i
31. a1 ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e)@i
32. s3 ∈ Memory-loc-class(new_23_sig_add_to_quorum(Cmd) ni;λloc.{<[], []>};new_23_sig_vote'base(Cmd;notify;propose;f))(
e)@i
33. a2 ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')@i
34. s4 ∈ Memory-loc-class(new_23_sig_add_to_quorum(Cmd) ni;λloc.{<[], []>};new_23_sig_vote'base(Cmd;notify;propose;f))(
e')@i
35. let cmds1,locs1 = s3
in let cmds2,locs2 = s4
in let x,i = a1
in let ni',c = x
in (ni = ni' ∈ (ℤ × ℤ)) ⇒ ((i ∈ locs2) ∧ ((¬(i ∈ locs1)) ⇒ (c ∈ cmds2)))@i
⊢ let cmds1,locs1 = s3
in let cmds2,locs2 = new_23_sig_add_to_quorum(Cmd) ni loc(e2) a2 s4
in let x,i = a1
in let ni',c = x
in (ni = ni' ∈ (ℤ × ℤ)) ⇒ ((i ∈ locs2) ∧ ((¬(i ∈ locs1)) ⇒ (c ∈ cmds2)))
BY
{ (DProdsAndUnions THEN All Reduce) }
1
1. Cmd : {T:Type| valueall-type(T)} @i'
2. notify : Atom List@i
3. propose : Atom List@i
4. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)@i'
5. (f propose) = (ℤ × Cmd) ∈ Type
6. (f notify) = (ℤ × Cmd) ∈ Type
7. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
8. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
9. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
10. f ∈ Name ─→ Type
11. es : EO+(Message(f))@i'
12. e1 : E@i
13. e2 : E@i
14. n1 : ℤ@i
15. n2 : ℤ@i
16. s11 : Cmd List@i
17. s12 : Id List@i
18. s9 : Cmd List@i
19. s10 : Id List@i
20. v5 : ℤ@i
21. v6 : ℤ@i
22. v4 : Cmd@i
23. v2 : Id@i
24. (e1 <loc e2)@i
25. <<<v5, v6>, v4>, v2> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e1)@i
26. <s11, s12> ∈ Memory-loc-class(new_23_sig_add_to_quorum(Cmd) <n1, n2>;λloc.{<[], []>};new_23_sig_vote'base(Cmd;notify\000C;propose;f))(e1)
27. <s9, s10> ∈ Memory-loc-class(new_23_sig_add_to_quorum(Cmd) <n1, n2>;λloc.{<[], []>};new_23_sig_vote'base(Cmd;notify;\000Cpropose;f))(e2)
28. a13 : ℤ@i
29. a14 : ℤ@i
30. a10 : Cmd@i
31. a6 : Id@i
32. a11 : ℤ@i
33. a12 : ℤ@i
34. a8 : Cmd@i
35. a4 : Id@i
36. s7 : Cmd List@i
37. s8 : Id List@i
38. s5 : Cmd List@i
39. s6 : Id List@i
40. e : E@i
41. e' : E@i
42. e1 ≤loc e @i
43. (e <loc e')@i
44. (e' <loc e2)@i
45. <<<a13, a14>, a10>, a6> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e)@i
46. <s7, s8> ∈ Memory-loc-class(new_23_sig_add_to_quorum(Cmd) <n1, n2>;λloc.{<[], []>};new_23_sig_vote'base(Cmd;notify;p\000Cropose;f))(e)@i
47. <<<a11, a12>, a8>, a4> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')@i
48. <s5, s6> ∈ Memory-loc-class(new_23_sig_add_to_quorum(Cmd) <n1, n2>;λloc.{<[], []>};new_23_sig_vote'base(Cmd;notify;p\000Cropose;f))(e')@i
49. (<n1, n2> = <a13, a14> ∈ (ℤ × ℤ)) ⇒ ((a6 ∈ s6) ∧ ((¬(a6 ∈ s8)) ⇒ (a10 ∈ s5)))@i
⊢ let cmds2,locs2 = new_23_sig_add_to_quorum(Cmd) <n1, n2> loc(e2) <<<a11, a12>, a8>, a4> <s5, s6>
in (<n1, n2> = <a13, a14> ∈ (ℤ × ℤ)) ⇒ ((a6 ∈ locs2) ∧ ((¬(a6 ∈ s8)) ⇒ (a10 ∈ cmds2)))
Latex:
Latex:
1. Cmd : \{T:Type| valueall-type(T)\} @i'
2. notify : Atom List@i
3. propose : Atom List@i
4. f : new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose)@i'
5. (f propose) = (\mBbbZ{} \mtimes{} Cmd)
6. (f notify) = (\mBbbZ{} \mtimes{} Cmd)
7. (f ``new\_23\_sig decided``) = (\mBbbZ{} \mtimes{} Cmd)
8. (f ``new\_23\_sig retry``) = (\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)
9. (f ``new\_23\_sig vote``) = (\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)
10. f \mmember{} Name {}\mrightarrow{} Type
11. es : EO+(Message(f))@i'
12. e1 : E@i
13. e2 : E@i
14. ni : \mBbbZ{} \mtimes{} \mBbbZ{}@i
15. s1 : Cmd List \mtimes{} (Id List)@i
16. s2 : Cmd List \mtimes{} (Id List)@i
17. v : \mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id@i
18. (e1 <loc e2)@i
19. v \mmember{} new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e1)@i
20. s1 \mmember{} Memory-loc-class(new\_23\_sig\_add\_to\_quorum(Cmd)
ni;\mlambda{}loc.\{<[], []>\};new\_23\_sig\_vote'base(Cmd;notify;propose;f))(e1)
21. s2 \mmember{} Memory-loc-class(new\_23\_sig\_add\_to\_quorum(Cmd)
ni;\mlambda{}loc.\{<[], []>\};new\_23\_sig\_vote'base(Cmd;notify;propose;f))(e2)
22. a1 : \mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id@i
23. a2 : \mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id@i
24. s3 : Cmd List \mtimes{} (Id List)@i
25. s4 : Cmd List \mtimes{} (Id List)@i
26. e : E@i
27. e' : E@i
28. e1 \mleq{}loc e @i
29. (e <loc e')@i
30. (e' <loc e2)@i
31. a1 \mmember{} new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e)@i
32. s3 \mmember{} Memory-loc-class(new\_23\_sig\_add\_to\_quorum(Cmd)
ni;\mlambda{}loc.\{<[], []>\};new\_23\_sig\_vote'base(Cmd;notify;propose;f))(e)@i
33. a2 \mmember{} new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e')@i
34. s4 \mmember{} Memory-loc-class(new\_23\_sig\_add\_to\_quorum(Cmd)
ni;\mlambda{}loc.\{<[], []>\};new\_23\_sig\_vote'base(Cmd;notify;propose;f))(e')@i
35. let cmds1,locs1 = s3
in let cmds2,locs2 = s4
in let x,i = a1
in let ni',c = x
in (ni = ni') {}\mRightarrow{} ((i \mmember{} locs2) \mwedge{} ((\mneg{}(i \mmember{} locs1)) {}\mRightarrow{} (c \mmember{} cmds2)))@i
\mvdash{} let cmds1,locs1 = s3
in let cmds2,locs2 = new\_23\_sig\_add\_to\_quorum(Cmd) ni loc(e2) a2 s4
in let x,i = a1
in let ni',c = x
in (ni = ni') {}\mRightarrow{} ((i \mmember{} locs2) \mwedge{} ((\mneg{}(i \mmember{} locs1)) {}\mRightarrow{} (c \mmember{} cmds2)))
By
Latex:
(DProdsAndUnions THEN All Reduce)
Home
Index