Termination of the following Term Rewriting System could be proven:

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

c → f(g(c))
f(g(X)) → g(X)

The replacement map contains the following entries:

c: empty set
f: empty set
g: empty set


↳ CSR
  ↳ CSRInnermostProof

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

c → f(g(c))
f(g(X)) → g(X)

The replacement map contains the following entries:

c: empty set
f: empty set
g: empty set

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:

c → f(g(c))
f(g(X)) → g(X)

The replacement map contains the following entries:

c: empty set
f: empty set
g: empty set

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 {f, g, F, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

C → F(g(c))


The hidden terms of R are:

c

Every hiding context is built from:none

Hence, the new unhiding pairs DPu are :

U(c) → C

The TRS R consists of the following rules:

c → f(g(c))
f(g(X)) → g(X)

The set Q consists of the following terms:

c
f(g(x0))


The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 2 less nodes.