The dsmpos ordering computes complete sets of minimal extensions to LP's registry when necessary to orient a formula. The noeq-dsmpos is the same ordering, except that it does not suggest assigning equal heights to two operators; as a result, it is faster, but less powerful than dsmpos.
Let s and t be two terms, with s = f(s1, ..., sm) and t = g(t1, ..., tn). Then s >= t in the dsmpos ordering iff
The dsmpos ordering is based on the recursive path ordering with status due to Dershowitz, Kamin, and Levy. The definition of the ordering >= is due to Forgaard. The generation of suggestions is due to Detlefs and Forgaard.
LP uses the following modification of the dsmpos ordering to orient equations that contain quantifiers. It replaces each quantifier (over a sort S) in an equation by a pseudo-operator with signature S, Bool -> Bool, and it replaces each bound variable by the constant true; in this way, it converts each subterm of the form \E x P(x) or \A x P(x) in an equation into a subterm \E(true, P(true)) or \A(true, P(true)). (In general, the resulting term does not sort check.) Then LP tries to orient the transformed equation with the aid of registry suggestions for the pseudo-operators. It it succeeds, it orients the original equation in the same direction as its transformation.