def Hex.GraphIso.Nauty.Sparse.Sort.Blocks (a base : Array Nat) (left right done : Nat) : Prop

Pointwise state of the two disjoint blocks after exchanging their first done entries.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.Sparse.Sort.Blocks.initial (a : Array Nat) (left right : Nat) : Blocks a a left right 0

theorem Hex.GraphIso.Nauty.Sparse.Sort.Blocks.step {a base : Array Nat} {left right count done : Nat} (h : Blocks a base left right done) (hleft : left + count ≤ right) (hright : right + count ≤ base.size) (hd : done < count) : Blocks (a.swapIfInBounds (left + done) (right + done)) base left right (done + 1)

theorem Hex.GraphIso.Nauty.Sparse.Sort.Cuts.left_block {x y out : Array Nat} {lo hi v a b d : Nat} (h : Cuts x y lo hi v a b b d) (hs : Blocks out x lo (b - min (a - lo) (b - a)) (min (a - lo) (b - a))) : Cuts out y lo hi v lo (lo + (b - a)) b d ∧ ∀ (q : Nat), lo + (b - a) ≤ q → q < b → y[out[q]!]! = v

After moving the equal keys from the left end, the left recursive fragment precedes that pivot block. The right half is unchanged.

structure Hex.GraphIso.Nauty.Sparse.Sort.Separated (x y : Array Nat) (lo hi v left right : Nat) : Prop

The final partition has strictly smaller keys, equal pivot keys, and strictly larger keys in three consecutive intervals.

• bounds : lo ≤ left ∧ left ≤ right ∧ right ≤ hi
• lt (q : Nat) : lo ≤ q → q < left → y[x[q]!]! < v
• eq (q : Nat) : left ≤ q → q < right → y[x[q]!]! = v
• gt (q : Nat) : right ≤ q → q < hi → v < y[x[q]!]!

theorem Hex.GraphIso.Nauty.Sparse.Sort.Cuts.right_block {x y out : Array Nat} {lo hi v left b d : Nat} (h : Cuts x y lo hi v lo left b d) (he : ∀ (q : Nat), left ≤ q → q < b → y[x[q]!]! = v) (hs : Blocks out x b (hi - min (d - b) (hi - d)) (min (d - b) (hi - d))) : Separated out y lo hi v left (hi - (d - b))