theorem Hex.GraphIso.Nauty.Max.rules {n k : Nat} (G : Colored n k) (tcLevel : Nat) : Rules G tcLevel

Every actual maximum and accumulated-trace rule composes in one recursive policy, including first-leaf installation and sweep completion.