theorem
Hex.GraphIso.Nauty.Generation.FirstTail.complete
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel runFuel level numcells tc len tv1 e boundary oRef : Nat}
{codes fs targets : List Nat}
{rsLab rsPtn : Array Nat}
{base : SearchSt n}
{key : Key n}
(hg : ctx.g = rowsOf G)
(hinf : inf = n + 2)
(hpath : level = codes.length)
(hrun : n + 2 < level + 1 + runFuel)
(hboundary : level < boundary)
(href : oRef < len)
(hp : ChildPath ctx tcLevel boundary level (LoopInv.frame rsLab rsPtn numcells) tc targets key oRef)
{loopFuel : Nat}
{cursor : Option Nat}
{tcell : VSet n}
{st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(sweep :
FirstTail G ctx inf tcLevel specFuel runFuel level numcells tc len tv1 e codes fs rsLab rsPtn base loopFuel cursor
tcell st best trail)
(hm : Matches ctx (level + 1) st targets key)
(heq : st.eqlevFirst = level)
(hsame : boundary ≤ st.allsamelevel)
(hfuel : n < cursorRank cursor + loopFuel)
(index : Nat)
:
(firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem cursor) tcell index st).fst = none
Once the guiding child has installed its reference, the first-path tail finishes its sweep. This rules out premature returns both above and below an inherited cheap-cell boundary.