---

Step * 3 1 of Lemma consensus-ts3-invariant0


1. [V] : Type
2. ¬(INITIAL = WITHDRAWN ∈ consensus-state3(V))
3. L : consensus-state3(V) List@i
4. y : consensus-state3(V) List@i
5. ∀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
6. ||y|| = ||L|| ∈ ℤ@i
7. i1 : ℕ||L||@i
8. ∀j:ℕ||L||. ((¬(j = i1 ∈ ℤ)) ⇒ (y[j] = L[j] ∈ consensus-state3(V)))@i
9. L[i1] = INITIAL ∈ consensus-state3(V)@i
10. v : V@i
11. ¬(COMMITED[v] = INITIAL ∈ consensus-state3(V))
12. ¬(CONSIDERING[v] = INITIAL ∈ consensus-state3(V))
13. ¬(COMMITED[v] = WITHDRAWN ∈ consensus-state3(V))
14. ¬(CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V))
15. ∀[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))
16. y[i1] = CONSIDERING[v] ∈ consensus-state3(V)@i
17. ∀j:ℕi1
      ((L[j] = WITHDRAWN ∈ consensus-state3(V))
      ∨ (L[j] = CONSIDERING[v] ∈ consensus-state3(V))
      ∨ (L[j] = COMMITED[v] ∈ consensus-state3(V)))@i
18. i : ℕ||y||@i
19. y[i] = INITIAL ∈ consensus-state3(V)
20. j : ℕ||y||@i
21. i < j
22. y[i] = L[i] ∈ consensus-state3(V)
23. L[j] = INITIAL ∈ consensus-state3(V)
24. j = i1 ∈ ℤ
25. y[i] = L[i] ∈ consensus-state3(V)
⊢ (y[j] = INITIAL ∈ consensus-state3(V)) ∨ (y[j] = WITHDRAWN ∈ consensus-state3(V))
BY
{ ((Assert (L[i] = WITHDRAWN ∈ consensus-state3(V))
          ∨ (L[i] = CONSIDERING[v] ∈ consensus-state3(V))
          ∨ (L[i] = COMMITED[v] ∈ consensus-state3(V)) BY
          (BackThruSomeHyp THEN Auto))
   THEN SplitOrHyps
   THEN RelRST) }

---

Latex:



1.  [V]  :  Type
2.  \mneg{}(INITIAL  =  WITHDRAWN)
3.  L  :  consensus-state3(V)  List@i
4.  y  :  consensus-state3(V)  List@i
5.  \mforall{}i:\mBbbN{}||L||
          \mforall{}j:\mBbbN{}||L||.  (L[j]  =  INITIAL)  \mvee{}  (L[j]  =  WITHDRAWN)  supposing  i  <  j  supposing  L[i]  =  INITIAL@i
6.  ||y||  =  ||L||@i
7.  i1  :  \mBbbN{}||L||@i
8.  \mforall{}j:\mBbbN{}||L||.  ((\mneg{}(j  =  i1))  {}\mRightarrow{}  (y[j]  =  L[j]))@i
9.  L[i1]  =  INITIAL@i
10.  v  :  V@i
11.  \mneg{}(COMMITED[v]  =  INITIAL)
12.  \mneg{}(CONSIDERING[v]  =  INITIAL)
13.  \mneg{}(COMMITED[v]  =  WITHDRAWN)
14.  \mneg{}(CONSIDERING[v]  =  WITHDRAWN)
15.  \mforall{}[v':V]
            ((\mneg{}(CONSIDERING[v]  =  COMMITED[v']))
            \mwedge{}  (\mneg{}(CONSIDERING[v]  =  CONSIDERING[v']))  \mwedge{}  (\mneg{}(COMMITED[v]  =  COMMITED[v']))  supposing  \mneg{}(v  =  v'))
16.  y[i1]  =  CONSIDERING[v]@i
17.  \mforall{}j:\mBbbN{}i1.  ((L[j]  =  WITHDRAWN)  \mvee{}  (L[j]  =  CONSIDERING[v])  \mvee{}  (L[j]  =  COMMITED[v]))@i
18.  i  :  \mBbbN{}||y||@i
19.  y[i]  =  INITIAL
20.  j  :  \mBbbN{}||y||@i
21.  i  <  j
22.  y[i]  =  L[i]
23.  L[j]  =  INITIAL
24.  j  =  i1
25.  y[i]  =  L[i]
\mvdash{}  (y[j]  =  INITIAL)  \mvee{}  (y[j]  =  WITHDRAWN)


By

((Assert  (L[i]  =  WITHDRAWN)  \mvee{}  (L[i]  =  CONSIDERING[v])  \mvee{}  (L[i]  =  COMMITED[v])  BY
                (BackThruSomeHyp  THEN  Auto))
  THEN  SplitOrHyps
  THEN  RelRST)

---

Home Index