def Hex.GraphIso.Nauty.Sparse.CountSort.firstRun (lab hits : Array Nat) (first last : Nat) : Nat

Equations

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

def Hex.GraphIso.Nauty.Sparse.CountSort.minima (lab hits : Array Nat) (cap first last begin : Nat) : Nat × Nat × Nat × Nat × Array Nat

Equations

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

def Hex.GraphIso.Nauty.Sparse.CountSort.finish {n : Nat} (level first last : Nat) (distance : Bool) (s : RefineSt n) (w1 v2 w2 v3 : Nat) : RefineSt n

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.splitCounts_parts {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) : splitCounts level first distance s = have last := s.cellend[first]! + 1; have r := s.hash first; have v2 := CountSort.firstRun s.lab s.hits first last; if (v2 == last) = true then r else have m := CountSort.minima s.lab s.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.