Termination of the following Term Rewriting System could be proven:
Context-sensitive rewrite system:
The TRS R consists of the following rules:
f(X, X) → f(a, b)
b → a
The replacement map contains the following entries:f: {1}
a: empty set
b: empty set
↳ CSR
↳ CSDependencyPairsProof
Context-sensitive rewrite system:
The TRS R consists of the following rules:
f(X, X) → f(a, b)
b → a
The replacement map contains the following entries:f: {1}
a: empty set
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:
For all symbols f in {f, F} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.
The ordinary context-sensitive dependency pairs DPo are:
F(X, X) → F(a, b)
The hidden terms of R are:
b
Every hiding context is built from:none
Hence, the new unhiding pairs DPu are :
U(b) → B
The TRS R consists of the following rules:
f(X, X) → f(a, b)
b → a
Q is empty.
The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs.
The rules F(z0, z0) → F(a, b) and F(x0, x0) → F(a, b) form no chain, because ECapµ(F(a, b)) = F(a, b) does not unify with F(x0, x0).