schema_version = 1
law = "de-morgan"
variant = "DeMorgan"
natural_language = "Applying the unary operation to the inner binary operation equals applying the dual operation to each unary result."
mathematical_statement = "forall a b . f(inner_op(a, b)) = dual_op(f(a), f(b))"
preconditions = ["f is unary", "inner_op and dual_op are defined on the same Boolean or bitwise domain"]
postcondition = "f(inner_op(a, b)) == dual_op(f(a), f(b))"
citation = "SPEC.md#algebraic-laws"
[[variables]]
name = "a"
type = "u32"
role = "input"
[[variables]]
name = "b"
type = "u32"
role = "input"
[[parameters]]
name = "inner_op"
type = "op-id"
source = "AlgebraicLaw::DeMorgan.inner_op"
[[parameters]]
name = "dual_op"
type = "op-id"
source = "AlgebraicLaw::DeMorgan.dual_op"