Termination of the following Term Rewriting System could be proven:
Context-sensitive rewrite system:
The TRS R consists of the following rules:
f(b, X, c) → f(X, c, X)
c → b
The replacement map contains the following entries:f: {2}
b: empty set
c: empty set
↳ CSR
↳ CSDependencyPairsProof
Context-sensitive rewrite system:
The TRS R consists of the following rules:
f(b, X, c) → f(X, c, X)
c → b
The replacement map contains the following entries:f: {2}
b: empty set
c: 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 ordinary context-sensitive dependency pairs DPo are:
F(b, X, c) → F(X, c, X)
F(b, X, c) → C
The TRS R consists of the following rules:
f(b, X, c) → f(X, c, X)
c → b
Q is empty.
The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs.
The rules F(b, z0, c) → F(z0, c, z0) and F(b, x0, c) → F(x0, c, x0) form no chain, because ECapµ(F(z0, c, z0)) = F(z0, x_1, z0) does not unify with F(b, x0, c). The rules F(b, z0, c) → F(z0, c, z0) and F(b, x0, c) → C form no chain, because ECapµ(F(z0, c, z0)) = F(z0, x_1, z0) does not unify with F(b, x0, c).