theorem Hex.GraphIso.Nauty.Sparse.CountTrace.count_pass {n : Nat} (level : Nat) (distance : Bool) (key : Nat → Nat) (cells : Array Nat) (s : RefineSt n) (hp : s.lab.toList.Perm (List.range n)) (hs : s.ptn.size = n) (hi : Index.Valid n s.lab s.ptn level s.cellstart s.cellend) (hn : cells.toList.Nodup) (hc : ∀ (a : Nat), a ∈ cells.toList → Ready level key a s.cellend[a]! s) : Pass level distance key cells.toList s (have s := s; do let __s ← forIn cells s fun (first : Nat) (__s : RefineSt n) => have s := __s; have s := splitCounts level first distance s; pure (ForInStep.yield s) have s : RefineSt n := __s pure s).run

The executed count-split iterator admits the semantic trace. Its pending original cells retain exact keys through earlier disjoint splits.