MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { 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(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x))) , min(cons(x, nil())) -> 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, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)) , replace(n, m, nil()) -> nil() , 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(cons(n, x)) -> false() , empty(nil()) -> true() , head(cons(n, x)) -> n , tail(cons(n, x)) -> x , tail(nil()) -> nil() , 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) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..