inductive Hex.GraphIso.Nauty.Generation.FirstTail {n k : Nat} (G : Colored n k) (ctx : Ctx n) (inf tcLevel specFuel runFuel level numcells tc len tv1 e : Nat) (codes fs : List Nat) (rsLab rsPtn : Array Nat) (base : SearchSt n) : Nat → Option Nat → VSet n → SearchSt n → Option (Key n) → FrameTrail → Prop

The actual visits after the guiding child of a first-path sweep. The counter is absent from this proof index because it does not affect which child is visited or which state is passed to that child.

• zero {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel level numcells tc len tv1 e : Nat} {codes fs : List Nat} {rsLab rsPtn : Array Nat} {base : SearchSt n} {cursor : Option Nat} {tcell : VSet n} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} {bs : List Nat} (hyp : FirstSweepHyp G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor e tv1 base st best trail) : FirstTail G ctx inf tcLevel specFuel runFuel level numcells tc len tv1 e codes fs rsLab rsPtn base 0 cursor tcell st best trail
• done {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel level numcells tc len tv1 e : Nat} {codes fs : List Nat} {rsLab rsPtn : Array Nat} {base : SearchSt n} {loopFuel : Nat} {cursor : Option Nat} {tcell : VSet n} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} {bs : List Nat} (hyp : FirstSweepHyp G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor e tv1 base st best trail) (next : tcell.nextElem cursor = none) : FirstTail G ctx inf tcLevel specFuel runFuel level numcells tc len tv1 e codes fs rsLab rsPtn base (loopFuel + 1) cursor tcell st best trail
• skip {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel level numcells tc len tv1 e : Nat} {codes fs : List Nat} {rsLab rsPtn : Array Nat} {base : SearchSt n} {loopFuel : Nat} {cursor : Option Nat} {tcell : VSet n} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} {bs : List Nat} {tv : Nat} (hyp : FirstSweepHyp G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor e tv1 base st best trail) (next : tcell.nextElem cursor = some tv) (orbit : (st.orbits[tv]! == tv) = false) (tail : FirstTail G ctx inf tcLevel specFuel runFuel level numcells tc len tv1 e codes fs rsLab rsPtn base loopFuel (some tv) tcell st best trail) : FirstTail G ctx inf tcLevel specFuel runFuel level numcells tc len tv1 e codes fs rsLab rsPtn base (loopFuel + 1) cursor tcell st best trail
• visit {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel level numcells tc len tv1 e : Nat} {codes fs : List Nat} {rsLab rsPtn : Array Nat} {base : SearchSt n} {loopFuel : Nat} {cursor : Option Nat} {tcell : VSet n} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} {bs : List Nat} {tv offset : Nat} {child out : SearchSt n} {r : Int} {childBest : Option (Key n)} {eventTrail : FrameTrail} (hyp : FirstSweepHyp G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor e tv1 base st best trail) (next : tcell.nextElem cursor = some tv) (orbit : (st.orbits[tv]! == tv) = true) (offsetLt : offset < len) (atOffset : rsLab[tc + offset]! = tv) (childEq : 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 := 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 }) (call : otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) child = (r, out)) (run : OtherRun G ctx tcLevel specFuel runFuel (level + 1) codes fs child out (numcells + 1) best childBest (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) eventTrail r) (keep : OtherKeep ctx (level + 1) child out) (clear : ¬r < Int.ofNat level → out.needshortprune = false) (continuation : ¬r < Int.ofNat level → FirstTail G ctx inf tcLevel specFuel runFuel level numcells tc len tv1 e codes fs rsLab rsPtn base loopFuel (some tv) tcell (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 })) childBest eventTrail) : FirstTail G ctx inf tcLevel specFuel runFuel level numcells tc len tv1 e codes fs rsLab rsPtn base (loopFuel + 1) cursor tcell st best trail

inductive Hex.GraphIso.Nauty.Generation.FirstHead {n k : Nat} (G : Colored n k) (ctx : Ctx n) (inf tcLevel specFuel runFuel level numcells tc len tv1 e : Nat) (codes : List Nat) (rsLab rsPtn : Array Nat) (tcell : VSet n) (pre : SearchSt n) (trail : FrameTrail) : Prop

The guiding visit of a first-path sweep and its actual recovered tail. This proof witness exposes the setup already established by the correctness induction, without rerunning or instrumenting the search.

• intro {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel level numcells tc len tv1 e : Nat} {codes : List Nat} {rsLab rsPtn : Array Nat} {tcell : VSet n} {pre : SearchSt n} {trail : FrameTrail} {offset : Nat} {child out : SearchSt n} {r : Int} {fs : List Nat} {best : Option (Key n)} {eventTrail : FrameTrail} (next : tcell.nextElem none = some tv1) (orbit : (pre.orbits[tv1]! == tv1) = true) (lab : pre.lab = rsLab) (ptn : pre.ptn = rsPtn) (path : PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level pre) (offsetLt : offset < len) (atOffset : rsLab[tc + offset]! = tv1) (childEq : child = { lab := (breakout n pre.lab pre.ptn (level + 1) tc tv1).fst, ptn := (breakout n pre.lab pre.ptn (level + 1) tc tv1).snd.fst, active := (breakout n pre.lab pre.ptn (level + 1) tc tv1).snd.snd, orbits := pre.orbits, fixedpts := pre.fixedpts.insert tv1, autos := pre.autos, wsCap := pre.wsCap, firstcode := pre.firstcode, canoncode := pre.canoncode, firsttc := pre.firsttc, firstlab := pre.firstlab, canonlab := pre.canonlab, canong := pre.canong, samerows := pre.samerows, compCanon := pre.compCanon, eqlevFirst := pre.eqlevFirst, eqlevCanon := pre.eqlevCanon, gcaFirst := pre.gcaFirst, gcaCanon := pre.gcaCanon, canonlevel := pre.canonlevel, noncheaplevel := pre.noncheaplevel, allsamelevel := pre.allsamelevel, cosetindex := tv1, stabvertex := pre.stabvertex, needshortprune := pre.needshortprune, numnodes := pre.numnodes, tctotal := pre.tctotal, canupdates := pre.canupdates, numorbits := pre.numorbits, numgenerators := pre.numgenerators, numbadleaves := pre.numbadleaves, maxlevel := pre.maxlevel, genTrace := pre.genTrace }) (first : FirstInv G ctx (level + 1) codes (numcells + 1) child (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset })) (childPath : PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst (level + 1) child) (boundary : child.noncheaplevel ≤ level + 1) (desc : CheapDesc ctx (level + 1) child.noncheaplevel (refine ctx (level + 1) child.lab child.ptn child.active (numcells + 1))) (orbits : OrbSound (OrbConn child.genTrace.toList n) child.orbits n) (call : firstPathNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) child = (r, out)) (run : FirstRun G ctx tcLevel specFuel runFuel (level + 1) codes fs child out (numcells + 1) best (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) eventTrail r) (keep : FirstKeep ctx (level + 1) child out fs best) (tail : ¬r < Int.ofNat level → let cleaned := { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv1, 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 }; let cleared := clearShortIf out.needshortprune cleaned; let cell := if out.needshortprune = true then shortprune tcell cleared else tcell; FirstTail G ctx inf tcLevel specFuel runFuel level numcells tc len tv1 e codes fs rsLab rsPtn pre n (some tv1) cell (recover n inf level cleared) best eventTrail) : FirstHead G ctx inf tcLevel specFuel runFuel level numcells tc len tv1 e codes rsLab rsPtn tcell pre trail