---

X+Y ==
  eclass-compose2(xs,ys.
                   if (bag-size(xs) = 1) then {inl only(xs) }
                   if (bag-size(ys) = 1) then {inr only(ys) }
                   else {}
                   fi ;X;Y)

---

Definitions occuring in Statement :  eclass-compose2: eclass-compose2(f;X;Y),  eq_int: (i = j),  ifthenelse: if b then t else f fi ,  lambda: x.A[x],  inr: inr x ,  inl: inl x ,  natural_number: $n,  bag-only: only(bs),  bag-size: bag-size(bs),  single-bag: {x},  empty-bag: {}
Definitions :  eclass-compose2: eclass-compose2(f;X;Y),  lambda: x.A[x],  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 :  es-interface-union

---

X+Y  ==
    eclass-compose2(\mlambda{}xs,ys.
                                      if  (bag-size(xs)  =\msubz{}  1)  then  \{inl  only(xs)  \}
                                      if  (bag-size(ys)  =\msubz{}  1)  then  \{inr  only(ys)  \}
                                      else  \{\}
                                      fi  ;X;Y)


Date html generated: 2011_08_16-PM-04_19_49
Last ObjectModification: 2011_01_15-PM-12_58_58

Home Index