### 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].`
`∀[s:S].`
`  ((f1 + f2 loc(e) X1 (+) X2@e s) = ((f1 o X1) || (f2 o 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)))`

Proof

Definitions occuring in Statement :  disjoint-union-tr: `tr1 + tr2` disjoint-union-comb: `X (+) Y` parallel-class: `X || Y` eclass1: `(f o 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: `b supposing a` uall: `∀[x:A]. B[x]` or: `P ∨ Q` apply: `f a` function: `x:A ─→ B[x]` universe: `Type` equal: `s = 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

Latex:
\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