theorem Hex.GraphIso.Nauty.firstChildLoop_skip {n : Nat} (ctx : Ctx n) (inf tcLevel runFuel loopFuel level numcells tc tv1 tv : Nat) (tcell : VSet n) (index : Nat) (st : SearchSt n) (horb : (st.orbits[tv]! == tv) = false) : firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st = firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem (some tv)) tcell (if (st.orbits[tv]! == tv1) = true then index + 1 else index) st

A vertex that is not its orbit's representative is skipped.

theorem Hex.GraphIso.Nauty.firstChildLoop_earlyOther {n : Nat} (ctx : Ctx n) (inf tcLevel runFuel loopFuel level numcells tc tv1 tv : Nat) (tcell : VSet n) (index : Nat) (st : SearchSt n) (value : Int) (out : SearchSt n) (hrep : (st.orbits[tv]! == tv) = true) (hother : (tv == tv1) = false) (hcall : otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { 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 := tv, 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 } = (value, out)) (hearly : value < Int.ofNat level) : firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st = (some value, index, { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace })

An early off-path child return leaves the loop after cleaning the temporary fixed vertex.

theorem Hex.GraphIso.Nauty.firstChildLoop_earlyGuide {n : Nat} (ctx : Ctx n) (inf tcLevel runFuel loopFuel level numcells tc tv1 tv : Nat) (tcell : VSet n) (index : Nat) (st : SearchSt n) (value : Int) (out : SearchSt n) (hrep : (st.orbits[tv]! == tv) = true) (hfirst : (tv == tv1) = true) (hcall : firstPathNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { 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 := tv, 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 } = (value, out)) (hearly : value < Int.ofNat level) : firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st = (some value, index, { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := level, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := tv1, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace })

An early guiding child return leaves the loop after installing the first-path controls and cleaning the temporary fixed vertex.

theorem Hex.GraphIso.Nauty.firstChildLoop_stayOther {n : Nat} (ctx : Ctx n) (inf tcLevel runFuel loopFuel level numcells tc tv1 tv : Nat) (tcell : VSet n) (index : Nat) (st : SearchSt n) (value : Int) (out : SearchSt n) (hrep : (st.orbits[tv]! == tv) = true) (hother : (tv == tv1) = false) (hcall : otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { 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 := tv, 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 } = (value, out)) (hstay : ¬value < Int.ofNat level) : have cleaned := { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace }; have cleared := clearShortIf cleaned.needshortprune cleaned; have tcell' := if cleaned.needshortprune = true then shortprune tcell cleared else tcell; have recSt := recover n inf level cleared; firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st = firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell'.nextElem (some tv)) tcell' (if (recSt.orbits[tv]! == tv1) = true then index + 1 else index) recSt

An off-path child that stays at the loop level continues with the recursive tail on the recovered, possibly filtered, state.

theorem Hex.GraphIso.Nauty.firstChildLoop_stayGuide {n : Nat} (ctx : Ctx n) (inf tcLevel runFuel loopFuel level numcells tc tv1 tv : Nat) (tcell : VSet n) (index : Nat) (st : SearchSt n) (value : Int) (out : SearchSt n) (hrep : (st.orbits[tv]! == tv) = true) (hfirst : (tv == tv1) = true) (hcall : firstPathNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { 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 := tv, 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 } = (value, out)) (hstay : ¬value < Int.ofNat level) : have cleaned := { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := level, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := tv1, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace }; have cleared := clearShortIf cleaned.needshortprune cleaned; have tcell' := if cleaned.needshortprune = true then shortprune tcell cleared else tcell; have recSt := recover n inf level cleared; firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st = firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell'.nextElem (some tv)) tcell' (if (recSt.orbits[tv]! == tv1) = true then index + 1 else index) recSt

The guiding child that stays at the loop level continues with the recursive tail on the recovered, possibly filtered, state carrying the installed first-path controls.

structure Hex.GraphIso.Nauty.FirstSweepRun {n k : Nat} (G : Colored n k) (ctx : Ctx n) (tcLevel specFuel runFuel loopFuel level : Nat) (stem codes fs : List Nat) (rsLab rsPtn : Array Nat) (tc len numcells : Nat) (tcell : VSet n) (cursor : Option Nat) (bound : Key n) (st out : SearchSt n) (best outBest : Option (Key n)) (receiptTrail eventTrail : FrameTrail) (r : Option Int) : Prop

A first-path sibling sweep result: the established loop proof, the exit classification, the one-shot short-prune provenance, and the first-leaf and canonical histories strictly below the loop level.

• proof : LoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest receiptTrail eventTrail r
• exit : LoopExit ctx tcLevel specFuel runFuel loopFuel level codes rsLab rsPtn tc len numcells tcell cursor bound st out best outBest receiptTrail r
• short : out.needshortprune = true → ∃ (value : Int), r = some value ∧ ShortSource G ctx out eventTrail value
• trail : FirstTrail ctx level out eventTrail
• canonTrail : CanonTrail ctx level out eventTrail
• guideLevel : level ≤ out.gcaFirst
• order : out.gcaFirst ≤ out.gcaCanon

theorem Hex.GraphIso.Nauty.FirstSweepRun.retrail {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell : VSet n} {cursor : Option Nat} {bound : Key n} {st out : SearchSt n} {best outBest : Option (Key n)} {source dest eventTrail : FrameTrail} {r : Option Int} (htrail : TrailExt level dest source) (h : FirstSweepRun G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest source eventTrail r) : FirstSweepRun G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest dest eventTrail r

Rebase the receipt trail onto any trail agreeing below the loop.

theorem Hex.GraphIso.Nauty.FirstSweepRun.prepend {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell : VSet n} {cursor : Option Nat} {bound : Key n} {st recSt out : SearchSt n} {best mid outBest : Option (Key n)} {receiptTrail eventTrail : FrameTrail} {r : Option Int} (hfixed : recSt.fixedpts = st.fixedpts) (hpre : LoopSound ctx bound best mid) (h : FirstSweepRun G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound recSt out mid outBest receiptTrail eventTrail r) : FirstSweepRun G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest receiptTrail eventTrail r

Prepending a sound fragment adjusts only the incoming incumbent.

theorem Hex.GraphIso.Nauty.FirstSweepRun.step {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level tv : Nat} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell : VSet n} {cursor : Option Nat} {bound : Key n} {st out : SearchSt n} {best outBest : Option (Key n)} {receiptTrail eventTrail : FrameTrail} {r : Option Int} (ha : After cursor tv) (h : FirstSweepRun G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell (some tv) bound st out best outBest receiptTrail eventTrail r) : FirstSweepRun G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest receiptTrail eventTrail r

Advancing the cursor by one visited vertex costs one unit of fuel.

theorem Hex.GraphIso.Nauty.FirstSweepRun.reindexSet {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell tcell' : VSet n} {cursor : Option Nat} {bound : Key n} {st out : SearchSt n} {best outBest : Option (Key n)} {receiptTrail eventTrail : FrameTrail} {r : Option Int} (h : FirstSweepRun G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest receiptTrail eventTrail r) : FirstSweepRun G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell' cursor bound st out best outBest receiptTrail eventTrail r

The recorded live set is bookkeeping only.

theorem Hex.GraphIso.Nauty.FirstSweepRun.zero {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel level numcells tc len : Nat} {tcell : VSet n} {tv1 index : Nat} {stem codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {tv? cursor : Option Nat} {bound : Key n} {base st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hpath : level = codes.length) (hstem : List.take stem.length codes = stem) (hpast : stem.length < level) (hnp : st.compCanon ≤ 0) (hinv : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) (hlive : Live ctx level st trail) (hcursor : ∀ (v : Nat), cursor = some v → v < n) (hfirst : FirstTrail ctx level st trail) (hcanon : CanonTrail ctx level st trail) (hguide : level ≤ st.gcaFirst) : FirstSweepRun G ctx tcLevel specFuel runFuel 0 level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel 0 level numcells tc tv1 tv? tcell index st).snd.snd best best trail trail (firstChildLoop ctx inf tcLevel runFuel 0 level numcells tc tv1 tv? tcell index st).fst

Zero cursor fuel is retained as exhaustion.

theorem Hex.GraphIso.Nauty.FirstSweepRun.done {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel loopFuel level numcells tc len tv1 index tail : Nat} {tcell : VSet n} {stem codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {bound : Key n} {base st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hpath : level = codes.length) (hstem : List.take stem.length codes = stem) (hpast : stem.length < level) (hnext : tcell.nextElem cursor = none) (hnp : st.compCanon ≤ 0) (hbound : bound = keysMax (sweepKey ctx tcLevel specFuel level codes rsLab rsPtn tc numcells 0) (List.map (fun (o : Nat) => sweepKey ctx tcLevel specFuel level codes rsLab rsPtn tc numcells (o + 1)) (List.range tail))) (hlen : len = tail + 1) (hinv : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) (hlive : Live ctx level st trail) (hfirst : FirstTrail ctx level st trail) (hcanon : CanonTrail ctx level st trail) (hguide : level ≤ st.gcaFirst) : FirstSweepRun G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 none tcell index st).snd.snd best best trail trail (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 none tcell index st).fst

A positive-fuel loop with no next vertex has covered the whole target cell and returns its exact maximum.

theorem Hex.GraphIso.Nauty.FirstSweepRun.childUnwind {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel loopFuel level numcells tc len tv tv1 index target offset : Nat} {tcell : VSet n} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {bound : Key n} {st out : SearchSt n} {value : Int} {best outBest : Option (Key n)} {trail eventTrail : FrameTrail} (hstem : List.take stem.length codes = stem) (hshorter : stem.length < codes.length) (hrep : (st.orbits[tv]! == tv) = true) (hother : (tv == tv1) = false) (hcall : otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { 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 := tv, 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 } = (value, out)) (hsound : NodeSound ctx tcLevel specFuel (level + 1) codes { 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 := tv, 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 } (numcells + 1) best outBest) (hkey : keyLe (nodeKey ctx tcLevel specFuel (level + 1) codes { 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 := tv, 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 } (numcells + 1)) bound) (hreturn : value = Int.ofNat target) (hbelow : target < level) (payload : Unwind ctx tcLevel target out outBest) (hloc : Unwind.Located (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) payload) (hcontrol : target = out.gcaFirst ∨ target = out.gcaCanon) (hchild : OtherRun G ctx tcLevel specFuel runFuel (level + 1) codes fs { 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 := tv, 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 } out (numcells + 1) best outBest (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) eventTrail value) (hfresh : st.fixedpts.mem tv = false) (htrail : FirstTrail ctx level { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace } eventTrail) (hcanon : CanonTrail ctx level { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace } eventTrail) (hguide : level ≤ st.gcaFirst) : FirstSweepRun G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).snd.snd best outBest trail eventTrail (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).fst

A located unwind below the loop from an off-path child leaves the sweep at once.

theorem Hex.GraphIso.Nauty.FirstSweepRun.childFrozen {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel loopFuel level numcells tc len tv1 tv tail offset index : Nat} {tcell : VSet n} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {bound : Key n} {st out : SearchSt n} {best outBest : Option (Key n)} {value : Int} {trail eventTrail : FrameTrail} (hpath : level = codes.length) (hstem : List.take stem.length codes = stem) (hshorter : stem.length < codes.length) (hrep : (st.orbits[tv]! == tv) = true) (hother : (tv == tv1) = false) (hcall : otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { 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 := tv, 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 } = (value, out)) (hchild : OtherRun G ctx tcLevel specFuel runFuel (level + 1) codes fs { 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 := tv, 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 } out (numcells + 1) best outBest (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) eventTrail value) (hbelow : value < Int.ofNat level) (hfreeze : FrozenOut ctx codes out outBest value) (hexactChild : outBest = some (incMax best (nodeKey ctx tcLevel specFuel (level + 1) codes { 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 := tv, 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 } (numcells + 1)))) (hkey : keyLe (nodeKey ctx tcLevel specFuel (level + 1) codes { 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 := tv, 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 } (numcells + 1)) bound) (hbound : bound = keysMax (sweepKey ctx tcLevel specFuel level codes rsLab rsPtn tc numcells 0) (List.map (fun (o : Nat) => sweepKey ctx tcLevel specFuel level codes rsLab rsPtn tc numcells (o + 1)) (List.range tail))) (hlen : len = tail + 1) (hcover : SweepCover ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells tcell (some tv) outBest) (hfresh : st.fixedpts.mem tv = false) (htrail : FirstTrail ctx level { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace } eventTrail) (hcanon : CanonTrail ctx level { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace } eventTrail) (hguide : level ≤ st.gcaFirst) : FirstSweepRun G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).snd.snd best outBest trail eventTrail (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).fst

A comparison-frozen off-path child return below the loop absorbs the whole sweep.

theorem Hex.GraphIso.Nauty.FirstSweepRun.childCheap {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel loopFuel level numcells tc len tv1 tv boundary offset index : Nat} {tcell : VSet n} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {bound childKey : Key n} {st out : SearchSt n} {best outBest : Option (Key n)} {trail eventTrail : FrameTrail} (hstem : List.take stem.length codes = stem) (hshorter : stem.length < codes.length) (hrep : (st.orbits[tv]! == tv) = true) (hother : (tv == tv1) = false) (hcall : otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { 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 := tv, 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 } = (Int.ofNat boundary - 1, out)) (hchild : OtherRun G ctx tcLevel specFuel runFuel (level + 1) codes fs { 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 := tv, 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 } out (numcells + 1) best outBest (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) eventTrail (Int.ofNat boundary - 1)) (hpositive : 1 ≤ boundary) (hbelow : boundary ≤ level) (hsaved : out.noncheaplevel = boundary) (hbound : bound = childKey) (hexact : outBest = some (incMax best childKey)) (hfresh : st.fixedpts.mem tv = false) (htrail : FirstTrail ctx level { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace } eventTrail) (hcanon : CanonTrail ctx level { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace } eventTrail) (hguide : level ≤ st.gcaFirst) : FirstSweepRun G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).snd.snd best outBest trail eventTrail (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).fst

A saved cheap-boundary off-path child return below the loop absorbs the whole verified small-cell sweep.

theorem Hex.GraphIso.Nauty.ShortSource.setFirst {n k : Nat} {G : Colored n k} {ctx : Ctx n} {out : SearchSt n} {trail : FrameTrail} {r : Int} (h : ShortSource G ctx out trail r) (gcaFirst stabvertex : Nat) : ShortSource G ctx { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace } trail r

The first-path controls do not affect a short-prune source.

theorem Hex.GraphIso.Nauty.FirstRun.markEvent {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel level numcells tc len offset tv1 : Nat} {cs fs : List Nat} {rsLab rsPtn : Array Nat} {child out : SearchSt n} {outBest : Option (Key n)} {trail eventTrail : FrameTrail} {r : Int} (hpath : cs.length = level) (hreturn : r < Int.ofNat level) (hgca : level + 1 ≤ out.gcaFirst) (h : FirstRun G ctx tcLevel specFuel runFuel (level + 1) cs fs child out (numcells + 1) outBest (trail.push level { frame := sweepFrame specFuel cs rsLab rsPtn tc numcells, offset := offset }) eventTrail r) (hdone : ChildDone ctx tcLevel specFuel level cs rsLab rsPtn tc numcells outBest offset) (hlevel : 1 ≤ level) (hls : rsLab.size = n) (hlab : LabOk rsLab n) (hps : rsPtn.size = n) (hend : rsPtn[rsPtn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), rsPtn[q]! ≤ level ∨ rsPtn[q]! = n + 2) (hcell : IsCell rsPtn level tc len) (hrange : tc + len ≤ n) (hoff : offset < len) (hfuel : level + 1 + specFuel ≤ n + 1) : EventOut G ctx tcLevel cs fs { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := level, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := tv1, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace } outBest eventTrail r

Installing the first-path controls after a guiding child that returned below its parent loop: the fully covered child supplies the guide.

theorem Hex.GraphIso.Nauty.FirstSweepRun.guideFrozen {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel loopFuel level numcells tc len tv1 tv tail offset index : Nat} {tcell : VSet n} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {bound : Key n} {st out : SearchSt n} {outBest : Option (Key n)} {value : Int} {trail eventTrail : FrameTrail} (hpath : level = codes.length) (hstem : List.take stem.length codes = stem) (hshorter : stem.length < codes.length) (hrep : (st.orbits[tv]! == tv) = true) (hfirst : (tv == tv1) = true) (hcall : firstPathNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { 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 := tv, 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 } = (value, out)) (hchild : FirstRun G ctx tcLevel specFuel runFuel (level + 1) codes fs { 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 := tv, 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 } out (numcells + 1) outBest (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) eventTrail value) (hgca : level + 1 ≤ out.gcaFirst) (hbelow : value < Int.ofNat level) (hfreeze : FrozenOut ctx codes out outBest value) (hexactChild : outBest = some (incMax none (nodeKey ctx tcLevel specFuel (level + 1) codes { 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 := tv, 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 } (numcells + 1)))) (hkey : keyLe (nodeKey ctx tcLevel specFuel (level + 1) codes { 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 := tv, 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 } (numcells + 1)) bound) (hbound : bound = keysMax (sweepKey ctx tcLevel specFuel level codes rsLab rsPtn tc numcells 0) (List.map (fun (o : Nat) => sweepKey ctx tcLevel specFuel level codes rsLab rsPtn tc numcells (o + 1)) (List.range tail))) (hlen : len = tail + 1) (hcover : SweepCover ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells tcell (some tv) outBest) (hdone : ChildDone ctx tcLevel specFuel level codes rsLab rsPtn tc numcells outBest offset) (hfresh : st.fixedpts.mem tv = false) (hlevel : 1 ≤ level) (hls : rsLab.size = n) (hlab : LabOk rsLab n) (hps : rsPtn.size = n) (hend : rsPtn[rsPtn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), rsPtn[q]! ≤ level ∨ rsPtn[q]! = n + 2) (hcell : IsCell rsPtn level tc len) (hrange : tc + len ≤ n) (hoff : offset < len) (hfuel : level + 1 + specFuel ≤ n + 1) : FirstSweepRun G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).snd.snd none outBest trail eventTrail (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).fst

A comparison-frozen guiding child return below the loop absorbs the whole sweep.

theorem Hex.GraphIso.Nauty.FirstSweepRun.guideCheap {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel loopFuel level numcells tc len tv1 tv boundary offset index : Nat} {tcell : VSet n} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {bound childKey : Key n} {st out : SearchSt n} {outBest : Option (Key n)} {trail eventTrail : FrameTrail} (hpath : level = codes.length) (hstem : List.take stem.length codes = stem) (hshorter : stem.length < codes.length) (hrep : (st.orbits[tv]! == tv) = true) (hfirst : (tv == tv1) = true) (hcall : firstPathNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { 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 := tv, 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 } = (Int.ofNat boundary - 1, out)) (hchild : FirstRun G ctx tcLevel specFuel runFuel (level + 1) codes fs { 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 := tv, 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 } out (numcells + 1) outBest (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) eventTrail (Int.ofNat boundary - 1)) (hgca : level + 1 ≤ out.gcaFirst) (hpositive : 1 ≤ boundary) (hbelow : boundary ≤ level) (hsaved : out.noncheaplevel = boundary) (hbound : bound = childKey) (hexact : outBest = some (incMax none childKey)) (hdone : ChildDone ctx tcLevel specFuel level codes rsLab rsPtn tc numcells outBest offset) (hfresh : st.fixedpts.mem tv = false) (hlevel : 1 ≤ level) (hls : rsLab.size = n) (hlab : LabOk rsLab n) (hps : rsPtn.size = n) (hend : rsPtn[rsPtn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), rsPtn[q]! ≤ level ∨ rsPtn[q]! = n + 2) (hcell : IsCell rsPtn level tc len) (hrange : tc + len ≤ n) (hoff : offset < len) (hfuel : level + 1 + specFuel ≤ n + 1) : FirstSweepRun G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).snd.snd none outBest trail eventTrail (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).fst

A saved cheap-boundary guiding child return below the loop absorbs the whole verified small-cell sweep.

theorem Hex.GraphIso.Nauty.FirstSweepRun.nextOther {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel loopFuel level numcells tc len tv1 tv index : Nat} {tcell : VSet n} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {bound : Key n} {st out : SearchSt n} {best mid outBest : Option (Key n)} {value : Int} {receiptTrail eventTrail : FrameTrail} (hnext : tcell.nextElem cursor = some tv) (hrep : (st.orbits[tv]! == tv) = true) (hother : (tv == tv1) = false) (hcall : otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { 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 := tv, 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 } = (value, out)) (hstay : ¬value < Int.ofNat level) (hfixed : (recover n inf level (clearShortIf out.needshortprune { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace })).fixedpts = st.fixedpts) (hpre : LoopSound ctx bound best mid) (hrec : FirstSweepRun G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells (if out.needshortprune = true then shortprune tcell (clearShortIf out.needshortprune { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace }) else tcell) (some tv) bound (recover n inf level (clearShortIf out.needshortprune { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace })) (firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 ((if out.needshortprune = true then shortprune tcell (clearShortIf out.needshortprune { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace }) else tcell).nextElem (some tv)) (if out.needshortprune = true then shortprune tcell (clearShortIf out.needshortprune { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace }) else tcell) (if ((recover n inf level (clearShortIf out.needshortprune { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace })).orbits[tv]! == tv1) = true then index + 1 else index) (recover n inf level (clearShortIf out.needshortprune { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace }))).snd.snd mid outBest receiptTrail eventTrail (firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 ((if out.needshortprune = true then shortprune tcell (clearShortIf out.needshortprune { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace }) else tcell).nextElem (some tv)) (if out.needshortprune = true then shortprune tcell (clearShortIf out.needshortprune { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace }) else tcell) (if ((recover n inf level (clearShortIf out.needshortprune { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace })).orbits[tv]! == tv1) = true then index + 1 else index) (recover n inf level (clearShortIf out.needshortprune { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace }))).fst) : FirstSweepRun G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).snd.snd best outBest receiptTrail eventTrail (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).fst

Compose an off-path child that stays at the loop level with the recursive tail on the recovered, possibly filtered, state.

theorem Hex.GraphIso.Nauty.FirstSweepRun.nextGuide {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel loopFuel level numcells tc len tv1 tv index : Nat} {tcell : VSet n} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {bound : Key n} {st out : SearchSt n} {best mid outBest : Option (Key n)} {value : Int} {receiptTrail eventTrail : FrameTrail} (hnext : tcell.nextElem cursor = some tv) (hrep : (st.orbits[tv]! == tv) = true) (hfirst : (tv == tv1) = true) (hcall : firstPathNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { 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 := tv, 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 } = (value, out)) (hstay : ¬value < Int.ofNat level) (hfixed : (recover n inf level (clearShortIf out.needshortprune { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := level, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := tv1, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace })).fixedpts = st.fixedpts) (hpre : LoopSound ctx bound best mid) (hrec : FirstSweepRun G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells (if out.needshortprune = true then shortprune tcell (clearShortIf out.needshortprune { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := level, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := tv1, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace }) else tcell) (some tv) bound (recover n inf level (clearShortIf out.needshortprune { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := level, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := tv1, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace })) (firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 ((if out.needshortprune = true then shortprune tcell (clearShortIf out.needshortprune { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := level, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := tv1, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace }) else tcell).nextElem (some tv)) (if out.needshortprune = true then shortprune tcell (clearShortIf out.needshortprune { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := level, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := tv1, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace }) else tcell) (if ((recover n inf level (clearShortIf out.needshortprune { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := level, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := tv1, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace })).orbits[tv]! == tv1) = true then index + 1 else index) (recover n inf level (clearShortIf out.needshortprune { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := level, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := tv1, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace }))).snd.snd mid outBest receiptTrail eventTrail (firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 ((if out.needshortprune = true then shortprune tcell (clearShortIf out.needshortprune { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := level, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := tv1, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace }) else tcell).nextElem (some tv)) (if out.needshortprune = true then shortprune tcell (clearShortIf out.needshortprune { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := level, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := tv1, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace }) else tcell) (if ((recover n inf level (clearShortIf out.needshortprune { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := level, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := tv1, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace })).orbits[tv]! == tv1) = true then index + 1 else index) (recover n inf level (clearShortIf out.needshortprune { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := level, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := tv1, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace }))).fst) : FirstSweepRun G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).snd.snd best outBest receiptTrail eventTrail (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).fst

Compose the guiding child, when it stays at the loop level, with the recursive tail on the recovered, possibly filtered, state carrying the installed first-path controls.

theorem Hex.GraphIso.Nauty.FirstSweepRun.skip {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel loopFuel level numcells tc len tv1 tv index : Nat} {tcell : VSet n} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {bound : Key n} {st : SearchSt n} {best outBest : Option (Key n)} {receiptTrail eventTrail : FrameTrail} (hnext : tcell.nextElem cursor = some tv) (horb : (st.orbits[tv]! == tv) = false) (hrec : FirstSweepRun G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell (some tv) bound st (firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem (some tv)) tcell (if (st.orbits[tv]! == tv1) = true then index + 1 else index) st).snd.snd best outBest receiptTrail eventTrail (firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem (some tv)) tcell (if (st.orbits[tv]! == tv1) = true then index + 1 else index) st).fst) : FirstSweepRun G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).snd.snd best outBest receiptTrail eventTrail (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).fst

Skipping a vertex that is not its orbit's representative.