Step
*
2
1
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. 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)))
BY
{ (RepUR ``new_23_sig_add_to_quorum new_23_sig_newvote`` 0 THEN RepeatFor 3 (AutoSplit)) }
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. ¬(a4 ∈ s6)
41. e : E@i
42. e' : E@i
43. e1 ≤loc e @i
44. (e <loc e')@i
45. (e' <loc e2)@i
46. <<<a13, a14>, a10>, a6> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e)@i
47. <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
48. <<<a11, a12>, a8>, a4> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')@i
49. <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
50. (<n1, n2> = <a13, a14> ∈ (ℤ × ℤ)) ⇒ ((a6 ∈ s6) ∧ ((¬(a6 ∈ s8)) ⇒ (a10 ∈ s5)))@i
51. n1 = a11 ∈ ℤ
52. n2 = a12 ∈ ℤ
⊢ (<n1, n2> = <a13, a14> ∈ (ℤ × ℤ)) ⇒ ((a6 ∈ [a4 / s6]) ∧ ((¬(a6 ∈ s8)) ⇒ (a10 ∈ [a8 / s5])))
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. n1 : \mBbbZ{}@i
15. n2 : \mBbbZ{}@i
16. s11 : Cmd List@i
17. s12 : Id List@i
18. s9 : Cmd List@i
19. s10 : Id List@i
20. v5 : \mBbbZ{}@i
21. v6 : \mBbbZ{}@i
22. v4 : Cmd@i
23. v2 : Id@i
24. (e1 <loc e2)@i
25. <<<v5, v6>, v4>, v2> \mmember{} new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e1)@i
26. <s11, s12> \mmember{} Memory-loc-class(new\_23\_sig\_add\_to\_quorum(Cmd)
<n1, n2>\mlambda{}loc.\{<[]
, []
>\};new\_23\_sig\_vote'base(Cmd;notify;propose;f))(e1)
27. <s9, s10> \mmember{} Memory-loc-class(new\_23\_sig\_add\_to\_quorum(Cmd)
<n1, n2>\mlambda{}loc.\{<[]
, []
>\};new\_23\_sig\_vote'base(Cmd;notify;propose;f))(e2)
28. a13 : \mBbbZ{}@i
29. a14 : \mBbbZ{}@i
30. a10 : Cmd@i
31. a6 : Id@i
32. a11 : \mBbbZ{}@i
33. a12 : \mBbbZ{}@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 \mleq{}loc e @i
43. (e <loc e')@i
44. (e' <loc e2)@i
45. <<<a13, a14>, a10>, a6> \mmember{} new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e)@i
46. <s7, s8> \mmember{} Memory-loc-class(new\_23\_sig\_add\_to\_quorum(Cmd) <n1, n2>\mlambda{}loc.\{<[], []>\};new\_23\_sig\_vo\000Cte'base(Cmd;notify;propose;f))(
e)@i
47. <<<a11, a12>, a8>, a4> \mmember{} new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e')@i
48. <s5, s6> \mmember{} Memory-loc-class(new\_23\_sig\_add\_to\_quorum(Cmd) <n1, n2>\mlambda{}loc.\{<[], []>\};new\_23\_sig\_vo\000Cte'base(Cmd;notify;propose;f))(
e')@i
49. (<n1, n2> = <a13, a14>) {}\mRightarrow{} ((a6 \mmember{} s6) \mwedge{} ((\mneg{}(a6 \mmember{} s8)) {}\mRightarrow{} (a10 \mmember{} s5)))@i
\mvdash{} 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>) {}\mRightarrow{} ((a6 \mmember{} locs2) \mwedge{} ((\mneg{}(a6 \mmember{} s8)) {}\mRightarrow{} (a10 \mmember{} cmds2)))
By
Latex:
(RepUR ``new\_23\_sig\_add\_to\_quorum new\_23\_sig\_newvote`` 0 THEN RepeatFor 3 (AutoSplit))
Home
Index