generic specification
   parameter elemdata
   using nat
target
   sorts store;
   constants 
       ∅ : store;
   
   functions 
       . [ . ] : store × elem × data → store;
       # . : store → nat;
       . -- . : store × elem → store prio 9 left;
   
   predicates 
       . ∈ . : elem × store;
       . ⊆ . : store × store;
   
   variables 
       st : store;
       st0 : store;
       st1 : store;
       st2 : store;
   
   partial functions 
       . [ . ] : store × elem → data with λ st, a. a ∈ st;
   
   
   induction 
      store generated by ∅, [ ];
   
   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-empty: ∅ -- a = ∅;
      used for: s, ls;
      
      Del-rec-same: st[a, d] -- a = st -- a;
      used for: s, ls;
      
      Del-rec-other: a ≠ b → st[b, d] -- a = (st -- a)[b, d];
   
   
end generic specification