Termination of the following Term Rewriting System could be proven:

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

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

The replacement map contains the following entries:

h: {1}
g: {1}
a: empty set
f: {1}
b: empty set


↳ CSR
  ↳ CSDependencyPairsProof

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

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

The replacement map contains the following entries:

h: {1}
g: {1}
a: empty set
f: {1}
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:
The symbols in {h, H} are replacing on all positions.
For all symbols f in {g, f, G, F} we have µ(f) = {1}.

The ordinary context-sensitive dependency pairs DPo are:

H(X) → G(X, X)
G(a, X) → F(b, X)
F(X, X) → H(a)
F(X, X) → A

The TRS R consists of the following rules:

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

Q is empty.

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


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {h, H} are replacing on all positions.
For all symbols f in {g, f, F, G} we have µ(f) = {1}.

The TRS P consists of the following rules:

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

The TRS R consists of the following rules:

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

Q is empty.

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

F(b, b) → H(a)



↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ QCSDP
          ↳ QCSDPInstantiationProcessor
            ↳ QCSDP
              ↳ QCSDPForwardInstantiationProcessor

Q-restricted context-sensitive dependency pair problem:
The symbols in {h, H} are replacing on all positions.
For all symbols f in {g, f, F, G} we have µ(f) = {1}.

The TRS P consists of the following rules:

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

The TRS R consists of the following rules:

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

Q is empty.

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

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



↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ QCSDP
          ↳ QCSDPInstantiationProcessor
            ↳ QCSDP
              ↳ QCSDPForwardInstantiationProcessor
                ↳ QCSDP
                  ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {h, H} are replacing on all positions.
For all symbols f in {g, f, F, G} we have µ(f) = {1}.

The TRS P consists of the following rules:

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

The TRS R consists of the following rules:

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

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 3 less nodes.
The rules H(x0) → G(x0, x0) and G(a, b) → F(b, b) form no chain, because ECapµR'(G(a, b)) = G(a, b) does not unify with G(x0, x0).
R' =

( g(X, X), h(X))
( f(b, X), g(a, X))
( h(a), f(X, X))
( b, a)