schema_version = 1
law = "absorbing"
variant = "Absorbing"
natural_language = "An absorbing element z returns z when used on either side of the operation."
mathematical_statement = "forall a . f(a, z) = z and f(z, a) = z"
preconditions = ["f is binary", "z is the declared absorbing element"]
postcondition = "f(a, z) == z && f(z, a) == z"
citation = "SPEC.md#algebraic-laws"
[[variables]]
name = "a"
type = "u32"
role = "input"
[[parameters]]
name = "z"
type = "u32"
source = "AlgebraicLaw::Absorbing.element"