In mathematics, the Dershowitz–Manna ordering is a well-founded ordering on multisets named after Nachum Dershowitz and Zohar Manna. It is often used in context of termination of programs or term rewriting systems.
Suppose that is a well-founded partial order and let be the set of all finite multisets on . For multisets we define the Dershowitz–Manna ordering as follows:
whenever there exist two multisets with the following properties: , , , and dominates , that is, for all , there is some such that .
An equivalent definition was given by Huet and Oppen as follows:
if and only if , and for all in , if then there is some in such that and .
References . (Also in Proceedings of the International Colloquium on Automata, Languages and Programming, Graz, Lecture Notes in Computer Science 71, Springer-Verlag, pp. 188–202 [July 1979].) . .