TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60559 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (226ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (1ms), PolynomialLinearRange4iUR (53ms), DependencyGraph (1ms), PolynomialOrderingProcessor (0ms), DependencyGraph (0ms), PolynomialLinearRange4 (201ms), DependencyGraph (1ms), PolynomialLinearRange4 (101ms), DependencyGraph (0ms), PolynomialLinearRange4 (72ms), DependencyGraph (0ms), PolynomialLinearRange4 (68ms), DependencyGraph (0ms), ReductionPairSAT (265ms), DependencyGraph (0ms), SizeChangePrinciple (timeout)].
| – Problem 3 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (11ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (0ms), PolynomialOrderingProcessor (0ms), DependencyGraph (1ms), PolynomialLinearRange4 (153ms), DependencyGraph (0ms), PolynomialLinearRange4 (95ms), DependencyGraph (13ms), PolynomialLinearRange4 (91ms), DependencyGraph (1ms), PolynomialLinearRange4 (69ms), DependencyGraph (1ms), ReductionPairSAT (395ms), DependencyGraph (0ms)].
| – Problem 4 was processed with processor PolynomialLinearRange4 (13ms).
| – Problem 5 was processed with processor PolynomialLinearRange4 (10ms).
| – Problem 6 was processed with processor PolynomialLinearRange4 (127ms).
| | – Problem 9 was processed with processor PolynomialLinearRange4 (37ms).
| | | – Problem 10 was processed with processor PolynomialLinearRange4 (14ms).
| – Problem 7 was processed with processor PolynomialLinearRange4 (94ms).
| – Problem 8 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (18ms), PolynomialLinearRange4iUR (17ms), DependencyGraph (2ms), PolynomialOrderingProcessor (0ms), DependencyGraph (1ms), PolynomialLinearRange4 (126ms), DependencyGraph (2ms), PolynomialLinearRange4 (99ms), DependencyGraph (1ms), PolynomialLinearRange4 (89ms), DependencyGraph (1ms), PolynomialLinearRange4 (85ms), DependencyGraph (2ms), ReductionPairSAT (261ms), DependencyGraph (4ms)].
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| sel#(s(X), cons(Y, Z)) | → | sel#(X, Z) |
Rewrite Rules
| sel(s(X), cons(Y, Z)) | → | sel(X, Z) | | sel(0, cons(X, Z)) | → | X |
| first(0, Z) | → | nil | | first(s(X), cons(Y, Z)) | → | cons(Y, first(X, Z)) |
| from(X) | → | cons(X, from(s(X))) | | sel1(s(X), cons(Y, Z)) | → | sel1(X, Z) |
| sel1(0, cons(X, Z)) | → | quote(X) | | first1(0, Z) | → | nil1 |
| first1(s(X), cons(Y, Z)) | → | cons1(quote(Y), first1(X, Z)) | | quote(0) | → | 01 |
| quote1(cons(X, Z)) | → | cons1(quote(X), quote1(Z)) | | quote1(nil) | → | nil1 |
| quote(s(X)) | → | s1(quote(X)) | | quote(sel(X, Z)) | → | sel1(X, Z) |
| quote1(first(X, Z)) | → | first1(X, Z) | | unquote(01) | → | 0 |
| unquote(s1(X)) | → | s(unquote(X)) | | unquote1(nil1) | → | nil |
| unquote1(cons1(X, Z)) | → | fcons(unquote(X), unquote1(Z)) | | fcons(X, Z) | → | cons(X, Z) |
Original Signature
Termination of terms over the following signature is verified: s1, cons1, fcons, from, 01, first1, quote1, unquote, 0, s, sel1, unquote1, quote, nil1, sel, first, cons, nil
Open Dependency Pair Problem 3
Dependency Pairs
| first1#(s(X), cons(Y, Z)) | → | first1#(X, Z) |
Rewrite Rules
| sel(s(X), cons(Y, Z)) | → | sel(X, Z) | | sel(0, cons(X, Z)) | → | X |
| first(0, Z) | → | nil | | first(s(X), cons(Y, Z)) | → | cons(Y, first(X, Z)) |
| from(X) | → | cons(X, from(s(X))) | | sel1(s(X), cons(Y, Z)) | → | sel1(X, Z) |
| sel1(0, cons(X, Z)) | → | quote(X) | | first1(0, Z) | → | nil1 |
| first1(s(X), cons(Y, Z)) | → | cons1(quote(Y), first1(X, Z)) | | quote(0) | → | 01 |
| quote1(cons(X, Z)) | → | cons1(quote(X), quote1(Z)) | | quote1(nil) | → | nil1 |
| quote(s(X)) | → | s1(quote(X)) | | quote(sel(X, Z)) | → | sel1(X, Z) |
| quote1(first(X, Z)) | → | first1(X, Z) | | unquote(01) | → | 0 |
| unquote(s1(X)) | → | s(unquote(X)) | | unquote1(nil1) | → | nil |
| unquote1(cons1(X, Z)) | → | fcons(unquote(X), unquote1(Z)) | | fcons(X, Z) | → | cons(X, Z) |
Original Signature
Termination of terms over the following signature is verified: s1, cons1, fcons, from, 01, first1, quote1, unquote, 0, s, sel1, unquote1, quote, nil1, sel, first, cons, nil
Open Dependency Pair Problem 8
Dependency Pairs
| quote#(sel(X, Z)) | → | sel1#(X, Z) | | sel1#(0, cons(X, Z)) | → | quote#(X) |
| quote#(s(X)) | → | quote#(X) | | sel1#(s(X), cons(Y, Z)) | → | sel1#(X, Z) |
Rewrite Rules
| sel(s(X), cons(Y, Z)) | → | sel(X, Z) | | sel(0, cons(X, Z)) | → | X |
| first(0, Z) | → | nil | | first(s(X), cons(Y, Z)) | → | cons(Y, first(X, Z)) |
| from(X) | → | cons(X, from(s(X))) | | sel1(s(X), cons(Y, Z)) | → | sel1(X, Z) |
| sel1(0, cons(X, Z)) | → | quote(X) | | first1(0, Z) | → | nil1 |
| first1(s(X), cons(Y, Z)) | → | cons1(quote(Y), first1(X, Z)) | | quote(0) | → | 01 |
| quote1(cons(X, Z)) | → | cons1(quote(X), quote1(Z)) | | quote1(nil) | → | nil1 |
| quote(s(X)) | → | s1(quote(X)) | | quote(sel(X, Z)) | → | sel1(X, Z) |
| quote1(first(X, Z)) | → | first1(X, Z) | | unquote(01) | → | 0 |
| unquote(s1(X)) | → | s(unquote(X)) | | unquote1(nil1) | → | nil |
| unquote1(cons1(X, Z)) | → | fcons(unquote(X), unquote1(Z)) | | fcons(X, Z) | → | cons(X, Z) |
Original Signature
Termination of terms over the following signature is verified: s1, cons1, fcons, from, 01, first1, quote1, unquote, 0, s, sel1, unquote1, quote, nil1, sel, first, cons, nil
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| first1#(s(X), cons(Y, Z)) | → | quote#(Y) | | T(from(x_1)) | → | T(x_1) |
| quote#(s(X)) | → | quote#(X) | | first1#(s(X), cons(Y, Z)) | → | first1#(X, Z) |
| quote#(sel(X, Z)) | → | T(X) | | quote1#(first(X, Z)) | → | first1#(X, Z) |
| sel1#(s(X), cons(Y, Z)) | → | T(Z) | | unquote1#(cons1(X, Z)) | → | fcons#(unquote(X), unquote1(Z)) |
| unquote1#(cons1(X, Z)) | → | unquote1#(Z) | | T(s(x_1)) | → | T(x_1) |
| quote1#(first(X, Z)) | → | T(X) | | T(first(x_1, x_2)) | → | T(x_2) |
| quote1#(cons(X, Z)) | → | quote#(X) | | quote#(sel(X, Z)) | → | sel1#(X, Z) |
| T(first(X, Z)) | → | first#(X, Z) | | sel#(s(X), cons(Y, Z)) | → | sel#(X, Z) |
| unquote#(s1(X)) | → | unquote#(X) | | first1#(s(X), cons(Y, Z)) | → | T(Z) |
| quote#(sel(X, Z)) | → | T(Z) | | unquote1#(cons1(X, Z)) | → | unquote#(X) |
| T(first(x_1, x_2)) | → | T(x_1) | | sel1#(s(X), cons(Y, Z)) | → | sel1#(X, Z) |
| quote1#(cons(X, Z)) | → | quote1#(Z) | | sel1#(0, cons(X, Z)) | → | quote#(X) |
| quote1#(first(X, Z)) | → | T(Z) | | sel#(s(X), cons(Y, Z)) | → | T(Z) |
| T(from(s(X))) | → | from#(s(X)) |
Rewrite Rules
| sel(s(X), cons(Y, Z)) | → | sel(X, Z) | | sel(0, cons(X, Z)) | → | X |
| first(0, Z) | → | nil | | first(s(X), cons(Y, Z)) | → | cons(Y, first(X, Z)) |
| from(X) | → | cons(X, from(s(X))) | | sel1(s(X), cons(Y, Z)) | → | sel1(X, Z) |
| sel1(0, cons(X, Z)) | → | quote(X) | | first1(0, Z) | → | nil1 |
| first1(s(X), cons(Y, Z)) | → | cons1(quote(Y), first1(X, Z)) | | quote(0) | → | 01 |
| quote1(cons(X, Z)) | → | cons1(quote(X), quote1(Z)) | | quote1(nil) | → | nil1 |
| quote(s(X)) | → | s1(quote(X)) | | quote(sel(X, Z)) | → | sel1(X, Z) |
| quote1(first(X, Z)) | → | first1(X, Z) | | unquote(01) | → | 0 |
| unquote(s1(X)) | → | s(unquote(X)) | | unquote1(nil1) | → | nil |
| unquote1(cons1(X, Z)) | → | fcons(unquote(X), unquote1(Z)) | | fcons(X, Z) | → | cons(X, Z) |
Original Signature
Termination of terms over the following signature is verified: s1, cons1, fcons, from, 01, first1, quote1, unquote, 0, s, sel1, unquote1, quote, nil1, first, sel, nil, cons
Strategy
Context-sensitive strategy:
μ(T) = μ(quote1#) = μ(quote) = μ(quote#) = μ(01) = μ(quote1) = μ(0) = μ(nil1) = μ(nil) = ∅
μ(from#) = μ(from) = μ(unquote) = μ(unquote1) = μ(unquote#) = μ(cons) = μ(unquote1#) = μ(s1) = μ(s) = {1}
μ(fcons#) = μ(cons1) = μ(sel#) = μ(sel1#) = μ(first#) = μ(first1#) = μ(sel1) = μ(fcons) = μ(first1) = μ(sel) = μ(first) = {1, 2}
The following SCCs where found
| quote1#(cons(X, Z)) → quote1#(Z) |
| quote#(sel(X, Z)) → sel1#(X, Z) | sel1#(0, cons(X, Z)) → quote#(X) |
| quote#(s(X)) → quote#(X) | sel1#(s(X), cons(Y, Z)) → sel1#(X, Z) |
| unquote1#(cons1(X, Z)) → unquote1#(Z) |
| sel#(s(X), cons(Y, Z)) → sel#(X, Z) |
| unquote#(s1(X)) → unquote#(X) |
| first1#(s(X), cons(Y, Z)) → first1#(X, Z) |
| T(first(x_1, x_2)) → T(x_2) | T(s(x_1)) → T(x_1) |
| T(from(x_1)) → T(x_1) | T(first(x_1, x_2)) → T(x_1) |
Problem 4: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| quote1#(cons(X, Z)) | → | quote1#(Z) |
Rewrite Rules
| sel(s(X), cons(Y, Z)) | → | sel(X, Z) | | sel(0, cons(X, Z)) | → | X |
| first(0, Z) | → | nil | | first(s(X), cons(Y, Z)) | → | cons(Y, first(X, Z)) |
| from(X) | → | cons(X, from(s(X))) | | sel1(s(X), cons(Y, Z)) | → | sel1(X, Z) |
| sel1(0, cons(X, Z)) | → | quote(X) | | first1(0, Z) | → | nil1 |
| first1(s(X), cons(Y, Z)) | → | cons1(quote(Y), first1(X, Z)) | | quote(0) | → | 01 |
| quote1(cons(X, Z)) | → | cons1(quote(X), quote1(Z)) | | quote1(nil) | → | nil1 |
| quote(s(X)) | → | s1(quote(X)) | | quote(sel(X, Z)) | → | sel1(X, Z) |
| quote1(first(X, Z)) | → | first1(X, Z) | | unquote(01) | → | 0 |
| unquote(s1(X)) | → | s(unquote(X)) | | unquote1(nil1) | → | nil |
| unquote1(cons1(X, Z)) | → | fcons(unquote(X), unquote1(Z)) | | fcons(X, Z) | → | cons(X, Z) |
Original Signature
Termination of terms over the following signature is verified: s1, cons1, fcons, from, 01, first1, quote1, unquote, 0, s, sel1, unquote1, quote, nil1, first, sel, nil, cons
Strategy
Context-sensitive strategy:
μ(T) = μ(quote1#) = μ(quote) = μ(quote#) = μ(01) = μ(quote1) = μ(0) = μ(nil1) = μ(nil) = ∅
μ(from#) = μ(from) = μ(unquote) = μ(unquote1) = μ(unquote#) = μ(cons) = μ(unquote1#) = μ(s1) = μ(s) = {1}
μ(cons1) = μ(fcons#) = μ(sel#) = μ(sel1#) = μ(first#) = μ(first1#) = μ(sel1) = μ(fcons) = μ(first1) = μ(first) = μ(sel) = {1, 2}
Polynomial Interpretation
- 0: 0
- 01: 0
- cons(x,y): y + 1
- cons1(x,y): 0
- fcons(x,y): 0
- first(x,y): 0
- first1(x,y): 0
- from(x): 0
- nil: 0
- nil1: 0
- quote(x): 0
- quote1(x): 0
- quote1#(x): 2x + 1
- s(x): 0
- s1(x): 0
- sel(x,y): 0
- sel1(x,y): 0
- unquote(x): 0
- unquote1(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:
| quote1#(cons(X, Z)) | → | quote1#(Z) |
Problem 5: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| unquote1#(cons1(X, Z)) | → | unquote1#(Z) |
Rewrite Rules
| sel(s(X), cons(Y, Z)) | → | sel(X, Z) | | sel(0, cons(X, Z)) | → | X |
| first(0, Z) | → | nil | | first(s(X), cons(Y, Z)) | → | cons(Y, first(X, Z)) |
| from(X) | → | cons(X, from(s(X))) | | sel1(s(X), cons(Y, Z)) | → | sel1(X, Z) |
| sel1(0, cons(X, Z)) | → | quote(X) | | first1(0, Z) | → | nil1 |
| first1(s(X), cons(Y, Z)) | → | cons1(quote(Y), first1(X, Z)) | | quote(0) | → | 01 |
| quote1(cons(X, Z)) | → | cons1(quote(X), quote1(Z)) | | quote1(nil) | → | nil1 |
| quote(s(X)) | → | s1(quote(X)) | | quote(sel(X, Z)) | → | sel1(X, Z) |
| quote1(first(X, Z)) | → | first1(X, Z) | | unquote(01) | → | 0 |
| unquote(s1(X)) | → | s(unquote(X)) | | unquote1(nil1) | → | nil |
| unquote1(cons1(X, Z)) | → | fcons(unquote(X), unquote1(Z)) | | fcons(X, Z) | → | cons(X, Z) |
Original Signature
Termination of terms over the following signature is verified: s1, cons1, fcons, from, 01, first1, quote1, unquote, 0, s, sel1, unquote1, quote, nil1, first, sel, nil, cons
Strategy
Context-sensitive strategy:
μ(T) = μ(quote1#) = μ(quote) = μ(quote#) = μ(01) = μ(quote1) = μ(0) = μ(nil1) = μ(nil) = ∅
μ(from#) = μ(from) = μ(unquote) = μ(unquote1) = μ(unquote#) = μ(cons) = μ(unquote1#) = μ(s1) = μ(s) = {1}
μ(cons1) = μ(fcons#) = μ(sel#) = μ(sel1#) = μ(first#) = μ(first1#) = μ(sel1) = μ(fcons) = μ(first1) = μ(first) = μ(sel) = {1, 2}
Polynomial Interpretation
- 0: 0
- 01: 0
- cons(x,y): 0
- cons1(x,y): y + 2
- fcons(x,y): 0
- first(x,y): 0
- first1(x,y): 0
- from(x): 0
- nil: 0
- nil1: 0
- quote(x): 0
- quote1(x): 0
- s(x): 0
- s1(x): 0
- sel(x,y): 0
- sel1(x,y): 0
- unquote(x): 0
- unquote1(x): 0
- unquote1#(x): x
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| unquote1#(cons1(X, Z)) | → | unquote1#(Z) |
Problem 6: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| T(first(x_1, x_2)) | → | T(x_2) | | T(s(x_1)) | → | T(x_1) |
| T(from(x_1)) | → | T(x_1) | | T(first(x_1, x_2)) | → | T(x_1) |
Rewrite Rules
| sel(s(X), cons(Y, Z)) | → | sel(X, Z) | | sel(0, cons(X, Z)) | → | X |
| first(0, Z) | → | nil | | first(s(X), cons(Y, Z)) | → | cons(Y, first(X, Z)) |
| from(X) | → | cons(X, from(s(X))) | | sel1(s(X), cons(Y, Z)) | → | sel1(X, Z) |
| sel1(0, cons(X, Z)) | → | quote(X) | | first1(0, Z) | → | nil1 |
| first1(s(X), cons(Y, Z)) | → | cons1(quote(Y), first1(X, Z)) | | quote(0) | → | 01 |
| quote1(cons(X, Z)) | → | cons1(quote(X), quote1(Z)) | | quote1(nil) | → | nil1 |
| quote(s(X)) | → | s1(quote(X)) | | quote(sel(X, Z)) | → | sel1(X, Z) |
| quote1(first(X, Z)) | → | first1(X, Z) | | unquote(01) | → | 0 |
| unquote(s1(X)) | → | s(unquote(X)) | | unquote1(nil1) | → | nil |
| unquote1(cons1(X, Z)) | → | fcons(unquote(X), unquote1(Z)) | | fcons(X, Z) | → | cons(X, Z) |
Original Signature
Termination of terms over the following signature is verified: s1, cons1, fcons, from, 01, first1, quote1, unquote, 0, s, sel1, unquote1, quote, nil1, first, sel, nil, cons
Strategy
Context-sensitive strategy:
μ(T) = μ(quote1#) = μ(quote) = μ(quote#) = μ(01) = μ(quote1) = μ(0) = μ(nil1) = μ(nil) = ∅
μ(from#) = μ(from) = μ(unquote) = μ(unquote1) = μ(unquote#) = μ(cons) = μ(unquote1#) = μ(s1) = μ(s) = {1}
μ(cons1) = μ(fcons#) = μ(sel#) = μ(sel1#) = μ(first#) = μ(first1#) = μ(sel1) = μ(fcons) = μ(first1) = μ(first) = μ(sel) = {1, 2}
Polynomial Interpretation
- 0: 0
- 01: 0
- T(x): x + 1
- cons(x,y): 0
- cons1(x,y): 0
- fcons(x,y): 0
- first(x,y): y + 2x
- first1(x,y): 0
- from(x): 2x + 1
- nil: 0
- nil1: 0
- quote(x): 0
- quote1(x): 0
- s(x): x
- s1(x): 0
- sel(x,y): 0
- sel1(x,y): 0
- unquote(x): 0
- unquote1(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 9: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| T(first(x_1, x_2)) | → | T(x_2) | | T(s(x_1)) | → | T(x_1) |
| T(first(x_1, x_2)) | → | T(x_1) |
Rewrite Rules
| sel(s(X), cons(Y, Z)) | → | sel(X, Z) | | sel(0, cons(X, Z)) | → | X |
| first(0, Z) | → | nil | | first(s(X), cons(Y, Z)) | → | cons(Y, first(X, Z)) |
| from(X) | → | cons(X, from(s(X))) | | sel1(s(X), cons(Y, Z)) | → | sel1(X, Z) |
| sel1(0, cons(X, Z)) | → | quote(X) | | first1(0, Z) | → | nil1 |
| first1(s(X), cons(Y, Z)) | → | cons1(quote(Y), first1(X, Z)) | | quote(0) | → | 01 |
| quote1(cons(X, Z)) | → | cons1(quote(X), quote1(Z)) | | quote1(nil) | → | nil1 |
| quote(s(X)) | → | s1(quote(X)) | | quote(sel(X, Z)) | → | sel1(X, Z) |
| quote1(first(X, Z)) | → | first1(X, Z) | | unquote(01) | → | 0 |
| unquote(s1(X)) | → | s(unquote(X)) | | unquote1(nil1) | → | nil |
| unquote1(cons1(X, Z)) | → | fcons(unquote(X), unquote1(Z)) | | fcons(X, Z) | → | cons(X, Z) |
Original Signature
Termination of terms over the following signature is verified: s1, cons1, fcons, from, 01, first1, quote1, unquote, 0, s, sel1, unquote1, quote, nil1, sel, first, cons, nil
Strategy
Context-sensitive strategy:
μ(T) = μ(quote1#) = μ(quote) = μ(quote#) = μ(01) = μ(quote1) = μ(0) = μ(nil1) = μ(nil) = ∅
μ(from#) = μ(from) = μ(unquote) = μ(unquote1) = μ(unquote#) = μ(cons) = μ(unquote1#) = μ(s1) = μ(s) = {1}
μ(fcons#) = μ(cons1) = μ(sel#) = μ(sel1#) = μ(first#) = μ(first1#) = μ(sel1) = μ(fcons) = μ(first1) = μ(sel) = μ(first) = {1, 2}
Polynomial Interpretation
- 0: 0
- 01: 0
- T(x): 2x
- cons(x,y): 0
- cons1(x,y): 0
- fcons(x,y): 0
- first(x,y): 2y + 2x + 1
- first1(x,y): 0
- from(x): 0
- nil: 0
- nil1: 0
- quote(x): 0
- quote1(x): 0
- s(x): 2x
- s1(x): 0
- sel(x,y): 0
- sel1(x,y): 0
- unquote(x): 0
- unquote1(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:
| T(first(x_1, x_2)) | → | T(x_2) | | T(first(x_1, x_2)) | → | T(x_1) |
Problem 10: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| sel(s(X), cons(Y, Z)) | → | sel(X, Z) | | sel(0, cons(X, Z)) | → | X |
| first(0, Z) | → | nil | | first(s(X), cons(Y, Z)) | → | cons(Y, first(X, Z)) |
| from(X) | → | cons(X, from(s(X))) | | sel1(s(X), cons(Y, Z)) | → | sel1(X, Z) |
| sel1(0, cons(X, Z)) | → | quote(X) | | first1(0, Z) | → | nil1 |
| first1(s(X), cons(Y, Z)) | → | cons1(quote(Y), first1(X, Z)) | | quote(0) | → | 01 |
| quote1(cons(X, Z)) | → | cons1(quote(X), quote1(Z)) | | quote1(nil) | → | nil1 |
| quote(s(X)) | → | s1(quote(X)) | | quote(sel(X, Z)) | → | sel1(X, Z) |
| quote1(first(X, Z)) | → | first1(X, Z) | | unquote(01) | → | 0 |
| unquote(s1(X)) | → | s(unquote(X)) | | unquote1(nil1) | → | nil |
| unquote1(cons1(X, Z)) | → | fcons(unquote(X), unquote1(Z)) | | fcons(X, Z) | → | cons(X, Z) |
Original Signature
Termination of terms over the following signature is verified: s1, cons1, fcons, from, 01, first1, quote1, unquote, 0, s, sel1, unquote1, quote, nil1, first, sel, nil, cons
Strategy
Context-sensitive strategy:
μ(T) = μ(quote1#) = μ(quote) = μ(quote#) = μ(01) = μ(quote1) = μ(0) = μ(nil1) = μ(nil) = ∅
μ(from#) = μ(from) = μ(unquote) = μ(unquote1) = μ(unquote#) = μ(cons) = μ(unquote1#) = μ(s1) = μ(s) = {1}
μ(cons1) = μ(fcons#) = μ(sel#) = μ(sel1#) = μ(first#) = μ(first1#) = μ(sel1) = μ(fcons) = μ(first1) = μ(first) = μ(sel) = {1, 2}
Polynomial Interpretation
- 0: 0
- 01: 0
- T(x): x + 1
- cons(x,y): 0
- cons1(x,y): 0
- fcons(x,y): 0
- first(x,y): 0
- first1(x,y): 0
- from(x): 0
- nil: 0
- nil1: 0
- quote(x): 0
- quote1(x): 0
- s(x): x + 2
- s1(x): 0
- sel(x,y): 0
- sel1(x,y): 0
- unquote(x): 0
- unquote1(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 7: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| unquote#(s1(X)) | → | unquote#(X) |
Rewrite Rules
| sel(s(X), cons(Y, Z)) | → | sel(X, Z) | | sel(0, cons(X, Z)) | → | X |
| first(0, Z) | → | nil | | first(s(X), cons(Y, Z)) | → | cons(Y, first(X, Z)) |
| from(X) | → | cons(X, from(s(X))) | | sel1(s(X), cons(Y, Z)) | → | sel1(X, Z) |
| sel1(0, cons(X, Z)) | → | quote(X) | | first1(0, Z) | → | nil1 |
| first1(s(X), cons(Y, Z)) | → | cons1(quote(Y), first1(X, Z)) | | quote(0) | → | 01 |
| quote1(cons(X, Z)) | → | cons1(quote(X), quote1(Z)) | | quote1(nil) | → | nil1 |
| quote(s(X)) | → | s1(quote(X)) | | quote(sel(X, Z)) | → | sel1(X, Z) |
| quote1(first(X, Z)) | → | first1(X, Z) | | unquote(01) | → | 0 |
| unquote(s1(X)) | → | s(unquote(X)) | | unquote1(nil1) | → | nil |
| unquote1(cons1(X, Z)) | → | fcons(unquote(X), unquote1(Z)) | | fcons(X, Z) | → | cons(X, Z) |
Original Signature
Termination of terms over the following signature is verified: s1, cons1, fcons, from, 01, first1, quote1, unquote, 0, s, sel1, unquote1, quote, nil1, first, sel, nil, cons
Strategy
Context-sensitive strategy:
μ(T) = μ(quote1#) = μ(quote) = μ(quote#) = μ(01) = μ(quote1) = μ(0) = μ(nil1) = μ(nil) = ∅
μ(from#) = μ(from) = μ(unquote) = μ(unquote1) = μ(unquote#) = μ(cons) = μ(unquote1#) = μ(s1) = μ(s) = {1}
μ(cons1) = μ(fcons#) = μ(sel#) = μ(sel1#) = μ(first#) = μ(first1#) = μ(sel1) = μ(fcons) = μ(first1) = μ(first) = μ(sel) = {1, 2}
Polynomial Interpretation
- 0: 0
- 01: 0
- cons(x,y): 0
- cons1(x,y): 0
- fcons(x,y): 0
- first(x,y): 0
- first1(x,y): 0
- from(x): 0
- nil: 0
- nil1: 0
- quote(x): 0
- quote1(x): 0
- s(x): 0
- s1(x): x + 1
- sel(x,y): 0
- sel1(x,y): 0
- unquote(x): 0
- unquote#(x): 2x + 1
- unquote1(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:
| unquote#(s1(X)) | → | unquote#(X) |