Proof of Nuprl Lemma : consensus-ts3-invariant0

Step * 1 2 of Lemma consensus-ts3-invariant0

1. [V] : Type
2. ¬(INITIAL = WITHDRAWN ∈ consensus-state3(V))
3. ∀[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))))
4. L : consensus-state3(V) List@i
5. y : consensus-state3(V) List@i
6. L @ [INITIAL] ∈ consensus-state3(V) List
7. ∀i:ℕ||L||

     ∀j:ℕ||L||. (L[j] = INITIAL ∈ consensus-state3(V)) ∨ (L[j] = WITHDRAWN ∈ consensus-state3(V)) supposing i < j

supposing L[i] = INITIAL ∈ consensus-state3(V)@i
8. i : ℕ||L @ [INITIAL]||
9. L @ [INITIAL][i] = INITIAL ∈ consensus-state3(V)
10. j : ℕ||L @ [INITIAL]||
11. i < j
12. ¬(j = ||L|| ∈ ℤ)

⊢ (L @ [INITIAL][j] = INITIAL ∈ consensus-state3(V)) ∨ (L @ [INITIAL][j] = WITHDRAWN ∈ consensus-state3(V))

BY
{ (Assert ||L @ [INITIAL]|| = (||L|| + 1) ∈ ℤ BY
((RWO "length_append" 0 THEN Reduce 0) THEN Auto)) }

1
1. [V] : Type
2. ¬(INITIAL = WITHDRAWN ∈ consensus-state3(V))
3. ∀[v:V]

     (((¬(COMMITED[v] = INITIAL ∈ consensus-state3(V))) ∧ (¬(CONSIDERING[v] = INITIAL ∈ consensus-state3(V))))

     ∀j:ℕ||L||. (L[j] = INITIAL ∈ consensus-state3(V)) ∨ (L[j] = WITHDRAWN ∈ consensus-state3(V)) supposing i < j

⊢ (L @ [INITIAL][j] = INITIAL ∈ consensus-state3(V)) ∨ (L @ [INITIAL][j] = WITHDRAWN ∈ consensus-state3(V))

Latex:

1. [V] : Type 2. \mneg{}(INITIAL = WITHDRAWN) 3. \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')))) 4. L : consensus-state3(V) List@i 5. y : consensus-state3(V) List@i 6. L @ [INITIAL] \mmember{} consensus-state3(V) List 7. \mforall{}i:\mBbbN{}||L|| \mforall{}j:\mBbbN{}||L||. (L[j] = INITIAL) \mvee{} (L[j] = WITHDRAWN) supposing i < j supposing L[i] = INITIAL@i 8. i : \mBbbN{}||L @ [INITIAL]|| 9. L @ [INITIAL][i] = INITIAL 10. j : \mBbbN{}||L @ [INITIAL]|| 11. i < j 12. \mneg{}(j = ||L||) \mvdash{} (L @ [INITIAL][j] = INITIAL) \mvee{} (L @ [INITIAL][j] = WITHDRAWN) By (Assert ||L @ [INITIAL]|| = (||L|| + 1) BY ((RWO "length\_append" 0 THEN Reduce 0) THEN Auto)) Home Index