theorem
Hex.GraphIso.Nauty.Sparse.Max.FirstInput.recovered
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel tv last : Nat}
{f : Frame n}
{parents : Parents n}
{leaf : State n}
{bs fs : List Nat}
{smaller : VSet 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)
(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)
(hr :
have p := Frame.firstParent G.graph tcLevel f [] tv;
have ch := Parent.child G.graph tcLevel p;
ReturnCodes G.graph ch.codes bs fs
(Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel ch.level ch.numcells ch.entry).snd)
(resume :
have p := Frame.firstParent G.graph tcLevel f [] tv;
Resumed G tcLevel p bs fs (Parent.firstBack G.graph tcLevel fuel p) parents)
(hd :
have p := Frame.firstParent G.graph tcLevel f [] tv;
have ch := Parent.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))
(hsub :
∀ (v : Nat),
smaller.mem v = true →
(Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry).snd.snd.fst.mem v = true)
(hc :
have l := { node := f, first := true };
have p := Frame.firstParent G.graph tcLevel f [] tv;
Cell.Cover G.graph tcLevel (Loop.cell G.graph tcLevel l) (Remaining (smaller.nextElem (some tv)) smaller)
(State.key G.graph bs (Parent.firstBack G.graph tcLevel fuel p)))
:
have p := Frame.firstParent G.graph tcLevel f [] tv;
SweepInput G tcLevel { node := f, first := true } bs fs (smaller.nextElem (some tv)) smaller
(Parent.firstBack G.graph tcLevel fuel p) parents
The actual first child's covered result establishes the complete later-sibling context. Saved traces, references and pruning pairs come from its executed first descent; only subtree coverage is inductive.