theorem Hex.GraphIso.Nauty.firstChild_ready {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel level numcells tv last : Nat} {st leaf : Search n} (hin : FirstPre G ctx level numcells st) (hn0 : 0 < n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hopen : (Generic.prepareFirst ctx tcLevel level numcells st).fst ≠ n) (htv : (Generic.prepareFirst ctx tcLevel level numcells st).snd.snd.fst.nextElem none = some tv) (horbit : (cheapCheck true level (Generic.prepareFirst ctx tcLevel level numcells st).snd.snd.snd.snd).orbits[tv]! = tv) (hpath : have r := Generic.prepareFirst ctx tcLevel level numcells st; Generic.FirstPath ctx tcLevel fuel (level + 1) (r.fst + 1) (child true level r.snd.fst.toNat tv (cheapCheck true level r.snd.snd.snd.snd)) last leaf) (hchild : have r := Generic.prepareFirst ctx tcLevel level numcells st; RunInv G ctx (node true ctx (n + 2) tcLevel fuel (level + 1) (r.fst + 1) (child true level r.snd.fst.toNat tv (cheapCheck true level r.snd.snd.snd.snd))).snd) (hgsz : ctx.g.size = n) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) : have r := Generic.prepareFirst ctx tcLevel level numcells st; have out := (node true ctx (n + 2) tcLevel fuel (level + 1) (r.fst + 1) (child true level r.snd.fst.toNat tv (cheapCheck true level r.snd.snd.snd.snd))).snd; have left := have __src := afterChildFirst level tv out; { lab := __src.lab, ptn := __src.ptn, active := __src.active, orbits := __src.orbits, fixedpts := out.fixedpts.erase tv, autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode, canoncode := __src.canoncode, firsttc := __src.firsttc, firstlab := __src.firstlab, canonlab := __src.canonlab, canong := __src.canong, samerows := __src.samerows, compCanon := __src.compCanon, eqlevFirst := __src.eqlevFirst, eqlevCanon := __src.eqlevCanon, gcaFirst := __src.gcaFirst, gcaCanon := __src.gcaCanon, canonlevel := __src.canonlevel, noncheaplevel := __src.noncheaplevel, allsamelevel := __src.allsamelevel, cosetindex := __src.cosetindex, stabvertex := __src.stabvertex, numnodes := __src.numnodes, tctotal := __src.tctotal, canupdates := __src.canupdates, numorbits := __src.numorbits, numgenerators := __src.numgenerators, numbadleaves := __src.numbadleaves, maxlevel := __src.maxlevel, order := __src.order, genTrace := __src.genTrace, workperm := __src.workperm }; SweepPre G ctx tcLevel true level r.fst r.snd.fst.toNat tv none r.snd.snd.fst (recover (n + 2) level left)

The first child installs the reference at its parent and supplies the recovered frame from which all later siblings use the off-path contract.