Termination of the following Term Rewriting System could be proven:

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

and(tt, X) → X
plus(N, 0) → N
plus(N, s(M)) → s(plus(N, M))

The replacement map contains the following entries:

and: {1}
tt: empty set
plus: {1, 2}
0: empty set
s: {1}


↳ CSR
  ↳ CSRInnermostProof

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

and(tt, X) → X
plus(N, 0) → N
plus(N, s(M)) → s(plus(N, M))

The replacement map contains the following entries:

and: {1}
tt: empty set
plus: {1, 2}
0: empty set
s: {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:

and(tt, X) → X
plus(N, 0) → N
plus(N, s(M)) → s(plus(N, M))

The replacement map contains the following entries:

and: {1}
tt: empty set
plus: {1, 2}
0: empty set
s: {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 {plus, s, PLUS} are replacing on all positions.
For all symbols f in {and, AND} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

PLUS(N, s(M)) → PLUS(N, M)

The collapsing dependency pairs are DPc:

AND(tt, X) → X


The hidden terms of R are:
none

Every hiding context is built from:none

Hence, the new unhiding pairs DPu are :

AND(tt, X) → U(X)

The TRS R consists of the following rules:

and(tt, X) → X
plus(N, 0) → N
plus(N, s(M)) → s(plus(N, M))

The set Q consists of the following terms:

and(tt, x0)
plus(x0, 0)
plus(x0, s(x1))


The approximation of the Context-Sensitive Dependency Graph contains 1 SCC.


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {plus, s, PLUS} are replacing on all positions.
For all symbols f in {and} we have µ(f) = {1}.

The TRS P consists of the following rules:

PLUS(N, s(M)) → PLUS(N, M)

The TRS R consists of the following rules:

and(tt, X) → X
plus(N, 0) → N
plus(N, s(M)) → s(plus(N, M))

The set Q consists of the following terms:

and(tt, x0)
plus(x0, 0)
plus(x0, s(x1))


We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


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

Subterm Order


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {plus, s} are replacing on all positions.
For all symbols f in {and} we have µ(f) = {1}.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

and(tt, X) → X
plus(N, 0) → N
plus(N, s(M)) → s(plus(N, M))

The set Q consists of the following terms:

and(tt, x0)
plus(x0, 0)
plus(x0, s(x1))


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