---

Step * 1 of Lemma consensus-ts4-inning-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.Inning(x;a) ≤ Inning(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) }

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. CR[x,y]@i
⊢ Inning(x;a) ≤ 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)\}  .
    ts-stable-rel(consensus-ts4(V;A;W);x,y.Inning(x;a)  \mleq{}  Inning(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)

---

Home Index