theorem
Hex.GraphIso.Nauty.Max.received_trace
{n : Nat}
(first : Bool)
(inf level tv1 tv : Nat)
(out : Search n)
:
have middle := if (first && tv == tv1) = true then afterChildFirst level tv1 out else out;
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 };
(recover inf level left).genTrace = out.genTrace
Cleanup and recovery retain every generator returned by the child.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.child_keeps
{n k : Nat}
{G : Colored n k}
{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 { g := rowsOf G } tcLevel fuel cfuel first level numcells tc tv1 (some tv) cell index st l bs fs parents)
(hn : (contract G tcLevel).nodeValid fuel (Generic.nodeCall { g := rowsOf G } (n + 2) tcLevel fuel))
:
The actual child input supplies preservation of its complete output trace from the same smaller contract that supplies its key bounds.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.received_generators
{n k : Nat}
{G : Colored n k}
{tcLevel fuel cfuel : Nat}
{first short : Bool}
{level numcells tc tv1 tv index : Nat}
{cell : VSet n}
{st out : Search n}
{l : Loop n}
{bs fs : List Nat}
{parents : Parents n}
(h :
SweepInput G { g := rowsOf G } tcLevel fuel cfuel first level numcells tc tv1 (some tv) cell index st l bs fs parents)
(hn : (contract G tcLevel).nodeValid fuel (Generic.nodeCall { g := rowsOf G } (n + 2) tcLevel fuel))
(hcall :
Nauty.node (first && tv == tv1) { g := rowsOf G } (n + 2) tcLevel fuel (level + 1) (numcells + 1)
(child first level tc tv st) = (Generic.Exit.unwind level short, out))
:
have ctx := { g := rowsOf G };
have middle := if (first && tv == tv1) = true then afterChildFirst level tv1 out else out;
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 };
have ready := recover (n + 2) level left;
(first = true →
∀ (γ : Array Nat),
γ ∈ ready.genTrace →
CellStab (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.ptn level (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.lab
γ) ∧ ∀ (t : Nat) (p : Parent n),
parents t = some p →
p.loop.first = true → ∀ (γ : Array Nat), γ ∈ ready.genTrace → CellStab p.state.ptn t p.state.lab γ
A received child's accumulated generators supply both the current frozen first-loop carriers and every older saved first-frame carrier.