---

Step * of Lemma eo-strict-forward-E

∀[Info:Type]. ∀[eo:EO+(Info)]. ∀[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-strict-forward eo-restrict`` 0
   THEN Folds ``es-base-E es-dom`` 0
   THEN Auto) }

---

Latex:


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


By

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

---

Home Index