TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60045 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (10957ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| – Problem 4 was processed with processor SubtermCriterion (1ms).
| – Problem 5 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (1838ms), PolynomialLinearRange4iUR (2021ms), DependencyGraph (1838ms), PolynomialLinearRange4iUR (2032ms), DependencyGraph (1970ms), PolynomialLinearRange4iUR (3333ms), DependencyGraph (1842ms), PolynomialLinearRange8NegiUR (10000ms), DependencyGraph (1840ms), ReductionPairSAT (timeout)].
| – Problem 6 was processed with processor SubtermCriterion (1ms).
| | – Problem 14 remains open; application of the following processors failed [DependencyGraph (5ms), PolynomialLinearRange4iUR (1ms), DependencyGraph (4ms), PolynomialLinearRange4iUR (18ms), DependencyGraph (4ms), PolynomialLinearRange4iUR (10ms), DependencyGraph (4ms), PolynomialLinearRange8NegiUR (26ms), DependencyGraph (4ms)].
| – Problem 7 was processed with processor SubtermCriterion (1ms).
| – Problem 8 was processed with processor SubtermCriterion (1ms).
| – Problem 9 was processed with processor SubtermCriterion (1ms).
| – Problem 10 was processed with processor SubtermCriterion (2ms).
| – Problem 11 was processed with processor SubtermCriterion (2ms).
| | – Problem 15 remains open; application of the following processors failed [DependencyGraph (5ms), PolynomialLinearRange4iUR (13ms), DependencyGraph (5ms), PolynomialLinearRange4iUR (12ms), DependencyGraph (4ms), PolynomialLinearRange4iUR (1ms), DependencyGraph (4ms), PolynomialLinearRange8NegiUR (37ms), DependencyGraph (5ms)].
| – Problem 12 was processed with processor SubtermCriterion (1ms).
| | – Problem 16 was processed with processor PolynomialLinearRange4iUR (54ms).
| | | – Problem 19 was processed with processor PolynomialLinearRange4iUR (25ms).
| – Problem 13 was processed with processor SubtermCriterion (1ms).
| | – Problem 17 was processed with processor PolynomialLinearRange4iUR (124ms).
| | | – Problem 18 was processed with processor PolynomialLinearRange4iUR (55ms).
The following open problems remain:
Open Dependency Pair Problem 5
Dependency Pairs
| active#(sel(0, cons(X, Y))) | → | mark#(X) | | mark#(dbls(X)) | → | mark#(X) |
| mark#(dbls(X)) | → | active#(dbls(mark(X))) | | mark#(sel1(X1, X2)) | → | active#(sel1(mark(X1), mark(X2))) |
| mark#(01) | → | active#(01) | | active#(dbl(s(X))) | → | mark#(s(s(dbl(X)))) |
| mark#(quote(X)) | → | mark#(X) | | mark#(dbl1(X)) | → | active#(dbl1(mark(X))) |
| active#(dbl1(s(X))) | → | mark#(s1(s1(dbl1(X)))) | | active#(sel(s(X), cons(Y, Z))) | → | mark#(sel(X, Z)) |
| mark#(nil) | → | active#(nil) | | active#(dbls(cons(X, Y))) | → | mark#(cons(dbl(X), dbls(Y))) |
| active#(indx(nil, X)) | → | mark#(nil) | | mark#(indx(X1, X2)) | → | active#(indx(mark(X1), X2)) |
| mark#(sel(X1, X2)) | → | mark#(X2) | | active#(quote(dbl(X))) | → | mark#(dbl1(X)) |
| mark#(quote(X)) | → | active#(quote(mark(X))) | | active#(indx(cons(X, Y), Z)) | → | mark#(cons(sel(X, Z), indx(Y, Z))) |
| mark#(sel(X1, X2)) | → | mark#(X1) | | mark#(dbl1(X)) | → | mark#(X) |
| active#(quote(s(X))) | → | mark#(s1(quote(X))) | | mark#(0) | → | active#(0) |
| active#(dbl1(0)) | → | mark#(01) | | active#(quote(0)) | → | mark#(01) |
| mark#(sel1(X1, X2)) | → | mark#(X2) | | mark#(dbl(X)) | → | active#(dbl(mark(X))) |
| active#(quote(sel(X, Y))) | → | mark#(sel1(X, Y)) | | mark#(indx(X1, X2)) | → | mark#(X1) |
| mark#(from(X)) | → | active#(from(X)) | | active#(from(X)) | → | mark#(cons(X, from(s(X)))) |
| mark#(sel(X1, X2)) | → | active#(sel(mark(X1), mark(X2))) | | mark#(s(X)) | → | active#(s(X)) |
| mark#(dbl(X)) | → | mark#(X) | | mark#(cons(X1, X2)) | → | active#(cons(X1, X2)) |
| mark#(s1(X)) | → | mark#(X) | | active#(sel1(s(X), cons(Y, Z))) | → | mark#(sel1(X, Z)) |
| active#(dbl(0)) | → | mark#(0) | | mark#(s1(X)) | → | active#(s1(mark(X))) |
| mark#(sel1(X1, X2)) | → | mark#(X1) | | active#(dbls(nil)) | → | mark#(nil) |
| active#(sel1(0, cons(X, Y))) | → | mark#(X) |
Rewrite Rules
| active(dbl(0)) | → | mark(0) | | active(dbl(s(X))) | → | mark(s(s(dbl(X)))) |
| active(dbls(nil)) | → | mark(nil) | | active(dbls(cons(X, Y))) | → | mark(cons(dbl(X), dbls(Y))) |
| active(sel(0, cons(X, Y))) | → | mark(X) | | active(sel(s(X), cons(Y, Z))) | → | mark(sel(X, Z)) |
| active(indx(nil, X)) | → | mark(nil) | | active(indx(cons(X, Y), Z)) | → | mark(cons(sel(X, Z), indx(Y, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(dbl1(0)) | → | mark(01) |
| active(dbl1(s(X))) | → | mark(s1(s1(dbl1(X)))) | | active(sel1(0, cons(X, Y))) | → | mark(X) |
| active(sel1(s(X), cons(Y, Z))) | → | mark(sel1(X, Z)) | | active(quote(0)) | → | mark(01) |
| active(quote(s(X))) | → | mark(s1(quote(X))) | | active(quote(dbl(X))) | → | mark(dbl1(X)) |
| active(quote(sel(X, Y))) | → | mark(sel1(X, Y)) | | mark(dbl(X)) | → | active(dbl(mark(X))) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(dbls(X)) | → | active(dbls(mark(X))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(indx(X1, X2)) | → | active(indx(mark(X1), X2)) | | mark(from(X)) | → | active(from(X)) |
| mark(dbl1(X)) | → | active(dbl1(mark(X))) | | mark(01) | → | active(01) |
| mark(s1(X)) | → | active(s1(mark(X))) | | mark(sel1(X1, X2)) | → | active(sel1(mark(X1), mark(X2))) |
| mark(quote(X)) | → | active(quote(mark(X))) | | dbl(mark(X)) | → | dbl(X) |
| dbl(active(X)) | → | dbl(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | dbls(mark(X)) | → | dbls(X) |
| dbls(active(X)) | → | dbls(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | sel(mark(X1), X2) | → | sel(X1, X2) |
| sel(X1, mark(X2)) | → | sel(X1, X2) | | sel(active(X1), X2) | → | sel(X1, X2) |
| sel(X1, active(X2)) | → | sel(X1, X2) | | indx(mark(X1), X2) | → | indx(X1, X2) |
| indx(X1, mark(X2)) | → | indx(X1, X2) | | indx(active(X1), X2) | → | indx(X1, X2) |
| indx(X1, active(X2)) | → | indx(X1, X2) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | dbl1(mark(X)) | → | dbl1(X) |
| dbl1(active(X)) | → | dbl1(X) | | s1(mark(X)) | → | s1(X) |
| s1(active(X)) | → | s1(X) | | sel1(mark(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, mark(X2)) | → | sel1(X1, X2) | | sel1(active(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, active(X2)) | → | sel1(X1, X2) | | quote(mark(X)) | → | quote(X) |
| quote(active(X)) | → | quote(X) |
Original Signature
Termination of terms over the following signature is verified: s1, dbl1, mark, dbl, from, 01, dbls, 0, sel1, s, indx, quote, active, sel, nil, cons
Open Dependency Pair Problem 14
Dependency Pairs
| cons#(X1, active(X2)) | → | cons#(X1, X2) | | cons#(X1, mark(X2)) | → | cons#(X1, X2) |
Rewrite Rules
| active(dbl(0)) | → | mark(0) | | active(dbl(s(X))) | → | mark(s(s(dbl(X)))) |
| active(dbls(nil)) | → | mark(nil) | | active(dbls(cons(X, Y))) | → | mark(cons(dbl(X), dbls(Y))) |
| active(sel(0, cons(X, Y))) | → | mark(X) | | active(sel(s(X), cons(Y, Z))) | → | mark(sel(X, Z)) |
| active(indx(nil, X)) | → | mark(nil) | | active(indx(cons(X, Y), Z)) | → | mark(cons(sel(X, Z), indx(Y, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(dbl1(0)) | → | mark(01) |
| active(dbl1(s(X))) | → | mark(s1(s1(dbl1(X)))) | | active(sel1(0, cons(X, Y))) | → | mark(X) |
| active(sel1(s(X), cons(Y, Z))) | → | mark(sel1(X, Z)) | | active(quote(0)) | → | mark(01) |
| active(quote(s(X))) | → | mark(s1(quote(X))) | | active(quote(dbl(X))) | → | mark(dbl1(X)) |
| active(quote(sel(X, Y))) | → | mark(sel1(X, Y)) | | mark(dbl(X)) | → | active(dbl(mark(X))) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(dbls(X)) | → | active(dbls(mark(X))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(indx(X1, X2)) | → | active(indx(mark(X1), X2)) | | mark(from(X)) | → | active(from(X)) |
| mark(dbl1(X)) | → | active(dbl1(mark(X))) | | mark(01) | → | active(01) |
| mark(s1(X)) | → | active(s1(mark(X))) | | mark(sel1(X1, X2)) | → | active(sel1(mark(X1), mark(X2))) |
| mark(quote(X)) | → | active(quote(mark(X))) | | dbl(mark(X)) | → | dbl(X) |
| dbl(active(X)) | → | dbl(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | dbls(mark(X)) | → | dbls(X) |
| dbls(active(X)) | → | dbls(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | sel(mark(X1), X2) | → | sel(X1, X2) |
| sel(X1, mark(X2)) | → | sel(X1, X2) | | sel(active(X1), X2) | → | sel(X1, X2) |
| sel(X1, active(X2)) | → | sel(X1, X2) | | indx(mark(X1), X2) | → | indx(X1, X2) |
| indx(X1, mark(X2)) | → | indx(X1, X2) | | indx(active(X1), X2) | → | indx(X1, X2) |
| indx(X1, active(X2)) | → | indx(X1, X2) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | dbl1(mark(X)) | → | dbl1(X) |
| dbl1(active(X)) | → | dbl1(X) | | s1(mark(X)) | → | s1(X) |
| s1(active(X)) | → | s1(X) | | sel1(mark(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, mark(X2)) | → | sel1(X1, X2) | | sel1(active(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, active(X2)) | → | sel1(X1, X2) | | quote(mark(X)) | → | quote(X) |
| quote(active(X)) | → | quote(X) |
Original Signature
Termination of terms over the following signature is verified: s1, dbl1, mark, dbl, from, 01, dbls, 0, sel1, s, indx, quote, active, sel, cons, nil
Open Dependency Pair Problem 15
Dependency Pairs
| sel1#(X1, mark(X2)) | → | sel1#(X1, X2) | | sel1#(X1, active(X2)) | → | sel1#(X1, X2) |
Rewrite Rules
| active(dbl(0)) | → | mark(0) | | active(dbl(s(X))) | → | mark(s(s(dbl(X)))) |
| active(dbls(nil)) | → | mark(nil) | | active(dbls(cons(X, Y))) | → | mark(cons(dbl(X), dbls(Y))) |
| active(sel(0, cons(X, Y))) | → | mark(X) | | active(sel(s(X), cons(Y, Z))) | → | mark(sel(X, Z)) |
| active(indx(nil, X)) | → | mark(nil) | | active(indx(cons(X, Y), Z)) | → | mark(cons(sel(X, Z), indx(Y, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(dbl1(0)) | → | mark(01) |
| active(dbl1(s(X))) | → | mark(s1(s1(dbl1(X)))) | | active(sel1(0, cons(X, Y))) | → | mark(X) |
| active(sel1(s(X), cons(Y, Z))) | → | mark(sel1(X, Z)) | | active(quote(0)) | → | mark(01) |
| active(quote(s(X))) | → | mark(s1(quote(X))) | | active(quote(dbl(X))) | → | mark(dbl1(X)) |
| active(quote(sel(X, Y))) | → | mark(sel1(X, Y)) | | mark(dbl(X)) | → | active(dbl(mark(X))) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(dbls(X)) | → | active(dbls(mark(X))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(indx(X1, X2)) | → | active(indx(mark(X1), X2)) | | mark(from(X)) | → | active(from(X)) |
| mark(dbl1(X)) | → | active(dbl1(mark(X))) | | mark(01) | → | active(01) |
| mark(s1(X)) | → | active(s1(mark(X))) | | mark(sel1(X1, X2)) | → | active(sel1(mark(X1), mark(X2))) |
| mark(quote(X)) | → | active(quote(mark(X))) | | dbl(mark(X)) | → | dbl(X) |
| dbl(active(X)) | → | dbl(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | dbls(mark(X)) | → | dbls(X) |
| dbls(active(X)) | → | dbls(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | sel(mark(X1), X2) | → | sel(X1, X2) |
| sel(X1, mark(X2)) | → | sel(X1, X2) | | sel(active(X1), X2) | → | sel(X1, X2) |
| sel(X1, active(X2)) | → | sel(X1, X2) | | indx(mark(X1), X2) | → | indx(X1, X2) |
| indx(X1, mark(X2)) | → | indx(X1, X2) | | indx(active(X1), X2) | → | indx(X1, X2) |
| indx(X1, active(X2)) | → | indx(X1, X2) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | dbl1(mark(X)) | → | dbl1(X) |
| dbl1(active(X)) | → | dbl1(X) | | s1(mark(X)) | → | s1(X) |
| s1(active(X)) | → | s1(X) | | sel1(mark(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, mark(X2)) | → | sel1(X1, X2) | | sel1(active(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, active(X2)) | → | sel1(X1, X2) | | quote(mark(X)) | → | quote(X) |
| quote(active(X)) | → | quote(X) |
Original Signature
Termination of terms over the following signature is verified: s1, dbl1, mark, dbl, from, 01, dbls, 0, sel1, s, indx, quote, active, sel, cons, nil
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(s1(X)) | → | s1#(mark(X)) | | mark#(dbls(X)) | → | dbls#(mark(X)) |
| active#(dbl(s(X))) | → | s#(dbl(X)) | | mark#(01) | → | active#(01) |
| active#(dbls(cons(X, Y))) | → | cons#(dbl(X), dbls(Y)) | | dbls#(mark(X)) | → | dbls#(X) |
| mark#(quote(X)) | → | mark#(X) | | active#(dbl1(s(X))) | → | mark#(s1(s1(dbl1(X)))) |
| active#(indx(nil, X)) | → | mark#(nil) | | mark#(indx(X1, X2)) | → | active#(indx(mark(X1), X2)) |
| mark#(sel(X1, X2)) | → | mark#(X1) | | indx#(mark(X1), X2) | → | indx#(X1, X2) |
| mark#(dbl1(X)) | → | mark#(X) | | s1#(active(X)) | → | s1#(X) |
| active#(sel(s(X), cons(Y, Z))) | → | sel#(X, Z) | | active#(dbl1(0)) | → | mark#(01) |
| active#(dbl(s(X))) | → | s#(s(dbl(X))) | | active#(quote(s(X))) | → | quote#(X) |
| mark#(dbl(X)) | → | active#(dbl(mark(X))) | | active#(quote(sel(X, Y))) | → | mark#(sel1(X, Y)) |
| mark#(indx(X1, X2)) | → | indx#(mark(X1), X2) | | active#(from(X)) | → | mark#(cons(X, from(s(X)))) |
| sel#(X1, mark(X2)) | → | sel#(X1, X2) | | quote#(mark(X)) | → | quote#(X) |
| sel#(X1, active(X2)) | → | sel#(X1, X2) | | active#(dbl(0)) | → | mark#(0) |
| mark#(s1(X)) | → | active#(s1(mark(X))) | | active#(quote(s(X))) | → | s1#(quote(X)) |
| active#(sel1(0, cons(X, Y))) | → | mark#(X) | | mark#(dbl1(X)) | → | dbl1#(mark(X)) |
| active#(sel(0, cons(X, Y))) | → | mark#(X) | | active#(dbl1(s(X))) | → | s1#(s1(dbl1(X))) |
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | mark#(cons(X1, X2)) | → | cons#(X1, X2) |
| from#(mark(X)) | → | from#(X) | | mark#(from(X)) | → | from#(X) |
| active#(indx(cons(X, Y), Z)) | → | indx#(Y, Z) | | active#(dbl(s(X))) | → | mark#(s(s(dbl(X)))) |
| sel1#(X1, mark(X2)) | → | sel1#(X1, X2) | | active#(dbls(cons(X, Y))) | → | mark#(cons(dbl(X), dbls(Y))) |
| active#(quote(sel(X, Y))) | → | sel1#(X, Y) | | cons#(X1, mark(X2)) | → | cons#(X1, X2) |
| active#(dbls(cons(X, Y))) | → | dbl#(X) | | mark#(0) | → | active#(0) |
| indx#(X1, active(X2)) | → | indx#(X1, X2) | | mark#(sel1(X1, X2)) | → | mark#(X2) |
| cons#(active(X1), X2) | → | cons#(X1, X2) | | mark#(cons(X1, X2)) | → | active#(cons(X1, X2)) |
| mark#(s1(X)) | → | mark#(X) | | active#(quote(dbl(X))) | → | dbl1#(X) |
| mark#(sel1(X1, X2)) | → | sel1#(mark(X1), mark(X2)) | | active#(dbls(nil)) | → | mark#(nil) |
| active#(from(X)) | → | from#(s(X)) | | quote#(active(X)) | → | quote#(X) |
| mark#(dbls(X)) | → | active#(dbls(mark(X))) | | dbls#(active(X)) | → | dbls#(X) |
| mark#(quote(X)) | → | quote#(mark(X)) | | mark#(sel1(X1, X2)) | → | active#(sel1(mark(X1), mark(X2))) |
| sel1#(X1, active(X2)) | → | sel1#(X1, X2) | | dbl1#(active(X)) | → | dbl1#(X) |
| mark#(dbl(X)) | → | dbl#(mark(X)) | | active#(quote(dbl(X))) | → | mark#(dbl1(X)) |
| active#(dbl(s(X))) | → | dbl#(X) | | active#(quote(s(X))) | → | mark#(s1(quote(X))) |
| mark#(sel(X1, X2)) | → | sel#(mark(X1), mark(X2)) | | mark#(sel(X1, X2)) | → | active#(sel(mark(X1), mark(X2))) |
| mark#(s(X)) | → | active#(s(X)) | | dbl1#(mark(X)) | → | dbl1#(X) |
| active#(indx(cons(X, Y), Z)) | → | cons#(sel(X, Z), indx(Y, Z)) | | active#(from(X)) | → | s#(X) |
| sel#(active(X1), X2) | → | sel#(X1, X2) | | cons#(X1, active(X2)) | → | cons#(X1, X2) |
| active#(dbl1(s(X))) | → | s1#(dbl1(X)) | | sel1#(mark(X1), X2) | → | sel1#(X1, X2) |
| from#(active(X)) | → | from#(X) | | indx#(active(X1), X2) | → | indx#(X1, X2) |
| sel#(mark(X1), X2) | → | sel#(X1, X2) | | mark#(dbls(X)) | → | mark#(X) |
| active#(dbls(cons(X, Y))) | → | dbls#(Y) | | active#(dbl1(s(X))) | → | dbl1#(X) |
| mark#(dbl1(X)) | → | active#(dbl1(mark(X))) | | active#(sel(s(X), cons(Y, Z))) | → | mark#(sel(X, Z)) |
| mark#(nil) | → | active#(nil) | | active#(sel1(s(X), cons(Y, Z))) | → | sel1#(X, Z) |
| active#(indx(cons(X, Y), Z)) | → | sel#(X, Z) | | mark#(sel(X1, X2)) | → | mark#(X2) |
| active#(from(X)) | → | cons#(X, from(s(X))) | | mark#(quote(X)) | → | active#(quote(mark(X))) |
| active#(indx(cons(X, Y), Z)) | → | mark#(cons(sel(X, Z), indx(Y, Z))) | | sel1#(active(X1), X2) | → | sel1#(X1, X2) |
| s1#(mark(X)) | → | s1#(X) | | active#(quote(0)) | → | mark#(01) |
| mark#(indx(X1, X2)) | → | mark#(X1) | | mark#(from(X)) | → | active#(from(X)) |
| dbl#(mark(X)) | → | dbl#(X) | | mark#(dbl(X)) | → | mark#(X) |
| indx#(X1, mark(X2)) | → | indx#(X1, X2) | | s#(mark(X)) | → | s#(X) |
| mark#(s(X)) | → | s#(X) | | active#(sel1(s(X), cons(Y, Z))) | → | mark#(sel1(X, Z)) |
| s#(active(X)) | → | s#(X) | | mark#(sel1(X1, X2)) | → | mark#(X1) |
| dbl#(active(X)) | → | dbl#(X) |
Rewrite Rules
| active(dbl(0)) | → | mark(0) | | active(dbl(s(X))) | → | mark(s(s(dbl(X)))) |
| active(dbls(nil)) | → | mark(nil) | | active(dbls(cons(X, Y))) | → | mark(cons(dbl(X), dbls(Y))) |
| active(sel(0, cons(X, Y))) | → | mark(X) | | active(sel(s(X), cons(Y, Z))) | → | mark(sel(X, Z)) |
| active(indx(nil, X)) | → | mark(nil) | | active(indx(cons(X, Y), Z)) | → | mark(cons(sel(X, Z), indx(Y, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(dbl1(0)) | → | mark(01) |
| active(dbl1(s(X))) | → | mark(s1(s1(dbl1(X)))) | | active(sel1(0, cons(X, Y))) | → | mark(X) |
| active(sel1(s(X), cons(Y, Z))) | → | mark(sel1(X, Z)) | | active(quote(0)) | → | mark(01) |
| active(quote(s(X))) | → | mark(s1(quote(X))) | | active(quote(dbl(X))) | → | mark(dbl1(X)) |
| active(quote(sel(X, Y))) | → | mark(sel1(X, Y)) | | mark(dbl(X)) | → | active(dbl(mark(X))) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(dbls(X)) | → | active(dbls(mark(X))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(indx(X1, X2)) | → | active(indx(mark(X1), X2)) | | mark(from(X)) | → | active(from(X)) |
| mark(dbl1(X)) | → | active(dbl1(mark(X))) | | mark(01) | → | active(01) |
| mark(s1(X)) | → | active(s1(mark(X))) | | mark(sel1(X1, X2)) | → | active(sel1(mark(X1), mark(X2))) |
| mark(quote(X)) | → | active(quote(mark(X))) | | dbl(mark(X)) | → | dbl(X) |
| dbl(active(X)) | → | dbl(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | dbls(mark(X)) | → | dbls(X) |
| dbls(active(X)) | → | dbls(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | sel(mark(X1), X2) | → | sel(X1, X2) |
| sel(X1, mark(X2)) | → | sel(X1, X2) | | sel(active(X1), X2) | → | sel(X1, X2) |
| sel(X1, active(X2)) | → | sel(X1, X2) | | indx(mark(X1), X2) | → | indx(X1, X2) |
| indx(X1, mark(X2)) | → | indx(X1, X2) | | indx(active(X1), X2) | → | indx(X1, X2) |
| indx(X1, active(X2)) | → | indx(X1, X2) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | dbl1(mark(X)) | → | dbl1(X) |
| dbl1(active(X)) | → | dbl1(X) | | s1(mark(X)) | → | s1(X) |
| s1(active(X)) | → | s1(X) | | sel1(mark(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, mark(X2)) | → | sel1(X1, X2) | | sel1(active(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, active(X2)) | → | sel1(X1, X2) | | quote(mark(X)) | → | quote(X) |
| quote(active(X)) | → | quote(X) |
Original Signature
Termination of terms over the following signature is verified: s1, dbl1, mark, dbl, from, 01, dbls, 0, sel1, s, indx, quote, active, sel, cons, nil
Strategy
The following SCCs where found
| dbls#(active(X)) → dbls#(X) | dbls#(mark(X)) → dbls#(X) |
| indx#(X1, active(X2)) → indx#(X1, X2) | indx#(active(X1), X2) → indx#(X1, X2) |
| indx#(mark(X1), X2) → indx#(X1, X2) | indx#(X1, mark(X2)) → indx#(X1, X2) |
| from#(active(X)) → from#(X) | from#(mark(X)) → from#(X) |
| quote#(mark(X)) → quote#(X) | quote#(active(X)) → quote#(X) |
| s1#(active(X)) → s1#(X) | s1#(mark(X)) → s1#(X) |
| dbl#(mark(X)) → dbl#(X) | dbl#(active(X)) → dbl#(X) |
| cons#(X1, active(X2)) → cons#(X1, X2) | cons#(mark(X1), X2) → cons#(X1, X2) |
| cons#(X1, mark(X2)) → cons#(X1, X2) | cons#(active(X1), X2) → cons#(X1, X2) |
| s#(mark(X)) → s#(X) | s#(active(X)) → s#(X) |
| dbl1#(active(X)) → dbl1#(X) | dbl1#(mark(X)) → dbl1#(X) |
| sel#(active(X1), X2) → sel#(X1, X2) | sel#(mark(X1), X2) → sel#(X1, X2) |
| sel#(X1, active(X2)) → sel#(X1, X2) | sel#(X1, mark(X2)) → sel#(X1, X2) |
| active#(sel(0, cons(X, Y))) → mark#(X) | mark#(dbls(X)) → mark#(X) |
| mark#(dbls(X)) → active#(dbls(mark(X))) | mark#(sel1(X1, X2)) → active#(sel1(mark(X1), mark(X2))) |
| mark#(01) → active#(01) | active#(dbl(s(X))) → mark#(s(s(dbl(X)))) |
| mark#(quote(X)) → mark#(X) | mark#(dbl1(X)) → active#(dbl1(mark(X))) |
| active#(dbl1(s(X))) → mark#(s1(s1(dbl1(X)))) | active#(sel(s(X), cons(Y, Z))) → mark#(sel(X, Z)) |
| mark#(nil) → active#(nil) | active#(dbls(cons(X, Y))) → mark#(cons(dbl(X), dbls(Y))) |
| active#(indx(nil, X)) → mark#(nil) | mark#(sel(X1, X2)) → mark#(X2) |
| mark#(indx(X1, X2)) → active#(indx(mark(X1), X2)) | active#(quote(dbl(X))) → mark#(dbl1(X)) |
| mark#(quote(X)) → active#(quote(mark(X))) | mark#(sel(X1, X2)) → mark#(X1) |
| active#(indx(cons(X, Y), Z)) → mark#(cons(sel(X, Z), indx(Y, Z))) | mark#(dbl1(X)) → mark#(X) |
| active#(quote(s(X))) → mark#(s1(quote(X))) | mark#(0) → active#(0) |
| active#(dbl1(0)) → mark#(01) | active#(quote(0)) → mark#(01) |
| mark#(dbl(X)) → active#(dbl(mark(X))) | mark#(sel1(X1, X2)) → mark#(X2) |
| active#(quote(sel(X, Y))) → mark#(sel1(X, Y)) | mark#(from(X)) → active#(from(X)) |
| mark#(indx(X1, X2)) → mark#(X1) | mark#(sel(X1, X2)) → active#(sel(mark(X1), mark(X2))) |
| active#(from(X)) → mark#(cons(X, from(s(X)))) | mark#(dbl(X)) → mark#(X) |
| mark#(s(X)) → active#(s(X)) | mark#(cons(X1, X2)) → active#(cons(X1, X2)) |
| mark#(s1(X)) → mark#(X) | active#(sel1(s(X), cons(Y, Z))) → mark#(sel1(X, Z)) |
| active#(dbl(0)) → mark#(0) | mark#(s1(X)) → active#(s1(mark(X))) |
| mark#(sel1(X1, X2)) → mark#(X1) | active#(dbls(nil)) → mark#(nil) |
| active#(sel1(0, cons(X, Y))) → mark#(X) |
| sel1#(X1, mark(X2)) → sel1#(X1, X2) | sel1#(mark(X1), X2) → sel1#(X1, X2) |
| sel1#(X1, active(X2)) → sel1#(X1, X2) | sel1#(active(X1), X2) → sel1#(X1, X2) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| dbl1#(active(X)) | → | dbl1#(X) | | dbl1#(mark(X)) | → | dbl1#(X) |
Rewrite Rules
| active(dbl(0)) | → | mark(0) | | active(dbl(s(X))) | → | mark(s(s(dbl(X)))) |
| active(dbls(nil)) | → | mark(nil) | | active(dbls(cons(X, Y))) | → | mark(cons(dbl(X), dbls(Y))) |
| active(sel(0, cons(X, Y))) | → | mark(X) | | active(sel(s(X), cons(Y, Z))) | → | mark(sel(X, Z)) |
| active(indx(nil, X)) | → | mark(nil) | | active(indx(cons(X, Y), Z)) | → | mark(cons(sel(X, Z), indx(Y, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(dbl1(0)) | → | mark(01) |
| active(dbl1(s(X))) | → | mark(s1(s1(dbl1(X)))) | | active(sel1(0, cons(X, Y))) | → | mark(X) |
| active(sel1(s(X), cons(Y, Z))) | → | mark(sel1(X, Z)) | | active(quote(0)) | → | mark(01) |
| active(quote(s(X))) | → | mark(s1(quote(X))) | | active(quote(dbl(X))) | → | mark(dbl1(X)) |
| active(quote(sel(X, Y))) | → | mark(sel1(X, Y)) | | mark(dbl(X)) | → | active(dbl(mark(X))) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(dbls(X)) | → | active(dbls(mark(X))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(indx(X1, X2)) | → | active(indx(mark(X1), X2)) | | mark(from(X)) | → | active(from(X)) |
| mark(dbl1(X)) | → | active(dbl1(mark(X))) | | mark(01) | → | active(01) |
| mark(s1(X)) | → | active(s1(mark(X))) | | mark(sel1(X1, X2)) | → | active(sel1(mark(X1), mark(X2))) |
| mark(quote(X)) | → | active(quote(mark(X))) | | dbl(mark(X)) | → | dbl(X) |
| dbl(active(X)) | → | dbl(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | dbls(mark(X)) | → | dbls(X) |
| dbls(active(X)) | → | dbls(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | sel(mark(X1), X2) | → | sel(X1, X2) |
| sel(X1, mark(X2)) | → | sel(X1, X2) | | sel(active(X1), X2) | → | sel(X1, X2) |
| sel(X1, active(X2)) | → | sel(X1, X2) | | indx(mark(X1), X2) | → | indx(X1, X2) |
| indx(X1, mark(X2)) | → | indx(X1, X2) | | indx(active(X1), X2) | → | indx(X1, X2) |
| indx(X1, active(X2)) | → | indx(X1, X2) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | dbl1(mark(X)) | → | dbl1(X) |
| dbl1(active(X)) | → | dbl1(X) | | s1(mark(X)) | → | s1(X) |
| s1(active(X)) | → | s1(X) | | sel1(mark(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, mark(X2)) | → | sel1(X1, X2) | | sel1(active(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, active(X2)) | → | sel1(X1, X2) | | quote(mark(X)) | → | quote(X) |
| quote(active(X)) | → | quote(X) |
Original Signature
Termination of terms over the following signature is verified: s1, dbl1, mark, dbl, from, 01, dbls, 0, sel1, s, indx, quote, active, sel, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| dbl1#(active(X)) | → | dbl1#(X) | | dbl1#(mark(X)) | → | dbl1#(X) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| s#(mark(X)) | → | s#(X) | | s#(active(X)) | → | s#(X) |
Rewrite Rules
| active(dbl(0)) | → | mark(0) | | active(dbl(s(X))) | → | mark(s(s(dbl(X)))) |
| active(dbls(nil)) | → | mark(nil) | | active(dbls(cons(X, Y))) | → | mark(cons(dbl(X), dbls(Y))) |
| active(sel(0, cons(X, Y))) | → | mark(X) | | active(sel(s(X), cons(Y, Z))) | → | mark(sel(X, Z)) |
| active(indx(nil, X)) | → | mark(nil) | | active(indx(cons(X, Y), Z)) | → | mark(cons(sel(X, Z), indx(Y, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(dbl1(0)) | → | mark(01) |
| active(dbl1(s(X))) | → | mark(s1(s1(dbl1(X)))) | | active(sel1(0, cons(X, Y))) | → | mark(X) |
| active(sel1(s(X), cons(Y, Z))) | → | mark(sel1(X, Z)) | | active(quote(0)) | → | mark(01) |
| active(quote(s(X))) | → | mark(s1(quote(X))) | | active(quote(dbl(X))) | → | mark(dbl1(X)) |
| active(quote(sel(X, Y))) | → | mark(sel1(X, Y)) | | mark(dbl(X)) | → | active(dbl(mark(X))) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(dbls(X)) | → | active(dbls(mark(X))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(indx(X1, X2)) | → | active(indx(mark(X1), X2)) | | mark(from(X)) | → | active(from(X)) |
| mark(dbl1(X)) | → | active(dbl1(mark(X))) | | mark(01) | → | active(01) |
| mark(s1(X)) | → | active(s1(mark(X))) | | mark(sel1(X1, X2)) | → | active(sel1(mark(X1), mark(X2))) |
| mark(quote(X)) | → | active(quote(mark(X))) | | dbl(mark(X)) | → | dbl(X) |
| dbl(active(X)) | → | dbl(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | dbls(mark(X)) | → | dbls(X) |
| dbls(active(X)) | → | dbls(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | sel(mark(X1), X2) | → | sel(X1, X2) |
| sel(X1, mark(X2)) | → | sel(X1, X2) | | sel(active(X1), X2) | → | sel(X1, X2) |
| sel(X1, active(X2)) | → | sel(X1, X2) | | indx(mark(X1), X2) | → | indx(X1, X2) |
| indx(X1, mark(X2)) | → | indx(X1, X2) | | indx(active(X1), X2) | → | indx(X1, X2) |
| indx(X1, active(X2)) | → | indx(X1, X2) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | dbl1(mark(X)) | → | dbl1(X) |
| dbl1(active(X)) | → | dbl1(X) | | s1(mark(X)) | → | s1(X) |
| s1(active(X)) | → | s1(X) | | sel1(mark(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, mark(X2)) | → | sel1(X1, X2) | | sel1(active(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, active(X2)) | → | sel1(X1, X2) | | quote(mark(X)) | → | quote(X) |
| quote(active(X)) | → | quote(X) |
Original Signature
Termination of terms over the following signature is verified: s1, dbl1, mark, dbl, from, 01, dbls, 0, sel1, s, indx, quote, active, sel, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| s#(mark(X)) | → | s#(X) | | s#(active(X)) | → | s#(X) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| s1#(active(X)) | → | s1#(X) | | s1#(mark(X)) | → | s1#(X) |
Rewrite Rules
| active(dbl(0)) | → | mark(0) | | active(dbl(s(X))) | → | mark(s(s(dbl(X)))) |
| active(dbls(nil)) | → | mark(nil) | | active(dbls(cons(X, Y))) | → | mark(cons(dbl(X), dbls(Y))) |
| active(sel(0, cons(X, Y))) | → | mark(X) | | active(sel(s(X), cons(Y, Z))) | → | mark(sel(X, Z)) |
| active(indx(nil, X)) | → | mark(nil) | | active(indx(cons(X, Y), Z)) | → | mark(cons(sel(X, Z), indx(Y, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(dbl1(0)) | → | mark(01) |
| active(dbl1(s(X))) | → | mark(s1(s1(dbl1(X)))) | | active(sel1(0, cons(X, Y))) | → | mark(X) |
| active(sel1(s(X), cons(Y, Z))) | → | mark(sel1(X, Z)) | | active(quote(0)) | → | mark(01) |
| active(quote(s(X))) | → | mark(s1(quote(X))) | | active(quote(dbl(X))) | → | mark(dbl1(X)) |
| active(quote(sel(X, Y))) | → | mark(sel1(X, Y)) | | mark(dbl(X)) | → | active(dbl(mark(X))) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(dbls(X)) | → | active(dbls(mark(X))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(indx(X1, X2)) | → | active(indx(mark(X1), X2)) | | mark(from(X)) | → | active(from(X)) |
| mark(dbl1(X)) | → | active(dbl1(mark(X))) | | mark(01) | → | active(01) |
| mark(s1(X)) | → | active(s1(mark(X))) | | mark(sel1(X1, X2)) | → | active(sel1(mark(X1), mark(X2))) |
| mark(quote(X)) | → | active(quote(mark(X))) | | dbl(mark(X)) | → | dbl(X) |
| dbl(active(X)) | → | dbl(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | dbls(mark(X)) | → | dbls(X) |
| dbls(active(X)) | → | dbls(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | sel(mark(X1), X2) | → | sel(X1, X2) |
| sel(X1, mark(X2)) | → | sel(X1, X2) | | sel(active(X1), X2) | → | sel(X1, X2) |
| sel(X1, active(X2)) | → | sel(X1, X2) | | indx(mark(X1), X2) | → | indx(X1, X2) |
| indx(X1, mark(X2)) | → | indx(X1, X2) | | indx(active(X1), X2) | → | indx(X1, X2) |
| indx(X1, active(X2)) | → | indx(X1, X2) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | dbl1(mark(X)) | → | dbl1(X) |
| dbl1(active(X)) | → | dbl1(X) | | s1(mark(X)) | → | s1(X) |
| s1(active(X)) | → | s1(X) | | sel1(mark(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, mark(X2)) | → | sel1(X1, X2) | | sel1(active(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, active(X2)) | → | sel1(X1, X2) | | quote(mark(X)) | → | quote(X) |
| quote(active(X)) | → | quote(X) |
Original Signature
Termination of terms over the following signature is verified: s1, dbl1, mark, dbl, from, 01, dbls, 0, sel1, s, indx, quote, active, sel, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| s1#(active(X)) | → | s1#(X) | | s1#(mark(X)) | → | s1#(X) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| cons#(X1, active(X2)) | → | cons#(X1, X2) | | cons#(mark(X1), X2) | → | cons#(X1, X2) |
| cons#(X1, mark(X2)) | → | cons#(X1, X2) | | cons#(active(X1), X2) | → | cons#(X1, X2) |
Rewrite Rules
| active(dbl(0)) | → | mark(0) | | active(dbl(s(X))) | → | mark(s(s(dbl(X)))) |
| active(dbls(nil)) | → | mark(nil) | | active(dbls(cons(X, Y))) | → | mark(cons(dbl(X), dbls(Y))) |
| active(sel(0, cons(X, Y))) | → | mark(X) | | active(sel(s(X), cons(Y, Z))) | → | mark(sel(X, Z)) |
| active(indx(nil, X)) | → | mark(nil) | | active(indx(cons(X, Y), Z)) | → | mark(cons(sel(X, Z), indx(Y, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(dbl1(0)) | → | mark(01) |
| active(dbl1(s(X))) | → | mark(s1(s1(dbl1(X)))) | | active(sel1(0, cons(X, Y))) | → | mark(X) |
| active(sel1(s(X), cons(Y, Z))) | → | mark(sel1(X, Z)) | | active(quote(0)) | → | mark(01) |
| active(quote(s(X))) | → | mark(s1(quote(X))) | | active(quote(dbl(X))) | → | mark(dbl1(X)) |
| active(quote(sel(X, Y))) | → | mark(sel1(X, Y)) | | mark(dbl(X)) | → | active(dbl(mark(X))) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(dbls(X)) | → | active(dbls(mark(X))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(indx(X1, X2)) | → | active(indx(mark(X1), X2)) | | mark(from(X)) | → | active(from(X)) |
| mark(dbl1(X)) | → | active(dbl1(mark(X))) | | mark(01) | → | active(01) |
| mark(s1(X)) | → | active(s1(mark(X))) | | mark(sel1(X1, X2)) | → | active(sel1(mark(X1), mark(X2))) |
| mark(quote(X)) | → | active(quote(mark(X))) | | dbl(mark(X)) | → | dbl(X) |
| dbl(active(X)) | → | dbl(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | dbls(mark(X)) | → | dbls(X) |
| dbls(active(X)) | → | dbls(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | sel(mark(X1), X2) | → | sel(X1, X2) |
| sel(X1, mark(X2)) | → | sel(X1, X2) | | sel(active(X1), X2) | → | sel(X1, X2) |
| sel(X1, active(X2)) | → | sel(X1, X2) | | indx(mark(X1), X2) | → | indx(X1, X2) |
| indx(X1, mark(X2)) | → | indx(X1, X2) | | indx(active(X1), X2) | → | indx(X1, X2) |
| indx(X1, active(X2)) | → | indx(X1, X2) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | dbl1(mark(X)) | → | dbl1(X) |
| dbl1(active(X)) | → | dbl1(X) | | s1(mark(X)) | → | s1(X) |
| s1(active(X)) | → | s1(X) | | sel1(mark(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, mark(X2)) | → | sel1(X1, X2) | | sel1(active(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, active(X2)) | → | sel1(X1, X2) | | quote(mark(X)) | → | quote(X) |
| quote(active(X)) | → | quote(X) |
Original Signature
Termination of terms over the following signature is verified: s1, dbl1, mark, dbl, from, 01, dbls, 0, sel1, s, indx, quote, active, sel, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | cons#(active(X1), X2) | → | cons#(X1, X2) |
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| dbl#(mark(X)) | → | dbl#(X) | | dbl#(active(X)) | → | dbl#(X) |
Rewrite Rules
| active(dbl(0)) | → | mark(0) | | active(dbl(s(X))) | → | mark(s(s(dbl(X)))) |
| active(dbls(nil)) | → | mark(nil) | | active(dbls(cons(X, Y))) | → | mark(cons(dbl(X), dbls(Y))) |
| active(sel(0, cons(X, Y))) | → | mark(X) | | active(sel(s(X), cons(Y, Z))) | → | mark(sel(X, Z)) |
| active(indx(nil, X)) | → | mark(nil) | | active(indx(cons(X, Y), Z)) | → | mark(cons(sel(X, Z), indx(Y, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(dbl1(0)) | → | mark(01) |
| active(dbl1(s(X))) | → | mark(s1(s1(dbl1(X)))) | | active(sel1(0, cons(X, Y))) | → | mark(X) |
| active(sel1(s(X), cons(Y, Z))) | → | mark(sel1(X, Z)) | | active(quote(0)) | → | mark(01) |
| active(quote(s(X))) | → | mark(s1(quote(X))) | | active(quote(dbl(X))) | → | mark(dbl1(X)) |
| active(quote(sel(X, Y))) | → | mark(sel1(X, Y)) | | mark(dbl(X)) | → | active(dbl(mark(X))) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(dbls(X)) | → | active(dbls(mark(X))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(indx(X1, X2)) | → | active(indx(mark(X1), X2)) | | mark(from(X)) | → | active(from(X)) |
| mark(dbl1(X)) | → | active(dbl1(mark(X))) | | mark(01) | → | active(01) |
| mark(s1(X)) | → | active(s1(mark(X))) | | mark(sel1(X1, X2)) | → | active(sel1(mark(X1), mark(X2))) |
| mark(quote(X)) | → | active(quote(mark(X))) | | dbl(mark(X)) | → | dbl(X) |
| dbl(active(X)) | → | dbl(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | dbls(mark(X)) | → | dbls(X) |
| dbls(active(X)) | → | dbls(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | sel(mark(X1), X2) | → | sel(X1, X2) |
| sel(X1, mark(X2)) | → | sel(X1, X2) | | sel(active(X1), X2) | → | sel(X1, X2) |
| sel(X1, active(X2)) | → | sel(X1, X2) | | indx(mark(X1), X2) | → | indx(X1, X2) |
| indx(X1, mark(X2)) | → | indx(X1, X2) | | indx(active(X1), X2) | → | indx(X1, X2) |
| indx(X1, active(X2)) | → | indx(X1, X2) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | dbl1(mark(X)) | → | dbl1(X) |
| dbl1(active(X)) | → | dbl1(X) | | s1(mark(X)) | → | s1(X) |
| s1(active(X)) | → | s1(X) | | sel1(mark(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, mark(X2)) | → | sel1(X1, X2) | | sel1(active(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, active(X2)) | → | sel1(X1, X2) | | quote(mark(X)) | → | quote(X) |
| quote(active(X)) | → | quote(X) |
Original Signature
Termination of terms over the following signature is verified: s1, dbl1, mark, dbl, from, 01, dbls, 0, sel1, s, indx, quote, active, sel, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| dbl#(mark(X)) | → | dbl#(X) | | dbl#(active(X)) | → | dbl#(X) |
Problem 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| from#(active(X)) | → | from#(X) | | from#(mark(X)) | → | from#(X) |
Rewrite Rules
| active(dbl(0)) | → | mark(0) | | active(dbl(s(X))) | → | mark(s(s(dbl(X)))) |
| active(dbls(nil)) | → | mark(nil) | | active(dbls(cons(X, Y))) | → | mark(cons(dbl(X), dbls(Y))) |
| active(sel(0, cons(X, Y))) | → | mark(X) | | active(sel(s(X), cons(Y, Z))) | → | mark(sel(X, Z)) |
| active(indx(nil, X)) | → | mark(nil) | | active(indx(cons(X, Y), Z)) | → | mark(cons(sel(X, Z), indx(Y, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(dbl1(0)) | → | mark(01) |
| active(dbl1(s(X))) | → | mark(s1(s1(dbl1(X)))) | | active(sel1(0, cons(X, Y))) | → | mark(X) |
| active(sel1(s(X), cons(Y, Z))) | → | mark(sel1(X, Z)) | | active(quote(0)) | → | mark(01) |
| active(quote(s(X))) | → | mark(s1(quote(X))) | | active(quote(dbl(X))) | → | mark(dbl1(X)) |
| active(quote(sel(X, Y))) | → | mark(sel1(X, Y)) | | mark(dbl(X)) | → | active(dbl(mark(X))) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(dbls(X)) | → | active(dbls(mark(X))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(indx(X1, X2)) | → | active(indx(mark(X1), X2)) | | mark(from(X)) | → | active(from(X)) |
| mark(dbl1(X)) | → | active(dbl1(mark(X))) | | mark(01) | → | active(01) |
| mark(s1(X)) | → | active(s1(mark(X))) | | mark(sel1(X1, X2)) | → | active(sel1(mark(X1), mark(X2))) |
| mark(quote(X)) | → | active(quote(mark(X))) | | dbl(mark(X)) | → | dbl(X) |
| dbl(active(X)) | → | dbl(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | dbls(mark(X)) | → | dbls(X) |
| dbls(active(X)) | → | dbls(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | sel(mark(X1), X2) | → | sel(X1, X2) |
| sel(X1, mark(X2)) | → | sel(X1, X2) | | sel(active(X1), X2) | → | sel(X1, X2) |
| sel(X1, active(X2)) | → | sel(X1, X2) | | indx(mark(X1), X2) | → | indx(X1, X2) |
| indx(X1, mark(X2)) | → | indx(X1, X2) | | indx(active(X1), X2) | → | indx(X1, X2) |
| indx(X1, active(X2)) | → | indx(X1, X2) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | dbl1(mark(X)) | → | dbl1(X) |
| dbl1(active(X)) | → | dbl1(X) | | s1(mark(X)) | → | s1(X) |
| s1(active(X)) | → | s1(X) | | sel1(mark(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, mark(X2)) | → | sel1(X1, X2) | | sel1(active(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, active(X2)) | → | sel1(X1, X2) | | quote(mark(X)) | → | quote(X) |
| quote(active(X)) | → | quote(X) |
Original Signature
Termination of terms over the following signature is verified: s1, dbl1, mark, dbl, from, 01, dbls, 0, sel1, s, indx, quote, active, sel, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| from#(active(X)) | → | from#(X) | | from#(mark(X)) | → | from#(X) |
Problem 9: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| dbls#(active(X)) | → | dbls#(X) | | dbls#(mark(X)) | → | dbls#(X) |
Rewrite Rules
| active(dbl(0)) | → | mark(0) | | active(dbl(s(X))) | → | mark(s(s(dbl(X)))) |
| active(dbls(nil)) | → | mark(nil) | | active(dbls(cons(X, Y))) | → | mark(cons(dbl(X), dbls(Y))) |
| active(sel(0, cons(X, Y))) | → | mark(X) | | active(sel(s(X), cons(Y, Z))) | → | mark(sel(X, Z)) |
| active(indx(nil, X)) | → | mark(nil) | | active(indx(cons(X, Y), Z)) | → | mark(cons(sel(X, Z), indx(Y, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(dbl1(0)) | → | mark(01) |
| active(dbl1(s(X))) | → | mark(s1(s1(dbl1(X)))) | | active(sel1(0, cons(X, Y))) | → | mark(X) |
| active(sel1(s(X), cons(Y, Z))) | → | mark(sel1(X, Z)) | | active(quote(0)) | → | mark(01) |
| active(quote(s(X))) | → | mark(s1(quote(X))) | | active(quote(dbl(X))) | → | mark(dbl1(X)) |
| active(quote(sel(X, Y))) | → | mark(sel1(X, Y)) | | mark(dbl(X)) | → | active(dbl(mark(X))) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(dbls(X)) | → | active(dbls(mark(X))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(indx(X1, X2)) | → | active(indx(mark(X1), X2)) | | mark(from(X)) | → | active(from(X)) |
| mark(dbl1(X)) | → | active(dbl1(mark(X))) | | mark(01) | → | active(01) |
| mark(s1(X)) | → | active(s1(mark(X))) | | mark(sel1(X1, X2)) | → | active(sel1(mark(X1), mark(X2))) |
| mark(quote(X)) | → | active(quote(mark(X))) | | dbl(mark(X)) | → | dbl(X) |
| dbl(active(X)) | → | dbl(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | dbls(mark(X)) | → | dbls(X) |
| dbls(active(X)) | → | dbls(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | sel(mark(X1), X2) | → | sel(X1, X2) |
| sel(X1, mark(X2)) | → | sel(X1, X2) | | sel(active(X1), X2) | → | sel(X1, X2) |
| sel(X1, active(X2)) | → | sel(X1, X2) | | indx(mark(X1), X2) | → | indx(X1, X2) |
| indx(X1, mark(X2)) | → | indx(X1, X2) | | indx(active(X1), X2) | → | indx(X1, X2) |
| indx(X1, active(X2)) | → | indx(X1, X2) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | dbl1(mark(X)) | → | dbl1(X) |
| dbl1(active(X)) | → | dbl1(X) | | s1(mark(X)) | → | s1(X) |
| s1(active(X)) | → | s1(X) | | sel1(mark(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, mark(X2)) | → | sel1(X1, X2) | | sel1(active(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, active(X2)) | → | sel1(X1, X2) | | quote(mark(X)) | → | quote(X) |
| quote(active(X)) | → | quote(X) |
Original Signature
Termination of terms over the following signature is verified: s1, dbl1, mark, dbl, from, 01, dbls, 0, sel1, s, indx, quote, active, sel, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| dbls#(active(X)) | → | dbls#(X) | | dbls#(mark(X)) | → | dbls#(X) |
Problem 10: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| quote#(mark(X)) | → | quote#(X) | | quote#(active(X)) | → | quote#(X) |
Rewrite Rules
| active(dbl(0)) | → | mark(0) | | active(dbl(s(X))) | → | mark(s(s(dbl(X)))) |
| active(dbls(nil)) | → | mark(nil) | | active(dbls(cons(X, Y))) | → | mark(cons(dbl(X), dbls(Y))) |
| active(sel(0, cons(X, Y))) | → | mark(X) | | active(sel(s(X), cons(Y, Z))) | → | mark(sel(X, Z)) |
| active(indx(nil, X)) | → | mark(nil) | | active(indx(cons(X, Y), Z)) | → | mark(cons(sel(X, Z), indx(Y, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(dbl1(0)) | → | mark(01) |
| active(dbl1(s(X))) | → | mark(s1(s1(dbl1(X)))) | | active(sel1(0, cons(X, Y))) | → | mark(X) |
| active(sel1(s(X), cons(Y, Z))) | → | mark(sel1(X, Z)) | | active(quote(0)) | → | mark(01) |
| active(quote(s(X))) | → | mark(s1(quote(X))) | | active(quote(dbl(X))) | → | mark(dbl1(X)) |
| active(quote(sel(X, Y))) | → | mark(sel1(X, Y)) | | mark(dbl(X)) | → | active(dbl(mark(X))) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(dbls(X)) | → | active(dbls(mark(X))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(indx(X1, X2)) | → | active(indx(mark(X1), X2)) | | mark(from(X)) | → | active(from(X)) |
| mark(dbl1(X)) | → | active(dbl1(mark(X))) | | mark(01) | → | active(01) |
| mark(s1(X)) | → | active(s1(mark(X))) | | mark(sel1(X1, X2)) | → | active(sel1(mark(X1), mark(X2))) |
| mark(quote(X)) | → | active(quote(mark(X))) | | dbl(mark(X)) | → | dbl(X) |
| dbl(active(X)) | → | dbl(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | dbls(mark(X)) | → | dbls(X) |
| dbls(active(X)) | → | dbls(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | sel(mark(X1), X2) | → | sel(X1, X2) |
| sel(X1, mark(X2)) | → | sel(X1, X2) | | sel(active(X1), X2) | → | sel(X1, X2) |
| sel(X1, active(X2)) | → | sel(X1, X2) | | indx(mark(X1), X2) | → | indx(X1, X2) |
| indx(X1, mark(X2)) | → | indx(X1, X2) | | indx(active(X1), X2) | → | indx(X1, X2) |
| indx(X1, active(X2)) | → | indx(X1, X2) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | dbl1(mark(X)) | → | dbl1(X) |
| dbl1(active(X)) | → | dbl1(X) | | s1(mark(X)) | → | s1(X) |
| s1(active(X)) | → | s1(X) | | sel1(mark(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, mark(X2)) | → | sel1(X1, X2) | | sel1(active(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, active(X2)) | → | sel1(X1, X2) | | quote(mark(X)) | → | quote(X) |
| quote(active(X)) | → | quote(X) |
Original Signature
Termination of terms over the following signature is verified: s1, dbl1, mark, dbl, from, 01, dbls, 0, sel1, s, indx, quote, active, sel, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| quote#(mark(X)) | → | quote#(X) | | quote#(active(X)) | → | quote#(X) |
Problem 11: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| sel1#(X1, mark(X2)) | → | sel1#(X1, X2) | | sel1#(mark(X1), X2) | → | sel1#(X1, X2) |
| sel1#(X1, active(X2)) | → | sel1#(X1, X2) | | sel1#(active(X1), X2) | → | sel1#(X1, X2) |
Rewrite Rules
| active(dbl(0)) | → | mark(0) | | active(dbl(s(X))) | → | mark(s(s(dbl(X)))) |
| active(dbls(nil)) | → | mark(nil) | | active(dbls(cons(X, Y))) | → | mark(cons(dbl(X), dbls(Y))) |
| active(sel(0, cons(X, Y))) | → | mark(X) | | active(sel(s(X), cons(Y, Z))) | → | mark(sel(X, Z)) |
| active(indx(nil, X)) | → | mark(nil) | | active(indx(cons(X, Y), Z)) | → | mark(cons(sel(X, Z), indx(Y, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(dbl1(0)) | → | mark(01) |
| active(dbl1(s(X))) | → | mark(s1(s1(dbl1(X)))) | | active(sel1(0, cons(X, Y))) | → | mark(X) |
| active(sel1(s(X), cons(Y, Z))) | → | mark(sel1(X, Z)) | | active(quote(0)) | → | mark(01) |
| active(quote(s(X))) | → | mark(s1(quote(X))) | | active(quote(dbl(X))) | → | mark(dbl1(X)) |
| active(quote(sel(X, Y))) | → | mark(sel1(X, Y)) | | mark(dbl(X)) | → | active(dbl(mark(X))) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(dbls(X)) | → | active(dbls(mark(X))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(indx(X1, X2)) | → | active(indx(mark(X1), X2)) | | mark(from(X)) | → | active(from(X)) |
| mark(dbl1(X)) | → | active(dbl1(mark(X))) | | mark(01) | → | active(01) |
| mark(s1(X)) | → | active(s1(mark(X))) | | mark(sel1(X1, X2)) | → | active(sel1(mark(X1), mark(X2))) |
| mark(quote(X)) | → | active(quote(mark(X))) | | dbl(mark(X)) | → | dbl(X) |
| dbl(active(X)) | → | dbl(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | dbls(mark(X)) | → | dbls(X) |
| dbls(active(X)) | → | dbls(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | sel(mark(X1), X2) | → | sel(X1, X2) |
| sel(X1, mark(X2)) | → | sel(X1, X2) | | sel(active(X1), X2) | → | sel(X1, X2) |
| sel(X1, active(X2)) | → | sel(X1, X2) | | indx(mark(X1), X2) | → | indx(X1, X2) |
| indx(X1, mark(X2)) | → | indx(X1, X2) | | indx(active(X1), X2) | → | indx(X1, X2) |
| indx(X1, active(X2)) | → | indx(X1, X2) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | dbl1(mark(X)) | → | dbl1(X) |
| dbl1(active(X)) | → | dbl1(X) | | s1(mark(X)) | → | s1(X) |
| s1(active(X)) | → | s1(X) | | sel1(mark(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, mark(X2)) | → | sel1(X1, X2) | | sel1(active(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, active(X2)) | → | sel1(X1, X2) | | quote(mark(X)) | → | quote(X) |
| quote(active(X)) | → | quote(X) |
Original Signature
Termination of terms over the following signature is verified: s1, dbl1, mark, dbl, from, 01, dbls, 0, sel1, s, indx, quote, active, sel, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| sel1#(mark(X1), X2) | → | sel1#(X1, X2) | | sel1#(active(X1), X2) | → | sel1#(X1, X2) |
Problem 12: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| sel#(active(X1), X2) | → | sel#(X1, X2) | | sel#(mark(X1), X2) | → | sel#(X1, X2) |
| sel#(X1, active(X2)) | → | sel#(X1, X2) | | sel#(X1, mark(X2)) | → | sel#(X1, X2) |
Rewrite Rules
| active(dbl(0)) | → | mark(0) | | active(dbl(s(X))) | → | mark(s(s(dbl(X)))) |
| active(dbls(nil)) | → | mark(nil) | | active(dbls(cons(X, Y))) | → | mark(cons(dbl(X), dbls(Y))) |
| active(sel(0, cons(X, Y))) | → | mark(X) | | active(sel(s(X), cons(Y, Z))) | → | mark(sel(X, Z)) |
| active(indx(nil, X)) | → | mark(nil) | | active(indx(cons(X, Y), Z)) | → | mark(cons(sel(X, Z), indx(Y, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(dbl1(0)) | → | mark(01) |
| active(dbl1(s(X))) | → | mark(s1(s1(dbl1(X)))) | | active(sel1(0, cons(X, Y))) | → | mark(X) |
| active(sel1(s(X), cons(Y, Z))) | → | mark(sel1(X, Z)) | | active(quote(0)) | → | mark(01) |
| active(quote(s(X))) | → | mark(s1(quote(X))) | | active(quote(dbl(X))) | → | mark(dbl1(X)) |
| active(quote(sel(X, Y))) | → | mark(sel1(X, Y)) | | mark(dbl(X)) | → | active(dbl(mark(X))) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(dbls(X)) | → | active(dbls(mark(X))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(indx(X1, X2)) | → | active(indx(mark(X1), X2)) | | mark(from(X)) | → | active(from(X)) |
| mark(dbl1(X)) | → | active(dbl1(mark(X))) | | mark(01) | → | active(01) |
| mark(s1(X)) | → | active(s1(mark(X))) | | mark(sel1(X1, X2)) | → | active(sel1(mark(X1), mark(X2))) |
| mark(quote(X)) | → | active(quote(mark(X))) | | dbl(mark(X)) | → | dbl(X) |
| dbl(active(X)) | → | dbl(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | dbls(mark(X)) | → | dbls(X) |
| dbls(active(X)) | → | dbls(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | sel(mark(X1), X2) | → | sel(X1, X2) |
| sel(X1, mark(X2)) | → | sel(X1, X2) | | sel(active(X1), X2) | → | sel(X1, X2) |
| sel(X1, active(X2)) | → | sel(X1, X2) | | indx(mark(X1), X2) | → | indx(X1, X2) |
| indx(X1, mark(X2)) | → | indx(X1, X2) | | indx(active(X1), X2) | → | indx(X1, X2) |
| indx(X1, active(X2)) | → | indx(X1, X2) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | dbl1(mark(X)) | → | dbl1(X) |
| dbl1(active(X)) | → | dbl1(X) | | s1(mark(X)) | → | s1(X) |
| s1(active(X)) | → | s1(X) | | sel1(mark(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, mark(X2)) | → | sel1(X1, X2) | | sel1(active(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, active(X2)) | → | sel1(X1, X2) | | quote(mark(X)) | → | quote(X) |
| quote(active(X)) | → | quote(X) |
Original Signature
Termination of terms over the following signature is verified: s1, dbl1, mark, dbl, from, 01, dbls, 0, sel1, s, indx, quote, active, sel, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| sel#(mark(X1), X2) | → | sel#(X1, X2) | | sel#(active(X1), X2) | → | sel#(X1, X2) |
Problem 16: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| sel#(X1, active(X2)) | → | sel#(X1, X2) | | sel#(X1, mark(X2)) | → | sel#(X1, X2) |
Rewrite Rules
| active(dbl(0)) | → | mark(0) | | active(dbl(s(X))) | → | mark(s(s(dbl(X)))) |
| active(dbls(nil)) | → | mark(nil) | | active(dbls(cons(X, Y))) | → | mark(cons(dbl(X), dbls(Y))) |
| active(sel(0, cons(X, Y))) | → | mark(X) | | active(sel(s(X), cons(Y, Z))) | → | mark(sel(X, Z)) |
| active(indx(nil, X)) | → | mark(nil) | | active(indx(cons(X, Y), Z)) | → | mark(cons(sel(X, Z), indx(Y, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(dbl1(0)) | → | mark(01) |
| active(dbl1(s(X))) | → | mark(s1(s1(dbl1(X)))) | | active(sel1(0, cons(X, Y))) | → | mark(X) |
| active(sel1(s(X), cons(Y, Z))) | → | mark(sel1(X, Z)) | | active(quote(0)) | → | mark(01) |
| active(quote(s(X))) | → | mark(s1(quote(X))) | | active(quote(dbl(X))) | → | mark(dbl1(X)) |
| active(quote(sel(X, Y))) | → | mark(sel1(X, Y)) | | mark(dbl(X)) | → | active(dbl(mark(X))) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(dbls(X)) | → | active(dbls(mark(X))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(indx(X1, X2)) | → | active(indx(mark(X1), X2)) | | mark(from(X)) | → | active(from(X)) |
| mark(dbl1(X)) | → | active(dbl1(mark(X))) | | mark(01) | → | active(01) |
| mark(s1(X)) | → | active(s1(mark(X))) | | mark(sel1(X1, X2)) | → | active(sel1(mark(X1), mark(X2))) |
| mark(quote(X)) | → | active(quote(mark(X))) | | dbl(mark(X)) | → | dbl(X) |
| dbl(active(X)) | → | dbl(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | dbls(mark(X)) | → | dbls(X) |
| dbls(active(X)) | → | dbls(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | sel(mark(X1), X2) | → | sel(X1, X2) |
| sel(X1, mark(X2)) | → | sel(X1, X2) | | sel(active(X1), X2) | → | sel(X1, X2) |
| sel(X1, active(X2)) | → | sel(X1, X2) | | indx(mark(X1), X2) | → | indx(X1, X2) |
| indx(X1, mark(X2)) | → | indx(X1, X2) | | indx(active(X1), X2) | → | indx(X1, X2) |
| indx(X1, active(X2)) | → | indx(X1, X2) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | dbl1(mark(X)) | → | dbl1(X) |
| dbl1(active(X)) | → | dbl1(X) | | s1(mark(X)) | → | s1(X) |
| s1(active(X)) | → | s1(X) | | sel1(mark(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, mark(X2)) | → | sel1(X1, X2) | | sel1(active(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, active(X2)) | → | sel1(X1, X2) | | quote(mark(X)) | → | quote(X) |
| quote(active(X)) | → | quote(X) |
Original Signature
Termination of terms over the following signature is verified: s1, dbl1, mark, dbl, from, 01, dbls, 0, sel1, s, indx, quote, active, sel, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- 01: 0
- active(x): 2x
- cons(x,y): 0
- dbl(x): 0
- dbl1(x): 0
- dbls(x): 0
- from(x): 0
- indx(x,y): 0
- mark(x): x + 1
- nil: 0
- quote(x): 0
- s(x): 0
- s1(x): 0
- sel(x,y): 0
- sel#(x,y): 2y + 3x
- sel1(x,y): 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:
| sel#(X1, mark(X2)) | → | sel#(X1, X2) |
Problem 19: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| sel#(X1, active(X2)) | → | sel#(X1, X2) |
Rewrite Rules
| active(dbl(0)) | → | mark(0) | | active(dbl(s(X))) | → | mark(s(s(dbl(X)))) |
| active(dbls(nil)) | → | mark(nil) | | active(dbls(cons(X, Y))) | → | mark(cons(dbl(X), dbls(Y))) |
| active(sel(0, cons(X, Y))) | → | mark(X) | | active(sel(s(X), cons(Y, Z))) | → | mark(sel(X, Z)) |
| active(indx(nil, X)) | → | mark(nil) | | active(indx(cons(X, Y), Z)) | → | mark(cons(sel(X, Z), indx(Y, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(dbl1(0)) | → | mark(01) |
| active(dbl1(s(X))) | → | mark(s1(s1(dbl1(X)))) | | active(sel1(0, cons(X, Y))) | → | mark(X) |
| active(sel1(s(X), cons(Y, Z))) | → | mark(sel1(X, Z)) | | active(quote(0)) | → | mark(01) |
| active(quote(s(X))) | → | mark(s1(quote(X))) | | active(quote(dbl(X))) | → | mark(dbl1(X)) |
| active(quote(sel(X, Y))) | → | mark(sel1(X, Y)) | | mark(dbl(X)) | → | active(dbl(mark(X))) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(dbls(X)) | → | active(dbls(mark(X))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(indx(X1, X2)) | → | active(indx(mark(X1), X2)) | | mark(from(X)) | → | active(from(X)) |
| mark(dbl1(X)) | → | active(dbl1(mark(X))) | | mark(01) | → | active(01) |
| mark(s1(X)) | → | active(s1(mark(X))) | | mark(sel1(X1, X2)) | → | active(sel1(mark(X1), mark(X2))) |
| mark(quote(X)) | → | active(quote(mark(X))) | | dbl(mark(X)) | → | dbl(X) |
| dbl(active(X)) | → | dbl(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | dbls(mark(X)) | → | dbls(X) |
| dbls(active(X)) | → | dbls(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | sel(mark(X1), X2) | → | sel(X1, X2) |
| sel(X1, mark(X2)) | → | sel(X1, X2) | | sel(active(X1), X2) | → | sel(X1, X2) |
| sel(X1, active(X2)) | → | sel(X1, X2) | | indx(mark(X1), X2) | → | indx(X1, X2) |
| indx(X1, mark(X2)) | → | indx(X1, X2) | | indx(active(X1), X2) | → | indx(X1, X2) |
| indx(X1, active(X2)) | → | indx(X1, X2) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | dbl1(mark(X)) | → | dbl1(X) |
| dbl1(active(X)) | → | dbl1(X) | | s1(mark(X)) | → | s1(X) |
| s1(active(X)) | → | s1(X) | | sel1(mark(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, mark(X2)) | → | sel1(X1, X2) | | sel1(active(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, active(X2)) | → | sel1(X1, X2) | | quote(mark(X)) | → | quote(X) |
| quote(active(X)) | → | quote(X) |
Original Signature
Termination of terms over the following signature is verified: s1, dbl1, mark, dbl, from, 01, dbls, 0, sel1, s, indx, quote, active, sel, cons, nil
Strategy
Polynomial Interpretation
- 0: 0
- 01: 0
- active(x): 2x + 1
- cons(x,y): 0
- dbl(x): 0
- dbl1(x): 0
- dbls(x): 0
- from(x): 0
- indx(x,y): 0
- mark(x): 0
- nil: 0
- quote(x): 0
- s(x): 0
- s1(x): 0
- sel(x,y): 0
- sel#(x,y): 2y + x
- sel1(x,y): 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:
| sel#(X1, active(X2)) | → | sel#(X1, X2) |
Problem 13: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| indx#(X1, active(X2)) | → | indx#(X1, X2) | | indx#(active(X1), X2) | → | indx#(X1, X2) |
| indx#(mark(X1), X2) | → | indx#(X1, X2) | | indx#(X1, mark(X2)) | → | indx#(X1, X2) |
Rewrite Rules
| active(dbl(0)) | → | mark(0) | | active(dbl(s(X))) | → | mark(s(s(dbl(X)))) |
| active(dbls(nil)) | → | mark(nil) | | active(dbls(cons(X, Y))) | → | mark(cons(dbl(X), dbls(Y))) |
| active(sel(0, cons(X, Y))) | → | mark(X) | | active(sel(s(X), cons(Y, Z))) | → | mark(sel(X, Z)) |
| active(indx(nil, X)) | → | mark(nil) | | active(indx(cons(X, Y), Z)) | → | mark(cons(sel(X, Z), indx(Y, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(dbl1(0)) | → | mark(01) |
| active(dbl1(s(X))) | → | mark(s1(s1(dbl1(X)))) | | active(sel1(0, cons(X, Y))) | → | mark(X) |
| active(sel1(s(X), cons(Y, Z))) | → | mark(sel1(X, Z)) | | active(quote(0)) | → | mark(01) |
| active(quote(s(X))) | → | mark(s1(quote(X))) | | active(quote(dbl(X))) | → | mark(dbl1(X)) |
| active(quote(sel(X, Y))) | → | mark(sel1(X, Y)) | | mark(dbl(X)) | → | active(dbl(mark(X))) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(dbls(X)) | → | active(dbls(mark(X))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(indx(X1, X2)) | → | active(indx(mark(X1), X2)) | | mark(from(X)) | → | active(from(X)) |
| mark(dbl1(X)) | → | active(dbl1(mark(X))) | | mark(01) | → | active(01) |
| mark(s1(X)) | → | active(s1(mark(X))) | | mark(sel1(X1, X2)) | → | active(sel1(mark(X1), mark(X2))) |
| mark(quote(X)) | → | active(quote(mark(X))) | | dbl(mark(X)) | → | dbl(X) |
| dbl(active(X)) | → | dbl(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | dbls(mark(X)) | → | dbls(X) |
| dbls(active(X)) | → | dbls(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | sel(mark(X1), X2) | → | sel(X1, X2) |
| sel(X1, mark(X2)) | → | sel(X1, X2) | | sel(active(X1), X2) | → | sel(X1, X2) |
| sel(X1, active(X2)) | → | sel(X1, X2) | | indx(mark(X1), X2) | → | indx(X1, X2) |
| indx(X1, mark(X2)) | → | indx(X1, X2) | | indx(active(X1), X2) | → | indx(X1, X2) |
| indx(X1, active(X2)) | → | indx(X1, X2) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | dbl1(mark(X)) | → | dbl1(X) |
| dbl1(active(X)) | → | dbl1(X) | | s1(mark(X)) | → | s1(X) |
| s1(active(X)) | → | s1(X) | | sel1(mark(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, mark(X2)) | → | sel1(X1, X2) | | sel1(active(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, active(X2)) | → | sel1(X1, X2) | | quote(mark(X)) | → | quote(X) |
| quote(active(X)) | → | quote(X) |
Original Signature
Termination of terms over the following signature is verified: s1, dbl1, mark, dbl, from, 01, dbls, 0, sel1, s, indx, quote, active, sel, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| indx#(active(X1), X2) | → | indx#(X1, X2) | | indx#(mark(X1), X2) | → | indx#(X1, X2) |
Problem 17: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| indx#(X1, active(X2)) | → | indx#(X1, X2) | | indx#(X1, mark(X2)) | → | indx#(X1, X2) |
Rewrite Rules
| active(dbl(0)) | → | mark(0) | | active(dbl(s(X))) | → | mark(s(s(dbl(X)))) |
| active(dbls(nil)) | → | mark(nil) | | active(dbls(cons(X, Y))) | → | mark(cons(dbl(X), dbls(Y))) |
| active(sel(0, cons(X, Y))) | → | mark(X) | | active(sel(s(X), cons(Y, Z))) | → | mark(sel(X, Z)) |
| active(indx(nil, X)) | → | mark(nil) | | active(indx(cons(X, Y), Z)) | → | mark(cons(sel(X, Z), indx(Y, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(dbl1(0)) | → | mark(01) |
| active(dbl1(s(X))) | → | mark(s1(s1(dbl1(X)))) | | active(sel1(0, cons(X, Y))) | → | mark(X) |
| active(sel1(s(X), cons(Y, Z))) | → | mark(sel1(X, Z)) | | active(quote(0)) | → | mark(01) |
| active(quote(s(X))) | → | mark(s1(quote(X))) | | active(quote(dbl(X))) | → | mark(dbl1(X)) |
| active(quote(sel(X, Y))) | → | mark(sel1(X, Y)) | | mark(dbl(X)) | → | active(dbl(mark(X))) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(dbls(X)) | → | active(dbls(mark(X))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(indx(X1, X2)) | → | active(indx(mark(X1), X2)) | | mark(from(X)) | → | active(from(X)) |
| mark(dbl1(X)) | → | active(dbl1(mark(X))) | | mark(01) | → | active(01) |
| mark(s1(X)) | → | active(s1(mark(X))) | | mark(sel1(X1, X2)) | → | active(sel1(mark(X1), mark(X2))) |
| mark(quote(X)) | → | active(quote(mark(X))) | | dbl(mark(X)) | → | dbl(X) |
| dbl(active(X)) | → | dbl(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | dbls(mark(X)) | → | dbls(X) |
| dbls(active(X)) | → | dbls(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | sel(mark(X1), X2) | → | sel(X1, X2) |
| sel(X1, mark(X2)) | → | sel(X1, X2) | | sel(active(X1), X2) | → | sel(X1, X2) |
| sel(X1, active(X2)) | → | sel(X1, X2) | | indx(mark(X1), X2) | → | indx(X1, X2) |
| indx(X1, mark(X2)) | → | indx(X1, X2) | | indx(active(X1), X2) | → | indx(X1, X2) |
| indx(X1, active(X2)) | → | indx(X1, X2) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | dbl1(mark(X)) | → | dbl1(X) |
| dbl1(active(X)) | → | dbl1(X) | | s1(mark(X)) | → | s1(X) |
| s1(active(X)) | → | s1(X) | | sel1(mark(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, mark(X2)) | → | sel1(X1, X2) | | sel1(active(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, active(X2)) | → | sel1(X1, X2) | | quote(mark(X)) | → | quote(X) |
| quote(active(X)) | → | quote(X) |
Original Signature
Termination of terms over the following signature is verified: s1, dbl1, mark, dbl, from, 01, dbls, 0, sel1, s, indx, quote, active, sel, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- 01: 0
- active(x): 2x + 1
- cons(x,y): 0
- dbl(x): 0
- dbl1(x): 0
- dbls(x): 0
- from(x): 0
- indx(x,y): 0
- indx#(x,y): 2y + x
- mark(x): x
- nil: 0
- quote(x): 0
- s(x): 0
- s1(x): 0
- sel(x,y): 0
- sel1(x,y): 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:
| indx#(X1, active(X2)) | → | indx#(X1, X2) |
Problem 18: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| indx#(X1, mark(X2)) | → | indx#(X1, X2) |
Rewrite Rules
| active(dbl(0)) | → | mark(0) | | active(dbl(s(X))) | → | mark(s(s(dbl(X)))) |
| active(dbls(nil)) | → | mark(nil) | | active(dbls(cons(X, Y))) | → | mark(cons(dbl(X), dbls(Y))) |
| active(sel(0, cons(X, Y))) | → | mark(X) | | active(sel(s(X), cons(Y, Z))) | → | mark(sel(X, Z)) |
| active(indx(nil, X)) | → | mark(nil) | | active(indx(cons(X, Y), Z)) | → | mark(cons(sel(X, Z), indx(Y, Z))) |
| active(from(X)) | → | mark(cons(X, from(s(X)))) | | active(dbl1(0)) | → | mark(01) |
| active(dbl1(s(X))) | → | mark(s1(s1(dbl1(X)))) | | active(sel1(0, cons(X, Y))) | → | mark(X) |
| active(sel1(s(X), cons(Y, Z))) | → | mark(sel1(X, Z)) | | active(quote(0)) | → | mark(01) |
| active(quote(s(X))) | → | mark(s1(quote(X))) | | active(quote(dbl(X))) | → | mark(dbl1(X)) |
| active(quote(sel(X, Y))) | → | mark(sel1(X, Y)) | | mark(dbl(X)) | → | active(dbl(mark(X))) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(X)) |
| mark(dbls(X)) | → | active(dbls(mark(X))) | | mark(nil) | → | active(nil) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(sel(X1, X2)) | → | active(sel(mark(X1), mark(X2))) |
| mark(indx(X1, X2)) | → | active(indx(mark(X1), X2)) | | mark(from(X)) | → | active(from(X)) |
| mark(dbl1(X)) | → | active(dbl1(mark(X))) | | mark(01) | → | active(01) |
| mark(s1(X)) | → | active(s1(mark(X))) | | mark(sel1(X1, X2)) | → | active(sel1(mark(X1), mark(X2))) |
| mark(quote(X)) | → | active(quote(mark(X))) | | dbl(mark(X)) | → | dbl(X) |
| dbl(active(X)) | → | dbl(X) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | dbls(mark(X)) | → | dbls(X) |
| dbls(active(X)) | → | dbls(X) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | sel(mark(X1), X2) | → | sel(X1, X2) |
| sel(X1, mark(X2)) | → | sel(X1, X2) | | sel(active(X1), X2) | → | sel(X1, X2) |
| sel(X1, active(X2)) | → | sel(X1, X2) | | indx(mark(X1), X2) | → | indx(X1, X2) |
| indx(X1, mark(X2)) | → | indx(X1, X2) | | indx(active(X1), X2) | → | indx(X1, X2) |
| indx(X1, active(X2)) | → | indx(X1, X2) | | from(mark(X)) | → | from(X) |
| from(active(X)) | → | from(X) | | dbl1(mark(X)) | → | dbl1(X) |
| dbl1(active(X)) | → | dbl1(X) | | s1(mark(X)) | → | s1(X) |
| s1(active(X)) | → | s1(X) | | sel1(mark(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, mark(X2)) | → | sel1(X1, X2) | | sel1(active(X1), X2) | → | sel1(X1, X2) |
| sel1(X1, active(X2)) | → | sel1(X1, X2) | | quote(mark(X)) | → | quote(X) |
| quote(active(X)) | → | quote(X) |
Original Signature
Termination of terms over the following signature is verified: s1, dbl1, mark, dbl, from, 01, dbls, 0, sel1, s, indx, quote, active, sel, cons, nil
Strategy
Polynomial Interpretation
- 0: 0
- 01: 0
- active(x): 0
- cons(x,y): 0
- dbl(x): 0
- dbl1(x): 0
- dbls(x): 0
- from(x): 0
- indx(x,y): 0
- indx#(x,y): y + x + 1
- mark(x): x + 2
- nil: 0
- quote(x): 0
- s(x): 0
- s1(x): 0
- sel(x,y): 0
- sel1(x,y): 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:
| indx#(X1, mark(X2)) | → | indx#(X1, X2) |