def Hex.GraphIso.Nauty.Max.Keeps {n : Nat} (parents : Parents n) (exit : Exit) (st : Search n) : Prop

Every accumulated generator stabilizes each saved first ancestor whose sweep survives the return. Ancestors unwound past need no carrier.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.Max.Scope.keeps {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level : Nat} {cs bs : List Nat} {st : Search n} {parents : Parents n} (h : Scope G ctx tcLevel level cs bs st parents) (exit : Exit) : Keeps parents exit st

The incoming scope already stabilizes every saved first frame.

theorem Hex.GraphIso.Nauty.Max.Keeps.congr {n : Nat} {parents : Parents n} {exit : Exit} {st out : Search n} (h : Keeps parents exit st) (he : out.genTrace = st.genTrace) : Keeps parents exit out

Cleanup and recovery preserve the accumulated carriers when they retain the generator trace.