---

Step * 1 of Lemma consensus-ts3-invariant1


∀V:Type. ∀L:ts-reachable(consensus-ts3(V)). ∀v:V.
  (((CONSIDERING[v] ∈ L) ∨ (COMMITED[v] ∈ L))
  ⇒ (∀v':V. (((CONSIDERING[v'] ∈ L) ∨ (COMMITED[v'] ∈ L)) ⇒ (v' = v ∈ V))))
BY
{ ((D 0 THENA Auto)
   THEN BLemma `ts-reachable-induction` 
   THEN Auto
   THEN Try (Complete (((All (Unfold `ts-reachable`) THEN AllHyps h.DSet h )
                        THEN All (RepUR ``consensus-ts3 ts-type ts-init ts-rel``)
                        THEN Auto)))) }

1
1. V : Type@i'
2. v : V@i
3. (CONSIDERING[v] ∈ ts-init(consensus-ts3(V))) ∨ (COMMITED[v] ∈ ts-init(consensus-ts3(V)))@i
4. v' : V@i
5. (CONSIDERING[v'] ∈ ts-init(consensus-ts3(V))) ∨ (COMMITED[v'] ∈ ts-init(consensus-ts3(V)))@i
⊢ v' = v ∈ V

2
1. V : Type@i'
2. L : ts-reachable(consensus-ts3(V))@i
3. y : ts-reachable(consensus-ts3(V))@i
4. ∀v:V
     (((CONSIDERING[v] ∈ L) ∨ (COMMITED[v] ∈ L))
     ⇒ (∀v':V. (((CONSIDERING[v'] ∈ L) ∨ (COMMITED[v'] ∈ L)) ⇒ (v' = v ∈ V))))@i
5. L ts-rel(consensus-ts3(V)) y@i
6. v : V@i
7. (CONSIDERING[v] ∈ y) ∨ (COMMITED[v] ∈ y)@i
8. v' : V@i
9. (CONSIDERING[v'] ∈ y) ∨ (COMMITED[v'] ∈ y)@i
⊢ v' = v ∈ V

---

Latex:



\mforall{}V:Type.  \mforall{}L:ts-reachable(consensus-ts3(V)).  \mforall{}v:V.
    (((CONSIDERING[v]  \mmember{}  L)  \mvee{}  (COMMITED[v]  \mmember{}  L))
    {}\mRightarrow{}  (\mforall{}v':V.  (((CONSIDERING[v']  \mmember{}  L)  \mvee{}  (COMMITED[v']  \mmember{}  L))  {}\mRightarrow{}  (v'  =  v))))


By

((D  0  THENA  Auto)
  THEN  BLemma  `ts-reachable-induction` 
  THEN  Auto
  THEN  Try  (Complete  (((All  (Unfold  `ts-reachable`)  THEN  AllHyps  h.DSet  h  )
                                            THEN  All  (RepUR  ``consensus-ts3  ts-type  ts-init  ts-rel``)
                                            THEN  Auto))))

---

Home Index