Multiset Ordering; A Theorem of Manna and Dershowitz

This note gives an elementary proof of a result, due to Manna and Der-showitz [1], on well-foundedness of an order relation over multisets (henceforth, called bags). Manna-Dershowitz Order Let (D,<) be a well-founded set. For finite bags X and Y over D define Y ≺ X ≡ 〈(A 6 = φ ∧ (∀y: y ∈ B: 〈∃x: x ∈ A: y < x〉)〉, where A = X − Y and B = Y −X. We may imagine that Y is constructed from X by removing the elements in A and adding the elements in B. It is required that some element be removed (A 6 = φ) and each element that is added be smaller than some removed element according to <. We show that finite bags are well-founded under the ≺ relation. Proof that ≺ is a well-founded relation Given a finite non-empty bag, a move removes a non-empty finite bag of elements from it and adds a finite bag of elements where for each added element y there is a removed element x such that y < x. A game a is a sequence of moves until the bag becomes empty; the