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