---

(X&Y) ==
  eclass-compose4(x,y,x',y'.
                   if (bag-size(x) = 1)
                     then if (bag-size(y) = 1) then {<only(x), only(y)>}
                          if (bag-size(y') = 1) then {<only(x), only(y')>}
                          else {}
                          fi 
                   if (bag-size(y) = 1)
                     then if (bag-size(x') = 1)
                          then {<only(x'), only(y)>}
                          else {}
                          fi 
                   else {}
                   fi ;X;Y;Prior(X);Prior(Y))

---

Definitions occuring in Statement :  primed-class: Prior(X),  eclass-compose4: eclass-compose4(f;X;Y;Z;V),  eq_int: (i = j),  ifthenelse: if b then t else f fi ,  lambda: x.A[x],  pair: <a, b>,  natural_number: $n,  bag-only: only(bs),  bag-size: bag-size(bs),  single-bag: {x},  empty-bag: {}
Definitions :  eclass-compose4: eclass-compose4(f;X;Y;Z;V),  lambda: x.A[x],  ifthenelse: if b then t else f fi ,  eq_int: (i = j),  bag-size: bag-size(bs),  natural_number: $n,  single-bag: {x},  pair: <a, b>,  bag-only: only(bs),  empty-bag: {},  primed-class: Prior(X)
FDL editor aliases :  latest-pair

---

(X\&Y)  ==
    eclass-compose4(\mlambda{}x,y,x',y'.
                                      if  (bag-size(x)  =\msubz{}  1)
                                          then  if  (bag-size(y)  =\msubz{}  1)  then  \{<only(x),  only(y)>\}
                                                    if  (bag-size(y')  =\msubz{}  1)  then  \{<only(x),  only(y')>\}
                                                    else  \{\}
                                                    fi 
                                      if  (bag-size(y)  =\msubz{}  1)
                                          then  if  (bag-size(x')  =\msubz{}  1)  then  \{<only(x'),  only(y)>\}  else  \{\}  fi 
                                      else  \{\}
                                      fi  ;X;Y;Prior(X);Prior(Y))


Date html generated: 2011_08_16-PM-05_36_02
Last ObjectModification: 2011_01_20-PM-03_23_59

Home Index