---

Step * 1 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. ∀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
7. y = (L @ [INITIAL]) ∈ (consensus-state3(V) List)@i
8. i : ℕ||y||@i
9. y[i] = INITIAL ∈ consensus-state3(V)
10. j : ℕ||y||@i
11. i < j
⊢ (y[j] = INITIAL ∈ consensus-state3(V)) ∨ (y[j] = WITHDRAWN ∈ consensus-state3(V))
BY
{ (ElimVar `y' THEN (Decide j = ||L|| ∈ ℤ THENA 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))))
     ∧ (¬(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))

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

---

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.  \mforall{}i:\mBbbN{}||L||
          \mforall{}j:\mBbbN{}||L||.  (L[j]  =  INITIAL)  \mvee{}  (L[j]  =  WITHDRAWN)  supposing  i  <  j  supposing  L[i]  =  INITIAL@i
7.  y  =  (L  @  [INITIAL])@i
8.  i  :  \mBbbN{}||y||@i
9.  y[i]  =  INITIAL
10.  j  :  \mBbbN{}||y||@i
11.  i  <  j
\mvdash{}  (y[j]  =  INITIAL)  \mvee{}  (y[j]  =  WITHDRAWN)


By

(ElimVar  `y'  THEN  (Decide  j  =  ||L||  THENA  Auto))

---

Home Index