Termination of the following Term Rewriting System could be proven:

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

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

The replacement map contains the following entries:

f: {1, 3}
a: empty set
b: empty set
c: empty set


↳ CSR
  ↳ CSDependencyPairsProof

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

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

The replacement map contains the following entries:

f: {1, 3}
a: empty set
b: empty set
c: empty set

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

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDPForwardInstantiationProcessor

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

The ordinary context-sensitive dependency pairs DPo are:

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

The TRS R consists of the following rules:

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

Q is empty.

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

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



↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDPForwardInstantiationProcessor
        ↳ QCSDP
          ↳ PIsEmptyProof

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

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

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

Q is empty.

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