(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(X)
activate(n__adx(X)) → adx(X)
activate(X) → X
Q is empty.
(1) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(2) Obligation:
Q DP problem:
The TRS P consists of the following rules:
NATS → ADX(zeros)
NATS → ZEROS
INCR(cons(X, Y)) → ACTIVATE(X)
INCR(cons(X, Y)) → ACTIVATE(Y)
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
ADX(cons(X, Y)) → ACTIVATE(X)
ADX(cons(X, Y)) → ACTIVATE(Y)
HD(cons(X, Y)) → ACTIVATE(X)
TL(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__0) → 01
ACTIVATE(n__zeros) → ZEROS
ACTIVATE(n__s(X)) → S(X)
ACTIVATE(n__incr(X)) → INCR(X)
ACTIVATE(n__adx(X)) → ADX(X)
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(X)
activate(n__adx(X)) → adx(X)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(3) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 7 less nodes.
(4) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ACTIVATE(n__incr(X)) → INCR(X)
INCR(cons(X, Y)) → ACTIVATE(X)
ACTIVATE(n__adx(X)) → ADX(X)
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
INCR(cons(X, Y)) → ACTIVATE(Y)
ADX(cons(X, Y)) → ACTIVATE(X)
ADX(cons(X, Y)) → ACTIVATE(Y)
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(X)
activate(n__adx(X)) → adx(X)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.