---

Step * 1 2 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. 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|| ∈ ℤ)
13. ||L @ [INITIAL]|| = (||L|| + 1) ∈ ℤ
⊢ (L @ [INITIAL][j] = INITIAL ∈ consensus-state3(V)) ∨ (L @ [INITIAL][j] = WITHDRAWN ∈ consensus-state3(V))
BY
{ ((RWO "select_append_front" 0 THENA Auto') THEN InstHyp [⌈i⌉;⌈j⌉] 7⋅ THEN 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.  L  @  [INITIAL]  \mmember{}  consensus-state3(V)  List
7.  \mforall{}i:\mBbbN{}||L||
          \mforall{}j:\mBbbN{}||L||.  (L[j]  =  INITIAL)  \mvee{}  (L[j]  =  WITHDRAWN)  supposing  i  <  j  supposing  L[i]  =  INITIAL@i
8.  i  :  \mBbbN{}||L  @  [INITIAL]||
9.  L  @  [INITIAL][i]  =  INITIAL
10.  j  :  \mBbbN{}||L  @  [INITIAL]||
11.  i  <  j
12.  \mneg{}(j  =  ||L||)
13.  ||L  @  [INITIAL]||  =  (||L||  +  1)
\mvdash{}  (L  @  [INITIAL][j]  =  INITIAL)  \mvee{}  (L  @  [INITIAL][j]  =  WITHDRAWN)


By

((RWO  "select\_append\_front"  0  THENA  Auto')  THEN  InstHyp  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{}]  7\mcdot{}  THEN  Auto)

---

Home Index