schema_version = 1
law = "inverse-of"
variant = "InverseOf"
natural_language = "Applying this binary operation to the paired result of another binary operation and the second operand recovers the first operand."
mathematical_statement = "forall a b . f(op(a, b), b) = a"
preconditions = ["f is binary", "op is binary", "op output is valid input to f"]
postcondition = "f(op(a, b), b) == a"
citation = "SPEC.md#algebraic-laws"
[[variables]]
name = "a"
type = "u32"
role = "input"
[[variables]]
name = "b"
type = "u32"
role = "input"
[[parameters]]
name = "op"
type = "op-id"
source = "AlgebraicLaw::InverseOf.op"