theorem Hex.GraphIso.Nauty.Sparse.FrameOut.target_eq {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st out : State n} (h : FrameOut G level level st out) (hs : Ready G level numcells st) (ho : Ready G level numcells out) (hn : 0 < n) (hl : 1 ≤ level) (hc : numcells < n) (tcLevel : Nat) (hint : Int) : maketargetcell (Graph.ofGraph G.graph) st.lab st.ptn level tcLevel hint = maketargetcell (Graph.ofGraph G.graph) out.lab out.ptn level tcLevel hint

Recovering an equitable parent preserves every field of its fresh target dispatch, for any fixed hint and depth cutoff.

theorem Hex.GraphIso.Nauty.Sparse.NodeInv.visit_target {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : NodeInv G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (tcLevel : Nat) (hint : Int) : have r := visit (Graph.ofGraph G.graph) level numcells st; have f := refine (Graph.ofGraph G.graph) level st.lab st.ptn st.active numcells; r.fst < n → have t := maketargetCached (Graph.ofGraph G.graph) r.snd.snd.lab r.snd.snd.ptn level tcLevel hint r.snd.snd.canong.scratch; (t.fst, t.snd.fst, t.snd.snd.fst) = maketargetcell (Graph.ofGraph G.graph) f.lab f.ptn level tcLevel hint

The cached target following an actual visit has the specification's fresh position, vertex set and size. The two visits may order labels differently within their cells.