TRS: { nats() -> adx(zeros()), zeros() -> cons(n__0(), n__zeros()), incr(cons(X, Y)) -> cons(n__s(activate(X)), n__incr(activate(Y))), adx(cons(X, Y)) -> incr(cons(activate(X), n__adx(activate(Y)))), hd(cons(X, Y)) -> activate(X), tl(cons(X, Y)) -> activate(Y), 0() -> n__0(), zeros() -> n__zeros(), s(X) -> n__s(X), incr(X) -> n__incr(X), adx(X) -> n__adx(X), activate(n__0()) -> 0(), activate(n__zeros()) -> zeros(), activate(n__s(X)) -> s(X), activate(n__incr(X)) -> incr(activate(X)), activate(n__adx(X)) -> adx(activate(X)), activate(X) -> X} Fail