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

Step * 1 1 2 2 1 6 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))
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
BY
{ (Assert v = v@0 ∈ V BY
         (RepUR ``cs-considering consensus-state3`` -3 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))))

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

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')) 22. (CONSIDERING[v] = 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' )) 23. (CONSIDERING[v] = 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' ) 24. (CONSIDERING[v] = WITHDRAWN) {}\mRightarrow{} (\mneg{}(\mexists{}v:V. in state s, inning i could commit v )) 25. (CONSIDERING[v] = WITHDRAWN) \mLeftarrow{}{} \mneg{}(\mexists{}v:V. in state s, inning i could commit v ) 26. v@0 : V@i 27. (CONSIDERING[v] = COMMITED[v@0]) {}\mRightarrow{} in state s, inning i has committed v@0 28. (CONSIDERING[v] = COMMITED[v@0]) \mLeftarrow{}{} in state s, inning i has committed v@0 29. CONSIDERING[v] = CONSIDERING[v@0]@i 30. v' : V@i 31. in state s, inning i could commit v' @i \mvdash{} v' = v@0 By (Assert v = v@0 BY (RepUR ``cs-considering consensus-state3`` -3 THEN Auto)) Home Index