---

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

∀[Info:Type]
  ∀P:es:EO+(Info) ⟶ E ⟶ 𝔹
    ∃X:EClass({e:E| ↑(P es e)} )
     ∀es:EO+(Info). ∀e:E.
       ((↑e ∈b X ⇐⇒ ∃a:E. (es-p-le-pred(es;λe.(↑(P es e))) e a))
       ∧ es-p-le-pred(es;λe.(↑(P es e))) e X(e) supposing ↑e ∈b X)
BY
{ (Auto THEN InstLemma `es-interface-le-pred` [⌜Info⌝;⌜λes,e. (↑(P es e))⌝]⋅ THEN All Reduce THEN Auto) }

1
1. [Info] : Type
2. P : es:EO+(Info) ⟶ E ⟶ 𝔹@i'
3. ∃X:EClass({e:E| ↑(P es e)} )
    ∀es:EO+(Info). ∀e:E.
      ((↑e ∈b X ⇐⇒ ∃a:{e:E| ↑(P es e)} . (es-p-le-pred(es;λe.(↑(P es e))) e a))
      ∧ es-p-le-pred(es;λe.(↑(P es e))) e X(e) supposing ↑e ∈b X)
⊢ ∃X:EClass({e:E| ↑(P es e)} )
   ∀es:EO+(Info). ∀e:E.
     ((↑e ∈b X ⇐⇒ ∃a:E. (es-p-le-pred(es;λe.(↑(P es e))) e a))
     ∧ es-p-le-pred(es;λe.(↑(P es e))) e X(e) supposing ↑e ∈b X)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  InstLemma  `es-interface-le-pred`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}\mlambda{}es,e.  (\muparrow{}(P  es  e))\mkleeneclose{}]\mcdot{}  THEN  All  Reduce  THEN  Auto\000C)

---

Home Index