theorem Hex.GraphIso.Nauty.canonSpecKey_eq_tracedKey {n k : Nat} (G : Colored n k) (hn0 : 0 < n) : canonSpecKey G = tracedKey G

The search computes the full specification key for every nonempty coloured graph.