theorem Hex.GraphIso.Nauty.SweepPre.child_key {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel level numcells tc tv1 tv len offset : Nat} {first : Bool} {cell : VSet n} {base st : Search n} (h : SweepPre G ctx tcLevel first level numcells tc tv1 (some tv) cell st) (hframe : SearchOut G level level base st) (hbase : SearchOk G level numcells base) (hn0 : 0 < n) (hcell : IsCell base.ptn level tc len) (hlen : 2 ≤ len) (hrange : tc + len ≤ n) (ho : offset < len) (hv : base.lab[tc + offset]! = tv) (hfuel : level + 1 + fuel ≤ n + 1) : childKey ctx tcLevel fuel level base.lab base.ptn tc numcells offset = specNode ctx tcLevel fuel (level + 1) (Nauty.child first level tc tv st).lab (Nauty.child first level tc tv st).ptn (Nauty.child first level tc tv st).active (numcells + 1)

The current child of a recovered sweep has the specification key of the same vertex in the parent frame, irrespective of its current offset.