Step
*
1
2
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. Dec(∃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. in state s, inning i could commit 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 [⌈WITHDRAWN⌉]⋅
THEN Auto
THEN Try (((Assert ¬(INITIAL = WITHDRAWN ∈ consensus-state3(V)) BY
(BLemma `consensus-state3-unequal` THEN Auto))
THEN D -1
THEN Complete (Auto)))
THEN Try (((Assert ¬(COMMITED[v] = WITHDRAWN ∈ consensus-state3(V)) BY
(BLemma `consensus-state3-unequal` THEN Auto))
THEN D -1
THEN Complete (Auto)))
THEN Try (((Assert ¬(CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V)) BY
(BLemma `consensus-state3-unequal` THEN Auto))
THEN D -1
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. Dec(∃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. in state s, inning i could commit v )
13. ∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v ∧ in state s, inning i could commit v' )@i
⊢ WITHDRAWN = INITIAL ∈ 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. Dec(∃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. in state s, inning i could commit v )
13. (WITHDRAWN = 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' ))
14. (WITHDRAWN = 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' )
15. (WITHDRAWN = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state s, inning i could commit v ))
16. (WITHDRAWN = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state s, inning i could commit v )
17. v : V@i
18. in state s, inning i has committed v@i
⊢ WITHDRAWN = COMMITED[v] ∈ 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. Dec(∃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. in state s, inning i could commit v )
13. (WITHDRAWN = 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' ))
14. (WITHDRAWN = 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' )
15. (WITHDRAWN = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state s, inning i could commit v ))
16. (WITHDRAWN = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state s, inning i could commit v )
17. v : V@i
18. (WITHDRAWN = COMMITED[v] ∈ consensus-state3(V)) ⇒ in state s, inning i has committed v
19. (WITHDRAWN = COMMITED[v] ∈ consensus-state3(V)) ⇐ in state s, inning i has committed v
20. in state s, inning i could commit v @i
21. ¬in state s, inning i has committed v@i
22. ∀v':V. (in state s, inning i could commit v' ⇒ (v' = v ∈ V))@i
⊢ WITHDRAWN = CONSIDERING[v] ∈ 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. Dec(\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. \mneg{}(\mexists{}v:V. in state s, inning i could commit 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{}WITHDRAWN\mkleeneclose{}]\mcdot{}
THEN Auto
THEN Try (((Assert \mneg{}(INITIAL = WITHDRAWN) BY
(BLemma `consensus-state3-unequal` THEN Auto))
THEN D -1
THEN Complete (Auto)))
THEN Try (((Assert \mneg{}(COMMITED[v] = WITHDRAWN) BY
(BLemma `consensus-state3-unequal` THEN Auto))
THEN D -1
THEN Complete (Auto)))
THEN Try (((Assert \mneg{}(CONSIDERING[v] = WITHDRAWN) BY
(BLemma `consensus-state3-unequal` THEN Auto))
THEN D -1
THEN Complete (Auto))))
Home
Index