generic specification
   parameter elemdata
   using nat
target
   sorts Map;
   constants 
       ∅ : Map;
   
   functions 
       . [ . ] : Map × Elem × Data → Map;
       # . : Map → Nat;
       . -- . : Map × Elem → Map prio 9 left;
   
   predicates 
       . ∈ . : Elem × Map;
       . ⊆ . : Map × Map;
   
   variables 
       st : Map;
       a : Elem;
       b : Elem;
       c : Elem;
       d : Data;
       n : Nat;
   
   partial functions 
       . [ . ] : Map × Elem → Data with λ st, a. a ∈ st;
   
   
   induction 
      Map 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