typedef unsigned short int Action;
typedef Action* MultiSetType;


void multiset_difference(MultiSetType mm1, MultiSetType mm2);

/*@ axiomatic IntMultiSetTheory {
  @ type int_multiset;
  @
  @ logic int_multiset empty_int_multiset;
  @ logic int_multiset add_int_multiset(int_multiset s, Action i);
  @ logic integer contains(int_multiset s, integer i);

  @
  @ axiom contains_empty_multiset:
  @  \forall Action i; 
  @         contains(empty_int_multiset, i) == 0;
  @
  @
  @ axiom add_int_multiset_trans:
  @  \forall int_multiset s, Action i, Action j; 
  @    add_int_multiset(add_int_multiset(s,i),j) == 
  @                           add_int_multiset(add_int_multiset(s,j),i); 
  @
  @ 
  @ axiom contains_add_multiset:
  @  \forall int_multiset s, Action i; contains(add_int_multiset(s,i),i) == contains(s,i) + 1;
  @
  @  
  @ axiom contains3_multiset:
  @  \forall int_multiset s, Action i, Action j; 
  @                  (i != j) 
  @               ==>  
  @                    (contains(add_int_multiset(s,i),j) == contains(s,j) );
  @ 
  @
  @
  @
  @	lemma test:
  @		\forall integer c, int_multiset s;
  @			
  @				(\forall integer i; (sizeof(Action) <= i < sizeof(c))
  @					==> (contains(s, i) == 0) );
  @ }
  @*/

#include <stdlib.h>
#include "multiset_diff.h"/*Added*/


void multiset_difference(MultiSetType/*MultiSet*/ mm1, MultiSetType/*MultiSet*/ mm2)
{

}