def Hex.GraphIso.Nauty.Sparse.RefineSt.position {n : Nat} (level : Nat) (s : RefineSt n) : Nat

The literal first-ten singleton-preference expression in refineWith. This name is used only to factor its proof; production keeps the inline loop.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.position_lt {n : Nat} (level : Nat) (s : RefineSt n) (h : 0 < s.queue.size) : position level s < s.queue.size

Singleton preference always selects an allocated entry when the queue is nonempty, including its fallback to the last entry.

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Equiv.position {n : Nat} {σ : Renaming n} {level : Nat} {s t : RefineSt n} (h : Equiv σ level s t) : RefineSt.position level s = RefineSt.position level t

The literal preference scan depends only on ordered partition and queue.

def Hex.GraphIso.Nauty.Sparse.RefineSt.selected {n : Nat} (g : Graph n) (level pos : Nat) (s : RefineSt n) : RefineSt n

The literal removal, hashing and splitter dispatch after selecting a queue position. This expression is kept separate only in the proof.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Valid.selected {n : Nat} (G : SparseGraph n) (level pos : Nat) (s : RefineSt n) (h : Valid level s) (hp : pos < s.queue.size) : Valid level (RefineSt.selected (Graph.ofGraph G) level pos s)

An actual selected splitter preserves the full working-state invariant.