theorem Hex.GraphIso.Nauty.Sparse.Sort.segment_perm {a b : Array Nat} {lo hi : Nat} (hb : lo ≤ hi ∧ hi ≤ a.size) (hp : b.toList.Perm a.toList) (he : ∀ (q : Nat), q < lo ∨ hi ≤ q → b[q]! = a[q]!) : (b.extract lo hi).toList.Perm (a.extract lo hi).toList

A whole-array permutation supported inside a segment induces a permutation of that segment, cancelling the fixed exterior.

theorem Hex.GraphIso.Nauty.Sparse.Sort.segment_mem {a b : Array Nat} {lo hi q : Nat} (hsize : hi ≤ b.size) (hp : (b.extract lo hi).toList.Perm (a.extract lo hi).toList) (hq : lo ≤ q ∧ q < hi) : ∃ (r : Nat), lo ≤ r ∧ r < hi ∧ b[q]! = a[r]!

def Hex.GraphIso.Nauty.Sparse.Sort.Apart (p q : Nat × Nat) : Prop

Two pending segments do not overlap.

Equations

• Hex.GraphIso.Nauty.Sparse.Sort.Apart p q = (p.fst + p.snd ≤ q.fst ∨ q.fst + q.snd ≤ p.fst)

def Hex.GraphIso.Nauty.Sparse.Sort.Pending (x y : Array Nat) (lo hi : Nat) (stack : List (Nat × Nat)) : Prop

All ordering obligations except pairs still in one pending segment.

Equations

• Hex.GraphIso.Nauty.Sparse.Sort.Pending x y lo hi stack = ∀ (i j : Nat), lo ≤ i → i < j → j < hi → y[x[i]!]! ≤ y[x[j]!]! ∨ ∃ (p : Nat × Nat), p ∈ stack ∧ p.fst ≤ i ∧ j < p.fst + p.snd

theorem Hex.GraphIso.Nauty.Sparse.Sort.Pending.replace {a b y : Array Nat} {lo hi start len : Nat} {rest parts : List (Nat × Nat)} (h : Pending a y lo hi ((start, len) :: rest)) (hb : lo ≤ start ∧ start + len ≤ hi) (hd : ∀ (p : Nat × Nat), p ∈ rest → Apart (start, len) p) (he : ∀ (q : Nat), q < start ∨ start + len ≤ q → b[q]! = a[q]!) (hm : ∀ (q : Nat), start ≤ q → q < start + len → ∃ (r : Nat), start ≤ r ∧ r < start + len ∧ b[q]! = a[r]!) (hl : Pending b y start (start + len) parts) : Pending b y lo hi (parts ++ rest)

Replacing one segment by a permutation cannot disturb its ordering against the disjoint pending segments or the already completed entries.