(from AG01 3.10)
(VAR x y m n)
(RULES
eq(0,0) -> true
eq(0,s(x)) -> false
eq(s(x),0) -> false
eq(s(x),s(y)) -> eq(x,y)
le(0,y) -> true
le(s(x),0) -> false
le(s(x),s(y)) -> le(x,y)
app(nil,y) -> y
app(add(n,x),y) -> add(n,app(x,y))
min(add(n,nil)) -> n
min(add(n,add(m,x))) -> if_min(le(n,m),add(n,add(m,x)))
if_min(true,add(n,add(m,x))) -> min(add(n,x))
if_min(false,add(n,add(m,x))) -> min(add(m,x))
rm(n,nil) -> nil
rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x))
if_rm(true,n,add(m,x)) -> rm(n,x)
if_rm(false,n,add(m,x)) -> add(m,rm(n,x))
minsort(nil,nil) -> nil
minsort(add(n,x),y) -> if_minsort(eq(n,min(add(n,x))),add(n,x),y)
if_minsort(true,add(n,x),y) -> add(n,minsort(app(rm(n,x),y),nil))
if_minsort(false,add(n,x),y) -> minsort(x,add(n,y)))