Nuprl Lemma : interface-predecessors-filter-image

[Info,A,B:Type]. ∀[f:A ─→ bag(B)]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[e:E].
  (≤(f[X])(e) filter(λe.(#(f X(e)) =z 1);≤(X)(e)))


Proof




Definitions occuring in Statement :  es-interface-predecessors: (X)(e) es-filter-image: f[X] eclass-val: X(e) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-E: E filter: filter(P;l) eq_int: (i =z j) uall: [x:A]. B[x] apply: a lambda: λx.A[x] function: x:A ─→ B[x] natural_number: $n universe: Type sqequal: t bag-size: #(bs) bag: bag(T)
Lemmas :  filter-filter filter-sq Id_wf es-loc_wf es-le-before_wf l_member_wf set_wf in-eclass_wf es-filter-image_wf top_wf subtype_rel_dep_function bag_wf subtype_rel_bag es-interface-subtype_rel2 es-E_wf event-ordering+_subtype bool_wf eqtt_to_assert eq_int_wf bag-size_wf eclass-val_wf nat_wf is-filter-image-sq assert_wf eclass_wf event-ordering+_wf

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  bag(B)].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(A)].  \mforall{}[e:E].
    (\mleq{}(f[X])(e)  \msim{}  filter(\mlambda{}e.(\#(f  X(e))  =\msubz{}  1);\mleq{}(X)(e)))



Date html generated: 2015_07_21-PM-03_39_24
Last ObjectModification: 2015_01_27-PM-06_29_33

Home Index