enrich
   ref-map, 
   node-heap, 
   list
with
   
   
   functions  Node : elem → node;
              dom . : heap → refset prio 1 left;
              ran . : ref-map → refset prio 1 left;
              reachset : ref × heap → refset;
              apply : heap × ref-map → heap;
              apply : successors × ref-map → successors;
   predicates  closed : heap;
               closed : successors × heap;
               inj : ref-map;
               hom : heap × ref-map × heap;
               connected : ref × heap;
               path : list × ref × ref × heap;
               reachable : ref × ref × heap;
   
   

   

   axioms hom :  ⊦ hom(H0, map, H1) ↔ apply(H0, map) = H1;
          path-emp :  ⊦ path([], r0, r1, H) ↔ r0 = r1 ∧ r0 ∈ H;
          path-rec :  ⊦ path(a ' + x, r0, r1, H) ↔ r0 ∈ H ∧ a ∈ H[r0].edges ∧ path(x, (H[r0].edges)[a], r1, H);
          reachable :  ⊦ reachable(r0, r1, H) ↔ (∃ x. path(x, r0, r1, H));
          reachset :  ⊦ r1 ∈ reachset(r0, H) ↔ reachable(r0, r1, H);
          connected :  ⊦ connected(r0, H) ↔ (∀ r1. reachable(r0, r1, H));
          ran :  ⊦ r ∈ ran map ↔ r ∈ran map;
          dom :  ⊦ r ∈ dom H ↔ r ∈ H;
          closed :  ⊦ closed(H) ↔ (∀ r. r ∈ H → closed(H[r].edges, H));
          closeds :  ⊦ closed(succ, H) ↔ (∀ a. a ∈ succ → succ[a] ∈ H);
          empty-node :  ⊦ Node(a) = Node(a, ∅);
          inj :  ⊦ inj(map) ↔ (∀ r0, r1. r0 ∈ map ∧ r1 ∈ map → (map[r0] = map[r1] ↔ r0 = r1));
          in-apply :  ⊦ ¬ ¬ r1 ∈ apply(H, map) ↔ (∃ r0. r0 ∈ map ∧ r0 ∈ H ∧ map[r0] = r1);
          at-apply
          :  ⊦ r0 ∈ map ∧ r0 ∈ H ∧ map[r0] = r1 → apply(H, map)[r1] = Node(H[r0].value, apply(H[r0].edges, map));
          in-apply-succ :  ⊦ a ∈ apply(succ, map) ↔ a ∈ succ;
          at-apply-succ :  ⊦ a ∈ succ → apply(succ, map)[a] = map[succ[a]]

   

   
end enrich