schema_version = 1
law = "commutative"
variant = "Commutative"
natural_language = "Swapping binary operands does not change the result."
mathematical_statement = "forall a b . f(a, b) = f(b, a)"
preconditions = ["f is binary", "a and b are valid U32 inputs"]
postcondition = "f(a, b) == f(b, a)"
citation = "SPEC.md#algebraic-laws"
[[variables]]
name = "a"
type = "u32"
role = "input"
[[variables]]
name = "b"
type = "u32"
role = "input"