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 ( S , < S ) is a partial order, and let M ( S ) be the set of all finite multisets on S . For multisets M , N ∈ M ( S ) we define the Dershowitz–Manna ordering M < D M N as follows:
M < D M N whenever there exist two multisets X , Y ∈ M ( S ) with the following properties:
X ≠ ∅ , X ⊆ N , M = ( N − X ) + Y , and X dominates Y , that is, for all y ∈ Y , there is some x ∈ X such that y < S x .An equivalent definition was given by Huet and Oppen as follows:
M < D M N if and only if
M ≠ N , andfor all y in S , if M ( y ) > N ( y ) then there is some x in S such that y < S x and M ( x ) < N ( x ) .