---

Step * of Lemma es-le-prior-interface-val

∀[Info:Type]. ∀es:EO+(Info). ∀X:EClass(Top). ∀e:E. ∀e':E(X).  ((e' <loc e) ⇒ e' ≤loc prior(X)(e) )
BY
{ (Auto
   THEN (Assert ↑e ∈b prior(X) BY
               (RWO "es-is-prior-interface" 0 THEN Auto))
   THEN ((InstLemma `es-prior-interface-val` [⌈Info⌉;⌈es⌉; ⌈X⌉; ⌈e⌉])⋅ THENM SupposeNot)
   THEN Auto
   THEN Try ((DoSubsume THEN Auto))
   THEN (InstHyp [⌈e'⌉] (-2))⋅
   THEN Auto
   THEN Try ((DoSubsume THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}e:E.  \mforall{}e':E(X).    ((e'  <loc  e)  {}\mRightarrow{}  e'  \mleq{}loc  prior(X)(e)  )


By

---

Latex:
(Auto
  THEN  (Assert  \muparrow{}e  \mmember{}\msubb{}  prior(X)  BY
                          (RWO  "es-is-prior-interface"  0  THEN  Auto))
  THEN  ((InstLemma  `es-prior-interface-val`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}X\mkleeneclose{};  \mkleeneopen{}e\mkleeneclose{}])\mcdot{}  THENM  SupposeNot)
  THEN  Auto
  THEN  Try  ((DoSubsume  THEN  Auto))
  THEN  (InstHyp  [\mkleeneopen{}e'\mkleeneclose{}]  (-2))\mcdot{}
  THEN  Auto
  THEN  Try  ((DoSubsume  THEN  Auto)))

---

Home Index