Nuprl Lemma : classfun-res-parallel-class-left

[Info,A:Type]. ∀[es:EO+(Info)]. ∀[X,Y:EClass(A)]. ∀[e:E].
  (X || Y@e X@e) supposing (disjoint-classrel(es;A;X;A;Y) and (↑e ∈b X))


Definitions occuring in Statement :  parallel-class: || Y classfun-res: X@e disjoint-classrel: disjoint-classrel(es;A;X;B;Y) member-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] universe: Type sqequal: t
Lemmas :  assert-member-eclass empty-bag-iff-no-member equal-empty-bag bag-append-empty bag-subtype-list disjoint-classrel_wf assert_wf member-eclass_wf es-E_wf event-ordering+_subtype eclass_wf event-ordering+_wf

\mforall{}[Info,A:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X,Y:EClass(A)].  \mforall{}[e:E].
    (X  ||  Y@e  \msim{}  X@e)  supposing  (disjoint-classrel(es;A;X;A;Y)  and  (\muparrow{}e  \mmember{}\msubb{}  X))

Date html generated: 2015_07_23-AM-11_29_01
Last ObjectModification: 2015_01_28-PM-11_12_55

Home Index