def Hex.GraphIso.Nauty.Sparse.produceNode {n : Nat} (G : SparseGraph n) (tcLevel : Nat) : Nat → Nat → Array Nat → Array Nat → VSet n → Nat → Key n → CertNode

Expand a native proof subtree against a supplied key, discarding nodes whose recomputed code is strictly smaller. The optimized canonical search supplies the key; this traversal produces proof records, not a new maximum.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.Sparse.produceNode G tcLevel 0 x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ = Hex.GraphIso.Nauty.Sparse.CertNode.leaf