Step
*
1
1
2
1
1
3
1
of Lemma
consensus-ts4-ref-map1
1. V : Type
2. v3 : V@i
3. v4 : V@i
4. ¬(v3 = v4 ∈ V)@i
5. ∀v,v':V. Dec(v = v' ∈ V)@i
6. A : Id List@i
7. W : {a:Id| (a ∈ A)} List List@i
8. two-intersection(A;W)@i
9. one-intersection(A;W)
10. s : ConsensusState@i
11. i : ℤ@i
12. v2 : V
13. v' : V
14. ¬(v2 = v' ∈ V)
15. in state s, inning i could commit v2
16. in state s, inning i could commit v'
17. ∀v:V. Dec(in state s, inning i has committed v)
18. v : V
19. in state s, inning i could commit v
20. ¬in state s, inning i has committed v
21. ¬(INITIAL = WITHDRAWN ∈ consensus-state3(V))
22. ∀[v:V]
(((¬(COMMITED[v] = INITIAL ∈ consensus-state3(V))) ∧ (¬(CONSIDERING[v] = INITIAL ∈ consensus-state3(V))))
∧ (¬(COMMITED[v] = WITHDRAWN ∈ consensus-state3(V)))
∧ (¬(CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V)))
∧ (∀[v':V]
((¬(CONSIDERING[v] = COMMITED[v'] ∈ consensus-state3(V)))
∧ (¬(CONSIDERING[v] = CONSIDERING[v'] ∈ consensus-state3(V)))
∧ (¬(COMMITED[v] = COMMITED[v'] ∈ consensus-state3(V)))
supposing ¬(v = v' ∈ V))))
23. (INITIAL = INITIAL ∈ consensus-state3(V))
⇒ (∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v ∧ in state s, inning i could commit v' ))
24. (INITIAL = INITIAL ∈ consensus-state3(V)) ⇐ ∃v,v':V
((¬(v = v' ∈ V))
∧ in state s, inning i could commit v
∧ in state s, inning i could commit v' )
25. (INITIAL = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state s, inning i could commit v ))
26. (INITIAL = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state s, inning i could commit v )
27. v1 : V@i
28. (INITIAL = COMMITED[v1] ∈ consensus-state3(V)) ⇒ in state s, inning i has committed v1
29. (INITIAL = COMMITED[v1] ∈ consensus-state3(V)) ⇐ in state s, inning i has committed v1
30. in state s, inning i could commit v1 @i
31. ¬in state s, inning i has committed v1@i
32. ∀v':V. (in state s, inning i could commit v' ⇒ (v' = v1 ∈ V))@i
⊢ INITIAL = CONSIDERING[v1] ∈ consensus-state3(V)
BY
{ D 14 }
1
1. V : Type
2. v3 : V@i
3. v4 : V@i
4. ¬(v3 = v4 ∈ V)@i
5. ∀v,v':V. Dec(v = v' ∈ V)@i
6. A : Id List@i
7. W : {a:Id| (a ∈ A)} List List@i
8. two-intersection(A;W)@i
9. one-intersection(A;W)
10. s : ConsensusState@i
11. i : ℤ@i
12. v2 : V
13. v' : V
14. in state s, inning i could commit v2
15. in state s, inning i could commit v'
16. ∀v:V. Dec(in state s, inning i has committed v)
17. v : V
18. in state s, inning i could commit v
19. ¬in state s, inning i has committed v
20. ¬(INITIAL = WITHDRAWN ∈ consensus-state3(V))
21. ∀[v:V]
(((¬(COMMITED[v] = INITIAL ∈ consensus-state3(V))) ∧ (¬(CONSIDERING[v] = INITIAL ∈ consensus-state3(V))))
∧ (¬(COMMITED[v] = WITHDRAWN ∈ consensus-state3(V)))
∧ (¬(CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V)))
∧ (∀[v':V]
((¬(CONSIDERING[v] = COMMITED[v'] ∈ consensus-state3(V)))
∧ (¬(CONSIDERING[v] = CONSIDERING[v'] ∈ consensus-state3(V)))
∧ (¬(COMMITED[v] = COMMITED[v'] ∈ consensus-state3(V)))
supposing ¬(v = v' ∈ V))))
22. (INITIAL = INITIAL ∈ consensus-state3(V))
⇒ (∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v ∧ in state s, inning i could commit v' ))
23. (INITIAL = INITIAL ∈ consensus-state3(V)) ⇐ ∃v,v':V
((¬(v = v' ∈ V))
∧ in state s, inning i could commit v
∧ in state s, inning i could commit v' )
24. (INITIAL = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state s, inning i could commit v ))
25. (INITIAL = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state s, inning i could commit v )
26. v1 : V@i
27. (INITIAL = COMMITED[v1] ∈ consensus-state3(V)) ⇒ in state s, inning i has committed v1
28. (INITIAL = COMMITED[v1] ∈ consensus-state3(V)) ⇐ in state s, inning i has committed v1
29. in state s, inning i could commit v1 @i
30. ¬in state s, inning i has committed v1@i
31. ∀v':V. (in state s, inning i could commit v' ⇒ (v' = v1 ∈ V))@i
⊢ v2 = v' ∈ V
Latex:
1. V : Type
2. v3 : V@i
3. v4 : V@i
4. \mneg{}(v3 = v4)@i
5. \mforall{}v,v':V. Dec(v = v')@i
6. A : Id List@i
7. W : \{a:Id| (a \mmember{} A)\} List List@i
8. two-intersection(A;W)@i
9. one-intersection(A;W)
10. s : ConsensusState@i
11. i : \mBbbZ{}@i
12. v2 : V
13. v' : V
14. \mneg{}(v2 = v')
15. in state s, inning i could commit v2
16. in state s, inning i could commit v'
17. \mforall{}v:V. Dec(in state s, inning i has committed v)
18. v : V
19. in state s, inning i could commit v
20. \mneg{}in state s, inning i has committed v
21. \mneg{}(INITIAL = WITHDRAWN)
22. \mforall{}[v:V]
(((\mneg{}(COMMITED[v] = INITIAL)) \mwedge{} (\mneg{}(CONSIDERING[v] = INITIAL)))
\mwedge{} (\mneg{}(COMMITED[v] = WITHDRAWN))
\mwedge{} (\mneg{}(CONSIDERING[v] = WITHDRAWN))
\mwedge{} (\mforall{}[v':V]
((\mneg{}(CONSIDERING[v] = COMMITED[v']))
\mwedge{} (\mneg{}(CONSIDERING[v] = CONSIDERING[v'])) \mwedge{} (\mneg{}(COMMITED[v] = COMMITED[v']))
supposing \mneg{}(v = v'))))
23. (INITIAL = INITIAL)
{}\mRightarrow{} (\mexists{}v,v':V
((\mneg{}(v = v')) \mwedge{} in state s, inning i could commit v \mwedge{} in state s, inning i could commit v' ))
24. (INITIAL = INITIAL) \mLeftarrow{}{} \mexists{}v,v':V
((\mneg{}(v = v'))
\mwedge{} in state s, inning i could commit v
\mwedge{} in state s, inning i could commit v' )
25. (INITIAL = WITHDRAWN) {}\mRightarrow{} (\mneg{}(\mexists{}v:V. in state s, inning i could commit v ))
26. (INITIAL = WITHDRAWN) \mLeftarrow{}{} \mneg{}(\mexists{}v:V. in state s, inning i could commit v )
27. v1 : V@i
28. (INITIAL = COMMITED[v1]) {}\mRightarrow{} in state s, inning i has committed v1
29. (INITIAL = COMMITED[v1]) \mLeftarrow{}{} in state s, inning i has committed v1
30. in state s, inning i could commit v1 @i
31. \mneg{}in state s, inning i has committed v1@i
32. \mforall{}v':V. (in state s, inning i could commit v' {}\mRightarrow{} (v' = v1))@i
\mvdash{} INITIAL = CONSIDERING[v1]
By
D 14
Home
Index