theorem
Hex.GraphIso.Nauty.FirstInv.head
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel runFuel level numcells : Nat}
{codes : List Nat}
{st : SearchSt n}
{trail : FrameTrail}
(hg : ctx.g = rowsOf G)
(hinf : inf = n + 2)
(hlevel : 1 ≤ level)
(hpath : level = codes.length + 1)
(hspec : level + 1 + specFuel = n + 1)
(hfuel : n + 2 < level + 1 + runFuel)
(hcheap : st.noncheaplevel ≤ level)
(hdesc : CheapDesc ctx level st.noncheaplevel (refine ctx level st.lab st.ptn st.active numcells))
(hfirst : FirstInv G ctx level codes numcells st trail)
(hpathOk : PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st)
(horb : OrbSound (OrbConn st.genTrace.toList n) st.orbits n)
(hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells < n)
:
have rs := refine ctx level st.lab st.ptn st.active numcells;
have full := codes ++ [rs.longcode];
∃ (tc : Nat), ∃ (len : Nat), have tcell := windowSet n rs.lab tc len;
2 ≤ len ∧ tc + len ≤ n ∧ maketargetcell ctx rs.lab rs.ptn level tcLevel (-1) = (tc, worksetOf n rs.lab tc (tc + len - 1), len) ∧ Generation.FirstHead G ctx inf tcLevel specFuel runFuel level rs.numcells tc len
((tcell.nextElem none).getD 0) st.noncheaplevel full rs.lab rs.ptn tcell
(Generation.firstStart ctx level numcells tc len st) trail
The established correctness induction exposes the actual guiding visit and recovered tail at an internal first-path node.