---

Step * 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
{ RemoveUniform Auto (Auto THEN (All (RepUR ``consensus-ts4 ts-type ts-rel``)⋅ THEN Auto))⋅ }

1
∀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))

---

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

RemoveUniform  Auto  (Auto  THEN  (All  (RepUR  ``consensus-ts4  ts-type  ts-rel``)\mcdot{}  THEN  Auto))\mcdot{}

---

Home Index