Nuprl Lemma : is-accum-class

[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[b,f:Top]. ∀[e:E].  (e ∈b accum-class(b,a.f[b;a];a.b[a];X) e ∈b X)


Proof




Definitions occuring in Statement :  accum-class: accum-class(a,x.f[a; x];x.base[x];X) in-eclass: e ∈b X eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-E: E uall: [x:A]. B[x] top: Top so_apply: x[s1;s2] so_apply: x[s] universe: Type sqequal: t
Lemmas :  eq_int_wf bag-size_wf bool_wf eqtt_to_assert assert_of_eq_int nat_wf bag_size_single_lemma eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int bag_size_empty_lemma es-E_wf event-ordering+_subtype top_wf event-ordering+_wf bag_wf

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[b,f:Top].  \mforall{}[e:E].
    (e  \mmember{}\msubb{}  accum-class(b,a.f[b;a];a.b[a];X)  \msim{}  e  \mmember{}\msubb{}  X)



Date html generated: 2015_07_20-PM-03_48_41
Last ObjectModification: 2015_01_27-PM-10_07_37

Home Index