theorem Hex.GraphIso.Nauty.Sparse.touch_scan (neighbor : Nat → Nat) (keys marks vmarks : Array Nat) (n stamp lo hi : Nat) (hm : Scratch.Marks n stamp marks) (hs : vmarks.size = n) (hv : ∀ (e : Nat), lo ≤ e → e < hi → neighbor e < n) (hk : ∀ (e : Nat), lo ≤ e → e < hi → keys[neighbor e]! ≤ n) : have r := (have marks := marks; have touched := #[]; have hitVertices := vmarks; do let __s ← forIn [lo:hi] (marks, touched, hitVertices) fun (e : Nat) (__s : Array Nat × Array Nat × Array Nat) => have marks := __s.fst; have __s := __s.snd; have touched := __s.fst; have hitVertices := __s.snd; have j := neighbor e; have hitVertices := hitVertices.set! j (stamp + 1); have k := keys[j]!; if (k != n && marks[k]! != stamp + 1) = true then have marks := marks.set! k (stamp + 1); have touched := touched.push k; pure (ForInStep.yield (marks, touched, hitVertices)) else pure (ForInStep.yield (marks, touched, hitVertices)) have marks : Array Nat := __s.fst have __s : Array Nat × Array Nat := __s.snd have touched : Array Nat := __s.fst have hitVertices : Array Nat := __s.snd pure (marks, touched, hitVertices)).run; Touched n stamp marks r.fst r.snd.fst (List.map (fun (e : Nat) => keys[neighbor e]!) (List.range' lo (hi - lo))) ∧ Index.Writes n vmarks r.snd.snd (List.map neighbor (List.range' lo (hi - lo))) (stamp + 1)

The singleton splitter's neighbour scan marks exactly the observed vertices and enumerates each touched nonsingleton cell once.