MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { g(x, 0()) -> 0() , g(d(), s(x)) -> s(s(g(d(), x))) , g(h(), s(0())) -> 0() , g(h(), s(s(x))) -> s(g(h(), x)) , double(x) -> g(d(), x) , half(x) -> g(h(), x) , f(s(x), y) -> f(half(s(x)), double(y)) , f(s(0()), y) -> y , id(x) -> f(x, s(0())) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..