def Hex.PermGroup.Chain.siftBudgeted {n : Nat} {budget : Execution.Budget} (c : Chain n) (base : Nat) (p : Perm n) : Execution.Run budget { result : SiftResult n // result = c.sift base p }

Sift with a reservation before each visited level and each permutation allocation. A missing orbit entry stops immediately, retaining the same result as the ordinary sift. This works on raw chains without assuming their depth.

Equations

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