---

Step * 3 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))) ∧ (¬(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)))
12. y[i1] = CONSIDERING[v] ∈ consensus-state3(V)@i
13. ∀j:ℕi1
      ((L[j] = WITHDRAWN ∈ consensus-state3(V))
      ∨ (L[j] = CONSIDERING[v] ∈ consensus-state3(V))
      ∨ (L[j] = COMMITED[v] ∈ consensus-state3(V)))@i
14. i : ℕ||y||@i
15. y[i] = INITIAL ∈ consensus-state3(V)
16. j : ℕ||y||@i
17. i < j
18. y[i] = L[i] ∈ consensus-state3(V)
19. (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))))) }

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

---

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