enrich
   heapfuns
with
   functions 
       . * . : (Heap[A] → Bool) × (Heap[A] → Bool) → Heap[A] → Bool prio 10 right;
       . ⊗ . : (Heap[A] → Bool) × (Heap[A] → Bool) → Heap[A] → Bool prio 10 right;
       . -* . : (Heap[A] → Bool) × (Heap[A] → Bool) → Heap[A] → Bool;
       . -⊗ . : (Heap[A] → Bool) × (Heap[A] → Bool) → Heap[A] → Bool;
       not . : (Heap[A] → Bool) → Heap[A] → Bool;
       . and . : (Heap[A] → Bool) × (Heap[A] → Bool) → Heap[A] → Bool prio 4 right;
       . or . : (Heap[A] → Bool) × (Heap[A] → Bool) → Heap[A] → Bool prio 3 right;
       . -> . : (Heap[A] → Bool) × (Heap[A] → Bool) → Heap[A] → Bool prio 2 right;
       ⌜ . ⌝ : Bool → Heap[A] → Bool;
       { . } : Heap[A] → Heap[A] → Bool;
       ite : Bool × (Heap[A] → Bool) × (Heap[A] → Bool) → Heap[A] → Bool;
   
   predicates 
       emp : Heap[A];
       true : Heap[A];
       false : Heap[A];
       precise : (Heap[A] → Bool);
       . ⊆ . : (Heap[A] → Bool) × (Heap[A] → Bool);
   
   variables 
       hP : Heap[A] → Bool;
       bv : Bool;
       h : Heap[A];
   
   
   axioms 
      ite: ite(bv, hP0, hP1) = (bv ⊃ hP0;hP1);
      used for: ls;
      
      emp: emp(h) ↔ h = ∅;
      used for: s, ls;
      
      true: true = ⌜true⌝ ;
      used for: ls;
      
      false: false = ⌜false⌝ ;
      used for: ls;
      
      sep: (hP0 * hP1)(h) ↔ (∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ hP0(h0) ∧ hP1(h1));
      
      sharing: (hP0 ⊗ hP1)(h) ↔ (∃ h0, h1, h2. h0 ⊥ h2 ∧ h0 ⊥ h1 ∧ h1 ⊥ h2 ∧ h = h0 ∪ h1 ∪ h2 ∧ hP0(h0 ∪ h2) ∧ hP1(h1 ∪ h2));
      
      wand: (hP0 -* hP1)(h) ↔ (∀ h1. h1 ⊥ h ∧ hP0(h1) → hP1(h1 ∪ h));
      
      septract: (hP0 -⊗ hP1)(h) ↔ (∃ h0, h1. h0 ⊥ h ∧ h1 = h0 ∪ h ∧ hP0(h0) ∧ hP1(h1));
      
      not: (¬ hP0)(h) ↔ ¬ hP0(h);
      used for: s, ls;
      
      and: (hP0 ∧ hP1)(h) ↔ hP0(h) ∧ hP1(h);
      used for: s, ls;
      
      or: (hP0 ∨ hP1)(h) ↔ hP0(h) ∨ hP1(h);
      used for: s, ls;
      
      imp: (hP0 → hP1)(h) ↔ hP0(h) → hP1(h);
      used for: s, ls;
      
      prop: ⌜bv⌝ (h) ↔ bv;
      used for: s, ls;
      
      this: {h} (h0) ↔ h = h0;
      used for: s, ls;
      
      precise: precise(hP) ↔ (∀ h, h0, h1, h2. hP(h) ∧ hP(h0) ∧ h ⊥ h1 ∧ h0 ⊥ h2 ∧ h ∪ h1 = h0 ∪ h2 → h = h0);
      
      Imp: hP0 ⊆ hP1 ↔ (∀ h. hP0(h) → hP1(h));
   
   
end enrich