Proof of Nuprl Lemma : consensus-ts4-ref-map1

Step * 1 1 2 2 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))
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 [⌈CONSIDERING[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. ¬(∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v  ∧ in state s, inning i could commit 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. (CONSIDERING[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. (CONSIDERING[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
⊢ CONSIDERING[v] = 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' ))

      (((¬(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. (CONSIDERING[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. (CONSIDERING[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. (CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state s, inning i could commit v ))
25. (CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state s, inning i could commit v )
26. v@0 : V@i
27. CONSIDERING[v] = COMMITED[v@0] ∈ consensus-state3(V)@i
⊢ in state s, inning i has committed v@0

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' ))

      (((¬(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. (CONSIDERING[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. (CONSIDERING[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. (CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state s, inning i could commit v ))
25. (CONSIDERING[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
⊢ CONSIDERING[v] = COMMITED[v@0] ∈ consensus-state3(V)

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. ¬(∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v  ∧ in state s, inning i could commit 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. (CONSIDERING[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. (CONSIDERING[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. (CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state s, inning i could commit v ))
25. (CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state s, inning i could commit v )
26. v@0 : V@i
27. (CONSIDERING[v] = COMMITED[v@0] ∈ consensus-state3(V)) ⇒ in state s, inning i has committed v@0
28. (CONSIDERING[v] = COMMITED[v@0] ∈ consensus-state3(V)) ⇐ in state s, inning i has committed v@0
29. CONSIDERING[v] = CONSIDERING[v@0] ∈ consensus-state3(V)@i
⊢ in state s, inning i could commit v@0

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. ¬(∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v  ∧ in state s, inning i could commit 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. (CONSIDERING[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. (CONSIDERING[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. (CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state s, inning i could commit v ))
25. (CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state s, inning i could commit v )
26. v@0 : V@i
27. (CONSIDERING[v] = COMMITED[v@0] ∈ consensus-state3(V)) ⇒ in state s, inning i has committed v@0
28. (CONSIDERING[v] = COMMITED[v@0] ∈ consensus-state3(V)) ⇐ in state s, inning i has committed v@0
29. CONSIDERING[v] = CONSIDERING[v@0] ∈ consensus-state3(V)@i
⊢ ¬in state s, inning i has committed 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. ¬(∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v  ∧ in state s, inning i could commit 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. (CONSIDERING[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. (CONSIDERING[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. (CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state s, inning i could commit v ))
25. (CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state s, inning i could commit v )
26. v@0 : V@i
27. (CONSIDERING[v] = COMMITED[v@0] ∈ consensus-state3(V)) ⇒ in state s, inning i has committed v@0
28. (CONSIDERING[v] = COMMITED[v@0] ∈ consensus-state3(V)) ⇐ in state s, inning i has committed v@0
29. CONSIDERING[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

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. ¬(∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v  ∧ in state s, inning i could commit 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. (CONSIDERING[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. (CONSIDERING[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. (CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state s, inning i could commit v ))
25. (CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state s, inning i could commit v )
26. v@0 : V@i
27. (CONSIDERING[v] = COMMITED[v@0] ∈ consensus-state3(V)) ⇒ in state s, inning i has committed v@0
28. (CONSIDERING[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
⊢ CONSIDERING[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. \mneg{}(\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) 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{}CONSIDERING[v]\mkleeneclose{}]\mcdot{} THEN Auto) Home Index