MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { nats() -> cons(0(), n__incr(n__nats())) , nats() -> n__nats() , pairs() -> cons(0(), n__incr(n__odds())) , odds() -> n__odds() , odds() -> incr(pairs()) , incr(X) -> n__incr(X) , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) , activate(X) -> X , activate(n__incr(X)) -> incr(activate(X)) , activate(n__nats()) -> nats() , activate(n__odds()) -> odds() , head(cons(X, XS)) -> X , tail(cons(X, XS)) -> activate(XS) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..