Anti-checker shrink rounds -- definitions

This layer records a sequence of samples built by repeatedly consing a valid survivor-shrinking input onto the prefix already constructed.

def Complexity.AntiChecker.IsShrinkTrace {arity : ℕ} (denominator : ℕ) (target : BitString arity → Bool) (threshold : ℕ) : List (BitString arity) → Prop

Every input in the list, read from tail to head, satisfies the requested shrink contract relative to the prefix constructed before it.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.AntiChecker.IsShrinkTrace denominator target threshold [] = True