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 
       { . } : 'a → bag('a);
       . -- . : bag('a) × 'a → bag('a) prio 9 left;
       . ∪ . : bag('a) × bag('a) → bag('a);
       . \ . : bag('a) × bag('a) → bag('a);
       # . : bag('a) → nat;
   
   predicates 
       . ∈ . : 'a × bag('a);
       . ⊆ . : bag('a) × bag('a);
   
   variables 
       bag : bag('a);
       a : 'a;
       b : 'a;
   
   
   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