structure Hex.GraphIso.Nauty.Sparse.Minima.Permuted (before lab hits : Array Nat) (first last v2 v3 upto w1 w2 cap : Nat) extends Hex.GraphIso.Nauty.Sparse.Minima.Bounded lab hits first last v2 v3 upto w1 w2 cap : Prop

The executed insertion keeps a bounded count partition and permutes vertices only inside the original cell.

• bounds : first < v2 ∧ v2 ≤ v3 ∧ v3 ≤ upto
• keys : w1 < w2
• minimum (q : Nat) : first ≤ q → q < v2 → hits[lab[q]!]! = w1
• second (q : Nat) : v2 ≤ q → q < v3 → hits[lab[q]!]! = w2
• larger (q : Nat) : v3 ≤ q → q < upto → w2 < hits[lab[q]!]!
• size : last ≤ lab.size
• scan : upto ≤ last
• values (q : Nat) : first ≤ q → q < last → hits[lab[q]!]! < cap
• empty : v2 = v3 → w2 = cap
• window : «Sort».Window before lab first last

theorem Hex.GraphIso.Nauty.Sparse.Minima.Permuted.initial {lab hits : Array Nat} {first last upto w1 cap : Nat} (hb : first < upto) (hu : upto ≤ last) (hs : last ≤ lab.size) (hv : ∀ (q : Nat), first ≤ q → q < last → hits[lab[q]!]! < cap) (hm : ∀ (q : Nat), first ≤ q → q < upto → hits[lab[q]!]! = w1) : Permuted lab lab hits first last upto upto upto w1 cap cap

theorem Hex.GraphIso.Nauty.Sparse.Minima.Permuted.hit_min {before lab hits : Array Nat} {first last v2 v3 upto w1 w2 cap : Nat} (h : Permuted before lab hits first last v2 v3 upto w1 w2 cap) (hu : upto < last) (hk : hits[lab[upto]!]! = w1) : Permuted before (((lab.set! upto lab[v3]!).set! v3 lab[v2]!).set! v2 lab[upto]!) hits first last (v2 + 1) (v3 + 1) (upto + 1) w1 w2 cap

theorem Hex.GraphIso.Nauty.Sparse.Minima.Permuted.hit_second {before lab hits : Array Nat} {first last v2 v3 upto w1 w2 cap : Nat} (h : Permuted before lab hits first last v2 v3 upto w1 w2 cap) (hu : upto < last) (hk : hits[lab[upto]!]! = w2) : Permuted before ((lab.set! upto lab[v3]!).set! v3 lab[upto]!) hits first last v2 (v3 + 1) (upto + 1) w1 w2 cap

theorem Hex.GraphIso.Nauty.Sparse.Minima.Permuted.new_min {before lab hits : Array Nat} {first last v2 v3 upto w1 w2 cap : Nat} (h : Permuted before lab hits first last v2 v3 upto w1 w2 cap) (hu : upto < last) (hk : hits[lab[upto]!]! < w1) : Permuted before (((lab.set! upto lab[v2]!).set! v2 lab[first]!).set! first lab[upto]!) hits first last (first + 1) (v2 + 1) (upto + 1) hits[lab[upto]!]! w1 cap

theorem Hex.GraphIso.Nauty.Sparse.Minima.Permuted.new_second {before lab hits : Array Nat} {first last v2 v3 upto w1 w2 cap : Nat} (h : Permuted before lab hits first last v2 v3 upto w1 w2 cap) (hu : upto < last) (hlo : w1 < hits[lab[upto]!]!) (hhi : hits[lab[upto]!]! < w2) : Permuted before ((lab.set! upto lab[v2]!).set! v2 lab[upto]!) hits first last v2 (v2 + 1) (upto + 1) w1 hits[lab[upto]!]! cap

theorem Hex.GraphIso.Nauty.Sparse.Minima.Permuted.above {before lab hits : Array Nat} {first last v2 v3 upto w1 w2 cap : Nat} (h : Permuted before lab hits first last v2 v3 upto w1 w2 cap) (hu : upto < last) (hk : w2 < hits[lab[upto]!]!) : Permuted before lab hits first last v2 v3 (upto + 1) w1 w2 cap