---

Step * 4 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,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)))))
BY
{ (((D 0 THENA Auto) THEN DVar `x' THEN Thin (-1) THEN RepUR ``ts-type consensus-ts4`` -1)
   THEN (D 0 THENA Auto)
   THEN DVar `y'
   THEN Thin (-1)
   THEN RepUR ``ts-type consensus-ts4`` -1
   THEN Auto) }

1
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
5. x : ConsensusState@i
6. y : ConsensusState@i
7. ∀i:ℤ. ((i ∈ fpf-domain(Estimate(x;a))) ⇒ (i ≤ Inning(x;a)))@i
8. x ts-rel(consensus-ts4(V;A;W)) y@i
9. i : ℤ@i
10. (i ∈ fpf-domain(Estimate(y;a)))@i
⊢ i ≤ Inning(y;a)

---

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


By

(((D  0  THENA  Auto)  THEN  DVar  `x'  THEN  Thin  (-1)  THEN  RepUR  ``ts-type  consensus-ts4``  -1)
  THEN  (D  0  THENA  Auto)
  THEN  DVar  `y'
  THEN  Thin  (-1)
  THEN  RepUR  ``ts-type  consensus-ts4``  -1
  THEN  Auto)

---

Home Index