Termination of the following Term Rewriting System could be proven:

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

f(a, X, X) → f(X, b, b)
b → a

The replacement map contains the following entries:

f: {2}
a: empty set
b: empty set


↳ CSR
  ↳ CSDependencyPairsProof

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

f(a, X, X) → f(X, b, b)
b → a

The replacement map contains the following entries:

f: {2}
a: empty set
b: empty set

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

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
For all symbols f in {f, F} we have µ(f) = {2}.
The symbols in {U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

F(a, X, X) → F(X, b, b)
F(a, X, X) → B


The hidden terms of R are:

b

Every hiding context is built from:none

Hence, the new unhiding pairs DPu are :

U(b) → B

The TRS R consists of the following rules:

f(a, X, X) → f(X, b, b)
b → a

Q is empty.

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


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ QCSDP
          ↳ QCSUsableRulesProof

Q-restricted context-sensitive dependency pair problem:
For all symbols f in {f, F} we have µ(f) = {2}.

The TRS P consists of the following rules:

F(a, X, X) → F(X, b, b)

The TRS R consists of the following rules:

f(a, X, X) → f(X, b, b)
b → a

Q is empty.

The following rules are not useable and can be deleted:

f(a, x0, x0) → f(x0, b, b)


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ QCSDP
          ↳ QCSUsableRulesProof
            ↳ QCSDP
              ↳ QCSDPInstantiationProcessor

Q-restricted context-sensitive dependency pair problem:
For all symbols f in {F} we have µ(f) = {2}.

The TRS P consists of the following rules:

F(a, X, X) → F(X, b, b)

The TRS R consists of the following rules:

b → a

Q is empty.

Using the Context-Sensitive Instantiation Processor
the pair F(a, X, X) → F(X, b, b)
was transformed to the following new pairs:

F(a, b, b) → F(b, b, b)



↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ QCSDP
          ↳ QCSUsableRulesProof
            ↳ QCSDP
              ↳ QCSDPInstantiationProcessor
                ↳ QCSDP
                  ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

b → a

Q is empty.

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