(VAR x y z v w)
(RULES
sort(nil()) -> nil()
sort(cons(x,y)) -> insert(x,sort(y))
insert(x,nil()) -> cons(x,nil())
insert(x,cons(v,w)) -> choose(x,cons(v,w),x,v)
choose(x,cons(v,w),y,0) -> cons(x,cons(v,w))
choose(x,cons(v,w),0,s(z)) -> cons(v,insert(x,w))
choose(x,cons(v,w),s(y),s(z)) -> choose(x,cons(v,w),y,z)
)
(COMMENT Example 32 in \cite{D33})