theorem
Hex.GraphIso.Nauty.Sparse.Max.FirstInput.sweep_done
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel tv last : Nat}
{f : Frame n}
{leaf : State n}
{parents : Parents n}
(h : FirstInput G tcLevel f parents)
(hi : (visit (Graph.ofGraph G.graph) f.level f.numcells f.entry).fst < n)
(htv :
(Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry).snd.snd.fst.nextElem none = some tv)
(horbit :
(cheapCheck true f.level
(Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells
f.entry).snd.snd.snd.snd).orbits[tv]! = tv)
(path :
have p := Frame.firstParent G.graph tcLevel f [] tv;
have ch := Parent.child G.graph tcLevel p;
Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel ch.level ch.numcells ch.entry last leaf)
(hf : n ≤ f.level + fuel)
(hreturn :
have p := Frame.firstParent G.graph tcLevel f [] tv;
have ch := Parent.child G.graph tcLevel p;
(Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel ch.level ch.numcells ch.entry).fst = Generic.Exit.unwind f.level false)
:
have p := Frame.firstParent G.graph tcLevel f [] tv;
(Generic.sweep true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (n + 1) f.level
(Frame.target G.graph tcLevel f).numcells p.tc tv (some tv) p.cell 0 p.state).fst = Generic.Exit.done
A normally returning guiding child initializes the full native sibling sweep, which finishes after all surviving targets are processed.
theorem
Hex.GraphIso.Nauty.Sparse.Max.FirstInput.returns
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel last : Nat}
{f : Frame n}
{leaf : State n}
{parents : Parents n}
(h : FirstInput G tcLevel f parents)
(path : Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel f.level f.numcells f.entry last leaf)
(hf : n + 1 ≤ f.level + fuel)
:
(Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel f.level f.numcells f.entry).fst = Generic.Exit.unwind (f.level - 1) false
Every actual first-path call returns normally to its immediate parent. The proof derives the guiding child's return by induction and then executes its entire remaining sibling sweep.