---

Step * of Lemma consensus-ts4-estimate-domain

∀V:Type. ∀A:Id List. ∀W:{a:Id| (a ∈ A)}  List List. ∀a:{a:Id| (a ∈ A)} . ∀x:ts-reachable(consensus-ts4(V;A;W)). ∀i:ℤ.
  ((i ∈ fpf-domain(Estimate(x;a))) ⇒ (i ≤ Inning(x;a)))
BY
{ (RepeatFor 4 ((D 0 THENA Auto)) THEN BLemma `ts-reachable-induction` THEN Try (Complete (Auto))) }

1
.....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)) ─→ ℙ

2
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))))

3
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)))

4
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,y:ts-reachable(consensus-ts4(V;A;W)).
    ((∀i:ℤ. ((i ∈ fpf-domain(Estimate(x;a))) ⇒ (i ≤ Inning(x;a))))
    ⇒ (x ts-rel(consensus-ts4(V;A;W)) y)
    ⇒ (∀i:ℤ. ((i ∈ fpf-domain(Estimate(y;a))) ⇒ (i ≤ Inning(y;a)))))

---

Latex:


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


By

(RepeatFor  4  ((D  0  THENA  Auto))  THEN  BLemma  `ts-reachable-induction`  THEN  Try  (Complete  (Auto)))

---

Home Index