Multiset Ordering

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 x0,...,xn such that 0≤i≤n xiRx to give the multiset a, then aPb.

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

References

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