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)) → c(f(g(f(a))))
The replacement map contains the following entries:f: {1}
a: empty set
c: empty set
g: {1}
↳ CSR
↳ CSRInnermostProof
Context-sensitive rewrite system:
The TRS R consists of the following rules:
f(f(a)) → c(f(g(f(a))))
The replacement map contains the following entries:f: {1}
a: empty set
c: empty set
g: {1}
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)) → c(f(g(f(a))))
The replacement map contains the following entries:f: {1}
a: empty set
c: empty set
g: {1}
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, g, F} are replacing on all positions.
The symbols in {c, U} are not replacing on any position.
The hidden terms of R are:
f(g(f(a)))
f(a)
Every hiding context is built from:
g on positions {1}
f on positions {1}
Hence, the new unhiding pairs DPu are :
U(g(x_0)) → U(x_0)
U(f(x_0)) → U(x_0)
U(f(g(f(a)))) → F(g(f(a)))
U(f(a)) → F(a)
The TRS R consists of the following rules:
f(f(a)) → c(f(g(f(a))))
The set Q consists of the following terms:
f(f(a))
The approximation of the Context-Sensitive Dependency Graph contains 1 SCC with 2 less nodes.
↳ CSR
↳ CSRInnermostProof
↳ CSR
↳ CSDependencyPairsProof
↳ QCSDP
↳ QCSDependencyGraphProof
↳ QCSDP
↳ QCSDPSubtermProof
Q-restricted context-sensitive dependency pair problem:
The symbols in {f, g} are replacing on all positions.
The symbols in {c, U} are not replacing on any position.
The TRS P consists of the following rules:
U(g(x_0)) → U(x_0)
U(f(x_0)) → U(x_0)
The TRS R consists of the following rules:
f(f(a)) → c(f(g(f(a))))
The set Q consists of the following terms:
f(f(a))
We use the subterm processor [20].
The following pairs can be oriented strictly and are deleted.
U(g(x_0)) → U(x_0)
U(f(x_0)) → U(x_0)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
U(x1) = x1
Subterm Order
↳ CSR
↳ CSRInnermostProof
↳ CSR
↳ CSDependencyPairsProof
↳ QCSDP
↳ QCSDependencyGraphProof
↳ QCSDP
↳ QCSDPSubtermProof
↳ QCSDP
↳ PIsEmptyProof
Q-restricted context-sensitive dependency pair problem:
The symbols in {f, g} are replacing on all positions.
The symbols in {c} are not replacing on any position.
The TRS P consists of the following rules:
none
The TRS R consists of the following rules:
f(f(a)) → c(f(g(f(a))))
The set Q consists of the following terms:
f(f(a))
The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.