---

Step * 2 of Lemma consensus-ts5-archive-invariant


1. V : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. ∃v,v':V. (¬(v = v' ∈ V))@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)}  List List@i
⊢ ∀v:V. ∀b:{a:Id| (a ∈ A)} . ∀i:ℤ.
    (state fst(ts-init(consensus-ts5(V;A;W))) may consider v in inning i) supposing 
       ((Estimate(fst(ts-init(consensus-ts5(V;A;W)));b)(i) = v ∈ V) and 
       (↑i ∈ dom(Estimate(fst(ts-init(consensus-ts5(V;A;W)));b))))
BY
{ (RepUR ``ts-init consensus-ts5 cs-estimate`` 0 THEN Auto) }

---

Latex:



1.  V  :  Type
2.  \mforall{}v1,v2:V.    Dec(v1  =  v2)@i
3.  \mexists{}v,v':V.  (\mneg{}(v  =  v'))@i
4.  A  :  Id  List@i
5.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
\mvdash{}  \mforall{}v:V.  \mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}i:\mBbbZ{}.
        (state  fst(ts-init(consensus-ts5(V;A;W)))  may  consider  v  in  inning  i)  supposing 
              ((Estimate(fst(ts-init(consensus-ts5(V;A;W)));b)(i)  =  v)  and 
              (\muparrow{}i  \mmember{}  dom(Estimate(fst(ts-init(consensus-ts5(V;A;W)));b))))


By

(RepUR  ``ts-init  consensus-ts5  cs-estimate``  0  THEN  Auto)

---

Home Index