[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