generic specification 
   parameter refobj
   using nat refset
    target 
         sorts 
            heap;
         constants 
            ∅ : heap;
         functions 
             . ++ . : heap × ref → heap prio 9 left;
             . -- . : heap × ref → heap prio 9 left;
            . [ . ] : heap × ref → obj;
            . [ . ] : heap × ref × obj → heap;
            # . : heap → nat;
             . ∪ . : heap × heap → heap;
             . \ . : heap × refset → heap;
             . \ . : heap × heap → heap;
         predicates 
             . ∈ . : ref × heap;
             . ⊆ . : heap × heap;
             . ⊥ . : heap × heap;
         variables 
            H, H0, H1, H2 : heap; 
         induction 
            heap generated by ∅, ++, [];
         axioms 
            ext :  ⊦ H0 = H1 ↔ (∀ r. (r ∈ H0 ↔ r ∈ H1) ∧ (r ∈ H0 → H0[r] = H1[r]));
            subset :  ⊦ H0 ⊆ H1 ↔ (∀ r. (r ∈ H0 → r ∈ H1) ∧ (r ∈ H0 → H0[r] = H1[r]));
            sanity :  ⊦ ¬ null ∈ H;
            used for : s, ls;
             
            in-emp :  ⊦ ¬ r ∈ ∅;
            used for : s, ls;
             
            in-alloc : r0 ≠ null, ¬ r0 ∈ H ⊦ r ∈ H ++ r0 ↔ ¬ ¬ (r = r0 ∨ r ∈ H);
            used for : s, ls;
             
            in-write : r ≠ null, r0 ∈ H ⊦ r ∈ H[r0, o] ↔ r ∈ H;
            at-alloc : r ∈ H, r0 ≠ null, ¬ r0 ∈ H ⊦ r ≠ r0 → (H ++ r0)[r] = H[r];
            used for : s, ls, c, lc;
             
            at-write : r ∈ H, r0 ∈ H ⊦ (H[r0, o][r]) = ((r = r0 ⊃ o; H[r]));
            used for : s, ls;
             
            in-del :  ⊦ r ∈ H -- r0 ↔ ¬ ¬ (r ≠ r0 ∧ r ∈ H);
            used for : s, ls;
             
            at-del : r ∈ H ⊦ r ≠ r0 → (H -- r0)[r] = H[r];
            used for : s, ls;
             
            uni-emp :  ⊦ H0 ∪ ∅ = H0;
            used for : s, ls;
             
            uni-alloc : r ≠ null, ¬ r ∈ H1, ¬ r ∈ H0, H0 ⊥ H1 ⊦ H0 ∪ (H1 ++ r) = (H0 ∪ H1) ++ r;
            used for : s, ls;
             
            uni-write : r ≠ null, r ∈ H1, H0 ⊥ H1 ⊦ H0 ∪ H1[r, o] = (H0 ∪ H1)[r, o];
            used for : s, ls;
             
            diff-emp :  ⊦ H0 \ ∅ = H0;
            used for : s, ls;
             
            diff-alloc : r ≠ null, ¬ r ∈ H1 ⊦ H0 \ (H1 ++ r) = (H0 -- r) \ H1;
            used for : s, ls;
             
            diff-write : r ∈ H1 ⊦ H0 \ H1[r, o] = H0 \ H1;
            used for : s, ls;
             
            diffs-emp :  ⊦ H0 \ ∅ = H0;
            used for : s, ls;
             
            diffs-ins :  ⊦ H0 \ (rs ++ r) = (H0 -- r) \ rs;
            used for : s, ls;
             
            disj :  ⊦ H0 ⊥ H1 ↔ (∀ r. ¬ r ∈ H0 ∨ ¬ r ∈ H1);
            size-emp :  ⊦ # ∅ = 0;
            used for : s, ls;
             
            size-alloc : ¬ r ∈ H, r ≠ null ⊦ # (H ++ r) = # H + 1;
            used for : s, ls;
             
            size-write : r ∈ H ⊦ # (H[r, o]) = # H;
            used for : s, ls;
             
   
end generic specification