theorem Hex.GraphIso.Nauty.Sparse.Binary.pass_loop {n : Nat} (step : Nat → RefineSt n → RefineSt n) (level stamp : Nat) (hstep : ∀ (first : Nat) (s : RefineSt n), s.lab.toList.Perm (List.range n) → s.ptn.size = n → Index.Valid n s.lab s.ptn level s.cellstart s.cellend → IsCell s.ptn level first (s.cellend[first]! + 1 - first) → first < s.cellend[first]! → s.cellend[first]! < n → Cell level first (s.cellend[first]! + 1) (fun (v : Nat) => s.vmarks[v]! == stamp) s (step first s)) (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 → IsCell s.ptn level a (s.cellend[a]! + 1 - a) ∧ a < s.cellend[a]! ∧ s.cellend[a]! < n) : Pass level stamp cells.toList s (have s := s; do let __s ← forIn cells s fun (first : Nat) (__s : RefineSt n) => have s := __s; have s := step first s; pure (ForInStep.yield s) have s : RefineSt n := __s pure s).run

The touched-cell iterator composes the executed cell contract. A cell already processed cannot invalidate the cache description of a later cell.