(fmod BAG is
  sorts Bin Bag .
  op z : -> Bin .
  op 0 : Bin -> Bin .
  op 1 : Bin -> Bin .
  op plus : Bin Bin -> Bin [assoc comm] .
  op mult : Bin Bin -> Bin [assoc comm] .
  op empty : -> Bag .
  op singl : Bin -> Bag .
  op union : Bag Bag -> Bag [assoc comm id: empty] .
  ops sum prod : Bag -> Bin .
  vars A B : Bag .
  vars X Y : Bin .
  eq 0(z) = z .
  eq plus(z,X) = X .
  eq plus(0(X),0(Y)) = 0(plus(X,Y)) .
  eq plus(0(X),1(Y)) = 1(plus(X,Y)) .
  eq plus(1(X),1(Y)) = 0(plus(plus(X,Y),1(z))) .
  eq mult(z,X) = z .
  eq mult(0(X),Y) = 0(mult(X,Y)) .
  eq mult(1(X),Y) = plus(0(mult(X,Y)),Y) .
  eq sum(empty) = 0(z) . 	
  eq sum(singl(X)) = X . 
  eq sum(union(A,B)) = plus(sum(A),sum(B)) .
  eq prod(empty) = 1(z) . 
  eq prod(singl(X)) = X . 
  eq prod(union(A,B)) = mult(prod(A),prod(B)) .
endfm)