---

Step * 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. ∀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|| ∈ ℤ@i
8. i1 : ℕ||L||@i
9. ∀j:ℕ||L||. ((¬(j = i1 ∈ ℤ)) ⇒ (y[j] = L[j] ∈ consensus-state3(V)))@i
10. L[i1] = INITIAL ∈ consensus-state3(V)@i
11. y[i1] = WITHDRAWN ∈ consensus-state3(V)@i
12. i : ℕ||y||@i
13. y[i] = INITIAL ∈ consensus-state3(V)
14. j : ℕ||y||@i
15. i < j
16. y[i] = L[i] ∈ consensus-state3(V)
17. (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.  \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||@i
8.  i1  :  \mBbbN{}||L||@i
9.  \mforall{}j:\mBbbN{}||L||.  ((\mneg{}(j  =  i1))  {}\mRightarrow{}  (y[j]  =  L[j]))@i
10.  L[i1]  =  INITIAL@i
11.  y[i1]  =  WITHDRAWN@i
12.  i  :  \mBbbN{}||y||@i
13.  y[i]  =  INITIAL
14.  j  :  \mBbbN{}||y||@i
15.  i  <  j
16.  y[i]  =  L[i]
17.  (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