Termination of the following Term Rewriting System could be proven:

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

g(X) → h(X)
c → d
h(d) → g(c)

The replacement map contains the following entries:

g: empty set
h: empty set
c: empty set
d: empty set


↳ CSR
  ↳ CSRInnermostProof

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

g(X) → h(X)
c → d
h(d) → g(c)

The replacement map contains the following entries:

g: empty set
h: empty set
c: empty set
d: 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:

g(X) → h(X)
c → d
h(d) → g(c)

The replacement map contains the following entries:

g: empty set
h: empty set
c: empty set
d: 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 {g, h, H, G, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

G(X) → H(X)
H(d) → 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:

g(X) → h(X)
c → d
h(d) → g(c)

The set Q consists of the following terms:

g(x0)
c
h(d)


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


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {g, h, G, H} are not replacing on any position.

The TRS P consists of the following rules:

H(d) → G(c)
G(X) → H(X)

The TRS R consists of the following rules:

g(X) → h(X)
c → d
h(d) → g(c)

The set Q consists of the following terms:

g(x0)
c
h(d)


The following rules are not useable and can be deleted:

g(x0) → h(x0)
c → d
h(d) → g(c)


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ QCSDP
              ↳ QCSUsableRulesProof
                ↳ QCSDP
                  ↳ QCSDPReductionPairProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {G, H, g, h} are not replacing on any position.

The TRS P consists of the following rules:

H(d) → G(c)
G(X) → H(X)

R is empty.
The set Q consists of the following terms:

g(x0)
c
h(d)


Using the order
Polynomial Order [21,25] with Interpretation:

POL( H(x1) ) = 2x1 + 1


POL( c ) = 1


POL( G(x1) ) = 2x1 + 2


POL( d ) = 2



the following usable rules
none

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

H(d) → G(c)
G(X) → H(X)

could be oriented strictly and thus removed.
All pairs have been removed.


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ QCSDP
              ↳ QCSUsableRulesProof
                ↳ QCSDP
                  ↳ QCSDPReductionPairProof
                    ↳ QCSDP
                      ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {g, h} are not replacing on any position.

The TRS P consists of the following rules:
none

R is empty.
The set Q consists of the following terms:

g(x0)
c
h(d)


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