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 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.