schema_version = 1
law = "trichotomy"
variant = "Trichotomy"
natural_language = "Exactly one of less-than, equality, or greater-than holds for any ordered pair."
mathematical_statement = "forall a b . exactly_one(less_op(a,b), equal_op(a,b), greater_op(a,b))"
preconditions = ["less_op, equal_op, and greater_op share the same ordered domain"]
postcondition = "one_true(less_op(a, b), equal_op(a, b), greater_op(a, b))"
citation = "SPEC.md#algebraic-laws"
[[variables]]
name = "a"
type = "u32"
role = "input"
[[variables]]
name = "b"
type = "u32"
role = "input"
[[parameters]]
name = "less_op"
type = "op-id"
source = "AlgebraicLaw::Trichotomy.less_op"
[[parameters]]
name = "equal_op"
type = "op-id"
source = "AlgebraicLaw::Trichotomy.equal_op"
[[parameters]]
name = "greater_op"
type = "op-id"
source = "AlgebraicLaw::Trichotomy.greater_op"