Note: The word status and the <status> can be abbreviated.<status-constraint> ::= status <status> <operator>+[,] <status> ::= left-to-right | right-to-left | multiset
status left-to-right f, g status multiset +
The left-to-right and right-to-left statuses are called lexicographic statuses. The assign more weight, respectively, to the leftmost or rightmost arguments of an operator. They are useful when orienting the associativity equation f(f(x,y),z) = f(x,f(y,z)). If f has left-to-right, this equation would be oriented from left to right. If f has right-to-left status, it would be would be oriented from right to left.
The multiset status is appropriate for ac and commutative operators, because it gives all arguments equal weight.
The dsmpos ordering is defined on terms containing an operator without a defined status if the ordering would produce the same results no matter what status was given to that operator. This property allows LP or the user to define the status of an operator without invalidating the proof of termination for previously oriented rewrite rules.