---

Step * of Lemma is-prior-interface

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

---

Latex:

---

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


By

---

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

---

Home Index