---

Step * 3 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
⊢ ∀i:ℤ. ((i ∈ fpf-domain(Estimate(ts-init(consensus-ts4(V;A;W));a))) ⇒ (i ≤ Inning(ts-init(consensus-ts4(V;A;W));a)))
BY
{ (RepUR ``ts-init consensus-ts4 cs-estimate cs-inning`` 0 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{}i:\mBbbZ{}
        ((i  \mmember{}  fpf-domain(Estimate(ts-init(consensus-ts4(V;A;W));a)))
        {}\mRightarrow{}  (i  \mleq{}  Inning(ts-init(consensus-ts4(V;A;W));a)))


By

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

---

Home Index