theorem Hex.GraphIso.Nauty.Sparse.Binary.Pass.lab_eq {n level stamp : Nat} {xs : List Nat} {s a : RefineSt n} (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) → s.ptn.size = n → t.lab = s.lab → 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 → (∀ (v : Nat), v < n → (s.vmarks[v]! == stamp) = (t.vmarks[v]! == otherStamp)) → a.lab = b.lab

The complete executed singleton-cell fold returns literally equal labels from equal input labels and partitions. Valid caches, retained marks and generation numbers may differ between the two traversals.