theorem
Hex.GraphIso.Nauty.NodeInv.otherGuide
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel level numcells len : Nat}
{codes bs fs : List Nat}
{st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(hnode : NodeInv G ctx tcLevel level codes bs fs numcells st best trail)
(hlive : Live ctx level st trail)
:
have pre := otherLeafSt ctx level numcells st;
have base :=
{ lab := pre.lab, ptn := pre.ptn, active := pre.active, orbits := pre.orbits, fixedpts := pre.fixedpts,
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 := pre.cosetindex,
stabvertex := pre.stabvertex, needshortprune := pre.needshortprune, numnodes := pre.numnodes,
tctotal := pre.tctotal + len, canupdates := pre.canupdates, numorbits := pre.numorbits,
numgenerators := pre.numgenerators, numbadleaves := pre.numbadleaves, maxlevel := pre.maxlevel,
genTrace := pre.genTrace };
have start :=
if cheapautom base.ptn level n = true then base
else { lab := base.lab, ptn := base.ptn, active := base.active, orbits := base.orbits, fixedpts := base.fixedpts,
autos := base.autos, wsCap := base.wsCap, firstcode := base.firstcode, canoncode := base.canoncode,
firsttc := base.firsttc, firstlab := base.firstlab, canonlab := base.canonlab, canong := base.canong,
samerows := base.samerows, compCanon := base.compCanon, eqlevFirst := base.eqlevFirst,
eqlevCanon := base.eqlevCanon, gcaFirst := base.gcaFirst, gcaCanon := base.gcaCanon,
canonlevel := base.canonlevel, noncheaplevel := level + 1, allsamelevel := base.allsamelevel,
cosetindex := base.cosetindex, stabvertex := base.stabvertex, needshortprune := base.needshortprune,
numnodes := base.numnodes, tctotal := base.tctotal, canupdates := base.canupdates, numorbits := base.numorbits,
numgenerators := base.numgenerators, numbadleaves := base.numbadleaves, maxlevel := base.maxlevel,
genTrace := base.genTrace };
GuideRel level st start
The executable bookkeeping that precedes an off-path sibling sweep preserves its entry guide relation.
theorem
Hex.GraphIso.Nauty.OtherOutcome.nextClear
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel runFuel level numcells tc len tv offset currentOffset inf : Nat}
{tcell : VSet n}
{codes bs fs : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{base st out : SearchSt n}
{best outBest : Option (Key n)}
{trail eventTrail : FrameTrail}
{r : Int}
(hinv : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail)
(hlive : OtherLive ctx level st trail)
(h :
OtherOutcome G ctx tcLevel specFuel runFuel (level + 1) codes fs
{ lab := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).fst,
ptn := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).snd.fst,
active := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).snd.snd, orbits := st.orbits,
fixedpts := st.fixedpts.insert st.lab[tc + currentOffset]!, autos := st.autos, wsCap := st.wsCap,
firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab,
canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon,
eqlevFirst := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon,
canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel,
cosetindex := st.cosetindex, stabvertex := st.stabvertex, needshortprune := st.needshortprune,
numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits,
numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel,
genTrace := st.genTrace }
out (numcells + 1) best outBest
(trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) eventTrail r)
(hout :
SearchOut G level (level + 1)
{ lab := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).fst,
ptn := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).snd.fst,
active := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).snd.snd, orbits := st.orbits,
fixedpts := st.fixedpts.insert st.lab[tc + currentOffset]!, autos := st.autos, wsCap := st.wsCap,
firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab,
canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon,
eqlevFirst := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon,
canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel,
cosetindex := st.cosetindex, stabvertex := st.stabvertex, needshortprune := st.needshortprune,
numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits,
numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel,
genTrace := st.genTrace }
out)
(hinf : inf = n + 2)
(hpath : codes.length = level)
(hfuel : runFuel ≠ 0)
(hstay : ¬r < Int.ofNat level)
(hnext : tcell.nextElem cursor = some tv)
(hoffset : offset < len)
(hcurrent : currentOffset < len)
(htv : rsLab[tc + offset]! = tv)
(hat : st.lab[tc + currentOffset]! = tv)
(heq :
∀ (o : Nat),
o < len →
rsLab[tc + o]! = tv →
sweepKey ctx tcLevel specFuel level codes rsLab rsPtn tc numcells o = nodeKey ctx tcLevel specFuel (level + 1) codes
{ lab := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).fst,
ptn := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).snd.fst,
active := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).snd.snd,
orbits := st.orbits, fixedpts := st.fixedpts.insert st.lab[tc + currentOffset]!, autos := st.autos,
wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc,
firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows,
compCanon := st.compCanon, eqlevFirst := st.eqlevFirst, eqlevCanon := st.eqlevCanon,
gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel,
noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex,
stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes,
tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits,
numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel,
genTrace := st.genTrace }
(numcells + 1))
:
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, 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 recovered := Nauty.recover n inf level cleaned;
∃ (bs' : List Nat), LoopInv G ctx tcLevel specFuel level codes bs' fs numcells rsLab rsPtn tc len tcell (some tv) base recovered outBest
eventTrail ∧ OtherLive ctx level recovered eventTrail
Resolving an ordinary off-path child after clearing a pending short-prune request rebuilds the parent invariant. This is the uniform recovery form used by both filtered and unfiltered executable branches.
theorem
Hex.GraphIso.Nauty.EventOut.ancestor
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel : Nat}
{stem codes fs : List Nat}
{out : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
{r : Int}
(h : EventOut G ctx tcLevel codes fs out best trail r)
(hprefix : List.take stem.length codes = stem)
(hshorter : stem.length < codes.length)
:
EventOut G ctx tcLevel stem fs out best trail r
Expose any shorter ancestor prefix of an existing search event.
theorem
Hex.GraphIso.Nauty.LoopInv.restrict
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel level numcells tc len : Nat}
{tcell tcell' : VSet n}
{codes bs fs : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{base st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(h : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail)
(hsub : ∀ (v : Nat), tcell'.mem v = true → tcell.mem v = true)
(hcover : SweepCover ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells tcell' cursor best)
:
LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell' cursor base st best trail
Replacing the mutable sweep set by a subset preserves the loop invariant once transitive coverage has been re-established for that set.
theorem
Hex.GraphIso.Nauty.LoopInv.fmptnFix
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel level numcells tc len : Nat}
{tcell : VSet n}
{offset : Nat}
{codes bs fs : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{base st out : SearchSt n}
{best outBest : Option (Key n)}
{trail eventTrail : FrameTrail}
{r : Int}
(hpathCodes : level = codes.length)
(h : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail)
(hpath : PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st)
(hevent : EventOut G ctx tcLevel codes fs out outBest eventTrail r)
(hpreserved :
TrailExt (level + 1)
(trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) eventTrail)
(hsaved : level ≤ out.noncheaplevel)
(v : Nat)
:
Every fixed vertex of the receiving parent lies in the fix set of
an implicit pair frozen at a deeper cheap-cell boundary. The result trail
identifies the parent's frozen frame, whose two closed singleton
boundaries are unchanged in the deeper event partition.
theorem
Hex.GraphIso.Nauty.LoopInv.fmptnPair
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel level numcells tc len : Nat}
{tcell : VSet n}
{offset : Nat}
{codes bs fs : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{base st out : SearchSt n}
{best outBest : Option (Key n)}
{trail eventTrail : FrameTrail}
{r : Int}
(hpathCodes : level = codes.length)
(h : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail)
(hpath : PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st)
(hevent : EventOut G ctx tcLevel codes fs out outBest eventTrail r)
(hpreserved :
TrailExt (level + 1)
(trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) eventTrail)
(hsaved : level ≤ out.noncheaplevel)
(hroot :
PairOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1
(fmptn out.lab out.ptn out.noncheaplevel n).fst (fmptn out.lab out.ptn out.noncheaplevel n).snd)
:
Root validity of the implicit pair and containment of the parent path
localize that pair to the exact frozen frame consumed by shortprune.
theorem
Hex.GraphIso.Nauty.LoopInv.ShortSource.atReceiver
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel runFuel level numcells tc len : Nat}
{tcell : VSet n}
{offset : Nat}
{codes bs fs : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{base st child out : SearchSt n}
{best outBest : Option (Key n)}
{trail eventTrail : FrameTrail}
{r : Int}
{fix mcr : VSet n}
(hpathCodes : level = codes.length)
(hinv : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail)
(hpath : PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st)
(hexit :
NodeExit ctx tcLevel specFuel runFuel (level + 1) codes child out (numcells + 1) best outBest
(trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) r)
(hevent : EventOut G ctx tcLevel codes fs out outBest eventTrail r)
(hpreserved :
TrailExt (level + 1)
(trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) eventTrail)
(hsource : ShortSource G ctx out eventTrail r)
(hstay : ¬r < Int.ofNat level)
(hback : out.autos.back? = some (fix, mcr))
:
A live short-prune source that reaches a receiving loop without a lower return is valid in that loop's frozen frame. The child exit bound identifies the recorded target with the receiver. Explicit pairs then use their stored frame, while implicit pairs are localized from the root.
theorem
Hex.GraphIso.Nauty.LoopInv.longprune
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel level numcells tc len : Nat}
{tcell : VSet n}
{codes bs fs : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{base st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(hgsz : ctx.g.size = n)
(h : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail)
(hpath : PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st)
:
LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len
(Nauty.longprune tcell st.fixedpts st.autos) cursor base st best trail
The long-prune filter preserves the full mutable sweep invariant. The root ledger supplies valid pairs at the current ordering, and the frozen-frame permutation transports their cell stabilization back to the specification ordering.
theorem
Hex.GraphIso.Nauty.LoopInv.shortpruneWith
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel level numcells tc len : Nat}
{tcell : VSet n}
{codes bs fs : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{base st out : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(hgsz : ctx.g.size = n)
(h : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail)
(hlast : ∀ (fix mcr : VSet n), out.autos.back? = some (fix, mcr) → PairOk ctx.g rsPtn rsLab level fix mcr)
:
LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len (Nauty.shortprune tcell out) cursor base st
best trail
The short-prune filter may read the newest pair from a descendant state. Validity at the frozen parent frame is the only fact needed to preserve the mutable sweep invariant.
theorem
Hex.GraphIso.Nauty.LoopInv.shortprune
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel level numcells tc len : Nat}
{tcell : VSet n}
{codes bs fs : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{base st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(hgsz : ctx.g.size = n)
(h : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail)
(hlast : ∀ (fix mcr : VSet n), st.autos.back? = some (fix, mcr) → PairOk ctx.g rsPtn rsLab level fix mcr)
:
LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len (Nauty.shortprune tcell st) cursor base st
best trail
The common case reads the newest pair from the current loop state.
theorem
Hex.GraphIso.Nauty.LoopInv.shortpruneChild
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel runFuel level numcells tc len : Nat}
{tcell : VSet n}
{offset : Nat}
{fixedpts : VSet n}
{codes bs fs : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{base st childSt child : SearchSt n}
{best childBest : Option (Key n)}
{trail eventTrail : FrameTrail}
{value : Int}
(hgsz : ctx.g.size = n)
(hpathCodes : level = codes.length)
(h : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail)
(hpath : PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st)
(hchild :
OtherRun G ctx tcLevel specFuel runFuel (level + 1) codes fs childSt child (numcells + 1) best childBest
(trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) eventTrail
value)
(hstay : ¬value < Int.ofNat level)
(hshort : child.needshortprune = true)
:
LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len
(Nauty.shortprune tcell
{ lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits, fixedpts := fixedpts,
autos := child.autos, wsCap := child.wsCap, firstcode := child.firstcode, canoncode := child.canoncode,
firsttc := child.firsttc, firstlab := child.firstlab, canonlab := child.canonlab, canong := child.canong,
samerows := child.samerows, compCanon := child.compCanon, eqlevFirst := child.eqlevFirst,
eqlevCanon := child.eqlevCanon, gcaFirst := child.gcaFirst, gcaCanon := child.gcaCanon,
canonlevel := child.canonlevel, noncheaplevel := child.noncheaplevel, allsamelevel := child.allsamelevel,
cosetindex := child.cosetindex, stabvertex := child.stabvertex, numnodes := child.numnodes,
tctotal := child.tctotal, canupdates := child.canupdates, numorbits := child.numorbits,
numgenerators := child.numgenerators, numbadleaves := child.numbadleaves, maxlevel := child.maxlevel,
genTrace := child.genTrace })
cursor base st best trail
A child result carrying a live request supplies exactly the local newest-pair premise required to filter its receiving parent sweep.
theorem
Hex.GraphIso.Nauty.LoopInv.childKey
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel level numcells tc len tv offset currentOffset coset : Nat}
{tcell : VSet n}
{codes bs fs : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{base st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(h : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail)
(hoffset : offset < len)
(hfrozen : rsLab[tc + offset]! = tv)
(hcurrentAt : st.lab[tc + currentOffset]! = tv)
:
sweepKey ctx tcLevel specFuel level codes rsLab rsPtn tc numcells offset = nodeKey ctx tcLevel specFuel (level + 1) codes
{ lab := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).fst,
ptn := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).snd.fst,
active := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).snd.snd, orbits := st.orbits,
fixedpts := st.fixedpts.insert st.lab[tc + currentOffset]!, 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 := coset, 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)
The mutable child selected for a frozen offset has exactly that offset's specification key.
theorem
Hex.GraphIso.Nauty.LoopInv.keyLeBound
{n : Nat}
{ctx : Ctx n}
{tcLevel specFuel level tc len numcells tail offset : Nat}
{codes : List Nat}
{rsLab rsPtn : Array Nat}
{bound : Key n}
(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)
(hoffset : offset < len)
:
Every original target-cell child key is below the fixed sweep bound.
theorem
Hex.GraphIso.Nauty.LoopInv.boundEq
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel level tc len numcells tail offset : Nat}
{codes bs fs : List Nat}
{rsLab rsPtn : Array Nat}
{bound : Key n}
{tcell : VSet n}
{cursor : Option Nat}
{base st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(hinv : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail)
(hsmall :
SubtreeOk ctx level
{ lab := rsLab, ptn := rsPtn, active := base.active, numcells := numcells, hint := 0, maxpos := 0,
longcode := numcells })
(hgsz : ctx.g.size = n)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
(hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false)
(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)
(hoffset : offset < len)
:
In a verified small-cell subtree, the fixed sibling-sweep bound is the key of any selected member. This is the semantic step that lets a saved cheap-boundary return absorb every unvisited sibling.
theorem
Hex.GraphIso.Nauty.OtherLoopRun.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 :
OtherLoopRun 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)
:
OtherLoopRun 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
theorem
Hex.GraphIso.Nauty.OtherLoopRun.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 :
OtherLoopRun 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)
:
OtherLoopRun 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
theorem
Hex.GraphIso.Nauty.OtherLoopRun.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)
(hcoset : recSt.cosetindex = st.cosetindex)
(hpre : LoopSound ctx bound best mid)
(h :
OtherLoopRun 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)
:
OtherLoopRun 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
theorem
Hex.GraphIso.Nauty.OtherLoopRun.next
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel runFuel loopFuel level numcells tc len tv1 tv : Nat}
{tcell : VSet n}
{stem codes fs : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{bound : Key n}
{st child recSt out : SearchSt n}
{best mid outBest : Option (Key n)}
{value : Int}
{receiptTrail eventTrail : FrameTrail}
{r : Option Int}
(hnext : tcell.nextElem cursor = some tv)
(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 := st.cosetindex,
stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes,
tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits,
numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel,
genTrace := st.genTrace } = (value, child))
(hstay : ¬value < Int.ofNat level)
(hshort : child.needshortprune = false)
(hother : (tv == tv1) = false)
(hrecover :
recSt = recover n inf level
{ lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits,
fixedpts := child.fixedpts.erase tv, autos := child.autos, wsCap := child.wsCap, firstcode := child.firstcode,
canoncode := child.canoncode, firsttc := child.firsttc, firstlab := child.firstlab, canonlab := child.canonlab,
canong := child.canong, samerows := child.samerows, compCanon := child.compCanon,
eqlevFirst := child.eqlevFirst, eqlevCanon := child.eqlevCanon, gcaFirst := child.gcaFirst,
gcaCanon := child.gcaCanon, canonlevel := child.canonlevel, noncheaplevel := child.noncheaplevel,
allsamelevel := child.allsamelevel, cosetindex := child.cosetindex, stabvertex := child.stabvertex,
needshortprune := child.needshortprune, numnodes := child.numnodes, tctotal := child.tctotal,
canupdates := child.canupdates, numorbits := child.numorbits, numgenerators := child.numgenerators,
numbadleaves := child.numbadleaves, maxlevel := child.maxlevel, genTrace := child.genTrace })
(hfixed : recSt.fixedpts = st.fixedpts)
(hcoset : recSt.cosetindex = st.cosetindex)
(hpre : LoopSound ctx bound best mid)
(hloop :
otherChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem (some tv)) tcell recSt = (r, out))
(hrec :
OtherLoopRun G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell (some tv)
bound recSt out mid outBest receiptTrail eventTrail r)
:
OtherLoopRun G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor
bound st (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).snd best
outBest receiptTrail eventTrail
(otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).fst
Compose an ordinary non-guiding child with the recursively proved tail of an off-path sweep.
theorem
Hex.GraphIso.Nauty.OtherLoopRun.nextLong
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel runFuel loopFuel level numcells tc len tv1 tv : Nat}
{tcell filtered : VSet n}
{stem codes fs : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{bound : Key n}
{st child recSt out : SearchSt n}
{best mid outBest : Option (Key n)}
{value : Int}
{receiptTrail eventTrail : FrameTrail}
{r : Option Int}
(hnext : tcell.nextElem cursor = some tv)
(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 := st.cosetindex,
stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes,
tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits,
numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel,
genTrace := st.genTrace } = (value, child))
(hstay : ¬value < Int.ofNat level)
(hshort : child.needshortprune = false)
(hfirst : (tv == tv1) = true)
(hfiltered : filtered = longprune tcell (child.fixedpts.erase tv) child.autos)
(hrecover :
recSt = recover n inf level
{ lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits,
fixedpts := child.fixedpts.erase tv, autos := child.autos, wsCap := child.wsCap, firstcode := child.firstcode,
canoncode := child.canoncode, firsttc := child.firsttc, firstlab := child.firstlab, canonlab := child.canonlab,
canong := child.canong, samerows := child.samerows, compCanon := child.compCanon,
eqlevFirst := child.eqlevFirst, eqlevCanon := child.eqlevCanon, gcaFirst := child.gcaFirst,
gcaCanon := child.gcaCanon, canonlevel := child.canonlevel, noncheaplevel := child.noncheaplevel,
allsamelevel := child.allsamelevel, cosetindex := child.cosetindex, stabvertex := child.stabvertex,
needshortprune := child.needshortprune, numnodes := child.numnodes, tctotal := child.tctotal,
canupdates := child.canupdates, numorbits := child.numorbits, numgenerators := child.numgenerators,
numbadleaves := child.numbadleaves, maxlevel := child.maxlevel, genTrace := child.genTrace })
(hfixed : recSt.fixedpts = st.fixedpts)
(hcoset : recSt.cosetindex = st.cosetindex)
(hpre : LoopSound ctx bound best mid)
(hloop :
otherChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (filtered.nextElem (some tv)) filtered recSt = (r, out))
(hrec :
OtherLoopRun G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells filtered
(some tv) bound recSt out mid outBest receiptTrail eventTrail r)
:
OtherLoopRun G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor
bound st (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).snd best
outBest receiptTrail eventTrail
(otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).fst
Compose a guiding child with the long-pruned recursive tail of an off-path sweep.
theorem
Hex.GraphIso.Nauty.OtherLoopRun.nextShort
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel runFuel loopFuel level numcells tc len tv1 tv : Nat}
{tcell filtered : VSet n}
{stem codes fs : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{bound : Key n}
{st child recSt out : SearchSt n}
{best mid outBest : Option (Key n)}
{value : Int}
{receiptTrail eventTrail : FrameTrail}
{r : Option Int}
(hnext : tcell.nextElem cursor = some tv)
(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 := st.cosetindex,
stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes,
tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits,
numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel,
genTrace := st.genTrace } = (value, child))
(hstay : ¬value < Int.ofNat level)
(hshort : child.needshortprune = true)
(hother : (tv == tv1) = false)
(hfiltered :
filtered = shortprune tcell
{ lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits,
fixedpts := child.fixedpts.erase tv, autos := child.autos, wsCap := child.wsCap, firstcode := child.firstcode,
canoncode := child.canoncode, firsttc := child.firsttc, firstlab := child.firstlab, canonlab := child.canonlab,
canong := child.canong, samerows := child.samerows, compCanon := child.compCanon,
eqlevFirst := child.eqlevFirst, eqlevCanon := child.eqlevCanon, gcaFirst := child.gcaFirst,
gcaCanon := child.gcaCanon, canonlevel := child.canonlevel, noncheaplevel := child.noncheaplevel,
allsamelevel := child.allsamelevel, cosetindex := child.cosetindex, stabvertex := child.stabvertex,
numnodes := child.numnodes, tctotal := child.tctotal, canupdates := child.canupdates,
numorbits := child.numorbits, numgenerators := child.numgenerators, numbadleaves := child.numbadleaves,
maxlevel := child.maxlevel, genTrace := child.genTrace })
(hrecover :
recSt = recover n inf level
{ lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits,
fixedpts := child.fixedpts.erase tv, autos := child.autos, wsCap := child.wsCap, firstcode := child.firstcode,
canoncode := child.canoncode, firsttc := child.firsttc, firstlab := child.firstlab, canonlab := child.canonlab,
canong := child.canong, samerows := child.samerows, compCanon := child.compCanon,
eqlevFirst := child.eqlevFirst, eqlevCanon := child.eqlevCanon, gcaFirst := child.gcaFirst,
gcaCanon := child.gcaCanon, canonlevel := child.canonlevel, noncheaplevel := child.noncheaplevel,
allsamelevel := child.allsamelevel, cosetindex := child.cosetindex, stabvertex := child.stabvertex,
numnodes := child.numnodes, tctotal := child.tctotal, canupdates := child.canupdates,
numorbits := child.numorbits, numgenerators := child.numgenerators, numbadleaves := child.numbadleaves,
maxlevel := child.maxlevel, genTrace := child.genTrace })
(hfixed : recSt.fixedpts = st.fixedpts)
(hcoset : recSt.cosetindex = st.cosetindex)
(hpre : LoopSound ctx bound best mid)
(hloop :
otherChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (filtered.nextElem (some tv)) filtered recSt = (r, out))
(hrec :
OtherLoopRun G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells filtered
(some tv) bound recSt out mid outBest receiptTrail eventTrail r)
:
OtherLoopRun G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor
bound st (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).snd best
outBest receiptTrail eventTrail
(otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).fst
Compose a non-guiding child with the short-pruned recursive tail of an off-path sweep.
theorem
Hex.GraphIso.Nauty.OtherLoopRun.nextBoth
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel runFuel loopFuel level numcells tc len tv1 tv : Nat}
{tcell shortSet filtered : VSet n}
{stem codes fs : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{bound : Key n}
{st child recSt out : SearchSt n}
{best mid outBest : Option (Key n)}
{value : Int}
{receiptTrail eventTrail : FrameTrail}
{r : Option Int}
(hnext : tcell.nextElem cursor = some tv)
(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 := st.cosetindex,
stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes,
tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits,
numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel,
genTrace := st.genTrace } = (value, child))
(hstay : ¬value < Int.ofNat level)
(hshort : child.needshortprune = true)
(hfirst : (tv == tv1) = true)
(hshortSet :
shortSet = shortprune tcell
{ lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits,
fixedpts := child.fixedpts.erase tv, autos := child.autos, wsCap := child.wsCap, firstcode := child.firstcode,
canoncode := child.canoncode, firsttc := child.firsttc, firstlab := child.firstlab, canonlab := child.canonlab,
canong := child.canong, samerows := child.samerows, compCanon := child.compCanon,
eqlevFirst := child.eqlevFirst, eqlevCanon := child.eqlevCanon, gcaFirst := child.gcaFirst,
gcaCanon := child.gcaCanon, canonlevel := child.canonlevel, noncheaplevel := child.noncheaplevel,
allsamelevel := child.allsamelevel, cosetindex := child.cosetindex, stabvertex := child.stabvertex,
numnodes := child.numnodes, tctotal := child.tctotal, canupdates := child.canupdates,
numorbits := child.numorbits, numgenerators := child.numgenerators, numbadleaves := child.numbadleaves,
maxlevel := child.maxlevel, genTrace := child.genTrace })
(hfiltered : filtered = longprune shortSet (child.fixedpts.erase tv) child.autos)
(hrecover :
recSt = recover n inf level
{ lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits,
fixedpts := child.fixedpts.erase tv, autos := child.autos, wsCap := child.wsCap, firstcode := child.firstcode,
canoncode := child.canoncode, firsttc := child.firsttc, firstlab := child.firstlab, canonlab := child.canonlab,
canong := child.canong, samerows := child.samerows, compCanon := child.compCanon,
eqlevFirst := child.eqlevFirst, eqlevCanon := child.eqlevCanon, gcaFirst := child.gcaFirst,
gcaCanon := child.gcaCanon, canonlevel := child.canonlevel, noncheaplevel := child.noncheaplevel,
allsamelevel := child.allsamelevel, cosetindex := child.cosetindex, stabvertex := child.stabvertex,
numnodes := child.numnodes, tctotal := child.tctotal, canupdates := child.canupdates,
numorbits := child.numorbits, numgenerators := child.numgenerators, numbadleaves := child.numbadleaves,
maxlevel := child.maxlevel, genTrace := child.genTrace })
(hfixed : recSt.fixedpts = st.fixedpts)
(hcoset : recSt.cosetindex = st.cosetindex)
(hpre : LoopSound ctx bound best mid)
(hloop :
otherChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (filtered.nextElem (some tv)) filtered recSt = (r, out))
(hrec :
OtherLoopRun G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells filtered
(some tv) bound recSt out mid outBest receiptTrail eventTrail r)
:
OtherLoopRun G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor
bound st (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).snd best
outBest receiptTrail eventTrail
(otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).fst
Compose a guiding child with the short- and long-pruned recursive tail of an off-path sweep.
theorem
Hex.GraphIso.Nauty.OtherLoopRun.childFrozen
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel runFuel loopFuel level numcells tc len tv1 tv tail offset : 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)
(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 := st.cosetindex,
stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes,
tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits,
numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel,
genTrace := st.genTrace } = (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 := st.cosetindex,
stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal,
canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators,
numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }
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 := st.cosetindex,
stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes,
tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits,
numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel,
genTrace := st.genTrace }
(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 := st.cosetindex,
stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes,
tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits,
numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel,
genTrace := st.genTrace }
(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)
:
OtherLoopRun G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor
bound st (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).snd best
outBest trail eventTrail
(otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).fst
A frozen child return below the receiving loop absorbs the live suffix, cleans the temporary fixed vertex, and exposes the ancestor event.
theorem
Hex.GraphIso.Nauty.OtherLoopRun.childCheap
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel runFuel loopFuel level numcells tc len tv1 tv boundary offset : 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)
(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 := st.cosetindex,
stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes,
tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits,
numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel,
genTrace := st.genTrace } = (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 := st.cosetindex,
stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal,
canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators,
numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }
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)
:
OtherLoopRun G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor
bound st (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).snd best
outBest trail eventTrail
(otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).fst
A saved cheap-boundary child return below the receiving loop absorbs the whole verified small-cell sweep and cleans its temporary fixed vertex.
theorem
Hex.GraphIso.Nauty.OtherLoopRun.frozen
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel runFuel loopFuel level numcells tc len tv tv1 : 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)}
{trail eventTrail : FrameTrail}
{value : Int}
(hstate :
otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st = (some value, out))
(hevent : EventOut G ctx tcLevel stem fs out outBest eventTrail value)
(hpreserved : TrailExt level trail eventTrail)
(hfixed : out.fixedpts = st.fixedpts)
(hcoset : out.cosetindex = st.cosetindex)
(hbelow : value < Int.ofNat level)
(hexact : outBest = some (incMax best bound))
(hfreeze : FrozenOut ctx codes out outBest value)
(hsource : out.needshortprune = true → ShortSource G ctx out eventTrail value)
:
OtherLoopRun G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor
bound st (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).snd best
outBest trail eventTrail
(otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).fst
Package an already established frozen early return as an off-path loop result.
theorem
Hex.GraphIso.Nauty.OtherLoopRun.cheap
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel runFuel loopFuel level numcells tc len tv tv1 boundary : 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)}
{trail eventTrail : FrameTrail}
(hstate :
otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st = (some (Int.ofNat boundary - 1), out))
(hevent : EventOut G ctx tcLevel stem fs out outBest eventTrail (Int.ofNat boundary - 1))
(hpreserved : TrailExt level trail eventTrail)
(hfixed : out.fixedpts = st.fixedpts)
(hcoset : out.cosetindex = st.cosetindex)
(hpositive : 1 ≤ boundary)
(hbelow : boundary ≤ level)
(hsaved : out.noncheaplevel = boundary)
(hexact : outBest = some (incMax best bound))
(hsource : out.needshortprune = true → ShortSource G ctx out eventTrail (Int.ofNat boundary - 1))
:
OtherLoopRun G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor
bound st (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).snd best
outBest trail eventTrail
(otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).fst
Package an already established cheap-cell jump as an off-path loop result.
theorem
Hex.GraphIso.Nauty.OtherLoopRun.unwind
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel runFuel loopFuel level numcells tc len tv tv1 target offset : 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)}
{trail eventTrail : FrameTrail}
(hstem : List.take stem.length codes = stem)
(hshorter : stem.length < codes.length)
(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 := st.cosetindex,
stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal,
canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators,
numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }
(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 := st.cosetindex,
stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes,
tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits,
numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel,
genTrace := st.genTrace }
(numcells + 1))
bound)
(hreturn :
(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 := st.cosetindex,
stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes,
tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits,
numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel,
genTrace := st.genTrace }).fst = Int.ofNat target)
(hbelow : target < level)
(payload :
Unwind ctx tcLevel target
(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 := st.cosetindex,
stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes,
tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits,
numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel,
genTrace := st.genTrace }).snd
outBest)
(hloc :
Unwind.Located (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset })
payload)
(hcontrol :
target = (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 := st.cosetindex, stabvertex := st.stabvertex, needshortprune := st.needshortprune,
numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits,
numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel,
genTrace := st.genTrace }).snd.gcaFirst ∨ target = (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 := st.cosetindex, stabvertex := st.stabvertex, needshortprune := st.needshortprune,
numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits,
numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel,
genTrace := st.genTrace }).snd.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 := st.cosetindex,
stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal,
canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators,
numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }
(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 := st.cosetindex,
stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes,
tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits,
numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel,
genTrace := st.genTrace }).snd
(numcells + 1) best outBest
(trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) eventTrail
(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 := st.cosetindex,
stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes,
tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits,
numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel,
genTrace := st.genTrace }).fst)
(hfresh : st.fixedpts.mem tv = false)
:
OtherLoopRun G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor
bound st (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).snd best
outBest trail eventTrail
(otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).fst
A generator unwind addressed strictly above this loop crosses the temporary fixed-vertex cleanup and returns immediately.
theorem
Hex.GraphIso.Nauty.OtherLoopRun.zero
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel runFuel level numcells tc len : Nat}
{tcell : VSet n}
{tv1 : 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)
:
OtherLoopRun G ctx tcLevel specFuel runFuel 0 level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st
(otherChildLoop ctx inf tcLevel runFuel 0 level numcells tc tv1 tv? tcell st).snd best best trail trail
(otherChildLoop ctx inf tcLevel runFuel 0 level numcells tc tv1 tv? tcell st).fst
Zero cursor fuel is retained as exhaustion, never mistaken for a completed sibling sweep.
theorem
Hex.GraphIso.Nauty.OtherLoopRun.done
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel runFuel loopFuel level numcells tc len tv1 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)
:
OtherLoopRun G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor
bound st (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 none tcell st).snd best best
trail trail (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 none tcell st).fst
A positive-fuel loop with no next vertex has genuinely covered the fixed original target cell and returns its exact maximum.
theorem
Hex.GraphIso.Nauty.firstChildLoop_index
{n : Nat}
(ctx : Ctx n)
(inf tcLevel fuel cfuel level numcells tc tv1 : Nat)
(tv? : Option Nat)
(tcell : VSet n)
(index index' : Nat)
(st : SearchSt n)
:
(firstChildLoop ctx inf tcLevel fuel cfuel level numcells tc tv1 tv? tcell index st).fst = (firstChildLoop ctx inf tcLevel fuel cfuel level numcells tc tv1 tv? tcell index' st).fst ∧ (firstChildLoop ctx inf tcLevel fuel cfuel level numcells tc tv1 tv? tcell index st).snd.snd = (firstChildLoop ctx inf tcLevel fuel cfuel level numcells tc tv1 tv? tcell index' st).snd.snd
The first-path loop's input index is bookkeeping only: it can change the returned index, but neither the return level nor the returned state.
theorem
Hex.GraphIso.Nauty.FirstLoopRun.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 :
FirstLoopRun 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)
:
FirstLoopRun 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
theorem
Hex.GraphIso.Nauty.FirstLoopRun.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 :
FirstLoopRun 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)
:
FirstLoopRun 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
theorem
Hex.GraphIso.Nauty.FirstLoopRun.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 :
FirstLoopRun 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)
:
FirstLoopRun 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
theorem
Hex.GraphIso.Nauty.FirstLoopRun.nextOther
{n k outIndex : 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 child recSt out : SearchSt n}
{best mid outBest : Option (Key n)}
{value : Int}
{receiptTrail eventTrail : FrameTrail}
{r : Option Int}
(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, child))
(hstay : ¬value < Int.ofNat level)
(hshort : child.needshortprune = false)
(hrecover :
recSt = recover n inf level
{ lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits,
fixedpts := child.fixedpts.erase tv, autos := child.autos, wsCap := child.wsCap, firstcode := child.firstcode,
canoncode := child.canoncode, firsttc := child.firsttc, firstlab := child.firstlab, canonlab := child.canonlab,
canong := child.canong, samerows := child.samerows, compCanon := child.compCanon,
eqlevFirst := child.eqlevFirst, eqlevCanon := child.eqlevCanon, gcaFirst := child.gcaFirst,
gcaCanon := child.gcaCanon, canonlevel := child.canonlevel, noncheaplevel := child.noncheaplevel,
allsamelevel := child.allsamelevel, cosetindex := child.cosetindex, stabvertex := child.stabvertex,
needshortprune := child.needshortprune, numnodes := child.numnodes, tctotal := child.tctotal,
canupdates := child.canupdates, numorbits := child.numorbits, numgenerators := child.numgenerators,
numbadleaves := child.numbadleaves, maxlevel := child.maxlevel, genTrace := child.genTrace })
(hfixed : recSt.fixedpts = st.fixedpts)
(hpre : LoopSound ctx bound best mid)
(hloop :
firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem (some tv)) tcell index recSt = (r, outIndex, out))
(hrec :
FirstLoopRun G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell (some tv)
bound recSt out mid outBest receiptTrail eventTrail r)
:
FirstLoopRun 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
Continue a first-path sweep after an ordinary non-guiding child.
theorem
Hex.GraphIso.Nauty.FirstLoopRun.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 child recSt out : SearchSt n}
{best mid outBest : Option (Key n)}
{value : Int}
{outIndex : Nat}
{receiptTrail eventTrail : FrameTrail}
{r : Option Int}
(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, child))
(hstay : ¬value < Int.ofNat level)
(hshort : child.needshortprune = false)
(hrecover :
recSt = recover n inf level
(have __src :=
have __src :=
{ lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits,
fixedpts := child.fixedpts.erase tv, autos := child.autos, wsCap := child.wsCap,
firstcode := child.firstcode, canoncode := child.canoncode, firsttc := child.firsttc,
firstlab := child.firstlab, canonlab := child.canonlab, canong := child.canong, samerows := child.samerows,
compCanon := child.compCanon, eqlevFirst := child.eqlevFirst, eqlevCanon := child.eqlevCanon,
gcaFirst := child.gcaFirst, gcaCanon := child.gcaCanon, canonlevel := child.canonlevel,
noncheaplevel := child.noncheaplevel, allsamelevel := child.allsamelevel, cosetindex := child.cosetindex,
stabvertex := child.stabvertex, needshortprune := child.needshortprune, numnodes := child.numnodes,
tctotal := child.tctotal, canupdates := child.canupdates, numorbits := child.numorbits,
numgenerators := child.numgenerators, numbadleaves := child.numbadleaves, maxlevel := child.maxlevel,
genTrace := child.genTrace };
{ lab := __src.lab, ptn := __src.ptn, active := __src.active, orbits := __src.orbits,
fixedpts := __src.fixedpts, autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode,
canoncode := __src.canoncode, firsttc := __src.firsttc, firstlab := __src.firstlab,
canonlab := __src.canonlab, canong := __src.canong, samerows := __src.samerows, compCanon := __src.compCanon,
eqlevFirst := __src.eqlevFirst, eqlevCanon := __src.eqlevCanon, gcaFirst := level, gcaCanon := __src.gcaCanon,
canonlevel := __src.canonlevel, noncheaplevel := __src.noncheaplevel, allsamelevel := __src.allsamelevel,
cosetindex := __src.cosetindex, stabvertex := __src.stabvertex, needshortprune := __src.needshortprune,
numnodes := __src.numnodes, tctotal := __src.tctotal, canupdates := __src.canupdates,
numorbits := __src.numorbits, numgenerators := __src.numgenerators, numbadleaves := __src.numbadleaves,
maxlevel := __src.maxlevel, genTrace := __src.genTrace };
{ lab := __src.lab, ptn := __src.ptn, active := __src.active, orbits := __src.orbits, fixedpts := __src.fixedpts,
autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode, canoncode := __src.canoncode,
firsttc := __src.firsttc, firstlab := __src.firstlab, canonlab := __src.canonlab, canong := __src.canong,
samerows := __src.samerows, compCanon := __src.compCanon, eqlevFirst := __src.eqlevFirst,
eqlevCanon := __src.eqlevCanon, gcaFirst := __src.gcaFirst, gcaCanon := __src.gcaCanon,
canonlevel := __src.canonlevel, noncheaplevel := __src.noncheaplevel, allsamelevel := __src.allsamelevel,
cosetindex := __src.cosetindex, stabvertex := tv1, needshortprune := __src.needshortprune,
numnodes := __src.numnodes, tctotal := __src.tctotal, canupdates := __src.canupdates,
numorbits := __src.numorbits, numgenerators := __src.numgenerators, numbadleaves := __src.numbadleaves,
maxlevel := __src.maxlevel, genTrace := __src.genTrace }))
(hfixed : recSt.fixedpts = st.fixedpts)
(hpre : LoopSound ctx bound best mid)
(hloop :
firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem (some tv)) tcell index recSt = (r, outIndex, out))
(hrec :
FirstLoopRun G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell (some tv)
bound recSt out mid outBest receiptTrail eventTrail r)
:
FirstLoopRun 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
Continue a first-path sweep after its guiding child.
theorem
Hex.GraphIso.Nauty.FirstLoopRun.nextOtherShort
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel runFuel loopFuel level numcells tc len tv1 tv index : Nat}
{tcell filtered : VSet n}
{stem codes fs : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{bound : Key n}
{st child recSt out : SearchSt n}
{best mid outBest : Option (Key n)}
{value : Int}
{outIndex : Nat}
{receiptTrail eventTrail : FrameTrail}
{r : Option Int}
(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, child))
(hstay : ¬value < Int.ofNat level)
(hshort : child.needshortprune = true)
(hfiltered :
filtered = shortprune tcell
(have __src :=
{ lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits,
fixedpts := child.fixedpts.erase tv, autos := child.autos, wsCap := child.wsCap, firstcode := child.firstcode,
canoncode := child.canoncode, firsttc := child.firsttc, firstlab := child.firstlab,
canonlab := child.canonlab, canong := child.canong, samerows := child.samerows, compCanon := child.compCanon,
eqlevFirst := child.eqlevFirst, eqlevCanon := child.eqlevCanon, gcaFirst := child.gcaFirst,
gcaCanon := child.gcaCanon, canonlevel := child.canonlevel, noncheaplevel := child.noncheaplevel,
allsamelevel := child.allsamelevel, cosetindex := child.cosetindex, stabvertex := child.stabvertex,
needshortprune := child.needshortprune, numnodes := child.numnodes, tctotal := child.tctotal,
canupdates := child.canupdates, numorbits := child.numorbits, numgenerators := child.numgenerators,
numbadleaves := child.numbadleaves, maxlevel := child.maxlevel, genTrace := child.genTrace };
{ lab := __src.lab, ptn := __src.ptn, active := __src.active, orbits := __src.orbits, fixedpts := __src.fixedpts,
autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode, canoncode := __src.canoncode,
firsttc := __src.firsttc, firstlab := __src.firstlab, canonlab := __src.canonlab, canong := __src.canong,
samerows := __src.samerows, compCanon := __src.compCanon, eqlevFirst := __src.eqlevFirst,
eqlevCanon := __src.eqlevCanon, gcaFirst := __src.gcaFirst, gcaCanon := __src.gcaCanon,
canonlevel := __src.canonlevel, noncheaplevel := __src.noncheaplevel, allsamelevel := __src.allsamelevel,
cosetindex := __src.cosetindex, stabvertex := __src.stabvertex, numnodes := __src.numnodes,
tctotal := __src.tctotal, canupdates := __src.canupdates, numorbits := __src.numorbits,
numgenerators := __src.numgenerators, numbadleaves := __src.numbadleaves, maxlevel := __src.maxlevel,
genTrace := __src.genTrace }))
(hrecover :
recSt = recover n inf level
(have __src :=
{ lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits,
fixedpts := child.fixedpts.erase tv, autos := child.autos, wsCap := child.wsCap, firstcode := child.firstcode,
canoncode := child.canoncode, firsttc := child.firsttc, firstlab := child.firstlab,
canonlab := child.canonlab, canong := child.canong, samerows := child.samerows, compCanon := child.compCanon,
eqlevFirst := child.eqlevFirst, eqlevCanon := child.eqlevCanon, gcaFirst := child.gcaFirst,
gcaCanon := child.gcaCanon, canonlevel := child.canonlevel, noncheaplevel := child.noncheaplevel,
allsamelevel := child.allsamelevel, cosetindex := child.cosetindex, stabvertex := child.stabvertex,
needshortprune := child.needshortprune, numnodes := child.numnodes, tctotal := child.tctotal,
canupdates := child.canupdates, numorbits := child.numorbits, numgenerators := child.numgenerators,
numbadleaves := child.numbadleaves, maxlevel := child.maxlevel, genTrace := child.genTrace };
{ lab := __src.lab, ptn := __src.ptn, active := __src.active, orbits := __src.orbits, fixedpts := __src.fixedpts,
autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode, canoncode := __src.canoncode,
firsttc := __src.firsttc, firstlab := __src.firstlab, canonlab := __src.canonlab, canong := __src.canong,
samerows := __src.samerows, compCanon := __src.compCanon, eqlevFirst := __src.eqlevFirst,
eqlevCanon := __src.eqlevCanon, gcaFirst := __src.gcaFirst, gcaCanon := __src.gcaCanon,
canonlevel := __src.canonlevel, noncheaplevel := __src.noncheaplevel, allsamelevel := __src.allsamelevel,
cosetindex := __src.cosetindex, stabvertex := __src.stabvertex, numnodes := __src.numnodes,
tctotal := __src.tctotal, canupdates := __src.canupdates, numorbits := __src.numorbits,
numgenerators := __src.numgenerators, numbadleaves := __src.numbadleaves, maxlevel := __src.maxlevel,
genTrace := __src.genTrace }))
(hfixed : recSt.fixedpts = st.fixedpts)
(hpre : LoopSound ctx bound best mid)
(hloop :
firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (filtered.nextElem (some tv)) filtered index
recSt = (r, outIndex, out))
(hrec :
FirstLoopRun G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells filtered
(some tv) bound recSt out mid outBest receiptTrail eventTrail r)
:
FirstLoopRun 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
Continue a non-guiding first-path sweep after consuming a short-prune request from its child.
theorem
Hex.GraphIso.Nauty.FirstLoopRun.nextGuideShort
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel runFuel loopFuel level numcells tc len tv1 tv index : Nat}
{tcell filtered : VSet n}
{stem codes fs : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{bound : Key n}
{st child recSt out : SearchSt n}
{best mid outBest : Option (Key n)}
{value : Int}
{outIndex : Nat}
{receiptTrail eventTrail : FrameTrail}
{r : Option Int}
(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, child))
(hstay : ¬value < Int.ofNat level)
(hshort : child.needshortprune = true)
(hfiltered :
filtered = shortprune tcell
(have __src :=
have __src :=
have __src :=
{ lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits,
fixedpts := child.fixedpts.erase tv, autos := child.autos, wsCap := child.wsCap,
firstcode := child.firstcode, canoncode := child.canoncode, firsttc := child.firsttc,
firstlab := child.firstlab, canonlab := child.canonlab, canong := child.canong,
samerows := child.samerows, compCanon := child.compCanon, eqlevFirst := child.eqlevFirst,
eqlevCanon := child.eqlevCanon, gcaFirst := child.gcaFirst, gcaCanon := child.gcaCanon,
canonlevel := child.canonlevel, noncheaplevel := child.noncheaplevel, allsamelevel := child.allsamelevel,
cosetindex := child.cosetindex, stabvertex := child.stabvertex, needshortprune := child.needshortprune,
numnodes := child.numnodes, tctotal := child.tctotal, canupdates := child.canupdates,
numorbits := child.numorbits, numgenerators := child.numgenerators, numbadleaves := child.numbadleaves,
maxlevel := child.maxlevel, genTrace := child.genTrace };
{ lab := __src.lab, ptn := __src.ptn, active := __src.active, orbits := __src.orbits,
fixedpts := __src.fixedpts, autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode,
canoncode := __src.canoncode, firsttc := __src.firsttc, firstlab := __src.firstlab,
canonlab := __src.canonlab, canong := __src.canong, samerows := __src.samerows,
compCanon := __src.compCanon, eqlevFirst := __src.eqlevFirst, eqlevCanon := __src.eqlevCanon,
gcaFirst := level, gcaCanon := __src.gcaCanon, canonlevel := __src.canonlevel,
noncheaplevel := __src.noncheaplevel, allsamelevel := __src.allsamelevel, cosetindex := __src.cosetindex,
stabvertex := __src.stabvertex, needshortprune := __src.needshortprune, numnodes := __src.numnodes,
tctotal := __src.tctotal, canupdates := __src.canupdates, numorbits := __src.numorbits,
numgenerators := __src.numgenerators, numbadleaves := __src.numbadleaves, maxlevel := __src.maxlevel,
genTrace := __src.genTrace };
{ lab := __src.lab, ptn := __src.ptn, active := __src.active, orbits := __src.orbits,
fixedpts := __src.fixedpts, autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode,
canoncode := __src.canoncode, firsttc := __src.firsttc, firstlab := __src.firstlab,
canonlab := __src.canonlab, canong := __src.canong, samerows := __src.samerows, compCanon := __src.compCanon,
eqlevFirst := __src.eqlevFirst, eqlevCanon := __src.eqlevCanon, gcaFirst := __src.gcaFirst,
gcaCanon := __src.gcaCanon, canonlevel := __src.canonlevel, noncheaplevel := __src.noncheaplevel,
allsamelevel := __src.allsamelevel, cosetindex := __src.cosetindex, stabvertex := tv1,
needshortprune := __src.needshortprune, numnodes := __src.numnodes, tctotal := __src.tctotal,
canupdates := __src.canupdates, numorbits := __src.numorbits, numgenerators := __src.numgenerators,
numbadleaves := __src.numbadleaves, maxlevel := __src.maxlevel, genTrace := __src.genTrace };
{ lab := __src.lab, ptn := __src.ptn, active := __src.active, orbits := __src.orbits, fixedpts := __src.fixedpts,
autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode, canoncode := __src.canoncode,
firsttc := __src.firsttc, firstlab := __src.firstlab, canonlab := __src.canonlab, canong := __src.canong,
samerows := __src.samerows, compCanon := __src.compCanon, eqlevFirst := __src.eqlevFirst,
eqlevCanon := __src.eqlevCanon, gcaFirst := __src.gcaFirst, gcaCanon := __src.gcaCanon,
canonlevel := __src.canonlevel, noncheaplevel := __src.noncheaplevel, allsamelevel := __src.allsamelevel,
cosetindex := __src.cosetindex, stabvertex := __src.stabvertex, numnodes := __src.numnodes,
tctotal := __src.tctotal, canupdates := __src.canupdates, numorbits := __src.numorbits,
numgenerators := __src.numgenerators, numbadleaves := __src.numbadleaves, maxlevel := __src.maxlevel,
genTrace := __src.genTrace }))
(hrecover :
recSt = recover n inf level
(have __src :=
have __src :=
have __src :=
{ lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits,
fixedpts := child.fixedpts.erase tv, autos := child.autos, wsCap := child.wsCap,
firstcode := child.firstcode, canoncode := child.canoncode, firsttc := child.firsttc,
firstlab := child.firstlab, canonlab := child.canonlab, canong := child.canong,
samerows := child.samerows, compCanon := child.compCanon, eqlevFirst := child.eqlevFirst,
eqlevCanon := child.eqlevCanon, gcaFirst := child.gcaFirst, gcaCanon := child.gcaCanon,
canonlevel := child.canonlevel, noncheaplevel := child.noncheaplevel, allsamelevel := child.allsamelevel,
cosetindex := child.cosetindex, stabvertex := child.stabvertex, needshortprune := child.needshortprune,
numnodes := child.numnodes, tctotal := child.tctotal, canupdates := child.canupdates,
numorbits := child.numorbits, numgenerators := child.numgenerators, numbadleaves := child.numbadleaves,
maxlevel := child.maxlevel, genTrace := child.genTrace };
{ lab := __src.lab, ptn := __src.ptn, active := __src.active, orbits := __src.orbits,
fixedpts := __src.fixedpts, autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode,
canoncode := __src.canoncode, firsttc := __src.firsttc, firstlab := __src.firstlab,
canonlab := __src.canonlab, canong := __src.canong, samerows := __src.samerows,
compCanon := __src.compCanon, eqlevFirst := __src.eqlevFirst, eqlevCanon := __src.eqlevCanon,
gcaFirst := level, gcaCanon := __src.gcaCanon, canonlevel := __src.canonlevel,
noncheaplevel := __src.noncheaplevel, allsamelevel := __src.allsamelevel, cosetindex := __src.cosetindex,
stabvertex := __src.stabvertex, needshortprune := __src.needshortprune, numnodes := __src.numnodes,
tctotal := __src.tctotal, canupdates := __src.canupdates, numorbits := __src.numorbits,
numgenerators := __src.numgenerators, numbadleaves := __src.numbadleaves, maxlevel := __src.maxlevel,
genTrace := __src.genTrace };
{ lab := __src.lab, ptn := __src.ptn, active := __src.active, orbits := __src.orbits,
fixedpts := __src.fixedpts, autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode,
canoncode := __src.canoncode, firsttc := __src.firsttc, firstlab := __src.firstlab,
canonlab := __src.canonlab, canong := __src.canong, samerows := __src.samerows, compCanon := __src.compCanon,
eqlevFirst := __src.eqlevFirst, eqlevCanon := __src.eqlevCanon, gcaFirst := __src.gcaFirst,
gcaCanon := __src.gcaCanon, canonlevel := __src.canonlevel, noncheaplevel := __src.noncheaplevel,
allsamelevel := __src.allsamelevel, cosetindex := __src.cosetindex, stabvertex := tv1,
needshortprune := __src.needshortprune, numnodes := __src.numnodes, tctotal := __src.tctotal,
canupdates := __src.canupdates, numorbits := __src.numorbits, numgenerators := __src.numgenerators,
numbadleaves := __src.numbadleaves, maxlevel := __src.maxlevel, genTrace := __src.genTrace };
{ lab := __src.lab, ptn := __src.ptn, active := __src.active, orbits := __src.orbits, fixedpts := __src.fixedpts,
autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode, canoncode := __src.canoncode,
firsttc := __src.firsttc, firstlab := __src.firstlab, canonlab := __src.canonlab, canong := __src.canong,
samerows := __src.samerows, compCanon := __src.compCanon, eqlevFirst := __src.eqlevFirst,
eqlevCanon := __src.eqlevCanon, gcaFirst := __src.gcaFirst, gcaCanon := __src.gcaCanon,
canonlevel := __src.canonlevel, noncheaplevel := __src.noncheaplevel, allsamelevel := __src.allsamelevel,
cosetindex := __src.cosetindex, stabvertex := __src.stabvertex, numnodes := __src.numnodes,
tctotal := __src.tctotal, canupdates := __src.canupdates, numorbits := __src.numorbits,
numgenerators := __src.numgenerators, numbadleaves := __src.numbadleaves, maxlevel := __src.maxlevel,
genTrace := __src.genTrace }))
(hfixed : recSt.fixedpts = st.fixedpts)
(hpre : LoopSound ctx bound best mid)
(hloop :
firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (filtered.nextElem (some tv)) filtered index
recSt = (r, outIndex, out))
(hrec :
FirstLoopRun G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells filtered
(some tv) bound recSt out mid outBest receiptTrail eventTrail r)
:
FirstLoopRun 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
Continue the guiding first-path sweep after consuming its child's short-prune request.
theorem
Hex.GraphIso.Nauty.FirstLoopRun.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 + 1) st trail)
(hcanon : CanonTrail ctx level st trail)
(hguide : level ≤ st.gcaFirst)
(horder : st.gcaFirst ≤ st.gcaCanon)
:
FirstLoopRun 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 for the first-path sweep.
theorem
Hex.GraphIso.Nauty.FirstLoopRun.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 + 1) st trail)
(hcanon : CanonTrail ctx level st trail)
(hguide : level ≤ st.gcaFirst)
(horder : st.gcaFirst ≤ st.gcaCanon)
:
FirstLoopRun 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
An absent next vertex completes a positive-fuel first-path sweep.