
#ifndef MULTISETRETAIN_H_INCLUDED
#define MULTISETRETAIN_H_INCLUDED

#include "CountLogic.h"

/*@
  predicate
    MultisetRetain{K,L}(value_type* a, integer n, value_type v) =
      Count{K}(a, n, v) == Count{L}(a, n, v);
*/

#endif /* MULTISETRETAIN_H_INCLUDED */

