---

Step * of Lemma es-interface-local-pred-bool

∀[Info:Type]
  ∀P:es:EO+(Info) ⟶ E ⟶ 𝔹
    ∃X:EClass({e':E| (e' <loc e) ∧ (↑(P es e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑(P es e''))))} )
     ∀es:EO+(Info). ∀e:E.
       ((↑e ∈b X ⇐⇒ ∃a:E. ((a <loc e) ∧ (↑(P es a)))) ∧ es-p-local-pred(es;λe.(↑(P es e))) e X(e) supposing ↑e ∈b X)
BY
{ ((InstLemma `es-local-pred-property` []
    THEN ParallelLast'
    THEN Auto
    THEN ((With ⌜local-pred-class(P)⌝ (D 0)⋅ THENA Auto)
    THENM (ParallelOp -2 THEN ParallelLast THEN (InstHyp [⌜P es⌝] (-1)⋅ THENA Auto))
    ))
   THEN MoveToConcl (-1)
   THEN (RepUR ``local-pred-class in-eclass eclass-val es-p-local-pred`` 0⋅ THEN RepUR ``can-apply do-apply`` 0⋅)
   THEN GenConclAtAddr [1;1;1;1;1]
   THEN D -2
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}P:es:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbB{}
        \mexists{}X:EClass(\{e':E| 
                              (e'  <loc  e)
                              \mwedge{}  (\muparrow{}(P  es  e'))
                              \mwedge{}  (\mforall{}e'':E.  ((e'  <loc  e'')  {}\mRightarrow{}  (e''  <loc  e)  {}\mRightarrow{}  (\mneg{}\muparrow{}(P  es  e''))))\}  )
          \mforall{}es:EO+(Info).  \mforall{}e:E.
              ((\muparrow{}e  \mmember{}\msubb{}  X  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:E.  ((a  <loc  e)  \mwedge{}  (\muparrow{}(P  es  a))))
              \mwedge{}  es-p-local-pred(es;\mlambda{}e.(\muparrow{}(P  es  e)))  e  X(e)  supposing  \muparrow{}e  \mmember{}\msubb{}  X)


By

---

Latex:
((InstLemma  `es-local-pred-property`  []
    THEN  ParallelLast'
    THEN  Auto
    THEN  ((With  \mkleeneopen{}local-pred-class(P)\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto)
    THENM  (ParallelOp  -2  THEN  ParallelLast  THEN  (InstHyp  [\mkleeneopen{}P  es\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto))
    ))
  THEN  MoveToConcl  (-1)
  THEN  (RepUR  ``local-pred-class  in-eclass  eclass-val  es-p-local-pred``  0\mcdot{}
              THEN  RepUR  ``can-apply  do-apply``  0\mcdot{}
              )
  THEN  GenConclAtAddr  [1;1;1;1;1]
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto)

---

Home Index