Step
*
of Lemma
es-interface-local-pred
∀[Info:Type]. ∀[P:es:EO+(Info) ─→ E ─→ ℙ].
((∀es:EO+(Info). ∀e:E. Dec(P es e))
⇒ (∃X:EClass(E)
∀es:EO+(Info). ∀e:E.
((↑e ∈b X
⇐⇒ ∃a:E. (es-p-local-pred(es;P es) e a)) ∧ es-p-local-pred(es;P es) e X(e) supposing ↑e ∈b X)))
BY
{ (Auto
THEN (InstLemma `es-interface-from-decidable` [⌈Info⌉;⌈λ2es e.E⌉;⌈so_lambda(es,e,a.es-p-local-pred(es;P es) e a)⌉])⋅
THEN Auto) }
Latex:
Latex:
\mforall{}[Info:Type]. \mforall{}[P:es:EO+(Info) {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}].
((\mforall{}es:EO+(Info). \mforall{}e:E. Dec(P es e))
{}\mRightarrow{} (\mexists{}X:EClass(E)
\mforall{}es:EO+(Info). \mforall{}e:E.
((\muparrow{}e \mmember{}\msubb{} X \mLeftarrow{}{}\mRightarrow{} \mexists{}a:E. (es-p-local-pred(es;P es) e a))
\mwedge{} es-p-local-pred(es;P es) e X(e) supposing \muparrow{}e \mmember{}\msubb{} X)))
By
Latex:
(Auto
THEN (InstLemma `es-interface-from-decidable` [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}es e.E\mkleeneclose{};
\mkleeneopen{}so\_lambda(es,e,a.es-p-local-pred(es;P es) e a)\mkleeneclose{}])\mcdot{}
THEN Auto)
Home
Index