theorem Hex.GraphIso.Nauty.Sparse.segN_extract (lab : Array Nat) (lo len : Nat) (hb : lo + len ≤ lab.size) : segN lab lo len = (lab.extract lo (lo + len)).toList

theorem Hex.GraphIso.Nauty.Sparse.splitCounts_segment {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) (hf : first ≤ s.cellend[first]!) (hb : s.cellend[first]! < s.lab.size) : ((splitCounts level first distance s).lab.extract first (s.cellend[first]! + 1)).toList.Perm (s.lab.extract first (s.cellend[first]! + 1)).toList

The cell's multiset of vertices survives its executed count split.

theorem Hex.GraphIso.Nauty.Sparse.splitCounts_cells {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) (hf : first ≤ s.cellend[first]!) (hb : s.cellend[first]! < s.lab.size) (hc : IsCell s.ptn level first (s.cellend[first]! + 1 - first)) : cellsPerm s.ptn level (splitCounts level first distance s).lab s.lab

Count splitting preserves the contents of every old partition cell. The refined cells can be treated as subdivisions of the original cell.