(GOAL COMPLEXITY) (STARTTERM CONSTRUCTOR-BASED) (STRATEGY INNERMOST) (STRATEGY INNERMOST) (VAR x y z) (DATATYPES A = µX.< nil, .(X, X), if(X, X, X), <=(X, X), =(X, X) >) (SIGNATURES msort :: [A] -> A min :: [A x A] -> A del :: [A x A] -> A) (RULES msort(nil()) -> nil() msort(.(x,y)) -> .(min(x,y) ,msort(del(min(x,y),.(x,y)))) min(x,nil()) -> x min(x,.(y,z)) -> if(<=(x,y) ,min(x,z) ,min(y,z)) del(x,nil()) -> nil() del(x,.(y,z)) -> if(=(x,y) ,z ,.(y,del(x,z))))