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