[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;
              bag0 : bag;
              bag1 : bag;
              bag2 : bag;
   
   

   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