---

Step * 2 of Lemma consensus-ts4-estimate-domain


1. V : Type@i'
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
4. a : {a:Id| (a ∈ A)} @i
⊢ ∀x:ts-reachable(consensus-ts4(V;A;W)). SqStable(∀i:ℤ. ((i ∈ fpf-domain(Estimate(x;a))) ⇒ (i ≤ Inning(x;a))))
BY
{ ((D 0 THENA Auto) THEN Try ((DVar `x' THEN All (RepUR ``ts-type consensus-ts4``))) THEN Auto) }

---

Latex:



1.  V  :  Type@i'
2.  A  :  Id  List@i
3.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
4.  a  :  \{a:Id|  (a  \mmember{}  A)\}  @i
\mvdash{}  \mforall{}x:ts-reachable(consensus-ts4(V;A;W))
        SqStable(\mforall{}i:\mBbbZ{}.  ((i  \mmember{}  fpf-domain(Estimate(x;a)))  {}\mRightarrow{}  (i  \mleq{}  Inning(x;a))))


By

((D  0  THENA  Auto)  THEN  Try  ((DVar  `x'  THEN  All  (RepUR  ``ts-type  consensus-ts4``)))  THEN  Auto)

---

Home Index