YES(?,ELEMENTARY) We are left with following problem, upon which TcT provides the certificate YES(?,ELEMENTARY). Strict Trs: { fib(0()) -> 0() , fib(s(0())) -> s(0()) , fib(s(s(x))) -> +(fib(s(x)), fib(x)) } Obligation: innermost runtime complexity Answer: YES(?,ELEMENTARY) The input was oriented with the instance of 'Lightweight Multiset Path Order' as induced by the safe mapping safe(fib) = {}, safe(0) = {}, safe(s) = {1}, safe(+) = {1, 2} and precedence empty . Following symbols are considered recursive: {fib} The recursion depth is 1. For your convenience, here are the satisfied ordering constraints: fib(0();) > 0() fib(s(; 0());) > s(; 0()) fib(s(; s(; x));) > +(; fib(s(; x);), fib(x;)) Hurray, we answered YES(?,ELEMENTARY)