schema_version = 1
law = "lattice-absorption"
variant = "LatticeAbsorption"
natural_language = "A lattice operation absorbs the result of its dual operation."
mathematical_statement = "forall a b . f(a, dual_op(a, b)) = a"
preconditions = ["f and dual_op are binary", "both operations share the same lattice domain"]
postcondition = "f(a, dual_op(a, b)) == a"
citation = "SPEC.md#algebraic-laws"
[[variables]]
name = "a"
type = "u32"
role = "input"
[[variables]]
name = "b"
type = "u32"
role = "input"
[[parameters]]
name = "dual_op"
type = "op-id"
source = "AlgebraicLaw::LatticeAbsorption.dual_op"