theorem
Hex.GraphIso.Nauty.Max.SweepInput.stabilizes
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel : Nat}
{first : Bool}
{level numcells tc tv1 index : Nat}
{cursor : Option 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 cursor cell index st l bs fs parents)
(hf : first = true)
{γ : Array Nat}
(hγ : γ ∈ st.genTrace)
:
Stabilization of a frozen sweep partition also holds in its current ordering, since every cell has the same contents.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.child_scope
{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)
:
Suspending the current sweep constructs every field of the child's ancestor scope at the actual individualization.