def Hex.GraphIso.Nauty.Sparse.Literal.distvals {n : Nat} (g : Graph n) (root : Nat) : Array Nat

Equations

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

def Hex.GraphIso.Nauty.Sparse.Literal.indexCells (n : Nat) (lab ptn : Array Nat) (level : Nat) (starts ends : Array Nat) : Array Nat × Array Nat

Equations

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

def Hex.GraphIso.Nauty.Sparse.Literal.splitCounts {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) : RefineSt n

Divide one cell by counts or distances. The first two minimum fragments use nauty's three-way insertion; later fragments use its exact indirect sort. distance selects the distinct distance-branch code updates.

Equations

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

def Hex.GraphIso.Nauty.Sparse.Literal.splitSingleton {n : Nat} (g : Graph n) (level split : Nat) (s : RefineSt n) : RefineSt n

A singleton splitter: untouched vertices keep their order and touched vertices are written in reverse order, as in HITS[--k].

Equations

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

def Hex.GraphIso.Nauty.Sparse.Literal.splitNontrivial {n : Nat} (g : Graph n) (level split : Nat) (s : RefineSt n) : RefineSt n

Count only vertices in touched nontrivial cells. Rows of hits are cleared on first touch, without a full vertex scan for each splitter.

Equations

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

def Hex.GraphIso.Nauty.Sparse.Literal.refineWith {n : Nat} (g : Graph n) (level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (scratch : Scratch) : RefineSt n

refine_sg, including its shallow distance split and preference for singleton splitters among the first ten active entries.

Equations

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

def Hex.GraphIso.Nauty.Sparse.Literal.refine {n : Nat} (g : Graph n) (level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) : RefineSt n

Standalone refinement with freshly initialized scratch storage.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Literal.distvals_eq : @distvals = @Sparse.distvals

theorem Hex.GraphIso.Nauty.Sparse.Literal.indexCells_eq : indexCells = Sparse.indexCells

theorem Hex.GraphIso.Nauty.Sparse.Literal.splitCounts_eq : @splitCounts = @Sparse.splitCounts

theorem Hex.GraphIso.Nauty.Sparse.Literal.splitSingleton_eq : @splitSingleton = @Sparse.splitSingleton

theorem Hex.GraphIso.Nauty.Sparse.Literal.splitNontrivial_eq : @splitNontrivial = @Sparse.splitNontrivial

theorem Hex.GraphIso.Nauty.Sparse.Literal.refineWith_eq : @refineWith = @Sparse.refineWith

theorem Hex.GraphIso.Nauty.Sparse.Literal.refine_eq : @refine = @Sparse.refine