Dershowitz–Manna ordering
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 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.
