def Hex.PermGroup.Search.Witness.ofElementBudgeted {n : Nat} {G : Group n} {test : Perm n → Bool} {budget : Budget} (p : Element G) (hp : test p.val = true) (m : Meter budget) : Measured budget (Witness G test)

Sift once to obtain the chain choices, reserve the exact number of program nodes, then construct the positive certificate in the original generators.

Equations

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