---

DisjointUnionComb() ==
  SimpleComb2(T.True;
              T.True;
              T1,T2.T1 + T2;
              v1,v2.if (bag-size(v1) = 1) then {inl only(v1) }
              if (bag-size(v2) = 1) then {inr only(v2) }
              else {}
              fi )

---

Definitions occuring in Statement :  SimpleComb2: SimpleComb2(T1.P1[T1];T2.P2[T2];T1,T2.F[T1; T2];a,b.H[a; b]),  eq_int: (i = j),  ifthenelse: if b then t else f fi ,  true: True,  inr: inr x ,  inl: inl x ,  union: left + right,  natural_number: $n,  bag-only: only(bs),  bag-size: bag-size(bs),  single-bag: {x},  empty-bag: {}
Definitions :  SimpleComb2: SimpleComb2(T1.P1[T1];T2.P2[T2];T1,T2.F[T1; T2];a,b.H[a; b]),  true: True,  union: left + right,  inl: inl x ,  ifthenelse: if b then t else f fi ,  eq_int: (i = j),  bag-size: bag-size(bs),  natural_number: $n,  single-bag: {x},  inr: inr x ,  bag-only: only(bs),  empty-bag: {}
FDL editor aliases :  DisjointUnionComb

---

DisjointUnionComb()  ==
    SimpleComb2(T.True;
                            T.True;
                            T1,T2.T1  +  T2;
                            v1,v2.if  (bag-size(v1)  =\msubz{}  1)  then  \{inl  only(v1)  \}
                            if  (bag-size(v2)  =\msubz{}  1)  then  \{inr  only(v2)  \}
                            else  \{\}
                            fi  )


Date html generated: 2011_08_17-PM-06_27_38
Last ObjectModification: 2011_01_20-AM-00_37_59

Home Index