Given a decidable 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 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