Termination proof of /tmp/tmpBu0TrB/Ex2

Termination of the following Term Rewriting System could be proven:

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

fst(0, Z) → nil
fst(s(X), cons(Y, Z)) → cons(Y, fst(X, Z))
from(X) → cons(X, from(s(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
len(nil) → 0
len(cons(X, Z)) → s(len(Z))

The replacement map contains the following entries:

fst: {1, 2}
0: empty set
nil: empty set
s: empty set
cons: {1}
from: {1}
add: {1, 2}
len: {1}

↳ CSR

  ↳ CSRInnermostProof

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

fst(0, Z) → nil
fst(s(X), cons(Y, Z)) → cons(Y, fst(X, Z))
from(X) → cons(X, from(s(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
len(nil) → 0
len(cons(X, Z)) → s(len(Z))

The replacement map contains the following entries:

fst: {1, 2}
0: empty set
nil: empty set
s: empty set
cons: {1}
from: {1}
add: {1, 2}
len: {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:

fst(0, Z) → nil
fst(s(X), cons(Y, Z)) → cons(Y, fst(X, Z))
from(X) → cons(X, from(s(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
len(nil) → 0
len(cons(X, Z)) → s(len(Z))

The replacement map contains the following entries:

fst: {1, 2}
0: empty set
nil: empty set
s: empty set
cons: {1}
from: {1}
add: {1, 2}
len: {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 {fst, from, add, len, FST, FROM, ADD, LEN} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {s, U} are not replacing on any position.

The hidden terms of R are:

fst(X, Z)
from(s(X))
add(X, Y)
len(Z)

Every hiding context is built from:

fst on positions {1, 2}
add on positions {1, 2}
len on positions {1}

Hence, the new unhiding pairs DP_u are :

U(fst(x_0, x_1)) → U(x_0)
U(fst(x_0, x_1)) → U(x_1)
U(add(x_0, x_1)) → U(x_0)
U(add(x_0, x_1)) → U(x_1)
U(len(x_0)) → U(x_0)
U(fst(X, Z)) → FST(X, Z)
U(from(s(X))) → FROM(s(X))
U(add(X, Y)) → ADD(X, Y)
U(len(Z)) → LEN(Z)

The TRS R consists of the following rules:

fst(0, Z) → nil
fst(s(X), cons(Y, Z)) → cons(Y, fst(X, Z))
from(X) → cons(X, from(s(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
len(nil) → 0
len(cons(X, Z)) → s(len(Z))

The set Q consists of the following terms:

fst(0, x0)
fst(s(x0), cons(x1, x2))
from(x0)
add(0, x0)
add(s(x0), x1)
len(nil)
len(cons(x0, x1))

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

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ QCSDP

              ↳ QCSDPSubtermProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {fst, from, add, len} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {s, U} are not replacing on any position.

The TRS P consists of the following rules:

U(fst(x_0, x_1)) → U(x_0)
U(fst(x_0, x_1)) → U(x_1)
U(add(x_0, x_1)) → U(x_0)
U(add(x_0, x_1)) → U(x_1)
U(len(x_0)) → U(x_0)

The TRS R consists of the following rules:

fst(0, Z) → nil
fst(s(X), cons(Y, Z)) → cons(Y, fst(X, Z))
from(X) → cons(X, from(s(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
len(nil) → 0
len(cons(X, Z)) → s(len(Z))

The set Q consists of the following terms:

fst(0, x0)
fst(s(x0), cons(x1, x2))
from(x0)
add(0, x0)
add(s(x0), x1)
len(nil)
len(cons(x0, x1))

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

U(fst(x_0, x_1)) → U(x_0)
U(fst(x_0, x_1)) → U(x_1)
U(add(x_0, x_1)) → U(x_0)
U(add(x_0, x_1)) → U(x_1)
U(len(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 {fst, from, add, len} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {s} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

fst(0, Z) → nil
fst(s(X), cons(Y, Z)) → cons(Y, fst(X, Z))
from(X) → cons(X, from(s(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
len(nil) → 0
len(cons(X, Z)) → s(len(Z))

The set Q consists of the following terms:

fst(0, x0)
fst(s(x0), cons(x1, x2))
from(x0)
add(0, x0)
add(s(x0), x1)
len(nil)
len(cons(x0, x1))

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