Nuprl Lemma : es-E-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((I|¬p)) ⊆E(I))


Proof




Definitions occuring in Statement :  es-interface-co-restrict: (I|¬p) es-E-interface: E(X) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-E: E decidable: Dec(P) subtype_rel: A ⊆B uall: [x:A]. B[x] prop: so_apply: x[s1;s2] all: x:A. B[x] function: x:A ─→ B[x] universe: Type
Lemmas :  es-E-interface_functionality es-interface-co-restrict_wf top_wf es-interface-subtype_rel2 es-E_wf event-ordering+_subtype es-is-interface-co-restrict assert_wf in-eclass_wf event-ordering+_wf all_wf decidable_wf eclass_wf

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)].
    (E((I|\mneg{}p))  \msubseteq{}r  E(I))



Date html generated: 2015_07_20-PM-03_31_14
Last ObjectModification: 2015_01_27-PM-10_17_24

Home Index