YES(?,PRIMREC) We are left with following problem, upon which TcT provides the certificate YES(?,PRIMREC). Strict Trs: { a__eq(X, Y) -> false() , a__eq(X1, X2) -> eq(X1, X2) , a__eq(0(), 0()) -> true() , a__eq(s(X), s(Y)) -> a__eq(X, Y) , a__inf(X) -> cons(X, inf(s(X))) , a__inf(X) -> inf(X) , a__take(X1, X2) -> take(X1, X2) , a__take(0(), X) -> nil() , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) , a__length(X) -> length(X) , a__length(cons(X, L)) -> s(length(L)) , a__length(nil()) -> 0() , mark(0()) -> 0() , mark(true()) -> true() , mark(s(X)) -> s(X) , mark(false()) -> false() , mark(cons(X1, X2)) -> cons(X1, X2) , mark(inf(X)) -> a__inf(mark(X)) , mark(nil()) -> nil() , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) , mark(length(X)) -> a__length(mark(X)) , mark(eq(X1, X2)) -> a__eq(X1, X2) } Obligation: innermost runtime complexity Answer: YES(?,PRIMREC) The input was oriented with the instance of'multiset path order' as induced by the precedence a__eq > 0, a__eq > s, a__eq > false, a__eq > a__inf, a__eq > cons, a__eq > inf, a__eq > a__take, a__eq > nil, a__eq > take, a__eq > a__length, a__eq > length, a__eq > eq, true > 0, true > s, true > false, true > a__inf, true > cons, true > inf, true > a__take, true > nil, true > take, true > a__length, true > length, true > eq, s > 0, s > false, s > cons, s > inf, s > take, s > length, false > 0, false > cons, false > inf, false > take, false > length, a__inf > 0, a__inf > s, a__inf > false, a__inf > cons, a__inf > inf, a__inf > take, a__inf > length, inf > 0, inf > cons, inf > take, inf > length, a__take > 0, a__take > s, a__take > false, a__take > cons, a__take > inf, a__take > take, a__take > length, nil > s, nil > false, nil > cons, nil > inf, nil > take, nil > length, a__length > 0, a__length > s, a__length > false, a__length > cons, a__length > inf, a__length > take, a__length > length, mark > a__eq, mark > 0, mark > true, mark > s, mark > false, mark > a__inf, mark > cons, mark > inf, mark > a__take, mark > nil, mark > take, mark > a__length, mark > length, mark > eq, eq > 0, eq > s, eq > false, eq > a__inf, eq > cons, eq > inf, eq > a__take, eq > nil, eq > take, eq > a__length, eq > length, a__eq ~ true, 0 ~ cons, 0 ~ take, 0 ~ length, a__inf ~ a__take, a__inf ~ nil, a__inf ~ a__length, cons ~ take, a__take ~ nil, a__take ~ a__length, nil ~ a__length, take ~ length . Hurray, we answered YES(?,PRIMREC)