TRS: { nats() -> adx(zeros()), zeros() -> cons(0(), zeros()), incr(cons(X, Y)) -> cons(s(X), incr(Y)), adx(cons(X, Y)) -> incr(cons(X, adx(Y))), hd(cons(X, Y)) -> X, tl(cons(X, Y)) -> Y} Fail