Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

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

The replacement map contains the following entries:

nats: empty set
adx: {1}
zeros: empty set
cons: empty set
0: empty set
incr: {1}
s: empty set
hd: {1}
tl: {1}


↳ CSR
  ↳ CSRInnermostProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

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

The replacement map contains the following entries:

nats: empty set
adx: {1}
zeros: empty set
cons: empty set
0: empty set
incr: {1}
s: empty set
hd: {1}
tl: {1}

The CSR is orthogonal. By [10] we can switch to innermost.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

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

The replacement map contains the following entries:

nats: empty set
adx: {1}
zeros: empty set
cons: empty set
0: empty set
incr: {1}
s: empty set
hd: {1}
tl: {1}

Innermost Strategy.

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {adx, incr, hd, tl, ADX, INCR, HD, TL} are replacing on all positions.
The symbols in {cons, s, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

NATS → ADX(zeros)
NATS → ZEROS
ADX(cons(X, Y)) → INCR(cons(X, adx(Y)))

The collapsing dependency pairs are DPc:

HD(cons(X, Y)) → X
TL(cons(X, Y)) → Y


The hidden terms of R are:

zeros
incr(Y)

Every hiding context is built from:

incr on positions {1}
adx on positions {1}

Hence, the new unhiding pairs DPu are :

HD(cons(X, Y)) → U(X)
TL(cons(X, Y)) → U(Y)
U(incr(x_0)) → U(x_0)
U(adx(x_0)) → U(x_0)
U(zeros) → ZEROS
U(incr(Y)) → INCR(Y)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

nats
zeros
incr(cons(x0, x1))
adx(cons(x0, x1))
hd(cons(x0, x1))
tl(cons(x0, x1))


The approximation of the Context-Sensitive Dependency Graph contains 1 SCC with 6 less nodes.


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ QCSDP
              ↳ QCSDPSubtermProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {adx, incr, hd, tl} are replacing on all positions.
The symbols in {cons, s, U} are not replacing on any position.

The TRS P consists of the following rules:

U(incr(x_0)) → U(x_0)
U(adx(x_0)) → U(x_0)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

nats
zeros
incr(cons(x0, x1))
adx(cons(x0, x1))
hd(cons(x0, x1))
tl(cons(x0, x1))


We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


U(incr(x_0)) → U(x_0)
U(adx(x_0)) → U(x_0)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
U(x1)  =  x1

Subterm Order


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ QCSDP
              ↳ QCSDPSubtermProof
                ↳ QCSDP
                  ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {adx, incr, hd, tl} are replacing on all positions.
The symbols in {cons, s} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

nats
zeros
incr(cons(x0, x1))
adx(cons(x0, x1))
hd(cons(x0, x1))
tl(cons(x0, x1))


The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.