schema_version = 1
law = "distributive"
variant = "DistributiveOver"
natural_language = "Applying an operation over a combined input equals combining the separately applied results."
mathematical_statement = "forall a b c . f(a, over_op(b, c)) = over_op(f(a, b), f(a, c))"
preconditions = ["f and over_op are binary", "both operations share the same domain"]
postcondition = "f(a, over_op(b, c)) == over_op(f(a, b), f(a, 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"
[[parameters]]
name = "over_op"
type = "op-id"
source = "AlgebraicLaw::DistributiveOver.over_op"