theorem
Hex.GraphIso.Nauty.child_frame
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel level numcells tc tv : Nat}
{first : Bool}
{cell : VSet n}
{st : Search n}
(h : SearchOk G level numcells st)
(hn0 : 0 < n)
(hlevel : 1 ≤ level)
(hpath : FixedCells level st)
(htarget : Generic.Target (fun (st : Search n) => st) level tc cell st)
(ht : cell.mem tv = true)
(childFirst : Bool)
:
have raw := (node childFirst ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child first level tc tv st)).snd;
have out :=
{ lab := raw.lab, ptn := raw.ptn, active := raw.active, orbits := raw.orbits, fixedpts := raw.fixedpts.erase tv,
autos := raw.autos, wsCap := raw.wsCap, firstcode := raw.firstcode, canoncode := raw.canoncode,
firsttc := raw.firsttc, firstlab := raw.firstlab, canonlab := raw.canonlab, canong := raw.canong,
samerows := raw.samerows, compCanon := raw.compCanon, eqlevFirst := raw.eqlevFirst, eqlevCanon := raw.eqlevCanon,
gcaFirst := raw.gcaFirst, gcaCanon := raw.gcaCanon, canonlevel := raw.canonlevel,
noncheaplevel := raw.noncheaplevel, allsamelevel := raw.allsamelevel, cosetindex := raw.cosetindex,
stabvertex := raw.stabvertex, numnodes := raw.numnodes, tctotal := raw.tctotal, canupdates := raw.canupdates,
numorbits := raw.numorbits, numgenerators := raw.numgenerators, numbadleaves := raw.numbadleaves,
maxlevel := raw.maxlevel, order := raw.order, genTrace := raw.genTrace, workperm := raw.workperm };
SearchOut G level level st out ∧ out.fixedpts = st.fixedpts
Leaving an actual child restores the parent's fixed set and preserves its partition frame, before any pruning or partition recovery occurs.
theorem
Hex.GraphIso.Nauty.SweepPre.child_frame
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel level numcells tc tv1 tv : Nat}
{first : Bool}
{cell : VSet n}
{st : Search n}
(h : SweepPre G ctx tcLevel first level numcells tc tv1 (some tv) cell st)
(hn0 : 0 < n)
(childFirst : Bool)
:
have raw := (node childFirst ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child first level tc tv st)).snd;
have out :=
{ lab := raw.lab, ptn := raw.ptn, active := raw.active, orbits := raw.orbits, fixedpts := raw.fixedpts.erase tv,
autos := raw.autos, wsCap := raw.wsCap, firstcode := raw.firstcode, canoncode := raw.canoncode,
firsttc := raw.firsttc, firstlab := raw.firstlab, canonlab := raw.canonlab, canong := raw.canong,
samerows := raw.samerows, compCanon := raw.compCanon, eqlevFirst := raw.eqlevFirst, eqlevCanon := raw.eqlevCanon,
gcaFirst := raw.gcaFirst, gcaCanon := raw.gcaCanon, canonlevel := raw.canonlevel,
noncheaplevel := raw.noncheaplevel, allsamelevel := raw.allsamelevel, cosetindex := raw.cosetindex,
stabvertex := raw.stabvertex, numnodes := raw.numnodes, tctotal := raw.tctotal, canupdates := raw.canupdates,
numorbits := raw.numorbits, numgenerators := raw.numgenerators, numbadleaves := raw.numbadleaves,
maxlevel := raw.maxlevel, order := raw.order, genTrace := raw.genTrace, workperm := raw.workperm };
SearchOut G level level st out ∧ out.fixedpts = st.fixedpts
Later siblings restore their fixed set before applying the returned filter.