schema_version = 1
law = "associative"
variant = "Associative"
natural_language = "Grouping does not change the result of a binary operation."
mathematical_statement = "forall a b c . f(f(a, b), c) = f(a, f(b, c))"
preconditions = ["f is binary", "intermediate results are valid inputs to f"]
postcondition = "f(f(a, b), c) == f(a, f(b, c))"
citation = "SPEC.md#algebraic-laws"
[[variables]]
name = "a"
type = "u32"
role = "input"
[[variables]]
name = "b"
type = "u32"
role = "input"
[[variables]]
name = "c"
type = "u32"
role = "input"