MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { r(xs, ys, zs, nil()) -> xs , r(xs, nil(), zs, cons(w, ws)) -> r(xs, xs, cons(succ(zero()), zs), ws) , r(xs, cons(y, ys), nil(), cons(w, ws)) -> r(xs, xs, cons(succ(zero()), nil()), ws) , r(xs, cons(y, ys), cons(z, zs), cons(w, ws)) -> r(ys, cons(y, ys), zs, cons(succ(zero()), cons(w, ws))) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..