(COMMENT harder variant of AG01 4.36) (VAR k m n x y z) (RULES eq(0,0) -> true eq(0,s(m)) -> false eq(s(n),0) -> false eq(s(n),s(m)) -> eq(n,m) le(0,m) -> true le(s(n),0) -> false le(s(n),s(m)) -> le(n,m) min(cons(x,nil)) -> x min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) if_min(true,cons(n,cons(m,x))) -> min(cons(n,x)) if_min(false,cons(n,cons(m,x))) -> min(cons(m,x)) replace(n,m,nil) -> nil replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true,n,m,cons(k,x)) -> cons(m,x) if_replace(false,n,m,cons(k,x)) -> cons(k,replace(n,m,x)) empty(nil) -> true empty(cons(n,x)) -> false head(cons(n,x)) -> n tail(nil) -> nil tail(cons(n,x)) -> x sort(x) -> sortIter(x,nil) sortIter(x,y) -> if(empty(x),x,y,append(y,cons(min(x),nil))) if(true,x,y,z) -> y if(false,x,y,z) -> sortIter(replace(min(x),head(x),tail(x)), z) )