theorem Hex.GraphIso.Nauty.runTraced_result (n : Nat) (g : Array (VSet n)) (lab0 : Array Nat) (cellEnds : List Nat) : (runTraced n g lab0 cellEnds).result = run n g lab0 cellEnds

The traced run's result is the production run's result.

theorem Hex.GraphIso.Nauty.runColoredTraced_result {n k : Nat} (G : Colored n k) : (runColoredTraced G).result = runColored G

The traced coloured-graph run agrees with the production run.