---

Step * of Lemma eo-forward-E

∀[eo:EO]. ∀[e:E].  (E ~ {e@0:es-base-E(eo)| ↑((es-dom(eo) e@0) ∧b (e ≤loc e@0 ∨b(¬bloc(e@0) = loc(e))))} )
BY
{ ((UnivCD THENA Auto) THEN RepUR ``es-E eo-forward eo-restrict`` 0 THEN Folds ``es-base-E es-dom`` 0 THEN Auto) }

---

Latex:


\mforall{}[eo:EO].  \mforall{}[e:E].
    (E  \msim{}  \{e@0:es-base-E(eo)|  \muparrow{}((es-dom(eo)  e@0)  \mwedge{}\msubb{}  (e  \mleq{}loc  e@0  \mvee{}\msubb{}(\mneg{}\msubb{}loc(e@0)  =  loc(e))))\}  )


By

((UnivCD  THENA  Auto)
  THEN  RepUR  ``es-E  eo-forward  eo-restrict``  0
  THEN  Folds  ``es-base-E  es-dom``  0
  THEN  Auto)

---

Home Index