---

Step * of Lemma decidable__cut-order

∀[Info:Type]. ∀es:EO+(Info). ∀X:EClass(Top). ∀f:sys-antecedent(es;X). ∀a,b:E(X).  Dec(a ≤(X;f) b)
BY
{ (Auto THEN Unfold `cut-order` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}f:sys-antecedent(es;X).  \mforall{}a,b:E(X).    Dec(a  \mleq{}(X;f)  b)


By

---

Latex:
(Auto  THEN  Unfold  `cut-order`  0  THEN  Auto)

---

Home Index