@[irreducible]

def Hex.PermGroup.Search.Certificate.nodes {Reason : Type} (certificate : Certificate Reason) : Nat

Number of nodes in a completeness certificate, including its root.

Equations

• (Hex.PermGroup.Search.Certificate.branch children).nodes = 1 + (List.map Hex.PermGroup.Search.Certificate.nodes children.toList).sum
• (Hex.PermGroup.Search.Certificate.rejected reason).nodes = 1
• Hex.PermGroup.Search.Certificate.covered.nodes = 1
• Hex.PermGroup.Search.Certificate.leaf.nodes = 1