The multiset ordering over the set
S is the transitive closure
of a relation
P on the collection of finite multisets over
R is a partial ordering
aPb if and only if for some
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
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.