---

Step * of Lemma es-prior-interface-val

∀[Info:Type]
  ∀es:EO+(Info). ∀X:EClass(Top). ∀e:E.
    (prior(X)(e) <loc e) ∧ (↑prior(X)(e) ∈b X) ∧ (∀e'':E. ((e'' <loc e) ⇒ (prior(X)(e) <loc e'') ⇒ (¬↑e'' ∈b X))) 
    supposing ↑e ∈b prior(X)
BY
{ ((UnivCD THENA Auto)
   THEN ((InstLemma `es-local-pred-property` [⌜Info⌝;⌜es⌝;⌜e⌝; ⌜λe.e ∈b X⌝])⋅ THENA Auto)
   THEN (MoveToConcl (-2)
         THEN MoveToConcl (-1)
         THEN RepUR ``es-prior-interface local-pred-class in-eclass eclass-val`` 0
         THEN RepUR ``can-apply do-apply`` 0
         THEN ((GenConclAtAddr [1;1;1;1;1] THENA (Reduce 0 THEN Auto)) THEN D (-2) THEN Reduce 0 THEN Auto)⋅)⋅) }

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}e:E.
        (prior(X)(e)  <loc  e)
        \mwedge{}  (\muparrow{}prior(X)(e)  \mmember{}\msubb{}  X)
        \mwedge{}  (\mforall{}e'':E.  ((e''  <loc  e)  {}\mRightarrow{}  (prior(X)(e)  <loc  e'')  {}\mRightarrow{}  (\mneg{}\muparrow{}e''  \mmember{}\msubb{}  X))) 
        supposing  \muparrow{}e  \mmember{}\msubb{}  prior(X)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  ((InstLemma  `es-local-pred-property`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};  \mkleeneopen{}\mlambda{}e.e  \mmember{}\msubb{}  X\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  (MoveToConcl  (-2)
              THEN  MoveToConcl  (-1)
              THEN  RepUR  ``es-prior-interface  local-pred-class  in-eclass  eclass-val``  0
              THEN  RepUR  ``can-apply  do-apply``  0
              THEN  ((GenConclAtAddr  [1;1;1;1;1]  THENA  (Reduce  0  THEN  Auto))
                          THEN  D  (-2)
                          THEN  Reduce  0
                          THEN  Auto)\mcdot{})\mcdot{})

---

Home Index