schema_version = 1
law = "monotonic"
variant = "Monotonic"
natural_language = "The operation preserves or reverses order according to its declared monotonic direction."
mathematical_statement = "forall a b . a <= b implies direction(f(a), f(b))"
preconditions = ["f is unary", "direction is declared", "a and b are ordered U32 values"]
postcondition = "direction == NonDecreasing => f(a) <= f(b); direction == NonIncreasing => f(a) >= f(b)"
citation = "SPEC.md#algebraic-laws"
[[variables]]
name = "a"
type = "u32"
role = "input"
[[variables]]
name = "b"
type = "u32"
role = "input"
[[parameters]]
name = "direction"
type = "MonotonicDirection"
source = "AlgebraicLaw::Monotonic.direction"