enrich
   nat, 
   set-union, 
   polyref
with
   sorts Heap[A];
   constants 
       ∅ : Heap[A];
   
   functions 
       # . : Heap[A] → Nat;
       . ∪ . : Heap[A] × Heap[A] → Heap[A];
       . \ . : Heap[A] × Set[Ref[A]] → Heap[A];
       . \ . : Heap[A] × Heap[A] → Heap[A];
       dom . : Heap[A] → Set[Ref[A]];
   
   predicates 
       . ∈ . : Ref[A] × Heap[A];
       . ⊆ . : Heap[A] × Heap[A];
       . ⊥ . : Heap[A] × Heap[A];
   
   variables 
       h : Heap[A];
       rs : Set[Ref[A]];
       r : Ref[A];
       o : A;
       d : A;
       hP : Heap[A] → Bool;
   
   partial functions 
       . ++ . : Heap[A] × Ref[A] → Heap[A] prio 9 left with λ h, r. r ≠ null ∧ ¬ r ∈ h;
       . -- . : Heap[A] × Ref[A] → Heap[A] prio 9 left with λ h, r. r ≠ null ∧ r ∈ h;
       . ( . ) : Heap[A] × Ref[A] → A with λ h, r. r ≠ null ∧ r ∈ h;
       . ( . := . ) : Heap[A] × Ref[A] × A → Heap[A] with λ h, r, o. r ≠ null ∧ r ∈ h;
   
   
   induction 
      Heap[A] generated by ∅ : Heap[A],  . ++ .  : (Heap[A] × Ref[A] → Heap[A]),  . (. := .) : (Heap[A] × Ref[A] × A → Heap[A]) ;
   
   axioms 
      ext: h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r)));
      
      dom: r ∈ dom h ↔ r ∈ h;
      used for: s, ls;
      
      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 ∈ h(r0 := o) ↔ r ∈ h;
      used for: s, ls;
      
      at-alloc: r ∈ h, r0 ≠ null, ¬ r0 ∈ h ⊦ r ≠ r0 → (h ++ r0)(r) = h(r);
      used for: s, ls, c, lc;
      
      at-write: h(r0 := o)(r) = (r = r0 ∧ r0 ∈ h ⊃ 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: 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 enrich