theorem Hex.GraphIso.Nauty.Sparse.CountSort.minima_valid (lab hits : Array Nat) (cap first last begin : Nat) (hf : first < begin) (he : begin ≤ last) (hb : last ≤ lab.size) (hk : ∀ (q : Nat), first ≤ q → q < last → hits[lab[q]!]! < cap) (hu : ∀ (q : Nat), first ≤ q → q < begin → hits[lab[q]!]! = hits[lab[first]!]!) : have r := minima lab hits cap first last begin; Minima.Permuted lab r.snd.snd.snd.snd hits first last r.snd.fst r.snd.snd.snd.fst last r.fst r.snd.snd.fst cap

Count insertion preserves the cell's vertices, its bounded counts, and the sentinel for an empty second fragment.

theorem Hex.GraphIso.Nauty.Sparse.splitCounts_induct {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) (P : RefineSt n → Prop) (hf : first ≤ s.cellend[first]!) (hb : s.cellend[first]! < s.lab.size) (hk : ∀ (q : Nat), first ≤ q → q ≤ s.cellend[first]! → s.hits[s.lab[q]!]! < n + 2) (uniform : (∀ (q : Nat), first ≤ q → q ≤ s.cellend[first]! → s.hits[s.lab[q]!]! = s.hits[s.lab[first]!]!) → P (s.hash first)) (finish : ∀ (lab : Array Nat) (w1 v2 w2 v3 : Nat), Minima.Permuted s.lab lab s.hits first (s.cellend[first]! + 1) v2 v3 (s.cellend[first]! + 1) w1 w2 (n + 2) → P (CountSort.finish level first (s.cellend[first]! + 1) distance (have __src := s.hash first; { lab := lab, ptn := __src.ptn, active := __src.active, queue := __src.queue, cellstart := __src.cellstart, cellend := __src.cellend, indexed := __src.indexed, hits := __src.hits, marks := __src.marks, vmarks := __src.vmarks, stamp := __src.stamp, numcells := __src.numcells, longcode := __src.longcode }) w1 v2 w2 v3)) : P (splitCounts level first distance s)

Prove a property of count splitting from its uniform-cell return and fragment installation. The latter receives the verified insertion result.