YES(?,O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(?,O(n^2)). Strict Trs: { app(nil(), YS) -> YS , app(cons(X), YS) -> cons(X) , from(X) -> cons(X) , zWadr(XS, nil()) -> nil() , zWadr(nil(), YS) -> nil() , zWadr(cons(X), cons(Y)) -> cons(app(Y, cons(X))) , prefix(L) -> cons(nil()) } Obligation: innermost runtime complexity Answer: YES(?,O(n^2)) The input was oriented with the instance of 'Small Polynomial Path Order (PS)' as induced by the safe mapping safe(app) = {1, 2}, safe(nil) = {}, safe(cons) = {1}, safe(from) = {}, safe(zWadr) = {1, 2}, safe(prefix) = {1} and precedence app > from, zWadr > app, zWadr > from, zWadr > prefix, prefix > from, app ~ prefix . Following symbols are considered recursive: {app, zWadr} The recursion depth is 2. For your convenience, here are the satisfied ordering constraints: app(; nil(), YS) > YS app(; cons(; X), YS) > cons(; X) from(X;) > cons(; X) zWadr(; XS, nil()) > nil() zWadr(; nil(), YS) > nil() zWadr(; cons(; X), cons(; Y)) > cons(; app(; Y, cons(; X))) prefix(; L) > cons(; nil()) Hurray, we answered YES(?,O(n^2))