theorem Hex.GraphIso.Nauty.Sparse.range_cursor {first last cur : Nat} {pref suff : List Nat} (h : first ≤ last) (hr : [first:last].toList = pref ++ cur :: suff) : cur + suff.length + 1 = last

theorem Hex.GraphIso.Nauty.Sparse.get_set (a : Array Nat) (i v q : Nat) (hq : q < a.size) : (a.set! i v)[q]! = if q = i then v else a[q]!

Reading after a bounded-array write, in the form used by refinement's insertion and scatter operations.

theorem Hex.GraphIso.Nauty.Sparse.exchange_eq (a : Array Nat) (i j : Nat) (hi : i < a.size) (hj : j < a.size) : (a.set! i a[j]!).set! j a[i]! = a.swapIfInBounds i j

The two-write exchange also covers equal indices.

theorem Hex.GraphIso.Nauty.Sparse.rotate_eq (a : Array Nat) (i j k : Nat) (hkj : k ≤ j) (hji : j ≤ i) (hi : i < a.size) : ((a.set! i a[j]!).set! j a[k]!).set! k a[i]! = (a.swapIfInBounds i j).swapIfInBounds j k

Nauty's three writes are two exchanges even when neighbouring cut positions coincide. The order excludes a nonadjacent index collision.

theorem Hex.GraphIso.Nauty.Sparse.swap_perm (a : Array Nat) (i j : Nat) : (a.swapIfInBounds i j).toList.Perm a.toList

theorem Hex.GraphIso.Nauty.Sparse.exchange_perm (a : Array Nat) (i j : Nat) (hi : i < a.size) (hj : j < a.size) : ((a.set! i a[j]!).set! j a[i]!).toList.Perm a.toList

theorem Hex.GraphIso.Nauty.Sparse.rotate_perm (a : Array Nat) (i j k : Nat) (hkj : k ≤ j) (hji : j ≤ i) (hi : i < a.size) : (((a.set! i a[j]!).set! j a[k]!).set! k a[i]!).toList.Perm a.toList

theorem Hex.GraphIso.Nauty.Sparse.rotate_read (a : Array Nat) (i j k : Nat) (hkj : k ≤ j) (hji : j ≤ i) (hi : i < a.size) : (a.set! i a[j]!)[k]! = a[k]!

The second source read in the executed rotation follows its first write. If that write aliases the read, all three positions coincide.

theorem Hex.GraphIso.Nauty.Sparse.perm_size {a b : Array Nat} (h : a.toList.Perm b.toList) : a.size = b.size

theorem Hex.GraphIso.Nauty.Sparse.indirect_perm {a b y : Array Nat} {start len : Nat} (h : a.toList.Perm b.toList) (hb : start + len ≤ b.size) : («Sort».indirect a y start len).toList.Perm b.toList