(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
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
Q is empty.