Step
*
1
1
2
1
1
of Lemma
consensus-ts4-ref-map1
1. [V] : Type
2. ∃v,v':V. (¬(v = v' ∈ V))@i
3. ∀v,v':V. Dec(v = v' ∈ V)@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)} List List@i
6. two-intersection(A;W)@i
7. one-intersection(A;W)
8. s : ConsensusState@i
9. i : ℤ@i
10. ∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v ∧ in state s, inning i could commit v' )
11. ∀v:V. Dec(in state s, inning i has committed v)
12. v : V
13. in state s, inning i could commit v
14. ¬in state s, inning i has committed v
15. (¬(INITIAL = WITHDRAWN ∈ consensus-state3(V)))
∧ (∀[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)))))
⊢ ∃x:consensus-state3(V)
((x = 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' ))
∧ (x = WITHDRAWN ∈ consensus-state3(V) ⇐⇒ ¬(∃v:V. in state s, inning i could commit v ))
∧ (∀v:V
((x = COMMITED[v] ∈ consensus-state3(V) ⇐⇒ in state s, inning i has committed v)
∧ (x = CONSIDERING[v] ∈ consensus-state3(V)
⇐⇒ in state s, inning i could commit v
∧ (¬in state s, inning i has committed v)
∧ (∀v':V. (in state s, inning i could commit v' ⇒ (v' = v ∈ V)))))))
BY
{ (InstConcl [⌈INITIAL⌉]⋅ THEN Auto THEN Try ((InstHyp [⌈v1⌉] 16⋅ THEN Complete (Auto)))) }
1
1. V : Type
2. ∃v,v':V. (¬(v = v' ∈ V))@i
3. ∀v,v':V. Dec(v = v' ∈ V)@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)} List List@i
6. two-intersection(A;W)@i
7. one-intersection(A;W)
8. s : ConsensusState@i
9. i : ℤ@i
10. ∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v ∧ in state s, inning i could commit v' )
11. ∀v:V. Dec(in state s, inning i has committed v)
12. v : V
13. in state s, inning i could commit v
14. ¬in state s, inning i has committed v
15. ¬(INITIAL = WITHDRAWN ∈ consensus-state3(V))
16. ∀[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))))
17. (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' ))
18. (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' )
19. ¬(∃v:V. in state s, inning i could commit v )@i
⊢ INITIAL = WITHDRAWN ∈ consensus-state3(V)
2
1. V : Type
2. ∃v,v':V. (¬(v = v' ∈ V))@i
3. ∀v,v':V. Dec(v = v' ∈ V)@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)} List List@i
6. two-intersection(A;W)@i
7. one-intersection(A;W)
8. s : ConsensusState@i
9. i : ℤ@i
10. ∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v ∧ in state s, inning i could commit v' )
11. ∀v:V. Dec(in state s, inning i has committed v)
12. v : V
13. in state s, inning i could commit v
14. ¬in state s, inning i has committed v
15. ¬(INITIAL = WITHDRAWN ∈ consensus-state3(V))
16. ∀[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))))
17. (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' ))
18. (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' )
19. (INITIAL = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state s, inning i could commit v ))
20. (INITIAL = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state s, inning i could commit v )
21. v1 : V@i
22. in state s, inning i has committed v1@i
⊢ INITIAL = COMMITED[v1] ∈ consensus-state3(V)
3
1. V : Type
2. ∃v,v':V. (¬(v = v' ∈ V))@i
3. ∀v,v':V. Dec(v = v' ∈ V)@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)} List List@i
6. two-intersection(A;W)@i
7. one-intersection(A;W)
8. s : ConsensusState@i
9. i : ℤ@i
10. ∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v ∧ in state s, inning i could commit v' )
11. ∀v:V. Dec(in state s, inning i has committed v)
12. v : V
13. in state s, inning i could commit v
14. ¬in state s, inning i has committed v
15. ¬(INITIAL = WITHDRAWN ∈ consensus-state3(V))
16. ∀[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))))
17. (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' ))
18. (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' )
19. (INITIAL = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state s, inning i could commit v ))
20. (INITIAL = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state s, inning i could commit v )
21. v1 : V@i
22. (INITIAL = COMMITED[v1] ∈ consensus-state3(V)) ⇒ in state s, inning i has committed v1
23. (INITIAL = COMMITED[v1] ∈ consensus-state3(V)) ⇐ in state s, inning i has committed v1
24. in state s, inning i could commit v1 @i
25. ¬in state s, inning i has committed v1@i
26. ∀v':V. (in state s, inning i could commit v' ⇒ (v' = v1 ∈ V))@i
⊢ INITIAL = CONSIDERING[v1] ∈ consensus-state3(V)
Latex:
1. [V] : Type
2. \mexists{}v,v':V. (\mneg{}(v = v'))@i
3. \mforall{}v,v':V. Dec(v = v')@i
4. A : Id List@i
5. W : \{a:Id| (a \mmember{} A)\} List List@i
6. two-intersection(A;W)@i
7. one-intersection(A;W)
8. s : ConsensusState@i
9. i : \mBbbZ{}@i
10. \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' )
11. \mforall{}v:V. Dec(in state s, inning i has committed v)
12. v : V
13. in state s, inning i could commit v
14. \mneg{}in state s, inning i has committed v
15. (\mneg{}(INITIAL = WITHDRAWN))
\mwedge{} (\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')))))
\mvdash{} \mexists{}x:consensus-state3(V)
((x = INITIAL
\mLeftarrow{}{}\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' ))
\mwedge{} (x = WITHDRAWN \mLeftarrow{}{}\mRightarrow{} \mneg{}(\mexists{}v:V. in state s, inning i could commit v ))
\mwedge{} (\mforall{}v:V
((x = COMMITED[v] \mLeftarrow{}{}\mRightarrow{} in state s, inning i has committed v)
\mwedge{} (x = CONSIDERING[v]
\mLeftarrow{}{}\mRightarrow{} in state s, inning i could commit v
\mwedge{} (\mneg{}in state s, inning i has committed v)
\mwedge{} (\mforall{}v':V. (in state s, inning i could commit v' {}\mRightarrow{} (v' = v)))))))
By
(InstConcl [\mkleeneopen{}INITIAL\mkleeneclose{}]\mcdot{} THEN Auto THEN Try ((InstHyp [\mkleeneopen{}v1\mkleeneclose{}] 16\mcdot{} THEN Complete (Auto))))
Home
Index