Termination of the following Term Rewriting System could be proven:
Context-sensitive rewrite system:
The TRS R consists of the following rules:
f(0) → cons(0, f(s(0)))
f(s(0)) → f(p(s(0)))
p(s(X)) → X
The replacement map contains the following entries:f: {1}
0: empty set
cons: {1}
s: {1}
p: {1}
↳ CSR
↳ CSRInnermostProof
Context-sensitive rewrite system:
The TRS R consists of the following rules:
f(0) → cons(0, f(s(0)))
f(s(0)) → f(p(s(0)))
p(s(X)) → X
The replacement map contains the following entries:f: {1}
0: empty set
cons: {1}
s: {1}
p: {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(0) → cons(0, f(s(0)))
f(s(0)) → f(p(s(0)))
p(s(X)) → X
The replacement map contains the following entries:f: {1}
0: empty set
cons: {1}
s: {1}
p: {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, s, p, F, P} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.
The ordinary context-sensitive dependency pairs DPo are:
F(s(0)) → F(p(s(0)))
F(s(0)) → P(s(0))
The hidden terms of R are:
f(s(0))
Every hiding context is built from:none
Hence, the new unhiding pairs DPu are :
U(f(s(0))) → F(s(0))
The TRS R consists of the following rules:
f(0) → cons(0, f(s(0)))
f(s(0)) → f(p(s(0)))
p(s(X)) → X
The set Q consists of the following terms:
f(0)
f(s(0))
p(s(x0))
The approximation of the Context-Sensitive Dependency Graph contains 1 SCC with 2 less nodes.
↳ CSR
↳ CSRInnermostProof
↳ CSR
↳ CSDependencyPairsProof
↳ QCSDP
↳ QCSDependencyGraphProof
↳ QCSDP
↳ QCSUsableRulesProof
Q-restricted context-sensitive dependency pair problem:
The symbols in {f, s, p, F} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The TRS P consists of the following rules:
F(s(0)) → F(p(s(0)))
The TRS R consists of the following rules:
f(0) → cons(0, f(s(0)))
f(s(0)) → f(p(s(0)))
p(s(X)) → X
The set Q consists of the following terms:
f(0)
f(s(0))
p(s(x0))
The following rules are not useable and can be deleted:
f(0) → cons(0, f(s(0)))
f(s(0)) → f(p(s(0)))
↳ CSR
↳ CSRInnermostProof
↳ CSR
↳ CSDependencyPairsProof
↳ QCSDP
↳ QCSDependencyGraphProof
↳ QCSDP
↳ QCSUsableRulesProof
↳ QCSDP
↳ QCSDPReductionPairProof
Q-restricted context-sensitive dependency pair problem:
The symbols in {p, s, F, f} are replacing on all positions.
The TRS P consists of the following rules:
F(s(0)) → F(p(s(0)))
The TRS R consists of the following rules:
p(s(X)) → X
The set Q consists of the following terms:
f(0)
f(s(0))
p(s(x0))
Using the order
Matrix interpretation [3]:
Non-tuple symbols:
Tuple symbols:
Matrix type:
We used a basic matrix type which is not further parametrizeable.
the following usable rules
p(s(X)) → X
could all be oriented weakly.
Furthermore, the pairs
F(s(0)) → F(p(s(0)))
could be oriented strictly and thus removed.
All pairs have been removed.
↳ CSR
↳ CSRInnermostProof
↳ CSR
↳ CSDependencyPairsProof
↳ QCSDP
↳ QCSDependencyGraphProof
↳ QCSDP
↳ QCSUsableRulesProof
↳ QCSDP
↳ QCSDPReductionPairProof
↳ QCSDP
↳ PIsEmptyProof
Q-restricted context-sensitive dependency pair problem:
The symbols in {p, s, f} are replacing on all positions.
The TRS P consists of the following rules:
none
The TRS R consists of the following rules:
p(s(X)) → X
The set Q consists of the following terms:
f(0)
f(s(0))
p(s(x0))
The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.