---

Step * of Lemma es-pred-le

∀the_es:EO. ∀j:E.  pred(j) ≤loc j  supposing ¬↑first(j)
BY
{ (Auto THEN Unfold `es-le` 0 THEN OrLeft THEN Auto THEN BLemma `es-pred-locl` THEN Auto)⋅ }

---

Latex:


\mforall{}the$_{es}$:EO.  \mforall{}j:E.    pred(j)  \mleq{}loc  j    supposing  \mneg{}\muparrow{}first(j)


By

(Auto  THEN  Unfold  `es-le`  0  THEN  OrLeft  THEN  Auto  THEN  BLemma  `es-pred-locl`  THEN  Auto)\mcdot{}

---

Home Index