enrich
   functions
with
   
   
   
   predicates  copy-node-prepost : heap × heap × ref-map;
               copy-edges-prepost : successors × heap × heap × ref-map;
               recursive-property
              : (ref × ref × heap × heap × ref-map × ref-map → bool) × (successors × successors × heap × heap × ref-map × ref-map → bool)
              ;
               recursive-node-property : nat × (ref × ref × heap × heap × ref-map × ref-map → bool);
               recursive-edges-property : nat × (successors × successors × heap × heap × ref-map × ref-map → bool);
   procedures copy# ref : ref, heap nonfunctional nondeterministic;;
              copy_node# ref : ref, ref-map, heap nonfunctional nondeterministic;;
              copy_edges# successors : successors, ref-map, heap nonfunctional nondeterministic;;
   variables  φn : ref × ref × heap × heap × ref-map × ref-map → bool;
              φn0 : ref × ref × heap × heap × ref-map × ref-map → bool;
              φn1 : ref × ref × heap × heap × ref-map × ref-map → bool;
              φe : successors × successors × heap × heap × ref-map × ref-map → bool;
              φe0 : successors × successors × heap × heap × ref-map × ref-map → bool;
              φe1 : successors × successors × heap × heap × ref-map × ref-map → bool;

   

   axioms recursive-property :  ⊦ recursive-property(φn, φe) ↔ (∀ n. recursive-node-property(n, φn) ∧ recursive-edges-property(n, φe));
          recursive-node-property
          : 
            ⊦   recursive-node-property(n, φn)
              ↔ (∀ r0, r1, H1, map1. [H0 := H1; map0 := map1; copy_node#(r0; r1, map1, H1): n ] φn(r0, r1, H0, H1, map0, map1));
          recursive-edges-property
          : 
            ⊦   recursive-edges-property(n, φe)
              ↔ (∀ succ0, succ1, H1, map1. 
                   [H0 := H1; map0 := map1; copy_edges#(succ0; succ1, map1, H1): n ] φe(succ0, succ1, H0, H1, map0, map1));
          copy-node-prepost
          : 
            ⊦   copy-node-prepost(H0, H, map)
              ↔ (∃ H1. H0 ∪ H1 = H ∧ H0 ⊥ H1 ∧ dom map ⊆ dom H0 ∧ ran map = dom H1 ∧ closed(H0) ∧ closed(H1) ∧ inj(map));
          copy-edges-prepost
          : 
            ⊦   copy-edges-prepost(succ, H0, H, map)
              ↔ (∃ H1. 
                     H0 ∪ H1 = H ∧ H0 ⊥ H1 ∧ dom map ⊆ dom H0 ∧ ran map = dom H1 ∧ closed(succ, H1) ∧ closed(H0) ∧ closed(H1) ∧ inj(map))

   

   declarations copy : copy#(r0; r1, H){let map = ∅ in copy_node#(r0; r1, map, H)};
                copy-node
                : copy_node#(r0; r1, map, H)
                  {if r0 ∈ map
                   then r1 := map[r0]
                   else {alloc(; r1, H); map := map[r0, r1]; 
                         let nd0 = [?], nd1 = [?], succ = ∅
                         in {read(r0, H; nd0); write(r1, Node(nd0.value); H); copy_edges#(nd0.edges; succ, map, H); 
                             write(r1, Node(nd0.value, succ); H)}}
                  }
                ;
                copy-edges
                : copy_edges#(succ0; succ1, map, H)
                  {if succ0 = ∅
                   then succ1 := ∅
                   else choose a
                        with a ∈ succ0
                        in let r = null
                           in {copy_node#(succ0[a]; r, map, H); succ0 := succ0 -- a; copy_edges#(succ0; succ1, map, H); succ1 := succ1[a, r]}
                  }
                ;
end enrich