enrich
   ex-maplet, 
   gownership
with
   functions 
       ! : Id × (Ref[A] → Id) × (Heap[A] → Bool) → Heap[A] → Bool;
   
   predicates 
       rely : Id × (Ref[A] → Id) × Heap[A] × (Ref[A] → Id) × Heap[A];
       guar : Id × (Ref[A] → Id) × Heap[A] × (Ref[A] → Id) × Heap[A];
   
   variables 
       me : Id;
       id : Id;
       of : Ref[A] → Id;
       hO : Ref[A] → Id;
       r : Ref[A];
       h : Heap[A];
       hP : Heap[A] → Bool;
       ohP : A → Heap[A] → Bool;
       o : A;
   
   
   axioms 
      rely: rely(me, of1, h1, of2, h2) ↔ (∀ r. (of1(r) = me ↔ of2(r) = me) ∧ (of1(r) = me → (r ∈ h1 ↔ r ∈ h2) ∧ (r ∈ h1 → h1(r) = h2(r))));
      
      guar: guar(me, of1, h1, of2, h2) ↔ (∀ id. id ≠ me → rely(id, of1, h1, of2, h2));
      
      owned: !(id, of, hP)(h) ↔ hP(h) ∧ (∀ r. r ∈ h → of(r) = id);
   
   
end enrich