Step
*
1
1
of Lemma
new_23_sig_quorum_inv_vote2
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. e : E@i
13. n1 : ℤ@i
14. n2 : ℤ@i
15. p1 : Cmd List@i
16. p2 : Id List@i
17. <p1, p2> ∈ Memory-loc-class(new_23_sig_add_to_quorum(Cmd) <n1, n2>;λloc.{<[], []>};new_23_sig_vote'base(Cmd;notify;p\000Cropose;f))(e)
18. a5 : ℤ@i
19. a6 : ℤ@i
20. a4 : Cmd@i
21. a2 : Id@i
22. e' : E@i
23. s1 : Cmd List@i
24. s2 : Id List@i
25. (e' <loc e)@i
26. <<<a5, a6>, a4>, a2> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')@i
27. <s1, s2> ∈ 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
28. no_repeats(Id;s2)@i
29. ||s2|| = ||s1|| ∈ ℤ@i
30. ∀i:ℕ||s2||
(↓∃e':E
((e' <loc e)
∧ <<<n1, n2>, s1[i]>, s2[i]> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')
∧ (∀e''∈[es-init(es;e);e').∀c:Cmd
(¬<<<n1, n2>, c>, s2[i]> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e'')))))@i
31. n1 = a5 ∈ ℤ
32. n2 = a6 ∈ ℤ
33. ¬(a2 ∈ s2)
34. i : ℕ||s2|| + 1@i
35. i = 0 ∈ ℤ
⊢ ↓∃e':E
((e' <loc e)
∧ <<<n1, n2>, [a4 / s1][i]>, [a2 / s2][i]> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')
∧ (∀e''∈[es-init(es;e);e').∀c:Cmd
(¬<<<n1, n2>, c>, [a2 / s2][i]> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e''))))
BY
{ ((Subst ⌈i ~ 0⌉ 0⋅ THENA Auto)
THEN Reduce 0
THEN D 0
THEN InstConcl [⌈e'⌉]⋅
THEN Auto
THEN RWO "l_all_iff" 0
THEN Auto
THEN (D 0 THENA Auto)) }
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. e : E@i
13. n1 : ℤ@i
14. n2 : ℤ@i
15. p1 : Cmd List@i
16. p2 : Id List@i
17. <p1, p2> ∈ Memory-loc-class(new_23_sig_add_to_quorum(Cmd) <n1, n2>;λloc.{<[], []>};new_23_sig_vote'base(Cmd;notify;p\000Cropose;f))(e)
18. a5 : ℤ@i
19. a6 : ℤ@i
20. a4 : Cmd@i
21. a2 : Id@i
22. e' : E@i
23. s1 : Cmd List@i
24. s2 : Id List@i
25. (e' <loc e)@i
26. <<<a5, a6>, a4>, a2> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')@i
27. <s1, s2> ∈ 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
28. no_repeats(Id;s2)@i
29. ||s2|| = ||s1|| ∈ ℤ@i
30. ∀i:ℕ||s2||
(↓∃e':E
((e' <loc e)
∧ <<<n1, n2>, s1[i]>, s2[i]> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')
∧ (∀e''∈[es-init(es;e);e').∀c:Cmd
(¬<<<n1, n2>, c>, s2[i]> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e'')))))@i
31. n1 = a5 ∈ ℤ
32. n2 = a6 ∈ ℤ
33. ¬(a2 ∈ s2)
34. i : ℕ||s2|| + 1@i
35. i = 0 ∈ ℤ
36. (e' <loc e)
37. <<<n1, n2>, a4>, a2> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')
38. e'' : E@i
39. (e'' ∈ [es-init(es;e);e'))@i
40. c : Cmd@i
41. <<<n1, n2>, c>, a2> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e'')@i
⊢ False
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. e : E@i
13. n1 : \mBbbZ{}@i
14. n2 : \mBbbZ{}@i
15. p1 : Cmd List@i
16. p2 : Id List@i
17. <p1, p2> \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)
18. a5 : \mBbbZ{}@i
19. a6 : \mBbbZ{}@i
20. a4 : Cmd@i
21. a2 : Id@i
22. e' : E@i
23. s1 : Cmd List@i
24. s2 : Id List@i
25. (e' <loc e)@i
26. <<<a5, a6>, a4>, a2> \mmember{} new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e')@i
27. <s1, s2> \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
28. no\_repeats(Id;s2)@i
29. ||s2|| = ||s1||@i
30. \mforall{}i:\mBbbN{}||s2||
(\mdownarrow{}\mexists{}e':E
((e' <loc e)
\mwedge{} <<<n1, n2>, s1[i]>, s2[i]> \mmember{} new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e')
\mwedge{} (\mforall{}e''\mmember{}[es-init(es;e);e').\mforall{}c:Cmd
(\mneg{}<<<n1, n2>, c>, s2[i]> \mmember{}
new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e'')))))@i
31. n1 = a5
32. n2 = a6
33. \mneg{}(a2 \mmember{} s2)
34. i : \mBbbN{}||s2|| + 1@i
35. i = 0
\mvdash{} \mdownarrow{}\mexists{}e':E
((e' <loc e)
\mwedge{} <<<n1, n2>, [a4 / s1][i]>, [a2 / s2][i]> \mmember{} new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e')
\mwedge{} (\mforall{}e''\mmember{}[es-init(es;e);e').\mforall{}c:Cmd
(\mneg{}<<<n1, n2>, c>, [a2 / s2][i]> \mmember{}
new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e''))))
By
Latex:
((Subst \mkleeneopen{}i \msim{} 0\mkleeneclose{} 0\mcdot{} THENA Auto)
THEN Reduce 0
THEN D 0
THEN InstConcl [\mkleeneopen{}e'\mkleeneclose{}]\mcdot{}
THEN Auto
THEN RWO "l\_all\_iff" 0
THEN Auto
THEN (D 0 THENA Auto))
Home
Index