Showing changes from revision #1 to #2:
Added | Removed | Changed
Definition
Given a decidable setoid set , with a functiondecidable universal quantifier s is adecidable strict order (also called decidable strict total order, decidable strict linear order, or decidable pseudo-order) if it comes with
an identity
representing the irreflexivity condition for the decidable binary relation, where the decidable predicate is defined as
an identity
representing the comparison condition for the binary relation, where the decidable predicate is defined as
an identity
representing the connectedness condition for the binary relation, where the decidable predicate is defined as
an identity
representing the asymmetry condition for the binary relation, where the decidable predicate is defined as
is called a decidable strictly ordered set.
a function is a decidable strict order (also called decidable strict total order, decidable strict linear order, or decidable pseudo-order) if it comes with
an identity
representing the irreflexivity condition for the decidable binary relation, where the decidable predicate
an identity
representing the comparison condition for the binary relation, where the decidable predicate
an identity
representing the connectedness condition for the binary relation, where the decidable predicate
an identity
representing the asymmetry condition for the binary relation, where the decidable predicate