---

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

∀[Info:Type]. ∀es:EO+(Info). ∀X:EClass(Top). ∀e:E(prior(X)). ∀e':E(X).  ((prior(X)(e) <loc e') ⇒ e ≤loc e' )
BY
{ (Auto
   THEN ((InstLemma `es-prior-interface-val` [⌜Info⌝;⌜es⌝; ⌜X⌝; ⌜e⌝])⋅ THENM SupposeNot)
   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(prior(X)).  \mforall{}e':E(X).    ((prior(X)(e)  <loc  e')  {}\mRightarrow{}  e  \mleq{}loc  e'  )


By

---

Latex:
(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  (InstHyp  [\mkleeneopen{}e'\mkleeneclose{}]  (-2))\mcdot{}
  THEN  Auto
  THEN  Try  ((DoSubsume  THEN  Auto)))

---

Home Index