def Hex.GraphIso.Nauty.Sparse.Sort.Sorted (x y : Array Nat) (start len : Nat) : Prop

Key order on a segment, using the same indirect reads as the executable.

Equations

• Hex.GraphIso.Nauty.Sparse.Sort.Sorted x y start len = ∀ (i j : Nat), i < j → j < len → y[x[start + i]!]! ≤ y[x[start + j]!]!

theorem Hex.GraphIso.Nauty.Sparse.Sort.Sorted.mono {x y : Array Nat} {start len small : Nat} (h : Sorted x y start len) (hs : small ≤ len) : Sorted x y start small

theorem Hex.GraphIso.Nauty.Sparse.Sort.insertion_sorted (x y : Array Nat) (start len : Nat) (hb : start + len ≤ x.size) : Sorted (insertion x y start len) y start len

The executed short-segment insertion sort orders the indirect keys.

theorem Hex.GraphIso.Nauty.Sparse.Sort.insertion_outside (x y : Array Nat) (start len q : Nat) (hq : q < start ∨ start + len ≤ q) : (insertion x y start len)[q]! = x[q]!

Insertion sort leaves every entry outside its segment unchanged.

theorem Hex.GraphIso.Nauty.Sparse.Sort.median_mem (a b c : Nat) : median a b c = a ∨ median a b c = b ∨ median a b c = c

A median is one of its samples, including when sample keys coincide.

theorem Hex.GraphIso.Nauty.Sparse.Sort.pivot_mem (x y : Array Nat) (start len : Nat) (hl : 0 < len) : ∃ (i : Nat), i < len ∧ pivot x y start len = y[x[start + i]!]!

Both pinned pivot schemes choose a key belonging to the nonempty segment.