schema_version = 1
law = "complement"
variant = "Complement"
natural_language = "Combining a value with its complement yields the declared universe."
mathematical_statement = "forall a . f(a, complement_op(a)) = universe"
preconditions = ["f is binary or checked as a unary complement relation", "complement_op is defined on the same domain"]
postcondition = "f(a, complement_op(a)) == universe"
citation = "SPEC.md#algebraic-laws"
[[variables]]
name = "a"
type = "u32"
role = "input"
[[parameters]]
name = "complement_op"
type = "op-id"
source = "AlgebraicLaw::Complement.complement_op"
[[parameters]]
name = "universe"
type = "u32"
source = "AlgebraicLaw::Complement.universe"