theorem
Hex.GraphIso.Nauty.Sparse.splitCounts_parts
{n : Nat}
(level first : Nat)
(distance : Bool)
(s : RefineSt n)
:
splitCounts level first distance s = have lab := s.lab;
have hits := s.hits;
have last := s.cellend[first]! + 1;
have r := s.hash first;
have v2 := CountSort.firstRun lab hits first last;
if (v2 == last) = true then r
else have m := CountSort.minima lab hits (n + 2) first last v2;
CountSort.finish level first last distance
{ lab := m.snd.snd.snd.snd, ptn := r.ptn, active := r.active, queue := r.queue, cellstart := r.cellstart,
cellend := r.cellend, indexed := r.indexed, hits := r.hits, marks := r.marks, vmarks := r.vmarks,
stamp := r.stamp, numcells := r.numcells, longcode := r.longcode }
m.fst m.snd.fst m.snd.snd.fst m.snd.snd.snd.fst
The named count-sort blocks are literally the executed splitter.