theorem Hex.GraphIso.Nauty.Sparse.Index.Tail.scanned {n first last upto : Nat} {oldlab hits oldstarts oldends : Array Nat} {s : RefineSt n} {b : Nat} (h : Tail n first last upto oldlab hits oldstarts oldends s) (r : RefineSt n) (hp : oldlab.toList.Perm (List.range n)) (hu : upto < last) (hbn : last < n) (ha : upto + 1 ≤ b) (hb : b ≤ last) (hk : hits[s.lab[b]!]! = hits[s.lab[upto + 1]!]!) (hn : b = upto + 1 + (last - (upto + 1)) ∨ hits[s.lab[b + 1]!]! ≠ hits[s.lab[upto + 1]!]!) (hs : Scatter n s.lab s.cellstart r.cellstart (upto + 1 + 1) (b + 1) (upto + 1)) : Tail n first last b oldlab hits oldstarts oldends { lab := s.lab, ptn := r.ptn, active := r.active, queue := r.queue, cellstart := r.cellstart.setIfInBounds s.lab[upto + 1]! (if b - (upto + 1) = 0 then n else upto + 1), cellend := s.cellend.setIfInBounds (upto + 1) b, indexed := r.indexed, hits := hits, marks := r.marks, vmarks := r.vmarks, stamp := r.stamp, numcells := r.numcells, longcode := r.longcode }

The scan's existing range bound and break condition supply a maximal run. Its writes preserve the other fields of the current working state.