---

Step * of Lemma es-le-iff

∀the_es:EO. ∀e,e':E.  (e ≤loc e'  ⇐⇒ ((¬↑first(e')) c∧ e ≤loc pred(e') ) ∨ (e = e' ∈ E))
BY
{ (InstLemma `es-locl-iff` []⋅
   THEN RepeatFor 3 (ParallelLast')
   THEN Unfold `es-le` 0
   THEN RWO "-1" 0
   THEN Auto
   THEN SplitOrHyps
   THEN Auto
   THEN RepeatFor 2 ((D -1 THEN Auto))) }

---

Latex:


\mforall{}the$_{es}$:EO.  \mforall{}e,e':E.    (e  \mleq{}loc  e'    \mLeftarrow{}{}\mRightarrow{}  ((\mneg{}\muparrow{}first(e'))  c\mwedge{}  e  \mleq{}loc  pred(e')  )  \mvee{}  \000C(e  =  e'))


By

(InstLemma  `es-locl-iff`  []\mcdot{}
  THEN  RepeatFor  3  (ParallelLast')
  THEN  Unfold  `es-le`  0
  THEN  RWO  "-1"  0
  THEN  Auto
  THEN  SplitOrHyps
  THEN  Auto
  THEN  RepeatFor  2  ((D  -1  THEN  Auto)))

---

Home Index