---

Step * of Lemma consensus-ts4-estimate-rel

∀[V:Type]. ∀[A:Id List]. ∀[W:{a:Id| (a ∈ A)}  List List]. ∀[a:{a:Id| (a ∈ A)} ].
  ts-stable-rel(consensus-ts4(V;A;W);x,y.Estimate(x;a) ⊆ Estimate(y;a))
BY
{ (Auto
   THEN BLemma `ts-transitive-stable`
   THEN Auto
   THEN All (RepUR ``consensus-ts4 ts-type ts-rel``)
   THEN Auto
   THEN D 0
   THEN Auto
   THEN All Reduce
   THEN Auto) }

1
1. V : Type
2. A : Id List
3. W : {a:Id| (a ∈ A)}  List List
4. a : {a:Id| (a ∈ A)} 
5. a@0 : ConsensusState@i
6. b : ConsensusState@i
7. c : ConsensusState@i
8. Estimate(a@0;a) ⊆ Estimate(b;a)@i
9. Estimate(b;a) ⊆ Estimate(c;a)@i
⊢ Estimate(a@0;a) ⊆ Estimate(c;a)

2
1. V : Type
2. A : Id List
3. W : {a:Id| (a ∈ A)}  List List
4. a : {a:Id| (a ∈ A)} 
5. x : ConsensusState@i
6. y : ConsensusState@i
7. CR[x,y]@i
⊢ Estimate(x;a) ⊆ Estimate(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)\}  ].
    ts-stable-rel(consensus-ts4(V;A;W);x,y.Estimate(x;a)  \msubseteq{}  Estimate(y;a))


By

(Auto
  THEN  BLemma  `ts-transitive-stable`
  THEN  Auto
  THEN  All  (RepUR  ``consensus-ts4  ts-type  ts-rel``)
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  All  Reduce
  THEN  Auto)

---

Home Index