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;
   
   
   
   

   

   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