schema_version = 1
law = "identity"
variant = "Identity"
natural_language = "The identity element leaves every value unchanged on either side."
mathematical_statement = "forall a . f(a, e) = a and f(e, a) = a"
preconditions = ["f is binary", "e is the declared identity element"]
postcondition = "f(a, e) == a && f(e, a) == a"
citation = "SPEC.md#algebraic-laws"
[[variables]]
name = "a"
type = "u32"
role = "input"
[[parameters]]
name = "e"
type = "u32"
source = "AlgebraicLaw::Identity.element"