YES(?,PRIMREC) We are left with following problem, upon which TcT provides the certificate YES(?,PRIMREC). 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(?,PRIMREC) The input was oriented with the instance of'multiset path order' as induced by the precedence nil > app, nil > cons, from > app, from > cons, zWadr > app, zWadr > cons, prefix > app, prefix > cons, nil ~ from, nil ~ zWadr, nil ~ prefix, from ~ zWadr, from ~ prefix, zWadr ~ prefix . Hurray, we answered YES(?,PRIMREC)