theorem Hex.GraphIso.Nauty.Sparse.NodeInv.visit_equiv {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) : have fresh := { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := have __src := st.canong; { toRows := __src.toRows, scratch := Scratch.fresh n }, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, order := st.order, genTrace := st.genTrace, workperm := st.workperm }; have f := visit (Graph.ofGraph G.graph) level numcells fresh; have r := visit (Graph.ofGraph G.graph) level numcells st; f.fst = r.fst ∧ f.snd.fst = r.snd.fst ∧ r.snd.snd.ptn = f.snd.snd.ptn ∧ FrameOut G level level f.snd.snd r.snd.snd ∧ Ready G level f.fst f.snd.snd ∧ Ready G level r.fst r.snd.snd

The actual cached visit and the fresh visit used by the unpruned specification have identical codes, counts and partitions, with labels permuted within their ordered cells. This supplies the parent frame needed to transport whole child maxima without requiring identical label arrays.