Proof of Nuprl Lemma : cs-ref-map-changed

Step * 1 1 2 2 of Lemma cs-ref-map-changed

1. [V] : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. {∃v,v':V. (¬(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. f : ConsensusState ─→ (consensus-state3(V) List)@i
8. ∀s:ConsensusState. ∀i:ℕ.
     ((i < ||f s|| ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a)))
     ∧ (i < ||f s||
       ⇒ ((f s[i] = 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' ))

          ∧ (f s[i] = WITHDRAWN ∈ consensus-state3(V) ⇐⇒ ¬(∃v:V. in state s, inning i could commit v ))
          ∧ (∀v:V
               ((f s[i] = COMMITED[v] ∈ consensus-state3(V) ⇐⇒ in state s, inning i has committed v)
               ∧ (f s[i] = 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)))))))))@i
9. x : ts-reachable(consensus-ts4(V;A;W))@i
10. y : ts-reachable(consensus-ts4(V;A;W))@i
11. x ∈ ConsensusState
12. y ∈ ConsensusState
13. x ts-rel(consensus-ts4(V;A;W)) y@i
14. i : ℕ@i
15. i < ||f x||
16. i < ||f y||
17. v : V@i
18. in state x, inning i could commit v @i
19. ¬in state y, inning i could commit v @i
20. f x[i] = INITIAL ∈ consensus-state3(V)
21. (f x[i] = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state x, inning i could commit v ))
22. (f x[i] = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state x, inning i could commit v )
23. ∀v:V
      ((f x[i] = COMMITED[v] ∈ consensus-state3(V) ⇐⇒ in state x, inning i has committed v)
      ∧ (f x[i] = CONSIDERING[v] ∈ consensus-state3(V)
        ⇐⇒ in state x, inning i could commit v
            ∧ (¬in state x, inning i has committed v)
            ∧ (∀v':V. (in state x, inning i could commit v'  ⇒ (v' = v ∈ V)))))

24. ∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state x, inning i could commit v  ∧ in state x, inning i could commit v' )

25. f x[i] = INITIAL ∈ consensus-state3(V)

26. ¬(∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state y, inning i could commit v  ∧ in state y, inning i could commit v' ))

⊢ (f y[i] = WITHDRAWN ∈ consensus-state3(V))
∨ ((f x[i] = INITIAL ∈ consensus-state3(V))
  ∧ ((f y[i] = INITIAL ∈ consensus-state3(V))
    ∨ (∃v':V
        ((∀j:ℕi. (¬(f x[j] = INITIAL ∈ consensus-state3(V))))

        ∧ ((f y[i] = CONSIDERING[v'] ∈ consensus-state3(V)) ∨ (f y[i] = COMMITED[v'] ∈ consensus-state3(V)))

∧ (∀j:ℕi. ∀v'':V.

             (((f x[j] = CONSIDERING[v''] ∈ consensus-state3(V)) ∨ (f x[j] = COMMITED[v''] ∈ consensus-state3(V)))

             ⇒ (v'' = v' ∈ V)))))))
BY
{ (InstLemma `decidable__cs-inning-committable-some` [⌈V⌉;⌈A⌉;⌈W⌉;⌈y⌉;⌈i⌉]⋅ THENA Auto) }

1
.....antecedent.....
1. [V] : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. {∃v,v':V. (¬(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. f : ConsensusState ─→ (consensus-state3(V) List)@i
8. ∀s:ConsensusState. ∀i:ℕ.
     ((i < ||f s|| ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a)))
     ∧ (i < ||f s||
       ⇒ ((f s[i] = 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':V. ((¬(v = v' ∈ V)) ∧ in state x, inning i could commit v  ∧ in state x, inning i could commit v' )

25. f x[i] = INITIAL ∈ consensus-state3(V)

26. ¬(∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state y, inning i could commit v  ∧ in state y, inning i could commit v' ))

⊢ one-intersection(A;W)

2
1. [V] : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. {∃v,v':V. (¬(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. f : ConsensusState ─→ (consensus-state3(V) List)@i
8. ∀s:ConsensusState. ∀i:ℕ.
     ((i < ||f s|| ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a)))
     ∧ (i < ||f s||
       ⇒ ((f s[i] = 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':V. ((¬(v = v' ∈ V)) ∧ in state x, inning i could commit v  ∧ in state x, inning i could commit v' )

25. f x[i] = INITIAL ∈ consensus-state3(V)

26. ¬(∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state y, inning i could commit v  ∧ in state y, inning i could commit v' ))

27. Dec(∃v:V. in state y, inning i could commit v )
⊢ (f y[i] = WITHDRAWN ∈ consensus-state3(V))
∨ ((f x[i] = INITIAL ∈ consensus-state3(V))
  ∧ ((f y[i] = INITIAL ∈ consensus-state3(V))
    ∨ (∃v':V
        ((∀j:ℕi. (¬(f x[j] = INITIAL ∈ consensus-state3(V))))

        ∧ ((f y[i] = CONSIDERING[v'] ∈ consensus-state3(V)) ∨ (f y[i] = COMMITED[v'] ∈ consensus-state3(V)))

∧ (∀j:ℕi. ∀v'':V.

             (((f x[j] = CONSIDERING[v''] ∈ consensus-state3(V)) ∨ (f x[j] = COMMITED[v''] ∈ consensus-state3(V)))

⇒ (v'' = v' ∈ V)))))))

Latex:

1. [V] : Type 2. \mforall{}v1,v2:V. Dec(v1 = v2)@i 3. \{\mexists{}v,v':V. (\mneg{}(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. f : ConsensusState {}\mrightarrow{} (consensus-state3(V) List)@i 8. \mforall{}s:ConsensusState. \mforall{}i:\mBbbN{}. ((i < ||f s|| \mLeftarrow{}{}\mRightarrow{} \mexists{}a:\{a:Id| (a \mmember{} A)\} . (i \mleq{} Inning(s;a))) \mwedge{} (i < ||f s|| {}\mRightarrow{} ((f s[i] = 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{} (f s[i] = WITHDRAWN \mLeftarrow{}{}\mRightarrow{} \mneg{}(\mexists{}v:V. in state s, inning i could commit v )) \mwedge{} (\mforall{}v:V ((f s[i] = COMMITED[v] \mLeftarrow{}{}\mRightarrow{} in state s, inning i has committed v) \mwedge{} (f s[i] = 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)))))))))@i 9. x : ts-reachable(consensus-ts4(V;A;W))@i 10. y : ts-reachable(consensus-ts4(V;A;W))@i 11. x \mmember{} ConsensusState 12. y \mmember{} ConsensusState 13. x ts-rel(consensus-ts4(V;A;W)) y@i 14. i : \mBbbN{}@i 15. i < ||f x|| 16. i < ||f y|| 17. v : V@i 18. in state x, inning i could commit v @i 19. \mneg{}in state y, inning i could commit v @i 20. f x[i] = INITIAL 21. (f x[i] = WITHDRAWN) {}\mRightarrow{} (\mneg{}(\mexists{}v:V. in state x, inning i could commit v )) 22. (f x[i] = WITHDRAWN) \mLeftarrow{}{} \mneg{}(\mexists{}v:V. in state x, inning i could commit v ) 23. \mforall{}v:V ((f x[i] = COMMITED[v] \mLeftarrow{}{}\mRightarrow{} in state x, inning i has committed v) \mwedge{} (f x[i] = CONSIDERING[v] \mLeftarrow{}{}\mRightarrow{} in state x, inning i could commit v \mwedge{} (\mneg{}in state x, inning i has committed v) \mwedge{} (\mforall{}v':V. (in state x, inning i could commit v' {}\mRightarrow{} (v' = v))))) 24. \mexists{}v,v':V ((\mneg{}(v = v')) \mwedge{} in state x, inning i could commit v \mwedge{} in state x, inning i could commit v' ) 25. f x[i] = INITIAL 26. \mneg{}(\mexists{}v,v':V ((\mneg{}(v = v')) \mwedge{} in state y, inning i could commit v \mwedge{} in state y, inning i could commit v' )) \mvdash{} (f y[i] = WITHDRAWN) \mvee{} ((f x[i] = INITIAL) \mwedge{} ((f y[i] = INITIAL) \mvee{} (\mexists{}v':V ((\mforall{}j:\mBbbN{}i. (\mneg{}(f x[j] = INITIAL))) \mwedge{} ((f y[i] = CONSIDERING[v']) \mvee{} (f y[i] = COMMITED[v'])) \mwedge{} (\mforall{}j:\mBbbN{}i. \mforall{}v'':V. (((f x[j] = CONSIDERING[v'']) \mvee{} (f x[j] = COMMITED[v''])) {}\mRightarrow{} (v'' = v'))))))) By (InstLemma `decidable\_\_cs-inning-committable-some` [\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}W\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{} THENA Auto) Home Index