theorem Hex.GraphIso.Nauty.tracePolicy {n : Nat} (ctx : Ctx n) (inf tcLevel : Nat) (γ : Array Nat) : Generic.StablePolicy ctx inf tcLevel fun (st : Search n) => γ ∈ st.genTrace

Every off-path operation retains each previously emitted generator.

theorem Hex.GraphIso.Nauty.node_contains {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : Search n) {γ : Array Nat} (h : γ ∈ st.genTrace) : γ ∈ (node false ctx inf tcLevel fuel level numcells st).snd.genTrace

An off-path node retains its whole incoming trace.

theorem Hex.GraphIso.Nauty.sweep_contains {n : Nat} (ctx : Ctx n) (inf tcLevel fuel cfuel : Nat) (first : Bool) (level numcells tc tv1 index : Nat) (cursor : Option Nat) (cell : VSet n) (st : Search n) (hpast : Generic.Past first tv1 cursor) {γ : Array Nat} (h : γ ∈ st.genTrace) : γ ∈ (sweep first ctx inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd.genTrace

A sibling suffix retains every child generator already received.