YES
The TRS could be proven terminating. The proof took 1835 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (142ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor PolynomialLinearRange4iUR (1489ms).
| | – Problem 6 was processed with processor DependencyGraph (2ms).
| | | – Problem 7 was processed with processor PolynomialLinearRange4iUR (16ms).
| | | | – Problem 8 was processed with processor PolynomialLinearRange4iUR (7ms).
| – Problem 4 was processed with processor SubtermCriterion (1ms).
| – Problem 5 was processed with processor SubtermCriterion (0ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| f#(s(X), cs(Y, Z)) | → | a#(Z) | | d#(s(X)) | → | s#(s(d(X))) |
| a#(nt(X)) | → | a#(X) | | a#(nf(X1, X2)) | → | a#(X1) |
| a#(ns(X)) | → | a#(X) | | a#(nf(X1, X2)) | → | a#(X2) |
| q#(s(X)) | → | p#(q(X), d(X)) | | p#(s(X), s(Y)) | → | s#(p(X, Y)) |
| q#(s(X)) | → | d#(X) | | a#(ns(X)) | → | s#(a(X)) |
| q#(s(X)) | → | s#(p(q(X), d(X))) | | q#(s(X)) | → | q#(X) |
| a#(nt(X)) | → | t#(a(X)) | | d#(s(X)) | → | d#(X) |
| t#(N) | → | q#(N) | | p#(s(X), s(Y)) | → | p#(X, Y) |
| p#(s(X), s(Y)) | → | s#(s(p(X, Y))) | | a#(nf(X1, X2)) | → | f#(a(X1), a(X2)) |
| d#(s(X)) | → | s#(d(X)) |
Rewrite Rules
| t(N) | → | cs(r(q(N)), nt(ns(N))) | | q(0) | → | 0 |
| q(s(X)) | → | s(p(q(X), d(X))) | | d(0) | → | 0 |
| d(s(X)) | → | s(s(d(X))) | | p(0, X) | → | X |
| p(X, 0) | → | X | | p(s(X), s(Y)) | → | s(s(p(X, Y))) |
| f(0, X) | → | nil | | f(s(X), cs(Y, Z)) | → | cs(Y, nf(X, a(Z))) |
| t(X) | → | nt(X) | | s(X) | → | ns(X) |
| f(X1, X2) | → | nf(X1, X2) | | a(nt(X)) | → | t(a(X)) |
| a(ns(X)) | → | s(a(X)) | | a(nf(X1, X2)) | → | f(a(X1), a(X2)) |
| a(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: f, nt, ns, d, a, cs, t, 0, s, r, q, p, nf, nil
Strategy
The following SCCs where found
| f#(s(X), cs(Y, Z)) → a#(Z) | a#(nt(X)) → a#(X) |
| a#(nf(X1, X2)) → a#(X1) | a#(ns(X)) → a#(X) |
| a#(nf(X1, X2)) → a#(X2) | a#(nf(X1, X2)) → f#(a(X1), a(X2)) |
| p#(s(X), s(Y)) → p#(X, Y) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| t(N) | → | cs(r(q(N)), nt(ns(N))) | | q(0) | → | 0 |
| q(s(X)) | → | s(p(q(X), d(X))) | | d(0) | → | 0 |
| d(s(X)) | → | s(s(d(X))) | | p(0, X) | → | X |
| p(X, 0) | → | X | | p(s(X), s(Y)) | → | s(s(p(X, Y))) |
| f(0, X) | → | nil | | f(s(X), cs(Y, Z)) | → | cs(Y, nf(X, a(Z))) |
| t(X) | → | nt(X) | | s(X) | → | ns(X) |
| f(X1, X2) | → | nf(X1, X2) | | a(nt(X)) | → | t(a(X)) |
| a(ns(X)) | → | s(a(X)) | | a(nf(X1, X2)) | → | f(a(X1), a(X2)) |
| a(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: f, nt, ns, d, a, cs, t, 0, s, r, q, p, nf, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| f#(s(X), cs(Y, Z)) | → | a#(Z) | | a#(nt(X)) | → | a#(X) |
| a#(nf(X1, X2)) | → | a#(X1) | | a#(ns(X)) | → | a#(X) |
| a#(nf(X1, X2)) | → | a#(X2) | | a#(nf(X1, X2)) | → | f#(a(X1), a(X2)) |
Rewrite Rules
| t(N) | → | cs(r(q(N)), nt(ns(N))) | | q(0) | → | 0 |
| q(s(X)) | → | s(p(q(X), d(X))) | | d(0) | → | 0 |
| d(s(X)) | → | s(s(d(X))) | | p(0, X) | → | X |
| p(X, 0) | → | X | | p(s(X), s(Y)) | → | s(s(p(X, Y))) |
| f(0, X) | → | nil | | f(s(X), cs(Y, Z)) | → | cs(Y, nf(X, a(Z))) |
| t(X) | → | nt(X) | | s(X) | → | ns(X) |
| f(X1, X2) | → | nf(X1, X2) | | a(nt(X)) | → | t(a(X)) |
| a(ns(X)) | → | s(a(X)) | | a(nf(X1, X2)) | → | f(a(X1), a(X2)) |
| a(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: f, nt, ns, d, a, cs, t, 0, s, r, q, p, nf, nil
Strategy
Polynomial Interpretation
- 0: 0
- a(x): x
- a#(x): x
- cs(x,y): y
- d(x): 2x
- f(x,y): 2y + x + 2
- f#(x,y): y + 2
- nf(x,y): 2y + x + 2
- nil: 2
- ns(x): x
- nt(x): x
- p(x,y): y
- q(x): 0
- r(x): 2x
- s(x): x
- t(x): x
Improved Usable rules
| t(N) | → | cs(r(q(N)), nt(ns(N))) | | a(nf(X1, X2)) | → | f(a(X1), a(X2)) |
| f(X1, X2) | → | nf(X1, X2) | | a(nt(X)) | → | t(a(X)) |
| f(s(X), cs(Y, Z)) | → | cs(Y, nf(X, a(Z))) | | a(X) | → | X |
| s(X) | → | ns(X) | | f(0, X) | → | nil |
| t(X) | → | nt(X) | | a(ns(X)) | → | s(a(X)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| f#(s(X), cs(Y, Z)) | → | a#(Z) | | a#(nf(X1, X2)) | → | a#(X1) |
| a#(nf(X1, X2)) | → | a#(X2) |
Problem 6: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a#(nt(X)) | → | a#(X) | | a#(ns(X)) | → | a#(X) |
| a#(nf(X1, X2)) | → | f#(a(X1), a(X2)) |
Rewrite Rules
| t(N) | → | cs(r(q(N)), nt(ns(N))) | | q(0) | → | 0 |
| q(s(X)) | → | s(p(q(X), d(X))) | | d(0) | → | 0 |
| d(s(X)) | → | s(s(d(X))) | | p(0, X) | → | X |
| p(X, 0) | → | X | | p(s(X), s(Y)) | → | s(s(p(X, Y))) |
| f(0, X) | → | nil | | f(s(X), cs(Y, Z)) | → | cs(Y, nf(X, a(Z))) |
| t(X) | → | nt(X) | | s(X) | → | ns(X) |
| f(X1, X2) | → | nf(X1, X2) | | a(nt(X)) | → | t(a(X)) |
| a(ns(X)) | → | s(a(X)) | | a(nf(X1, X2)) | → | f(a(X1), a(X2)) |
| a(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: f, nt, ns, d, a, cs, t, 0, s, r, q, p, nf, nil
Strategy
The following SCCs where found
| a#(nt(X)) → a#(X) | a#(ns(X)) → a#(X) |
Problem 7: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| a#(nt(X)) | → | a#(X) | | a#(ns(X)) | → | a#(X) |
Rewrite Rules
| t(N) | → | cs(r(q(N)), nt(ns(N))) | | q(0) | → | 0 |
| q(s(X)) | → | s(p(q(X), d(X))) | | d(0) | → | 0 |
| d(s(X)) | → | s(s(d(X))) | | p(0, X) | → | X |
| p(X, 0) | → | X | | p(s(X), s(Y)) | → | s(s(p(X, Y))) |
| f(0, X) | → | nil | | f(s(X), cs(Y, Z)) | → | cs(Y, nf(X, a(Z))) |
| t(X) | → | nt(X) | | s(X) | → | ns(X) |
| f(X1, X2) | → | nf(X1, X2) | | a(nt(X)) | → | t(a(X)) |
| a(ns(X)) | → | s(a(X)) | | a(nf(X1, X2)) | → | f(a(X1), a(X2)) |
| a(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: f, nt, ns, d, a, cs, t, 0, s, r, q, p, nf, nil
Strategy
Polynomial Interpretation
- 0: 0
- a(x): 0
- a#(x): 3x
- cs(x,y): 0
- d(x): 0
- f(x,y): 0
- nf(x,y): 0
- nil: 0
- ns(x): 3x
- nt(x): x + 1
- p(x,y): 0
- q(x): 0
- r(x): 0
- s(x): 0
- t(x): 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
Problem 8: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| t(N) | → | cs(r(q(N)), nt(ns(N))) | | q(0) | → | 0 |
| q(s(X)) | → | s(p(q(X), d(X))) | | d(0) | → | 0 |
| d(s(X)) | → | s(s(d(X))) | | p(0, X) | → | X |
| p(X, 0) | → | X | | p(s(X), s(Y)) | → | s(s(p(X, Y))) |
| f(0, X) | → | nil | | f(s(X), cs(Y, Z)) | → | cs(Y, nf(X, a(Z))) |
| t(X) | → | nt(X) | | s(X) | → | ns(X) |
| f(X1, X2) | → | nf(X1, X2) | | a(nt(X)) | → | t(a(X)) |
| a(ns(X)) | → | s(a(X)) | | a(nf(X1, X2)) | → | f(a(X1), a(X2)) |
| a(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: f, nt, ns, d, a, cs, t, 0, s, r, q, p, nf, nil
Strategy
Polynomial Interpretation
- 0: 0
- a(x): 0
- a#(x): 2x + 1
- cs(x,y): 0
- d(x): 0
- f(x,y): 0
- nf(x,y): 0
- nil: 0
- ns(x): x + 1
- nt(x): 0
- p(x,y): 0
- q(x): 0
- r(x): 0
- s(x): 0
- t(x): 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| p#(s(X), s(Y)) | → | p#(X, Y) |
Rewrite Rules
| t(N) | → | cs(r(q(N)), nt(ns(N))) | | q(0) | → | 0 |
| q(s(X)) | → | s(p(q(X), d(X))) | | d(0) | → | 0 |
| d(s(X)) | → | s(s(d(X))) | | p(0, X) | → | X |
| p(X, 0) | → | X | | p(s(X), s(Y)) | → | s(s(p(X, Y))) |
| f(0, X) | → | nil | | f(s(X), cs(Y, Z)) | → | cs(Y, nf(X, a(Z))) |
| t(X) | → | nt(X) | | s(X) | → | ns(X) |
| f(X1, X2) | → | nf(X1, X2) | | a(nt(X)) | → | t(a(X)) |
| a(ns(X)) | → | s(a(X)) | | a(nf(X1, X2)) | → | f(a(X1), a(X2)) |
| a(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: f, nt, ns, d, a, cs, t, 0, s, r, q, p, nf, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| p#(s(X), s(Y)) | → | p#(X, Y) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| t(N) | → | cs(r(q(N)), nt(ns(N))) | | q(0) | → | 0 |
| q(s(X)) | → | s(p(q(X), d(X))) | | d(0) | → | 0 |
| d(s(X)) | → | s(s(d(X))) | | p(0, X) | → | X |
| p(X, 0) | → | X | | p(s(X), s(Y)) | → | s(s(p(X, Y))) |
| f(0, X) | → | nil | | f(s(X), cs(Y, Z)) | → | cs(Y, nf(X, a(Z))) |
| t(X) | → | nt(X) | | s(X) | → | ns(X) |
| f(X1, X2) | → | nf(X1, X2) | | a(nt(X)) | → | t(a(X)) |
| a(ns(X)) | → | s(a(X)) | | a(nf(X1, X2)) | → | f(a(X1), a(X2)) |
| a(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: f, nt, ns, d, a, cs, t, 0, s, r, q, p, nf, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed: