Nuprl Lemma : classfun-res-disjoint-union-comb-as-parallel-eclass1

[Info,A,B,S:Type]. ∀[es:EO+(Info)]. ∀[X1:EClass(A)]. ∀[X2:EClass(B)]. ∀[e:E]. ∀[f1:Id ─→ A ─→ S ─→ S]. ∀[f2:Id
                                                                                                             ─→ B
                                                                                                             ─→ S
                                                                                                             ─→ S].
  ((f1 f2 loc(e) X1 (+) X2@e s) ((f1 X1) || (f2 X2)@e s) ∈ S) supposing 
     (disjoint-classrel(es;A;X1;B;X2) and 
     single-valued-classrel(es;X1;A) and 
     single-valued-classrel(es;X2;B) and 
     ((↑e ∈b X1) ∨ (↑e ∈b X2)))


Definitions occuring in Statement :  disjoint-union-tr: tr1 tr2 disjoint-union-comb: (+) Y parallel-class: || Y eclass1: (f X) classfun-res: X@e single-valued-classrel: single-valued-classrel(es;X;T) disjoint-classrel: disjoint-classrel(es;A;X;B;Y) member-eclass: e ∈b X eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-loc: loc(e) es-E: E Id: Id assert: b uimplies: supposing a uall: [x:A]. B[x] or: P ∨ Q apply: a function: x:A ─→ B[x] universe: Type equal: t ∈ T
Lemmas :  classfun-res-parallel-class-left eclass1_wf member-eclass-eclass1 event-ordering+_subtype eclass1-disjoint-classrel disjoint-classrel-symm disjoint-union-tr_wf es-loc_wf classfun-res-disjoint-union-comb-left classfun-res_wf eclass1-single-val iff_weakening_equal disj_un_tr_ap_inl_lemma classfun-res-eclass1 classfun-res-parallel-class-right classfun-res-disjoint-union-comb-right disj_un_tr_ap_inr_lemma

\mforall{}[Info,A,B,S:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X1:EClass(A)].  \mforall{}[X2:EClass(B)].  \mforall{}[e:E].  \mforall{}[f1:Id
                                                                                                                                                                        {}\mrightarrow{}  A
                                                                                                                                                                        {}\mrightarrow{}  S
                                                                                                                                                                        {}\mrightarrow{}  S].
\mforall{}[f2:Id  {}\mrightarrow{}  B  {}\mrightarrow{}  S  {}\mrightarrow{}  S].  \mforall{}[s:S].
    ((f1  +  f2  loc(e)  X1  (+)  X2@e  s)  =  ((f1  o  X1)  ||  (f2  o  X2)@e  s))  supposing 
          (disjoint-classrel(es;A;X1;B;X2)  and 
          single-valued-classrel(es;X1;A)  and 
          single-valued-classrel(es;X2;B)  and 
          ((\muparrow{}e  \mmember{}\msubb{}  X1)  \mvee{}  (\muparrow{}e  \mmember{}\msubb{}  X2)))

Date html generated: 2015_07_23-AM-11_29_26
Last ObjectModification: 2015_02_04-PM-04_44_36

Home Index