def Hex.PermGroup.Search.Bounded.leaf {n : Nat} {G : Group n} {P : Predicate n} {budget : Budget} (C : Constraint G P) (Q : Tester P budget) (t : Node G) {S : Array (Perm n)} {words : Vector Program S.size} (hs : t.suffix = Chain.leaf S words) (a : Accumulator G P) (m : Meter budget) : Result C t a budget

A leaf predicate is one constraint test. Its membership queries share the sift allowance with coverage checks. Successful leaves are retained even if certificate allocation subsequently exhausts its allowance.

Equations

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