YES
The TRS could be proven terminating. The proof took 19 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (7ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| copy#(0, y, z) | → | f#(z) | | f#(cons(f(cons(nil, y)), z)) | → | copy#(n, y, z) |
| copy#(s(x), y, z) | → | f#(y) | | copy#(s(x), y, z) | → | copy#(x, y, cons(f(y), z)) |
Rewrite Rules
| f(cons(nil, y)) | → | y | | f(cons(f(cons(nil, y)), z)) | → | copy(n, y, z) |
| copy(0, y, z) | → | f(z) | | copy(s(x), y, z) | → | copy(x, y, cons(f(y), z)) |
Original Signature
Termination of terms over the following signature is verified: f, 0, s, n, nil, cons, copy
Strategy
The following SCCs where found
| copy#(s(x), y, z) → copy#(x, y, cons(f(y), z)) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| copy#(s(x), y, z) | → | copy#(x, y, cons(f(y), z)) |
Rewrite Rules
| f(cons(nil, y)) | → | y | | f(cons(f(cons(nil, y)), z)) | → | copy(n, y, z) |
| copy(0, y, z) | → | f(z) | | copy(s(x), y, z) | → | copy(x, y, cons(f(y), z)) |
Original Signature
Termination of terms over the following signature is verified: f, 0, s, n, nil, cons, copy
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| copy#(s(x), y, z) | → | copy#(x, y, cons(f(y), z)) |