---

Step * of Lemma es-le-pred

∀the_es:EO. ∀e,e':E.  e ≤loc pred(e')  ⇐⇒ (e <loc e') supposing ¬↑first(e')
BY
{ ((UnivCD THENA Auto)
   THEN RWO "es-locl-iff" 0
   THEN Auto
   THEN (All (Unfold `es-le`))
   THEN ((D (-1)) THENL [OrRight; OrLeft])
   THEN Auto) }

---

Latex:


\mforall{}the$_{es}$:EO.  \mforall{}e,e':E.    e  \mleq{}loc  pred(e')    \mLeftarrow{}{}\mRightarrow{}  (e  <loc  e')  supposing  \mneg{}\muparrow{}first(e')


By

((UnivCD  THENA  Auto)
  THEN  RWO  "es-locl-iff"  0
  THEN  Auto
  THEN  (All  (Unfold  `es-le`))
  THEN  ((D  (-1))  THENL  [OrRight;  OrLeft])
  THEN  Auto)

---

Home Index