Specification bag-union

[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,

enrich
   bag-basic
with
   functions 
       { . } : elem → bag;
       . -- . : bag × elem → bag prio 9 left;
       . ∪ . : bag × bag → bag;
       . \ . : bag × bag → bag;
       # . : bag → nat;
   
   predicates 
       . ∈ . : elem × bag;
       . ⊆ . : bag × bag;
   
   variables 
       bag : bag;
       a : elem;
       b : elem;
   
   
   axioms 
      size-empty: # ∅ = 0;
      used for: s, ls;
      
      size-rec: #(bag ++ a) = # bag + 1;
      used for: s, ls;
      
      del-empty: ∅ -- a = ∅;
      used for: s, ls;
      
      del-rec: (bag ++ a) -- b = (a = b ⊃ bag;(bag -- b) ++ a);
      used for: s, ls;
      
      union-empty: ∅ ∪ bag = bag;
      used for: s, ls;
      
      union-rec: (bag0 ++ a) ∪ bag1 = (bag0 ∪ bag1) ++ a;
      used for: s, ls;
      
      diff-empty: bag0 \ ∅ = bag0;
      used for: s, ls;
      
      diff-rec: bag0 \ (bag1 ++ a) = (bag0 -- a) \ bag1;
      used for: ls;
      
      one: {a}  = ∅ ++ a;
      used for: s, ls;
      
      in: a ∈ bag ↔ count(a, bag) ≠ 0;
      used for: s, ls;
      
      count-subset: bag0 ⊆ bag1 ↔ (∀ a. count(a, bag0) ≤ count(a, bag1));
      used for: ls;
   
   
end enrich