The use of multiset ordering in proving termination

Based on the definition of a multiset and the information in this paper, why do we use multisets in proving the termination of a program? Is not the well-founded order enough?

• Doesn't the abstract already answer your question? – Juho Jan 20 '13 at 4:48
• @Juho, NO! He does not – M.M Jan 20 '13 at 13:05
• Have you read the paper? If multisets are unnecessary, you should be able to do everything they do without them. I expect, though, that they include an example showing off their method. – Raphael Jan 21 '13 at 10:52

As I understand the paper (and I was not familiar with it before) to prove termination of a program using the method of Floyd it is enough to find a function $\tau$ that maps the states of the program into some well-founded set $(S,\prec)$ such that this function is consistent with the program steps. Here consistency means that if a state $s$ follows $s^\prime$, then $\tau(s^\prime)\prec \tau(s)$.
Prior to Manna and Dershowitz the method of Floyd was used by mapping the states into the set of natural numbers or into the set of $n$-tuples thereof with lexicographic ordering (both sets are well-founded). The authors suggest a new source of well-founded sets for the Floyd method, that is the set of multisets of finite structures with multiset ordering and show how this can simplify termination proofs.
Note also that contrary to the sets of natural numbers and lexicographically ordered $n$-tuples, multisets ordering is only a partial ordering.