NO
The TRS could be proven non-terminating. The proof took 1095 ms.
The following reduction sequence is a witness for non-termination:
f#(0) →* f#(0)
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (10ms).
| – Problem 2 was processed with processor ForwardNarrowing (1ms).
| | – Problem 3 was processed with processor Propagation (1ms).
| | | – Problem 4 remains open; application of the following processors failed [ForwardNarrowing (1ms), BackwardInstantiation (1ms), ForwardInstantiation (0ms), Propagation (1ms)].
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| f#(s(0)) | → | f#(p(s(0))) | | f#(s(0)) | → | p#(s(0)) |
| f#(0) | → | f#(s(0)) |
Rewrite Rules
| f(0) | → | cons(0, f(s(0))) | | f(s(0)) | → | f(p(s(0))) |
| p(s(0)) | → | 0 |
Original Signature
Termination of terms over the following signature is verified: f, 0, s, p, cons
Strategy
The following SCCs where found
| f#(s(0)) → f#(p(s(0))) | f#(0) → f#(s(0)) |
Problem 2: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(s(0)) | → | f#(p(s(0))) | | f#(0) | → | f#(s(0)) |
Rewrite Rules
| f(0) | → | cons(0, f(s(0))) | | f(s(0)) | → | f(p(s(0))) |
| p(s(0)) | → | 0 |
Original Signature
Termination of terms over the following signature is verified: f, 0, s, p, cons
Strategy
The right-hand side of the rule f
#(s(0)) → f
#(p(s(0))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
| f#(0) | |
Thus, the rule f
#(s(0)) → f
#(p(s(0))) is replaced by the following rules:
Problem 3: Propagation
Dependency Pair Problem
Dependency Pairs
| f#(s(0)) | → | f#(0) | | f#(0) | → | f#(s(0)) |
Rewrite Rules
| f(0) | → | cons(0, f(s(0))) | | f(s(0)) | → | f(p(s(0))) |
| p(s(0)) | → | 0 |
Original Signature
Termination of terms over the following signature is verified: f, 0, s, p, cons
Strategy
The dependency pairs f
#(s(0)) → f
#(0) and f
#(0) → f
#(s(0)) are consolidated into the rule f
#(s(0)) → f
#(s(0)) .
This is possible as
- all subterms of f#(0) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in f#(0), but non-replacing in both f#(s(0)) and f#(s(0))
The dependency pairs f
#(s(0)) → f
#(0) and f
#(0) → f
#(s(0)) are consolidated into the rule f
#(s(0)) → f
#(s(0)) .
This is possible as
- all subterms of f#(0) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in f#(0), but non-replacing in both f#(s(0)) and f#(s(0))
The dependency pairs f
#(0) → f
#(s(0)) and f
#(s(0)) → f
#(0) are consolidated into the rule f
#(0) → f
#(0) .
This is possible as
- all subterms of f#(s(0)) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in f#(s(0)), but non-replacing in both f#(0) and f#(0)
The dependency pairs f
#(0) → f
#(s(0)) and f
#(s(0)) → f
#(0) are consolidated into the rule f
#(0) → f
#(0) .
This is possible as
- all subterms of f#(s(0)) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in f#(s(0)), but non-replacing in both f#(0) and f#(0)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| f#(s(0)) → f#(0) | f#(0) → f#(0) |
| f#(0) → f#(s(0)) | f#(s(0)) → f#(s(0)) |