theorem
Hex.GraphIso.Nauty.Sparse.Max.Parent.Guided.first_back
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel last : Nat}
{p : Parent n}
{ds fs : List Nat}
{cell : VSet n}
{tv : Nat}
{leaf : State n}
(h : Guided G.graph tcLevel p)
(hp : Valid G tcLevel p)
(hb : p.state.gcaCanon ≤ p.node.level)
(path :
have ch := child G.graph tcLevel p;
Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel ch.level ch.numcells ch.entry last leaf)
(hg : Grows (State.key G.graph p.bs p.state) (State.key G.graph ds (firstBack G.graph tcLevel fuel p)))
(hr :
have ch := child G.graph tcLevel p;
ReturnCodes G.graph ch.codes ds fs
(Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel ch.level ch.numcells ch.entry).snd)
(hd :
have ch := child G.graph tcLevel p;
Covers (Frame.key G.graph tcLevel ch)
(State.best G.graph
(Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel ch.level ch.numcells ch.entry).snd))
:
Receiving the first child establishes both covered references for the actual next sibling. The newly saved first label comes from the executed first descent; only the completed child's coverage is inductive.