theorem Hex.GraphIso.Nauty.Sparse.reverse_read (hit : Array Nat) (i : Nat) (hi : i < hit.size) : hit[hit.size - 1 - i]! = hit.toList.reverse[i]!

Reverse indexing in the executed reinsertion loop reads the corresponding entry of the reversed hit list.

theorem Hex.GraphIso.Nauty.Sparse.restore_scan (before hit starts : Array Nat) (first n : Nat) (hb : first + hit.size ≤ before.size) (hs : starts.size = n) (hv : ∀ (v : Nat), v ∈ hit.toList → v < n) : have r := (have lab := before; have starts := starts; have v3 := first; do let __s ← forIn [:hit.size] (lab, starts, v3) fun (t : Nat) (__s : Array Nat × Array Nat × Nat) => have lab := __s.fst; have __s := __s.snd; have starts := __s.fst; have v3 := __s.snd; have j := hit[hit.size - 1 - t]!; have starts := starts.set! j first; have lab := lab.set! v3 j; have v3 := v3 + 1; pure (ForInStep.yield (lab, starts, v3)) have lab : Array Nat := __s.fst have __s : Array Nat × Nat := __s.snd have starts : Array Nat := __s.fst have v3 : Nat := __s.snd pure (lab, starts, v3)).run; Fill before hit.toList.reverse first hit.toList.reverse.length r.fst ∧ Index.Writes n starts r.snd.fst hit.toList.reverse first ∧ r.snd.snd = first + hit.size

The actual reverse hit loop copies every hit and writes its new cell start. Its bounds permit empty hit lists and repeated input vertices.