theorem Hex.GraphIso.Nauty.Sparse.Binary.Pass.equiv {n level stamp : Nat} {xs : List Nat} {s a : RefineSt n} (f : Nat → Nat) (h : Pass level stamp xs s a) {t b : RefineSt n} {otherStamp : Nat} : Pass level otherStamp 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 f s.lab) → (∀ (v : Nat), v < n → (s.vmarks[v]! == stamp) = (t.vmarks[f v]! == otherStamp)) → CountTrace.control s = CountTrace.control t → s.numcells = t.numcells → a.ptn = b.ptn ∧ cellsPerm a.ptn level b.lab (Array.map f a.lab) ∧ CountTrace.control a = CountTrace.control b ∧ a.numcells = b.numcells

Paired touched-cell traces preserve ordered partition, cell contents, hash, active set, ordered queue and exact cell count. Their caches and mark generations may differ.