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