theorem
Hex.GraphIso.Nauty.Sparse.Max.SweepInput.reference_child
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel boundary tv o : Nat}
{l : Loop n}
{bs fs : List Nat}
{cell : VSet n}
{st : State n}
{parents : Parents n}
{targets : List Nat}
{key : Key n}
(h : SweepInput G tcLevel l bs fs (some tv) cell st parents)
:
have c := Loop.cell G.graph tcLevel l;
have R := State.refined (Graph.ofGraph G.graph) l.node.level l.node.numcells l.node.entry;
have ch := Generic.Policy.child l.first l.node.level c.tc tv st;
o < c.len →
c.entry.lab[c.tc + o]! = tv →
Generation.ChildPath G.graph tcLevel boundary l.node.level R c.tc targets key o →
Generation.RefPath G.graph tcLevel boundary (l.node.level + 1)
(State.refined (Graph.ofGraph G.graph) (l.node.level + 1) (c.numcells + 1) ch) targets key
A reference in the frozen target child occurs in the exact cached child entered by the production sweep, after any sibling reordering.