structure Hex.GraphIso.Nauty.Sparse.CountFrame {n : Nat} (s t : RefineSt n) : Prop

Storage unaffected by dividing a cell using already computed counts. The label, partition, and index contents may change, but keep their allocation.

• lab_size : t.lab.size = s.lab.size
• ptn_size : t.ptn.size = s.ptn.size
• starts_size : t.cellstart.size = s.cellstart.size
• ends_size : t.cellend.size = s.cellend.size
• hits : t.hits = s.hits
• marks : t.marks = s.marks
• vmarks : t.vmarks = s.vmarks
• stamp : t.stamp = s.stamp
• indexed : t.indexed = s.indexed

theorem Hex.GraphIso.Nauty.Sparse.splitCounts_frame {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) : CountFrame s (splitCounts level first distance s)

All branches of the actual count splitter retain their count and mark arrays, generation, cache flag, and label/partition/index allocations.