[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
generic specification
   parameter elem
   using nat
target
   sorts Bag;
   constants 
       ∅ : Bag;
   
   functions 
       . ++ . : Bag × Elem → Bag prio 9 left;
       count : Elem × Bag → Nat;
   
   variables 
       bag : Bag;
       a : Elem;
       b : Elem;
   
   induction 
      Bag generated by ∅,  . ++ . ;
   
   axioms 
      extension: bag0 = bag1 ↔ (∀ a. count(a, bag0) = count(a, bag1));
      
      count-empty: count(a, ∅) = 0;
      used for: s, ls;
      
      count-insert: count(a, bag ++ b) = (a = b ⊃ 1;0) + count(a, bag);
      used for: ls;
   
   
end generic specification