MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { app(l, nil()) -> l , app(nil(), k) -> k , app(cons(x, l), k) -> cons(x, app(l, k)) , sum(cons(x, nil())) -> cons(x, nil()) , sum(cons(x, cons(y, l))) -> sum(cons(a(x, y, h()), l)) , a(x, s(y), h()) -> a(x, y, s(h())) , a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z)) , a(h(), h(), x) -> s(x) , a(s(x), h(), z) -> a(x, z, z) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..