Nuprl Lemma : es-interface-or-hasright

[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B:EClass(Top)]. ∀[e:E].  oob-hasright((A B)(e)) e ∈b supposing ↑e ∈b (A B)


Proof




Definitions occuring in Statement :  es-interface-or: (X Y) eclass-val: X(e) in-eclass: e ∈b X eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-E: E assert: b uimplies: supposing a uall: [x:A]. B[x] top: Top universe: Type sqequal: t oob-hasright: oob-hasright(x)
Lemmas :  eq_int_wf bag-size_wf bool_wf eqtt_to_assert assert_of_eq_int nat_wf bag_only_single_lemma subtype_base_sq bool_subtype_base btrue_wf eqff_to_assert equal_wf bool_cases_sqequal bag_size_single_lemma assert-bnot neg_assert_of_eq_int bfalse_wf assert_wf one_or_both_wf single-bag_wf oobboth_wf oobleft_wf bag_size_empty_lemma in-eclass_wf es-interface-or_wf top_wf es-interface-subtype_rel2 es-E_wf event-ordering+_subtype event-ordering+_wf subtype_top eclass_wf

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A,B:EClass(Top)].  \mforall{}[e:E].
    oob-hasright((A  |  B)(e))  \msim{}  e  \mmember{}\msubb{}  B  supposing  \muparrow{}e  \mmember{}\msubb{}  (A  |  B)



Date html generated: 2015_07_20-PM-03_25_56
Last ObjectModification: 2015_01_27-PM-10_20_02

Home Index