The *multiset ordering* over the set `S`

is the transitive closure
of a relation `P`

on the collection of finite multisets over `S`

.
If `R`

is a partial ordering
on `S`

then `aPb`

if and only if for some `x∈D(b)`

:

`a(x)=b(x)-1`

`wRx⇒a(w)≥b(w)`

`(¬wRx∧¬w=x)⇒a(w)=b(w)`

So, if we have a multiset `b`

and we replace some element `x∈D(b)`

with occurrences of elements
`x`

such that _{0},...,x_{n}`0≤i≤n x`

to give the
multiset _{i}Rx`a`

, then `aPb`

.

The multiset ordering over a well-founded ordering is well-founded.

Doets, Kees. *From Logic to Logic Programming.* MIT Press, 1994.

Copyright © 2014 Barry Watson. All rights reserved.