MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { max(nil()) -> 0() , max(cons(x, nil())) -> x , max(cons(x, cons(y, xs))) -> if1(ge(x, y), x, y, xs) , if1(true(), x, y, xs) -> max(cons(x, xs)) , if1(false(), x, y, xs) -> max(cons(y, xs)) , ge(x, 0()) -> true() , ge(0(), s(x)) -> false() , ge(s(x), s(y)) -> ge(x, y) , del(x, nil()) -> nil() , del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs) , if2(true(), x, y, xs) -> xs , if2(false(), x, y, xs) -> cons(y, del(x, xs)) , eq(0(), 0()) -> true() , eq(0(), s(y)) -> false() , eq(s(x), 0()) -> false() , eq(s(x), s(y)) -> eq(x, y) , sort(xs) -> if3(empty(xs), xs) , if3(true(), xs) -> nil() , if3(false(), xs) -> sort(del(max(xs), xs)) , empty(nil()) -> true() , empty(cons(x, xs)) -> false() } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..