enrich
   store-base, 
   set-union
, 
   dataset
with
   

   
   
   functions  . [ . ] : store × elem → data;
              # . : store → nat;
              . -- . : store × elem → store prio 9 left;
              dom . : store → set;
              ran . : store → dataset;
   predicates  . ∈ . : elem × store;
               . ∈ . : data × store;
               . ⊆ . : store × store;
   
   

   

   axioms Extension :  ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ st1[a] = st2[a]);
          used for: ls;
          In-empty :  ⊦ ¬ a ∈ ∅;
          used for: s, ls;
          In-insert :  ⊦ a ∈ st[b, d] ↔ a = b ∨ a ∈ st;
          used for: s, ls;
          At-same :  ⊦ st[a, d][a] = d;
          used for: s, ls;
          At-other :  ⊦ a ≠ b → st[b, d][a] = st[a];
          used for: s, ls;
          Subset :  ⊦ st1 ⊆ st2 ↔ (∀ a. a ∈ st1 → a ∈ st2 ∧ st1[a] = st2[a]);
          used for: ls;
          Size-empty :  ⊦ # ∅ = 0;
          used for: s, ls;
          Size-insert :  ⊦ ¬ a ∈ st → # st[a, d] = # st + 1;
          used for: s, ls;
          Del-in :  ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st;
          used for: s, ls;
          Del-at :  ⊦ a ≠ b → (st -- b)[a] = st[a];
          used for: s, ls;
          Data-in :  ⊦ d ∈ st ↔ (∃ a. a ∈ st ∧ st[a] = d);
          Dom :  ⊦ a ∈ dom st ↔ a ∈ st;
          used for: s, ls;
          Ran :  ⊦ d ∈ ran st ↔ d ∈ st;
          used for: s, ls;

   

   
end enrich