Step
*
2
of Lemma
new_23_sig_quorum_mem
.....antecedent.....
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)
⊢ ∀a1,a2:ℤ × ℤ × Cmd × Id. ∀s1,s2:Cmd List × (Id List). ∀e,e':E.
(e1 ≤loc e
⇒ (e <loc e')
⇒ (e' <loc e2)
⇒ a1 ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e)
⇒ s1 ∈ Memory-loc-class(new_23_sig_add_to_quorum(Cmd)
ni;λloc.{<[], []>};new_23_sig_vote'base(Cmd;notify;propose;f))(e)
⇒ a2 ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')
⇒ s2 ∈ Memory-loc-class(new_23_sig_add_to_quorum(Cmd)
ni;λloc.{<[], []>};new_23_sig_vote'base(Cmd;notify;propose;f))(e')
⇒ (λ2s2.let cmds1,locs1 = s1
in let cmds2,locs2 = s2
in let x,i = a1
in let ni',c = x
in (ni = ni' ∈ (ℤ × ℤ)) ⇒ ((i ∈ locs2) ∧ ((¬(i ∈ locs1)) ⇒ (c ∈ cmds2)))
s2)
⇒ (λ2s2.let cmds1,locs1 = s1
in let cmds2,locs2 = s2
in let x,i = a1
in let ni',c = x
in (ni = ni' ∈ (ℤ × ℤ)) ⇒ ((i ∈ locs2) ∧ ((¬(i ∈ locs1)) ⇒ (c ∈ cmds2)))
(new_23_sig_add_to_quorum(Cmd) ni loc(e2) a2 s2)))
BY
{ ReduceAutoMemory⋅⋅ }
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. 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)))
Latex:
Latex:
.....antecedent.....
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)
\mvdash{} \mforall{}a1,a2:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id. \mforall{}s1,s2:Cmd List \mtimes{} (Id List). \mforall{}e,e':E.
(e1 \mleq{}loc e
{}\mRightarrow{} (e <loc e')
{}\mRightarrow{} (e' <loc e2)
{}\mRightarrow{} a1 \mmember{} new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e)
{}\mRightarrow{} s1 \mmember{} Memory-loc-class(new\_23\_sig\_add\_to\_quorum(Cmd)
ni;\mlambda{}loc.\{<[], []>\};new\_23\_sig\_vote'base(Cmd;notify;propose;f))(e)
{}\mRightarrow{} a2 \mmember{} new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e')
{}\mRightarrow{} s2 \mmember{} Memory-loc-class(new\_23\_sig\_add\_to\_quorum(Cmd)
ni;\mlambda{}loc.\{<[], []>\};new\_23\_sig\_vote'base(Cmd;notify;propose;f))(e')
{}\mRightarrow{} (\mlambda{}\msubtwo{}s2.let cmds1,locs1 = s1
in let cmds2,locs2 = s2
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)))
s2)
{}\mRightarrow{} (\mlambda{}\msubtwo{}s2.let cmds1,locs1 = s1
in let cmds2,locs2 = s2
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)))
(new\_23\_sig\_add\_to\_quorum(Cmd) ni loc(e2) a2 s2)))
By
Latex:
ReduceAutoMemory\mcdot{}\mcdot{}
Home
Index