theorem
Hex.GraphIso.Nauty.FirstSweepHyp.reference
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel runFuel level numcells tc len tv1 e boundary : Nat}
{codes bs fs targets : List Nat}
{rsLab rsPtn : Array Nat}
{base st : SearchSt n}
{key : Key n}
{cursor : Option Nat}
{tcell : VSet n}
{best : Option (Key n)}
{trail : FrameTrail}
(hh :
FirstSweepHyp G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor e tv1 base st best
trail)
(hg : ctx.g = rowsOf G)
(hinf : inf = n + 2)
(hpath : level = codes.length)
(hfuel : n + 2 < level + 1 + runFuel)
{tv o : Nat}
(hnext : tcell.nextElem cursor = some tv)
(ho : o < len)
(hat : rsLab[tc + o]! = tv)
(hm : Generation.Matches ctx (level + 1) st targets key)
(heq : st.eqlevFirst = level)
(hsame : boundary ≤ st.allsamelevel)
(hp : Generation.ChildPath ctx tcLevel boundary level (LoopInv.frame rsLab rsPtn numcells) tc targets key o)
:
have 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 };
Generation.RefReturn ctx (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) child).snd
(otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) child).fst
A matching child of a first-path sweep invokes the general off-path reference theorem with its individualized vertex as the coset index.
theorem
Hex.GraphIso.Nauty.FirstSweepHyp.visitLevel
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel runFuel level numcells tc len tv1 e boundary : Nat}
{codes bs fs targets : List Nat}
{rsLab rsPtn : Array Nat}
{base st : SearchSt n}
{key : Key n}
{cursor : Option Nat}
{tcell : VSet n}
{best : Option (Key n)}
{trail : FrameTrail}
(hh :
FirstSweepHyp G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor e tv1 base st best
trail)
(hg : ctx.g = rowsOf G)
(hinf : inf = n + 2)
(hpath : level = codes.length)
(hfuel : n + 2 < level + 1 + runFuel)
{tv oRef offset : Nat}
{child out : SearchSt n}
{r : Int}
{outBest : Option (Key n)}
{eventTrail : FrameTrail}
(hnext : tcell.nextElem cursor = some tv)
(hm : Generation.Matches ctx (level + 1) st targets key)
(heq : st.eqlevFirst = level)
(hsame : boundary ≤ st.allsamelevel)
(hboundary : level < boundary)
(href : oRef < len)
(hp : Generation.ChildPath ctx tcLevel boundary level (LoopInv.frame rsLab rsPtn numcells) tc targets key oRef)
(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 := 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 })
(hcall : otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) child = (r, out))
(hrun :
OtherRun G ctx tcLevel specFuel runFuel (level + 1) codes fs child out (numcells + 1) best outBest
(trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) eventTrail r)
(hkeep : OtherKeep ctx (level + 1) child out)
:
No off-path visit in this first-path sweep can cross its receiver. Above both boundaries this follows from return classification. At a cheap boundary every child contains the saved reference, so the reference return theorem rules out an early non-generator return there as well.