Extension functions for multiset orderings (Q1104349)

A multiset or bag on a set S is an unordered sequence of elements of S. \textit{N. Dershowitz} and \textit{Z. Manna} showed [Commun. ACM 22, 465-476 (1979; Zbl 0431.68016)] how to construct an ordering \(\gg\) on \({\mathcal M}(S)\), the set of multisets in S, from any ordering \(>\) on the underlying set S. This order, which we shall call the standard multiset ordering, has proved particularly useful in proofs of program termination and in constructing orderings which prove the termination of term- rewriting systems. In this paper we shall construct many other orderings on multisets which reflect the ordering on S, and share the usual properties of multiset orderings.