Step
*
1
1
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. 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
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. ¬(COMMITED[v] = INITIAL ∈ consensus-state3(V))
18. ¬(CONSIDERING[v] = INITIAL ∈ consensus-state3(V))
19. ¬(COMMITED[v] = WITHDRAWN ∈ consensus-state3(V))
20. ¬(CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V))
21. ∀[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 [⌈COMMITED[v]⌉]⋅ THEN 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
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. ¬(COMMITED[v] = INITIAL ∈ consensus-state3(V))
18. ¬(CONSIDERING[v] = INITIAL ∈ consensus-state3(V))
19. ¬(COMMITED[v] = WITHDRAWN ∈ consensus-state3(V))
20. ¬(CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V))
21. ∀[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. ∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v ∧ in state s, inning i could commit v' )@i
⊢ COMMITED[v] = 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
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. ¬(COMMITED[v] = INITIAL ∈ consensus-state3(V))
18. ¬(CONSIDERING[v] = INITIAL ∈ consensus-state3(V))
19. ¬(COMMITED[v] = WITHDRAWN ∈ consensus-state3(V))
20. ¬(CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V))
21. ∀[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. (COMMITED[v] = 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. (COMMITED[v] = 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. ¬(∃v:V. in state s, inning i could commit v )@i
⊢ COMMITED[v] = WITHDRAWN ∈ 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
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. ¬(COMMITED[v] = INITIAL ∈ consensus-state3(V))
18. ¬(CONSIDERING[v] = INITIAL ∈ consensus-state3(V))
19. ¬(COMMITED[v] = WITHDRAWN ∈ consensus-state3(V))
20. ¬(CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V))
21. ∀[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. (COMMITED[v] = 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. (COMMITED[v] = 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. (COMMITED[v] = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state s, inning i could commit v ))
25. (COMMITED[v] = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state s, inning i could commit v )
26. v@0 : V@i
27. COMMITED[v] = COMMITED[v@0] ∈ consensus-state3(V)@i
⊢ in state s, inning i has committed v@0
4
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
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. ¬(COMMITED[v] = INITIAL ∈ consensus-state3(V))
18. ¬(CONSIDERING[v] = INITIAL ∈ consensus-state3(V))
19. ¬(COMMITED[v] = WITHDRAWN ∈ consensus-state3(V))
20. ¬(CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V))
21. ∀[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. (COMMITED[v] = 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. (COMMITED[v] = 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. (COMMITED[v] = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state s, inning i could commit v ))
25. (COMMITED[v] = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state s, inning i could commit v )
26. v@0 : V@i
27. in state s, inning i has committed v@0@i
⊢ COMMITED[v] = COMMITED[v@0] ∈ consensus-state3(V)
5
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
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. ¬(COMMITED[v] = INITIAL ∈ consensus-state3(V))
18. ¬(CONSIDERING[v] = INITIAL ∈ consensus-state3(V))
19. ¬(COMMITED[v] = WITHDRAWN ∈ consensus-state3(V))
20. ¬(CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V))
21. ∀[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. (COMMITED[v] = 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. (COMMITED[v] = 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. (COMMITED[v] = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state s, inning i could commit v ))
25. (COMMITED[v] = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state s, inning i could commit v )
26. v@0 : V@i
27. (COMMITED[v] = COMMITED[v@0] ∈ consensus-state3(V)) ⇒ in state s, inning i has committed v@0
28. (COMMITED[v] = COMMITED[v@0] ∈ consensus-state3(V)) ⇐ in state s, inning i has committed v@0
29. COMMITED[v] = CONSIDERING[v@0] ∈ consensus-state3(V)@i
⊢ in state s, inning i could commit v@0
6
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
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. ¬(COMMITED[v] = INITIAL ∈ consensus-state3(V))
18. ¬(CONSIDERING[v] = INITIAL ∈ consensus-state3(V))
19. ¬(COMMITED[v] = WITHDRAWN ∈ consensus-state3(V))
20. ¬(CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V))
21. ∀[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. (COMMITED[v] = 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. (COMMITED[v] = 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. (COMMITED[v] = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state s, inning i could commit v ))
25. (COMMITED[v] = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state s, inning i could commit v )
26. v@0 : V@i
27. (COMMITED[v] = COMMITED[v@0] ∈ consensus-state3(V)) ⇒ in state s, inning i has committed v@0
28. (COMMITED[v] = COMMITED[v@0] ∈ consensus-state3(V)) ⇐ in state s, inning i has committed v@0
29. COMMITED[v] = CONSIDERING[v@0] ∈ consensus-state3(V)@i
⊢ ¬in state s, inning i has committed v@0
7
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
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. ¬(COMMITED[v] = INITIAL ∈ consensus-state3(V))
18. ¬(CONSIDERING[v] = INITIAL ∈ consensus-state3(V))
19. ¬(COMMITED[v] = WITHDRAWN ∈ consensus-state3(V))
20. ¬(CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V))
21. ∀[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. (COMMITED[v] = 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. (COMMITED[v] = 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. (COMMITED[v] = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state s, inning i could commit v ))
25. (COMMITED[v] = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state s, inning i could commit v )
26. v@0 : V@i
27. (COMMITED[v] = COMMITED[v@0] ∈ consensus-state3(V)) ⇒ in state s, inning i has committed v@0
28. (COMMITED[v] = COMMITED[v@0] ∈ consensus-state3(V)) ⇐ in state s, inning i has committed v@0
29. COMMITED[v] = CONSIDERING[v@0] ∈ consensus-state3(V)@i
30. v' : V@i
31. in state s, inning i could commit v' @i
⊢ v' = v@0 ∈ V
8
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
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. ¬(COMMITED[v] = INITIAL ∈ consensus-state3(V))
18. ¬(CONSIDERING[v] = INITIAL ∈ consensus-state3(V))
19. ¬(COMMITED[v] = WITHDRAWN ∈ consensus-state3(V))
20. ¬(CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V))
21. ∀[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. (COMMITED[v] = 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. (COMMITED[v] = 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. (COMMITED[v] = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state s, inning i could commit v ))
25. (COMMITED[v] = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state s, inning i could commit v )
26. v@0 : V@i
27. (COMMITED[v] = COMMITED[v@0] ∈ consensus-state3(V)) ⇒ in state s, inning i has committed v@0
28. (COMMITED[v] = COMMITED[v@0] ∈ consensus-state3(V)) ⇐ in state s, inning i has committed v@0
29. in state s, inning i could commit v@0 @i
30. ¬in state s, inning i has committed v@0@i
31. ∀v':V. (in state s, inning i could commit v' ⇒ (v' = v@0 ∈ V))@i
⊢ COMMITED[v] = CONSIDERING[v@0] ∈ 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. v : V
13. in state s, inning i could commit v
14. in state s, inning i has committed v
15. \mneg{}(INITIAL = WITHDRAWN)
16. \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'))))
17. \mneg{}(COMMITED[v] = INITIAL)
18. \mneg{}(CONSIDERING[v] = INITIAL)
19. \mneg{}(COMMITED[v] = WITHDRAWN)
20. \mneg{}(CONSIDERING[v] = WITHDRAWN)
21. \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{}COMMITED[v]\mkleeneclose{}]\mcdot{} THEN Auto)
Home
Index