specification
   using nat
   sorts store('a, 'b);
   constants 
       ∅ : store('a, 'b);
   
   functions 
       . [ . := . ] : store('a, 'b) × 'a × 'b → store('a, 'b);
       # . : store('a, 'b) → nat;
       . -- . : store('a, 'b) × 'a → store('a, 'b) prio 9 left;
   
   predicates 
       . ∈ . : 'a × store('a, 'b);
       . ⊆ . : store('a, 'b) × store('a, 'b);
   
   variables 
       st : store('a, 'b);
       st0 : store('a, 'b);
       st1 : store('a, 'b);
       st2 : store('a, 'b);
       a : 'a;
       b : 'a;
       c : 'a;
       d : 'b;
   
   partial functions 
       . [ . ] : store('a, 'b) × 'a → 'b with λ st, a. a ∈ st;
   
   
   induction 
      store('a, 'b) 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 specification