Termination of the following Term Rewriting System could be proven:
Context-sensitive rewrite system:
The TRS R consists of the following rules:
f(f(a)) → f(g(f(a)))
The replacement map contains the following entries:f: {1}
a: empty set
g: empty set
↳ CSR
↳ CSRInnermostProof
Context-sensitive rewrite system:
The TRS R consists of the following rules:
f(f(a)) → f(g(f(a)))
The replacement map contains the following entries:f: {1}
a: 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:
f(f(a)) → f(g(f(a)))
The replacement map contains the following entries:f: {1}
a: 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, F} are replacing on all positions.
The symbols in {g} are not replacing on any position.
The ordinary context-sensitive dependency pairs DPo are:
F(f(a)) → F(g(f(a)))
The TRS R consists of the following rules:
f(f(a)) → f(g(f(a)))
The set Q consists of the following terms:
f(f(a))
The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs.
The rules F(f(a)) → F(g(f(a))) and F(f(a)) → F(g(f(a))) form no chain, because ECapµ(F(g(f(a)))) = F(g(f(a))) does not unify with F(f(a)).