[Solved]: The use of multiset ordering in proving termination

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.