theorem
Hex.GraphIso.Nauty.Generation.PathCover.visit
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel runFuel boundary level numcells tc len tv current : Nat}
{codes bs fs targets : List Nat}
{rsLab rsPtn : Array Nat}
{key : Key n}
{tcell : VSet n}
{cursor : Option Nat}
{base st child out : SearchSt n}
{best outBest : Option (Key n)}
{trail childTrail eventTrail : FrameTrail}
{r : Int}
(h : PathCover ctx tcLevel boundary level (LoopInv.frame rsLab rsPtn numcells) tc len targets key tcell cursor)
(hinv : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail)
(hgsz : ctx.g.size = n)
(hnext : tcell.nextElem cursor = some tv)
(hpast : CanonPast level tc cursor st)
(hcurrent : current < len)
(hat : st.lab[tc + current]! = tv)
(hchild :
child = { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst,
ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst,
active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits,
fixedpts := st.fixedpts.insert tv, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode,
canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab,
canong := st.canong, 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, needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal,
canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators,
numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace })
(hrun :
OtherRun G ctx tcLevel specFuel runFuel (level + 1) codes fs child out (numcells + 1) best outBest childTrail
eventTrail r)
(hout : SearchOut G level (level + 1) child out)
(hguide : st.gcaFirst < level)
(hstay : ¬r < Int.ofNat level)
(hreceipt :
∀ (o : Nat),
o < len →
rsLab[tc + o]! = tv →
ChildPath ctx tcLevel boundary level (LoopInv.frame rsLab rsPtn numcells) tc targets key o →
RefReturn ctx out r)
:
PathCover ctx tcLevel boundary level (LoopInv.frame rsLab rsPtn numcells) tc len targets key tcell (some tv)
A child that stays at an off-path sweep either lacks the sought reference or returns a canonical carrier from an earlier child. Both cases advance reference coverage without asserting exhaustive search.