theorem
Hex.GraphIso.Nauty.Sparse.CountSort.finish_window
{n : Nat}
(level first last : Nat)
(distance : Bool)
(s : RefineSt n)
(w1 v2 w2 v3 : Nat)
(old : Array Nat)
(h : «Sort».Window old s.lab first last)
(hf : first ≤ v3)
(he : v3 ≤ last)
(hb : last ≤ s.lab.size)
:
«Sort».Window old (finish level first last distance s w1 v2 w2 v3).lab first last
Installing fragments preserves the original cell's vertex multiset and its exterior. The indirect sort stays inside the larger-count tail.
theorem
Hex.GraphIso.Nauty.Sparse.splitCounts_window
{n : Nat}
(level first : Nat)
(distance : Bool)
(s : RefineSt n)
(hf : first ≤ s.cellend[first]!)
(hb : s.cellend[first]! < s.lab.size)
:
«Sort».Window s.lab (splitCounts level first distance s).lab first (s.cellend[first]! + 1)
Count splitting permutes exactly the selected cell and retains every label outside it, without requiring bounds on the count values.