structure Hex.GraphIso.Nauty.Sparse.Sort.Window (before after : Array Nat) (first last : Nat) : Prop

A permutation supported inside a half-open position interval.

• perm : after.toList.Perm before.toList
• outside (q : Nat) : q < first ∨ last ≤ q → after[q]! = before[q]!

theorem Hex.GraphIso.Nauty.Sparse.Sort.Window.refl (lab : Array Nat) (first last : Nat) : Window lab lab first last

theorem Hex.GraphIso.Nauty.Sparse.Sort.Window.size {before after : Array Nat} {first last : Nat} (h : Window before after first last) : after.size = before.size

theorem Hex.GraphIso.Nauty.Sparse.Sort.Window.exchange {before after : Array Nat} {first last i j : Nat} (h : Window before after first last) (hi : first ≤ i ∧ i < last) (hj : first ≤ j ∧ j < last) (hb : last ≤ after.size) : Window before ((after.setIfInBounds i after[j]!).setIfInBounds j after[i]!) first last

theorem Hex.GraphIso.Nauty.Sparse.Sort.Window.rotate {before after : Array Nat} {first last k j i : Nat} (h : Window before after first last) (hk : first ≤ k) (hkj : k ≤ j) (hji : j ≤ i) (hi : i < last) (hb : last ≤ after.size) : Window before (((after.setIfInBounds i after[j]!).setIfInBounds j after[k]!).setIfInBounds k after[i]!) first last

theorem Hex.GraphIso.Nauty.Sparse.Sort.Window.indirect {before after : Array Nat} {first last start len : Nat} {hits : Array Nat} (h : Window before after first last) (hl : first ≤ start) (hh : start + len ≤ last) (hb : last ≤ after.size) : Window before («Sort».indirect after hits start len) first last

theorem Hex.GraphIso.Nauty.Sparse.Sort.Window.mem {before after : Array Nat} {first last q : Nat} (h : Window before after first last) (hb : last ≤ after.size) (hq : first ≤ q ∧ q < last) : ∃ (r : Nat), first ≤ r ∧ r < last ∧ after[q]! = before[r]!

theorem Hex.GraphIso.Nauty.Sparse.perm_bound {lab : Array Nat} {n i : Nat} (h : lab.toList.Perm (List.range n)) (hi : i < n) : lab[i]! < n

theorem Hex.GraphIso.Nauty.Sparse.perm_injective {lab : Array Nat} {n i j : Nat} (h : lab.toList.Perm (List.range n)) (hi : i < n) (hj : j < n) (he : lab[i]! = lab[j]!) : i = j