[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification bag-basic
enrich
   nat
with
   sorts Bag[A];
   constants 
       ∅ : Bag[A];
   
   functions 
       . ++ . : Bag[A] × A → Bag[A] prio 9 left;
       . count ( . ) : Bag[A] × A → Nat;
   
   variables 
       bag : Bag[A];
       a : A;
       b : A;
   
   induction 
      Bag[A] generated by ∅ : Bag[A],  . ++ .  : (Bag[A] × A → Bag[A]);
   
   axioms 
      extension: bag0 = bag1 ↔ (∀ a. bag0.count(a) = bag1.count(a));
      
      count-empty: ∅.count(a) = 0;
      used for: s, ls;
      
      count-insert: (bag ++ b).count(a) = (a = b ⊃ 1;0) + bag.count(a);
      used for: ls;
   
   
end enrich