---

Step * 4 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. v : V@i
10. ((¬(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)))
11. L[i1] = CONSIDERING[v] ∈ consensus-state3(V)@i
12. y[i1] = COMMITED[v] ∈ consensus-state3(V)@i
13. i : ℕ||y||@i
14. y[i] = INITIAL ∈ consensus-state3(V)
15. j : ℕ||y||@i
16. i < j
17. y[i] = L[i] ∈ consensus-state3(V)
18. (L[j] = INITIAL ∈ consensus-state3(V)) ∨ (L[j] = WITHDRAWN ∈ consensus-state3(V))
⊢ (y[j] = INITIAL ∈ consensus-state3(V)) ∨ (y[j] = WITHDRAWN ∈ consensus-state3(V))
BY
{ (Decide j = i1 ∈ ℤ
   THEN Auto
   THEN Try ((Assert y[i] = L[i] ∈ consensus-state3(V) BY Auto))
   THEN SplitOrHyps
   THEN Auto
   THEN Try (OnMaybeHyp 16 (\h. (D h THEN Complete (Auto))))) }

---

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.  v  :  V@i
10.  ((\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')))
11.  L[i1]  =  CONSIDERING[v]@i
12.  y[i1]  =  COMMITED[v]@i
13.  i  :  \mBbbN{}||y||@i
14.  y[i]  =  INITIAL
15.  j  :  \mBbbN{}||y||@i
16.  i  <  j
17.  y[i]  =  L[i]
18.  (L[j]  =  INITIAL)  \mvee{}  (L[j]  =  WITHDRAWN)
\mvdash{}  (y[j]  =  INITIAL)  \mvee{}  (y[j]  =  WITHDRAWN)


By

(Decide  j  =  i1
  THEN  Auto
  THEN  Try  ((Assert  y[i]  =  L[i]  BY  Auto))
  THEN  SplitOrHyps
  THEN  Auto
  THEN  Try  (OnMaybeHyp  16  (\mbackslash{}h.  (D  h  THEN  Complete  (Auto)))))

---

Home Index