schema_version = 1
law = "involution"
variant = "Involution"
natural_language = "Applying the operation twice returns the original value."
mathematical_statement = "forall a . f(f(a)) = a"
preconditions = ["f is unary", "f output is a valid input to f"]
postcondition = "f(f(a)) == a"
citation = "SPEC.md#algebraic-laws"
[[variables]]
name = "a"
type = "u32"
role = "input"