---

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

.....wf..... 
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.∀i:ℤ. ((i ∈ fpf-domain(Estimate(x;a))) ⇒ (i ≤ Inning(x;a))) ∈ ts-reachable(consensus-ts4(V;A;W)) ─→ ℙ
BY
{ (MemCD THEN Try ((DVar `x' THEN All (RepUR ``ts-type consensus-ts4``))) THEN Auto) }

---

Latex:


.....wf..... 
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{}  \mlambda{}x.\mforall{}i:\mBbbZ{}.  ((i  \mmember{}  fpf-domain(Estimate(x;a)))  {}\mRightarrow{}  (i  \mleq{}  Inning(x;a)))
    \mmember{}  ts-reachable(consensus-ts4(V;A;W))  {}\mrightarrow{}  \mBbbP{}


By

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

---

Home Index