theorem
Hex.GraphIso.Nauty.Max.firstPath_returns
{n k : Nat}
{G : Colored n k}
{tcLevel fuel level numcells last : Nat}
{st leaf : Search n}
(hp : Generic.FirstPath { g := rowsOf G } tcLevel fuel level numcells st last leaf)
(hn : ∀ (f : Nat), f < fuel → (contract G tcLevel).nodeValid f (Generic.nodeCall { g := rowsOf G } (n + 2) tcLevel f))
{cs bs fs : List Nat}
{parents : Parents n}
(hi :
NodeInput G { g := rowsOf G } tcLevel fuel true { level := level, numcells := numcells, codes := cs, entry := st } bs
fs parents)
:
A first call returns normally to its parent. The induction proves the guiding child's return and initializes its actual remaining sweep.
theorem
Hex.GraphIso.Nauty.Max.firstPath_complete
{n k : Nat}
{G : Colored n k}
{tcLevel fuel level numcells last : Nat}
{st leaf : Search n}
(hp : Generic.FirstPath { g := rowsOf G } tcLevel fuel level numcells st last leaf)
(hn : ∀ (f : Nat), f < fuel → (contract G tcLevel).nodeValid f (Generic.nodeCall { g := rowsOf G } (n + 2) tcLevel f))
{cs bs fs : List Nat}
{parents : Parents n}
(hi :
NodeInput G { g := rowsOf G } tcLevel fuel true { level := level, numcells := numcells, codes := cs, entry := st } bs
fs parents)
:
have ctx := { g := rowsOf G };
have out := node true ctx (n + 2) tcLevel fuel level numcells st;
out.fst = Generic.Exit.unwind (level - 1) false ∧ ∃ (targets : List Nat), ∃ (key : Key n), Generation.RefPath ctx tcLevel out.snd.allsamelevel level (SearchState.refined ctx level numcells st) targets
key ∧ Generation.Matches ctx level out.snd targets key
The complete first-path conclusion uses only smaller maximum and trace contracts, with no assumed return or reference-covering sweep.