---

Step * of Lemma eo-strict-forward-E-subtype2

∀[Info:Type]. ∀[eo:EO+(Info)]. ∀[e:E].  ({e':E| (loc(e') = loc(e) ∈ Id) ⇒ (e <loc e')}  ⊆r E)
BY
{ (Auto
   THEN RWO "eo-strict-forward-E" 0
   THEN Auto
   THEN D 0
   THEN Auto
   THEN Try (((MemTypeCD THEN Folds ``es-base-E es-dom`` 0) THEN Auto))) }

1
.....subterm..... T:t
1:n
1. Info : Type
2. eo : EO+(Info)
3. e : E
4. x : {e':E| (loc(e') = loc(e) ∈ Id) ⇒ (e <loc e')} @i
⊢ x ∈ {e@0:es-base-E(eo)| ↑((es-dom(eo) e@0) ∧b (e <loc e@0 ∨b(¬bloc(e@0) = loc(e))))} 

---

Latex:


\mforall{}[Info:Type].  \mforall{}[eo:EO+(Info)].  \mforall{}[e:E].    (\{e':E|  (loc(e')  =  loc(e))  {}\mRightarrow{}  (e  <loc  e')\}    \msubseteq{}r  E)


By

(Auto
  THEN  RWO  "eo-strict-forward-E"  0
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  Try  (((MemTypeCD  THEN  Folds  ``es-base-E  es-dom``  0)  THEN  Auto)))

---

Home Index