theorem Hex.GraphIso.Nauty.Sparse.CountTrace.Pass.equiv {n level : Nat} {distance : Bool} {key : Nat → Nat} {xs : List Nat} {s a : RefineSt n} (σ : Renaming n) (h : Pass level distance key xs s a) {t b : RefineSt n} {other : Nat → Nat} : Pass level distance other xs t b → s.lab.toList.Perm (List.range n) → t.lab.toList.Perm (List.range n) → s.ptn.size = n → t.ptn = s.ptn → Index.Valid n s.lab s.ptn level s.cellstart s.cellend → Index.Valid n t.lab t.ptn level t.cellstart t.cellend → cellsPerm s.ptn level t.lab (Array.map σ.toFun s.lab) → (∀ (v : Nat), v < n → other (σ.toFun v) = key v) → control s = control t → s.numcells = t.numcells → a.ptn = b.ptn ∧ cellsPerm a.ptn level b.lab (Array.map σ.toFun a.lab) ∧ control a = control b ∧ a.numcells = b.numcells

Count-split traces transport all observations when their semantic counts commute with renaming. Only processed cells constrain scratch hits.