Termination proof of /tmp/tmp53NGzr/Ex1_2

Termination of the following Term Rewriting System could be proven:

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

from(X) → cons(X, from(s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, Z))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, Z))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)

The replacement map contains the following entries:

from: {1}
cons: {1}
s: {1}
2ndspos: {1, 2}
0: empty set
rnil: empty set
rcons: {1, 2}
posrecip: {1}
2ndsneg: {1, 2}
negrecip: {1}
pi: {1}
plus: {1, 2}
times: {1, 2}
square: {1}

↳ CSR

  ↳ CSRInnermostProof

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

from(X) → cons(X, from(s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, Z))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, Z))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)

The replacement map contains the following entries:

from: {1}
cons: {1}
s: {1}
2ndspos: {1, 2}
0: empty set
rnil: empty set
rcons: {1, 2}
posrecip: {1}
2ndsneg: {1, 2}
negrecip: {1}
pi: {1}
plus: {1, 2}
times: {1, 2}
square: {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:

from(X) → cons(X, from(s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, Z))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, Z))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)

The replacement map contains the following entries:

from: {1}
cons: {1}
s: {1}
2ndspos: {1, 2}
0: empty set
rnil: empty set
rcons: {1, 2}
posrecip: {1}
2ndsneg: {1, 2}
negrecip: {1}
pi: {1}
plus: {1, 2}
times: {1, 2}
square: {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 {from, s, 2ndspos, rcons, posrecip, 2ndsneg, negrecip, pi, plus, times, square, 2NDSNEG, 2NDSPOS, PI, FROM, PLUS, TIMES, SQUARE} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DP_o are:

2NDSPOS(s(N), cons(X, cons(Y, Z))) → 2NDSNEG(N, Z)
2NDSNEG(s(N), cons(X, cons(Y, Z))) → 2NDSPOS(N, Z)
PI(X) → 2NDSPOS(X, from(0))
PI(X) → FROM(0)
PLUS(s(X), Y) → PLUS(X, Y)
TIMES(s(X), Y) → PLUS(Y, times(X, Y))
TIMES(s(X), Y) → TIMES(X, Y)
SQUARE(X) → TIMES(X, X)

The collapsing dependency pairs are DP_c:

2NDSPOS(s(N), cons(X, cons(Y, Z))) → Y
2NDSPOS(s(N), cons(X, cons(Y, Z))) → Z
2NDSNEG(s(N), cons(X, cons(Y, Z))) → Y
2NDSNEG(s(N), cons(X, cons(Y, Z))) → Z

The hidden terms of R are:

from(s(X))

Every hiding context is built from:

s on positions {1}
from on positions {1}

Hence, the new unhiding pairs DP_u are :

2NDSPOS(s(N), cons(X, cons(Y, Z))) → U(Y)
2NDSPOS(s(N), cons(X, cons(Y, Z))) → U(Z)
2NDSNEG(s(N), cons(X, cons(Y, Z))) → U(Y)
2NDSNEG(s(N), cons(X, cons(Y, Z))) → U(Z)
U(s(x_0)) → U(x_0)
U(from(x_0)) → U(x_0)
U(from(s(X))) → FROM(s(X))

The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, Z))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, Z))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)

The set Q consists of the following terms:

from(x0)
2ndspos(0, x0)
2ndspos(s(x0), cons(x1, cons(x2, x3)))
2ndsneg(0, x0)
2ndsneg(s(x0), cons(x1, cons(x2, x3)))
pi(x0)
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
square(x0)

The approximation of the Context-Sensitive Dependency Graph contains 4 SCCs with 7 less nodes.
The rules PI(x0) → 2NDSPOS(x0, from(0)) and 2NDSPOS(s(z0), cons(z1, cons(z2, z3))) → 2NDSNEG(z0, z3) form no chain, because ECap^µ_R'(2NDSPOS(s(z0), cons(z1, cons(z2, z3)))) = 2NDSPOS(s(x_1), cons(x_2, cons(z2, z3))) does not unify with 2NDSPOS(x0, from(0)).
R' =

( cons(X, from(s(X))), from(X))

The rules PI(x0) → 2NDSPOS(x0, from(0)) and 2NDSPOS(s(z0), cons(z1, cons(z2, z3))) → U(z2) form no chain, because ECap^µ_R'(2NDSPOS(s(z0), cons(z1, cons(z2, z3)))) = 2NDSPOS(s(x_1), cons(x_2, cons(z2, z3))) does not unify with 2NDSPOS(x0, from(0)).
R' =

( cons(X, from(s(X))), from(X))

The rules PI(x0) → 2NDSPOS(x0, from(0)) and 2NDSPOS(s(z0), cons(z1, cons(z2, z3))) → U(z3) form no chain, because ECap^µ_R'(2NDSPOS(s(z0), cons(z1, cons(z2, z3)))) = 2NDSPOS(s(x_1), cons(x_2, cons(z2, z3))) does not unify with 2NDSPOS(x0, from(0)).
R' =

( cons(X, from(s(X))), from(X))

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

                ↳ QCSDPSubtermProof

              ↳ QCSDP

              ↳ QCSDP

              ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {from, s, 2ndspos, rcons, posrecip, 2ndsneg, negrecip, pi, plus, times, square} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The TRS P consists of the following rules:

U(s(x_0)) → U(x_0)
U(from(x_0)) → U(x_0)

The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, Z))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, Z))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)

The set Q consists of the following terms:

from(x0)
2ndspos(0, x0)
2ndspos(s(x0), cons(x1, cons(x2, x3)))
2ndsneg(0, x0)
2ndsneg(s(x0), cons(x1, cons(x2, x3)))
pi(x0)
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
square(x0)

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

U(s(x_0)) → U(x_0)
U(from(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

            ↳ AND

              ↳ QCSDP

                ↳ QCSDPSubtermProof

                  ↳ QCSDP

                    ↳ PIsEmptyProof

              ↳ QCSDP

              ↳ QCSDP

              ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {from, s, 2ndspos, rcons, posrecip, 2ndsneg, negrecip, pi, plus, times, square} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, Z))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, Z))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)

The set Q consists of the following terms:

from(x0)
2ndspos(0, x0)
2ndspos(s(x0), cons(x1, cons(x2, x3)))
2ndsneg(0, x0)
2ndsneg(s(x0), cons(x1, cons(x2, x3)))
pi(x0)
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
square(x0)

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

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

              ↳ QCSDP

                ↳ QCSDPSubtermProof

              ↳ QCSDP

              ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {from, s, 2ndspos, rcons, posrecip, 2ndsneg, negrecip, pi, plus, times, square, PLUS} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.

The TRS P consists of the following rules:

PLUS(s(X), Y) → PLUS(X, Y)

The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, Z))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, Z))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)

The set Q consists of the following terms:

from(x0)
2ndspos(0, x0)
2ndspos(s(x0), cons(x1, cons(x2, x3)))
2ndsneg(0, x0)
2ndsneg(s(x0), cons(x1, cons(x2, x3)))
pi(x0)
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
square(x0)

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

PLUS(s(X), Y) → PLUS(X, Y)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
PLUS(x1, x2) = x1

Subterm Order

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

              ↳ QCSDP

                ↳ QCSDPSubtermProof

                  ↳ QCSDP

                    ↳ PIsEmptyProof

              ↳ QCSDP

              ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {from, s, 2ndspos, rcons, posrecip, 2ndsneg, negrecip, pi, plus, times, square} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, Z))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, Z))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)

The set Q consists of the following terms:

from(x0)
2ndspos(0, x0)
2ndspos(s(x0), cons(x1, cons(x2, x3)))
2ndsneg(0, x0)
2ndsneg(s(x0), cons(x1, cons(x2, x3)))
pi(x0)
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
square(x0)

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

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

              ↳ QCSDP

              ↳ QCSDP

                ↳ QCSDPSubtermProof

              ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {from, s, 2ndspos, rcons, posrecip, 2ndsneg, negrecip, pi, plus, times, square, TIMES} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.

The TRS P consists of the following rules:

TIMES(s(X), Y) → TIMES(X, Y)

The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, Z))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, Z))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)

The set Q consists of the following terms:

from(x0)
2ndspos(0, x0)
2ndspos(s(x0), cons(x1, cons(x2, x3)))
2ndsneg(0, x0)
2ndsneg(s(x0), cons(x1, cons(x2, x3)))
pi(x0)
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
square(x0)

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

TIMES(s(X), Y) → TIMES(X, Y)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
TIMES(x1, x2) = x1

Subterm Order

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

              ↳ QCSDP

              ↳ QCSDP

                ↳ QCSDPSubtermProof

                  ↳ QCSDP

                    ↳ PIsEmptyProof

              ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {from, s, 2ndspos, rcons, posrecip, 2ndsneg, negrecip, pi, plus, times, square} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, Z))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, Z))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)

The set Q consists of the following terms:

from(x0)
2ndspos(0, x0)
2ndspos(s(x0), cons(x1, cons(x2, x3)))
2ndsneg(0, x0)
2ndsneg(s(x0), cons(x1, cons(x2, x3)))
pi(x0)
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
square(x0)

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

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

              ↳ QCSDP

              ↳ QCSDP

              ↳ QCSDP

                ↳ QCSDPSubtermProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {from, s, 2ndspos, rcons, posrecip, 2ndsneg, negrecip, pi, plus, times, square, 2NDSPOS, 2NDSNEG} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.

The TRS P consists of the following rules:

2NDSNEG(s(N), cons(X, cons(Y, Z))) → 2NDSPOS(N, Z)
2NDSPOS(s(N), cons(X, cons(Y, Z))) → 2NDSNEG(N, Z)

The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, Z))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, Z))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)

The set Q consists of the following terms:

from(x0)
2ndspos(0, x0)
2ndspos(s(x0), cons(x1, cons(x2, x3)))
2ndsneg(0, x0)
2ndsneg(s(x0), cons(x1, cons(x2, x3)))
pi(x0)
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
square(x0)

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

2NDSNEG(s(N), cons(X, cons(Y, Z))) → 2NDSPOS(N, Z)
2NDSPOS(s(N), cons(X, cons(Y, Z))) → 2NDSNEG(N, Z)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
2NDSPOS(x1, x2) = x1
2NDSNEG(x1, x2) = x1

Subterm Order

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

              ↳ QCSDP

              ↳ QCSDP

              ↳ QCSDP

                ↳ QCSDPSubtermProof

                  ↳ QCSDP

                    ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {from, s, 2ndspos, rcons, posrecip, 2ndsneg, negrecip, pi, plus, times, square} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, Z))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, Z))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)

The set Q consists of the following terms:

from(x0)
2ndspos(0, x0)
2ndspos(s(x0), cons(x1, cons(x2, x3)))
2ndsneg(0, x0)
2ndsneg(s(x0), cons(x1, cons(x2, x3)))
pi(x0)
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
square(x0)

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