-- --------------------------------------------------------------
-- Axioms for class BoundedBag
-- --------------------------------------------------------------


ax1	equal( remove(gen(MX), int e), 
                gen(MX)         	)

ax2  	equal( remove(add(BBag S, int e1), int e2)
  	        ,(e1==e2)
     	            ? (has(S,e) ? add(remove(S,e),e) : S)
    	            : add(remove(S,e2),e1))

ax2a	equal( remove(add_many(S, e, int c), e)
		, (c != 0)
		    ? add_many(S, e, int(int(c)-1))
		    : remove(S, e))

ax3  	has(gen(MX), e) == false

ax4  	has(add(S,e1),e2) == ( (e1==e2) ? true : has(S,e2) )

ax5  	empty(gen(MX)) == true

ax6  	empty(add(S,e)) == false

addCommutes	
   equal( add(add(S,e1),e2),
      	   add(add(S,e2),e1)	)

addRemCommute
   equal(remove(add(S,e),e),	(has(S,e) ? add(remove(S,e),e) : S))

sizeUp
   size(add(S,e)) == size(S)+1