theorem Hex.GraphIso.Nauty.Max.SweepInput.restore {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel cfuel : Nat} {first : Bool} {level numcells tc tv1 tv index : Nat} {cell : VSet n} {st : Search n} {l : Loop n} {bs fs : List Nat} {parents : Parents n} (h : SweepInput G ctx tcLevel fuel cfuel first level numcells tc tv1 (some tv) cell index st l bs fs parents) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hvisit : (!first || st.orbits[tv]! == tv) = true) : have raw := (Nauty.node (first && tv == tv1) ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child first level tc tv st)).snd; have middle := if (first && tv == tv1) = true then afterChildFirst level tv1 raw else raw; have left := { lab := middle.lab, ptn := middle.ptn, active := middle.active, orbits := middle.orbits, fixedpts := middle.fixedpts.erase tv, autos := middle.autos, wsCap := middle.wsCap, firstcode := middle.firstcode, canoncode := middle.canoncode, firsttc := middle.firsttc, firstlab := middle.firstlab, canonlab := middle.canonlab, canong := middle.canong, samerows := middle.samerows, compCanon := middle.compCanon, eqlevFirst := middle.eqlevFirst, eqlevCanon := middle.eqlevCanon, gcaFirst := middle.gcaFirst, gcaCanon := middle.gcaCanon, canonlevel := middle.canonlevel, noncheaplevel := middle.noncheaplevel, allsamelevel := middle.allsamelevel, cosetindex := middle.cosetindex, stabvertex := middle.stabvertex, numnodes := middle.numnodes, tctotal := middle.tctotal, canupdates := middle.canupdates, numorbits := middle.numorbits, numgenerators := middle.numgenerators, numbadleaves := middle.numbadleaves, maxlevel := middle.maxlevel, order := middle.order, genTrace := middle.genTrace, workperm := middle.workperm }; SweepPre G ctx tcLevel first level numcells tc tv1 none cell (recover (n + 2) level left)

Returning from either sweep phase establishes the common off-path state used by all remaining siblings.