structure Hex.GraphIso.Nauty.Sparse.Sort.Agree (y z : Array Nat) (lo hi : Nat) (x : Array Nat) : Prop

The two key arrays agree on entries currently stored in a bounded segment. Neither array is constrained on vertices outside that segment.

• bound : hi ≤ x.size
• keys (q : Nat) : lo ≤ q → q < hi → y[x[q]!]! = z[x[q]!]!

theorem Hex.GraphIso.Nauty.Sparse.Sort.Agree.mono {y z : Array Nat} {lo hi : Nat} {x : Array Nat} {first last : Nat} (h : Agree y z lo hi x) (hf : lo ≤ first) (hl : last ≤ hi) : Agree y z first last x

theorem Hex.GraphIso.Nauty.Sparse.Sort.Agree.write {y z : Array Nat} {lo hi : Nat} {x : Array Nat} {v : Nat} (h : Agree y z lo hi x) (hk : y[v]! = z[v]!) (i : Nat) : Agree y z lo hi (x.set! i v)

theorem Hex.GraphIso.Nauty.Sparse.Sort.Agree.swap {y z : Array Nat} {lo hi : Nat} {x : Array Nat} {i j : Nat} (h : Agree y z lo hi x) (hi' : lo ≤ i ∧ i < hi) (hj : lo ≤ j ∧ j < hi) : Agree y z lo hi (x.swapIfInBounds i j)

theorem Hex.GraphIso.Nauty.Sparse.Sort.Agree.window {y z : Array Nat} {lo hi : Nat} {x out : Array Nat} (h : Agree y z lo hi x) (hw : Window x out lo hi) : Agree y z lo hi out

theorem Hex.GraphIso.Nauty.Sparse.Sort.pivot_congr {y z : Array Nat} {start len : Nat} {x : Array Nat} (h : Agree y z start (start + len) x) (hl : 0 < len) : pivot x y start len = pivot x z start len

Both pinned pivot sampling schemes read only their nonempty segment.

theorem Hex.GraphIso.Nauty.Sparse.Sort.insertion_congr {y z : Array Nat} {start len : Nat} {x : Array Nat} (h : Agree y z start (start + len) x) : insertion x y start len = insertion x z start len

The exact short-segment insertion sort is unaffected by keys outside the segment. Equal-key stability is retained literally.