theorem Hex.GraphIso.Nauty.pushAuto_trace {n : Nat} {κ : Type} (st : SearchState n κ) (pair : VSet n × VSet n) : (pushAuto st pair).genTrace = st.genTrace

The bounded workspace does not change the full generator trace.

theorem Hex.GraphIso.Nauty.admit_trace {n : Nat} {κ : Type} (st : SearchState n κ) : (admit st).genTrace = st.genTrace.push st.workperm

Admission appends the completed scratch permutation to the full trace.

theorem Hex.GraphIso.Nauty.admit_checked {n : Nat} {ctx : Ctx n} {st : Search n} (htrace : ∀ (γ : Array Nat), γ ∈ st.genTrace → checkAutom ctx.g γ = true) (hwork : checkAutom ctx.g st.workperm = true) (γ : Array Nat) : γ ∈ (admit st).genTrace → checkAutom ctx.g γ = true

Admitting a checked permutation preserves validity of the full trace.