Step
*
of Lemma
es-is-interface-co-restrict
∀[Info,A:Type]. ∀[I:EClass(A)]. ∀[P:es:EO+(Info) ─→ E ─→ ℙ]. ∀[p:∀es:EO+(Info). ∀e:E. Dec(P[es;e])]. ∀[es:EO+(Info)].
∀[e:E].
uiff(↑e ∈b (I|¬p);(↑e ∈b I) ∧ (¬P[es;e]))
BY
{ ((UnivCD THENA (Auto THEN Auto))
THEN RepUR ``es-interface-co-restrict in-eclass eclass-val`` 0
THEN (GenConcl ⌈(p es e) = Z ∈ Dec(P[es;e])⌉⋅ THENA (Auto THEN Auto))
THEN D (-2)
THEN Reduce 0
THEN Auto) }
Latex:
Latex:
\mforall{}[Info,A:Type]. \mforall{}[I:EClass(A)]. \mforall{}[P:es:EO+(Info) {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}].
\mforall{}[p:\mforall{}es:EO+(Info). \mforall{}e:E. Dec(P[es;e])]. \mforall{}[es:EO+(Info)]. \mforall{}[e:E].
uiff(\muparrow{}e \mmember{}\msubb{} (I|\mneg{}p);(\muparrow{}e \mmember{}\msubb{} I) \mwedge{} (\mneg{}P[es;e]))
By
Latex:
((UnivCD THENA (Auto THEN Auto))
THEN RepUR ``es-interface-co-restrict in-eclass eclass-val`` 0
THEN (GenConcl \mkleeneopen{}(p es e) = Z\mkleeneclose{}\mcdot{} THENA (Auto THEN Auto))
THEN D (-2)
THEN Reduce 0
THEN Auto)
Home
Index