TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60001 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (7901ms).
| – Problem 2 was processed with processor SubtermCriterion (2ms).
| – Problem 3 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (4ms), PolynomialLinearRange4iUR (3333ms), DependencyGraph (6ms), PolynomialLinearRange4iUR (7549ms), DependencyGraph (4ms), PolynomialLinearRange8NegiUR (30000ms), ReductionPairSAT (7887ms), DependencyGraph (20ms), SizeChangePrinciple (timeout)].
| – Problem 4 was processed with processor SubtermCriterion (1ms).
| – Problem 5 was processed with processor SubtermCriterion (3ms).
| – Problem 6 was processed with processor SubtermCriterion (1ms).
| – Problem 7 was processed with processor SubtermCriterion (1ms).
| – Problem 8 was processed with processor SubtermCriterion (1ms).
| – Problem 9 was processed with processor SubtermCriterion (3ms).
| | – Problem 16 was processed with processor PolynomialLinearRange4iUR (77ms).
| – Problem 10 was processed with processor SubtermCriterion (2ms).
| – Problem 11 was processed with processor SubtermCriterion (2ms).
| – Problem 12 was processed with processor SubtermCriterion (3ms).
| – Problem 13 was processed with processor SubtermCriterion (1ms).
| | – Problem 17 was processed with processor PolynomialLinearRange4iUR (57ms).
| – Problem 14 was processed with processor SubtermCriterion (2ms).
| – Problem 15 was processed with processor SubtermCriterion (1ms).
The following open problems remain:
Open Dependency Pair Problem 3
Dependency Pairs
| top#(mark(X)) | → | top#(proper(X)) | | top#(ok(X)) | → | top#(active(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)) | | active(dbl(X)) | → | dbl(active(X)) |
| active(dbls(X)) | → | dbls(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(indx(X1, X2)) | → | indx(active(X1), X2) |
| active(dbl1(X)) | → | dbl1(active(X)) | | active(s1(X)) | → | s1(active(X)) |
| active(sel1(X1, X2)) | → | sel1(active(X1), X2) | | active(sel1(X1, X2)) | → | sel1(X1, active(X2)) |
| active(quote(X)) | → | quote(active(X)) | | dbl(mark(X)) | → | mark(dbl(X)) |
| dbls(mark(X)) | → | mark(dbls(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | indx(mark(X1), X2) | → | mark(indx(X1, X2)) |
| dbl1(mark(X)) | → | mark(dbl1(X)) | | s1(mark(X)) | → | mark(s1(X)) |
| sel1(mark(X1), X2) | → | mark(sel1(X1, X2)) | | sel1(X1, mark(X2)) | → | mark(sel1(X1, X2)) |
| quote(mark(X)) | → | mark(quote(X)) | | proper(dbl(X)) | → | dbl(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(dbls(X)) | → | dbls(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(indx(X1, X2)) | → | indx(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(dbl1(X)) | → | dbl1(proper(X)) | | proper(01) | → | ok(01) |
| proper(s1(X)) | → | s1(proper(X)) | | proper(sel1(X1, X2)) | → | sel1(proper(X1), proper(X2)) |
| proper(quote(X)) | → | quote(proper(X)) | | dbl(ok(X)) | → | ok(dbl(X)) |
| s(ok(X)) | → | ok(s(X)) | | dbls(ok(X)) | → | ok(dbls(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| indx(ok(X1), ok(X2)) | → | ok(indx(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| dbl1(ok(X)) | → | ok(dbl1(X)) | | s1(ok(X)) | → | ok(s1(X)) |
| sel1(ok(X1), ok(X2)) | → | ok(sel1(X1, X2)) | | quote(ok(X)) | → | ok(quote(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(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, ok, proper, sel, top, nil, cons
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| proper#(sel1(X1, X2)) | → | proper#(X1) | | proper#(cons(X1, X2)) | → | proper#(X1) |
| top#(ok(X)) | → | top#(active(X)) | | dbls#(ok(X)) | → | dbls#(X) |
| active#(sel1(X1, X2)) | → | active#(X2) | | proper#(s1(X)) | → | proper#(X) |
| active#(dbl(s(X))) | → | s#(dbl(X)) | | active#(sel1(X1, X2)) | → | active#(X1) |
| cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) | | active#(dbls(cons(X, Y))) | → | cons#(dbl(X), dbls(Y)) |
| dbls#(mark(X)) | → | dbls#(X) | | from#(ok(X)) | → | from#(X) |
| active#(s1(X)) | → | active#(X) | | active#(sel(X1, X2)) | → | active#(X2) |
| indx#(ok(X1), ok(X2)) | → | indx#(X1, X2) | | proper#(quote(X)) | → | quote#(proper(X)) |
| active#(s1(X)) | → | s1#(active(X)) | | sel1#(ok(X1), ok(X2)) | → | sel1#(X1, X2) |
| active#(dbl(s(X))) | → | dbl#(X) | | proper#(indx(X1, X2)) | → | proper#(X1) |
| top#(mark(X)) | → | proper#(X) | | indx#(mark(X1), X2) | → | indx#(X1, X2) |
| proper#(from(X)) | → | proper#(X) | | active#(quote(X)) | → | quote#(active(X)) |
| top#(mark(X)) | → | top#(proper(X)) | | active#(sel(s(X), cons(Y, Z))) | → | sel#(X, Z) |
| proper#(cons(X1, X2)) | → | proper#(X2) | | active#(dbl(s(X))) | → | s#(s(dbl(X))) |
| s1#(ok(X)) | → | s1#(X) | | active#(quote(s(X))) | → | quote#(X) |
| sel#(X1, mark(X2)) | → | sel#(X1, X2) | | dbl1#(mark(X)) | → | dbl1#(X) |
| active#(indx(cons(X, Y), Z)) | → | cons#(sel(X, Z), indx(Y, Z)) | | dbl1#(ok(X)) | → | dbl1#(X) |
| active#(from(X)) | → | s#(X) | | proper#(s(X)) | → | proper#(X) |
| quote#(mark(X)) | → | quote#(X) | | active#(dbl1(s(X))) | → | s1#(dbl1(X)) |
| active#(dbl1(X)) | → | active#(X) | | sel1#(mark(X1), X2) | → | sel1#(X1, X2) |
| proper#(sel1(X1, X2)) | → | proper#(X2) | | sel#(ok(X1), ok(X2)) | → | sel#(X1, X2) |
| active#(dbls(X)) | → | active#(X) | | proper#(quote(X)) | → | proper#(X) |
| active#(dbls(X)) | → | dbls#(active(X)) | | active#(quote(s(X))) | → | s1#(quote(X)) |
| sel#(mark(X1), X2) | → | sel#(X1, X2) | | active#(dbl1(s(X))) | → | s1#(s1(dbl1(X))) |
| active#(dbls(cons(X, Y))) | → | dbls#(Y) | | proper#(indx(X1, X2)) | → | proper#(X2) |
| active#(sel1(X1, X2)) | → | sel1#(X1, active(X2)) | | active#(dbl1(s(X))) | → | dbl1#(X) |
| active#(indx(cons(X, Y), Z)) | → | indx#(Y, Z) | | top#(ok(X)) | → | active#(X) |
| proper#(sel(X1, X2)) | → | sel#(proper(X1), proper(X2)) | | active#(dbl1(X)) | → | dbl1#(active(X)) |
| sel1#(X1, mark(X2)) | → | sel1#(X1, X2) | | quote#(ok(X)) | → | quote#(X) |
| active#(sel1(s(X), cons(Y, Z))) | → | sel1#(X, Z) | | active#(quote(sel(X, Y))) | → | sel1#(X, Y) |
| active#(sel(X1, X2)) | → | active#(X1) | | active#(indx(cons(X, Y), Z)) | → | sel#(X, Z) |
| proper#(s1(X)) | → | s1#(proper(X)) | | active#(from(X)) | → | cons#(X, from(s(X))) |
| active#(dbl(X)) | → | active#(X) | | proper#(from(X)) | → | from#(proper(X)) |
| proper#(sel(X1, X2)) | → | proper#(X2) | | active#(dbls(cons(X, Y))) | → | dbl#(X) |
| proper#(indx(X1, X2)) | → | indx#(proper(X1), proper(X2)) | | proper#(dbls(X)) | → | dbls#(proper(X)) |
| active#(sel1(X1, X2)) | → | sel1#(active(X1), X2) | | active#(sel(X1, X2)) | → | sel#(X1, active(X2)) |
| active#(sel(X1, X2)) | → | sel#(active(X1), X2) | | s1#(mark(X)) | → | s1#(X) |
| active#(indx(X1, X2)) | → | active#(X1) | | proper#(dbl(X)) | → | proper#(X) |
| dbl#(mark(X)) | → | dbl#(X) | | active#(dbl(X)) | → | dbl#(active(X)) |
| s#(ok(X)) | → | s#(X) | | proper#(sel1(X1, X2)) | → | sel1#(proper(X1), proper(X2)) |
| proper#(sel(X1, X2)) | → | proper#(X1) | | dbl#(ok(X)) | → | dbl#(X) |
| proper#(cons(X1, X2)) | → | cons#(proper(X1), proper(X2)) | | proper#(dbl(X)) | → | dbl#(proper(X)) |
| proper#(dbl1(X)) | → | proper#(X) | | active#(quote(dbl(X))) | → | dbl1#(X) |
| proper#(s(X)) | → | s#(proper(X)) | | proper#(dbls(X)) | → | proper#(X) |
| active#(quote(X)) | → | active#(X) | | proper#(dbl1(X)) | → | dbl1#(proper(X)) |
| active#(indx(X1, X2)) | → | indx#(active(X1), X2) | | active#(from(X)) | → | from#(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)) | | active(dbl(X)) | → | dbl(active(X)) |
| active(dbls(X)) | → | dbls(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(indx(X1, X2)) | → | indx(active(X1), X2) |
| active(dbl1(X)) | → | dbl1(active(X)) | | active(s1(X)) | → | s1(active(X)) |
| active(sel1(X1, X2)) | → | sel1(active(X1), X2) | | active(sel1(X1, X2)) | → | sel1(X1, active(X2)) |
| active(quote(X)) | → | quote(active(X)) | | dbl(mark(X)) | → | mark(dbl(X)) |
| dbls(mark(X)) | → | mark(dbls(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | indx(mark(X1), X2) | → | mark(indx(X1, X2)) |
| dbl1(mark(X)) | → | mark(dbl1(X)) | | s1(mark(X)) | → | mark(s1(X)) |
| sel1(mark(X1), X2) | → | mark(sel1(X1, X2)) | | sel1(X1, mark(X2)) | → | mark(sel1(X1, X2)) |
| quote(mark(X)) | → | mark(quote(X)) | | proper(dbl(X)) | → | dbl(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(dbls(X)) | → | dbls(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(indx(X1, X2)) | → | indx(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(dbl1(X)) | → | dbl1(proper(X)) | | proper(01) | → | ok(01) |
| proper(s1(X)) | → | s1(proper(X)) | | proper(sel1(X1, X2)) | → | sel1(proper(X1), proper(X2)) |
| proper(quote(X)) | → | quote(proper(X)) | | dbl(ok(X)) | → | ok(dbl(X)) |
| s(ok(X)) | → | ok(s(X)) | | dbls(ok(X)) | → | ok(dbls(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| indx(ok(X1), ok(X2)) | → | ok(indx(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| dbl1(ok(X)) | → | ok(dbl1(X)) | | s1(ok(X)) | → | ok(s1(X)) |
| sel1(ok(X1), ok(X2)) | → | ok(sel1(X1, X2)) | | quote(ok(X)) | → | ok(quote(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(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, ok, proper, sel, cons, nil, top
Strategy
The following SCCs where found
| sel#(mark(X1), X2) → sel#(X1, X2) | sel#(ok(X1), ok(X2)) → sel#(X1, X2) |
| sel#(X1, mark(X2)) → sel#(X1, X2) |
| dbl#(ok(X)) → dbl#(X) | dbl#(mark(X)) → dbl#(X) |
| dbl1#(ok(X)) → dbl1#(X) | dbl1#(mark(X)) → dbl1#(X) |
| sel1#(X1, mark(X2)) → sel1#(X1, X2) | sel1#(mark(X1), X2) → sel1#(X1, X2) |
| sel1#(ok(X1), ok(X2)) → sel1#(X1, X2) |
| proper#(sel1(X1, X2)) → proper#(X1) | proper#(cons(X1, X2)) → proper#(X1) |
| proper#(cons(X1, X2)) → proper#(X2) | proper#(s1(X)) → proper#(X) |
| proper#(dbl(X)) → proper#(X) | proper#(indx(X1, X2)) → proper#(X2) |
| proper#(sel(X1, X2)) → proper#(X1) | proper#(s(X)) → proper#(X) |
| proper#(dbl1(X)) → proper#(X) | proper#(sel1(X1, X2)) → proper#(X2) |
| proper#(dbls(X)) → proper#(X) | proper#(quote(X)) → proper#(X) |
| proper#(sel(X1, X2)) → proper#(X2) | proper#(indx(X1, X2)) → proper#(X1) |
| proper#(from(X)) → proper#(X) |
| cons#(ok(X1), ok(X2)) → cons#(X1, X2) |
| dbls#(ok(X)) → dbls#(X) | dbls#(mark(X)) → dbls#(X) |
| active#(dbl1(X)) → active#(X) | active#(sel(X1, X2)) → active#(X2) |
| active#(s1(X)) → active#(X) | active#(sel1(X1, X2)) → active#(X2) |
| active#(indx(X1, X2)) → active#(X1) | active#(sel(X1, X2)) → active#(X1) |
| active#(dbl(X)) → active#(X) | active#(dbls(X)) → active#(X) |
| active#(sel1(X1, X2)) → active#(X1) | active#(quote(X)) → active#(X) |
| indx#(ok(X1), ok(X2)) → indx#(X1, X2) | indx#(mark(X1), X2) → indx#(X1, X2) |
| s1#(mark(X)) → s1#(X) | s1#(ok(X)) → s1#(X) |
| quote#(ok(X)) → quote#(X) | quote#(mark(X)) → quote#(X) |
| top#(mark(X)) → top#(proper(X)) | top#(ok(X)) → top#(active(X)) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| dbl1#(ok(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)) | | active(dbl(X)) | → | dbl(active(X)) |
| active(dbls(X)) | → | dbls(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(indx(X1, X2)) | → | indx(active(X1), X2) |
| active(dbl1(X)) | → | dbl1(active(X)) | | active(s1(X)) | → | s1(active(X)) |
| active(sel1(X1, X2)) | → | sel1(active(X1), X2) | | active(sel1(X1, X2)) | → | sel1(X1, active(X2)) |
| active(quote(X)) | → | quote(active(X)) | | dbl(mark(X)) | → | mark(dbl(X)) |
| dbls(mark(X)) | → | mark(dbls(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | indx(mark(X1), X2) | → | mark(indx(X1, X2)) |
| dbl1(mark(X)) | → | mark(dbl1(X)) | | s1(mark(X)) | → | mark(s1(X)) |
| sel1(mark(X1), X2) | → | mark(sel1(X1, X2)) | | sel1(X1, mark(X2)) | → | mark(sel1(X1, X2)) |
| quote(mark(X)) | → | mark(quote(X)) | | proper(dbl(X)) | → | dbl(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(dbls(X)) | → | dbls(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(indx(X1, X2)) | → | indx(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(dbl1(X)) | → | dbl1(proper(X)) | | proper(01) | → | ok(01) |
| proper(s1(X)) | → | s1(proper(X)) | | proper(sel1(X1, X2)) | → | sel1(proper(X1), proper(X2)) |
| proper(quote(X)) | → | quote(proper(X)) | | dbl(ok(X)) | → | ok(dbl(X)) |
| s(ok(X)) | → | ok(s(X)) | | dbls(ok(X)) | → | ok(dbls(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| indx(ok(X1), ok(X2)) | → | ok(indx(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| dbl1(ok(X)) | → | ok(dbl1(X)) | | s1(ok(X)) | → | ok(s1(X)) |
| sel1(ok(X1), ok(X2)) | → | ok(sel1(X1, X2)) | | quote(ok(X)) | → | ok(quote(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(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, ok, proper, sel, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| dbl1#(ok(X)) | → | dbl1#(X) | | dbl1#(mark(X)) | → | dbl1#(X) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| indx#(ok(X1), ok(X2)) | → | indx#(X1, X2) | | indx#(mark(X1), 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)) | | active(dbl(X)) | → | dbl(active(X)) |
| active(dbls(X)) | → | dbls(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(indx(X1, X2)) | → | indx(active(X1), X2) |
| active(dbl1(X)) | → | dbl1(active(X)) | | active(s1(X)) | → | s1(active(X)) |
| active(sel1(X1, X2)) | → | sel1(active(X1), X2) | | active(sel1(X1, X2)) | → | sel1(X1, active(X2)) |
| active(quote(X)) | → | quote(active(X)) | | dbl(mark(X)) | → | mark(dbl(X)) |
| dbls(mark(X)) | → | mark(dbls(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | indx(mark(X1), X2) | → | mark(indx(X1, X2)) |
| dbl1(mark(X)) | → | mark(dbl1(X)) | | s1(mark(X)) | → | mark(s1(X)) |
| sel1(mark(X1), X2) | → | mark(sel1(X1, X2)) | | sel1(X1, mark(X2)) | → | mark(sel1(X1, X2)) |
| quote(mark(X)) | → | mark(quote(X)) | | proper(dbl(X)) | → | dbl(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(dbls(X)) | → | dbls(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(indx(X1, X2)) | → | indx(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(dbl1(X)) | → | dbl1(proper(X)) | | proper(01) | → | ok(01) |
| proper(s1(X)) | → | s1(proper(X)) | | proper(sel1(X1, X2)) | → | sel1(proper(X1), proper(X2)) |
| proper(quote(X)) | → | quote(proper(X)) | | dbl(ok(X)) | → | ok(dbl(X)) |
| s(ok(X)) | → | ok(s(X)) | | dbls(ok(X)) | → | ok(dbls(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| indx(ok(X1), ok(X2)) | → | ok(indx(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| dbl1(ok(X)) | → | ok(dbl1(X)) | | s1(ok(X)) | → | ok(s1(X)) |
| sel1(ok(X1), ok(X2)) | → | ok(sel1(X1, X2)) | | quote(ok(X)) | → | ok(quote(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(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, ok, proper, sel, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| indx#(ok(X1), ok(X2)) | → | indx#(X1, X2) | | indx#(mark(X1), X2) | → | indx#(X1, X2) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| s1#(mark(X)) | → | s1#(X) | | s1#(ok(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)) | | active(dbl(X)) | → | dbl(active(X)) |
| active(dbls(X)) | → | dbls(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(indx(X1, X2)) | → | indx(active(X1), X2) |
| active(dbl1(X)) | → | dbl1(active(X)) | | active(s1(X)) | → | s1(active(X)) |
| active(sel1(X1, X2)) | → | sel1(active(X1), X2) | | active(sel1(X1, X2)) | → | sel1(X1, active(X2)) |
| active(quote(X)) | → | quote(active(X)) | | dbl(mark(X)) | → | mark(dbl(X)) |
| dbls(mark(X)) | → | mark(dbls(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | indx(mark(X1), X2) | → | mark(indx(X1, X2)) |
| dbl1(mark(X)) | → | mark(dbl1(X)) | | s1(mark(X)) | → | mark(s1(X)) |
| sel1(mark(X1), X2) | → | mark(sel1(X1, X2)) | | sel1(X1, mark(X2)) | → | mark(sel1(X1, X2)) |
| quote(mark(X)) | → | mark(quote(X)) | | proper(dbl(X)) | → | dbl(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(dbls(X)) | → | dbls(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(indx(X1, X2)) | → | indx(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(dbl1(X)) | → | dbl1(proper(X)) | | proper(01) | → | ok(01) |
| proper(s1(X)) | → | s1(proper(X)) | | proper(sel1(X1, X2)) | → | sel1(proper(X1), proper(X2)) |
| proper(quote(X)) | → | quote(proper(X)) | | dbl(ok(X)) | → | ok(dbl(X)) |
| s(ok(X)) | → | ok(s(X)) | | dbls(ok(X)) | → | ok(dbls(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| indx(ok(X1), ok(X2)) | → | ok(indx(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| dbl1(ok(X)) | → | ok(dbl1(X)) | | s1(ok(X)) | → | ok(s1(X)) |
| sel1(ok(X1), ok(X2)) | → | ok(sel1(X1, X2)) | | quote(ok(X)) | → | ok(quote(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(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, ok, proper, sel, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| s1#(mark(X)) | → | s1#(X) | | s1#(ok(X)) | → | s1#(X) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| cons#(ok(X1), ok(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)) | | active(dbl(X)) | → | dbl(active(X)) |
| active(dbls(X)) | → | dbls(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(indx(X1, X2)) | → | indx(active(X1), X2) |
| active(dbl1(X)) | → | dbl1(active(X)) | | active(s1(X)) | → | s1(active(X)) |
| active(sel1(X1, X2)) | → | sel1(active(X1), X2) | | active(sel1(X1, X2)) | → | sel1(X1, active(X2)) |
| active(quote(X)) | → | quote(active(X)) | | dbl(mark(X)) | → | mark(dbl(X)) |
| dbls(mark(X)) | → | mark(dbls(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | indx(mark(X1), X2) | → | mark(indx(X1, X2)) |
| dbl1(mark(X)) | → | mark(dbl1(X)) | | s1(mark(X)) | → | mark(s1(X)) |
| sel1(mark(X1), X2) | → | mark(sel1(X1, X2)) | | sel1(X1, mark(X2)) | → | mark(sel1(X1, X2)) |
| quote(mark(X)) | → | mark(quote(X)) | | proper(dbl(X)) | → | dbl(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(dbls(X)) | → | dbls(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(indx(X1, X2)) | → | indx(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(dbl1(X)) | → | dbl1(proper(X)) | | proper(01) | → | ok(01) |
| proper(s1(X)) | → | s1(proper(X)) | | proper(sel1(X1, X2)) | → | sel1(proper(X1), proper(X2)) |
| proper(quote(X)) | → | quote(proper(X)) | | dbl(ok(X)) | → | ok(dbl(X)) |
| s(ok(X)) | → | ok(s(X)) | | dbls(ok(X)) | → | ok(dbls(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| indx(ok(X1), ok(X2)) | → | ok(indx(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| dbl1(ok(X)) | → | ok(dbl1(X)) | | s1(ok(X)) | → | ok(s1(X)) |
| sel1(ok(X1), ok(X2)) | → | ok(sel1(X1, X2)) | | quote(ok(X)) | → | ok(quote(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(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, ok, proper, sel, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
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)) | | active(dbl(X)) | → | dbl(active(X)) |
| active(dbls(X)) | → | dbls(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(indx(X1, X2)) | → | indx(active(X1), X2) |
| active(dbl1(X)) | → | dbl1(active(X)) | | active(s1(X)) | → | s1(active(X)) |
| active(sel1(X1, X2)) | → | sel1(active(X1), X2) | | active(sel1(X1, X2)) | → | sel1(X1, active(X2)) |
| active(quote(X)) | → | quote(active(X)) | | dbl(mark(X)) | → | mark(dbl(X)) |
| dbls(mark(X)) | → | mark(dbls(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | indx(mark(X1), X2) | → | mark(indx(X1, X2)) |
| dbl1(mark(X)) | → | mark(dbl1(X)) | | s1(mark(X)) | → | mark(s1(X)) |
| sel1(mark(X1), X2) | → | mark(sel1(X1, X2)) | | sel1(X1, mark(X2)) | → | mark(sel1(X1, X2)) |
| quote(mark(X)) | → | mark(quote(X)) | | proper(dbl(X)) | → | dbl(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(dbls(X)) | → | dbls(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(indx(X1, X2)) | → | indx(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(dbl1(X)) | → | dbl1(proper(X)) | | proper(01) | → | ok(01) |
| proper(s1(X)) | → | s1(proper(X)) | | proper(sel1(X1, X2)) | → | sel1(proper(X1), proper(X2)) |
| proper(quote(X)) | → | quote(proper(X)) | | dbl(ok(X)) | → | ok(dbl(X)) |
| s(ok(X)) | → | ok(s(X)) | | dbls(ok(X)) | → | ok(dbls(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| indx(ok(X1), ok(X2)) | → | ok(indx(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| dbl1(ok(X)) | → | ok(dbl1(X)) | | s1(ok(X)) | → | ok(s1(X)) |
| sel1(ok(X1), ok(X2)) | → | ok(sel1(X1, X2)) | | quote(ok(X)) | → | ok(quote(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(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, ok, proper, sel, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
Problem 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| dbl#(ok(X)) | → | dbl#(X) | | dbl#(mark(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)) | | active(dbl(X)) | → | dbl(active(X)) |
| active(dbls(X)) | → | dbls(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(indx(X1, X2)) | → | indx(active(X1), X2) |
| active(dbl1(X)) | → | dbl1(active(X)) | | active(s1(X)) | → | s1(active(X)) |
| active(sel1(X1, X2)) | → | sel1(active(X1), X2) | | active(sel1(X1, X2)) | → | sel1(X1, active(X2)) |
| active(quote(X)) | → | quote(active(X)) | | dbl(mark(X)) | → | mark(dbl(X)) |
| dbls(mark(X)) | → | mark(dbls(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | indx(mark(X1), X2) | → | mark(indx(X1, X2)) |
| dbl1(mark(X)) | → | mark(dbl1(X)) | | s1(mark(X)) | → | mark(s1(X)) |
| sel1(mark(X1), X2) | → | mark(sel1(X1, X2)) | | sel1(X1, mark(X2)) | → | mark(sel1(X1, X2)) |
| quote(mark(X)) | → | mark(quote(X)) | | proper(dbl(X)) | → | dbl(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(dbls(X)) | → | dbls(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(indx(X1, X2)) | → | indx(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(dbl1(X)) | → | dbl1(proper(X)) | | proper(01) | → | ok(01) |
| proper(s1(X)) | → | s1(proper(X)) | | proper(sel1(X1, X2)) | → | sel1(proper(X1), proper(X2)) |
| proper(quote(X)) | → | quote(proper(X)) | | dbl(ok(X)) | → | ok(dbl(X)) |
| s(ok(X)) | → | ok(s(X)) | | dbls(ok(X)) | → | ok(dbls(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| indx(ok(X1), ok(X2)) | → | ok(indx(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| dbl1(ok(X)) | → | ok(dbl1(X)) | | s1(ok(X)) | → | ok(s1(X)) |
| sel1(ok(X1), ok(X2)) | → | ok(sel1(X1, X2)) | | quote(ok(X)) | → | ok(quote(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(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, ok, proper, sel, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| dbl#(ok(X)) | → | dbl#(X) | | dbl#(mark(X)) | → | dbl#(X) |
Problem 9: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| sel1#(X1, mark(X2)) | → | sel1#(X1, X2) | | sel1#(mark(X1), X2) | → | sel1#(X1, X2) |
| sel1#(ok(X1), ok(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)) | | active(dbl(X)) | → | dbl(active(X)) |
| active(dbls(X)) | → | dbls(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(indx(X1, X2)) | → | indx(active(X1), X2) |
| active(dbl1(X)) | → | dbl1(active(X)) | | active(s1(X)) | → | s1(active(X)) |
| active(sel1(X1, X2)) | → | sel1(active(X1), X2) | | active(sel1(X1, X2)) | → | sel1(X1, active(X2)) |
| active(quote(X)) | → | quote(active(X)) | | dbl(mark(X)) | → | mark(dbl(X)) |
| dbls(mark(X)) | → | mark(dbls(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | indx(mark(X1), X2) | → | mark(indx(X1, X2)) |
| dbl1(mark(X)) | → | mark(dbl1(X)) | | s1(mark(X)) | → | mark(s1(X)) |
| sel1(mark(X1), X2) | → | mark(sel1(X1, X2)) | | sel1(X1, mark(X2)) | → | mark(sel1(X1, X2)) |
| quote(mark(X)) | → | mark(quote(X)) | | proper(dbl(X)) | → | dbl(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(dbls(X)) | → | dbls(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(indx(X1, X2)) | → | indx(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(dbl1(X)) | → | dbl1(proper(X)) | | proper(01) | → | ok(01) |
| proper(s1(X)) | → | s1(proper(X)) | | proper(sel1(X1, X2)) | → | sel1(proper(X1), proper(X2)) |
| proper(quote(X)) | → | quote(proper(X)) | | dbl(ok(X)) | → | ok(dbl(X)) |
| s(ok(X)) | → | ok(s(X)) | | dbls(ok(X)) | → | ok(dbls(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| indx(ok(X1), ok(X2)) | → | ok(indx(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| dbl1(ok(X)) | → | ok(dbl1(X)) | | s1(ok(X)) | → | ok(s1(X)) |
| sel1(ok(X1), ok(X2)) | → | ok(sel1(X1, X2)) | | quote(ok(X)) | → | ok(quote(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(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, ok, proper, sel, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| sel1#(mark(X1), X2) | → | sel1#(X1, X2) | | sel1#(ok(X1), ok(X2)) | → | sel1#(X1, X2) |
Problem 16: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| sel1#(X1, mark(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)) | | active(dbl(X)) | → | dbl(active(X)) |
| active(dbls(X)) | → | dbls(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(indx(X1, X2)) | → | indx(active(X1), X2) |
| active(dbl1(X)) | → | dbl1(active(X)) | | active(s1(X)) | → | s1(active(X)) |
| active(sel1(X1, X2)) | → | sel1(active(X1), X2) | | active(sel1(X1, X2)) | → | sel1(X1, active(X2)) |
| active(quote(X)) | → | quote(active(X)) | | dbl(mark(X)) | → | mark(dbl(X)) |
| dbls(mark(X)) | → | mark(dbls(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | indx(mark(X1), X2) | → | mark(indx(X1, X2)) |
| dbl1(mark(X)) | → | mark(dbl1(X)) | | s1(mark(X)) | → | mark(s1(X)) |
| sel1(mark(X1), X2) | → | mark(sel1(X1, X2)) | | sel1(X1, mark(X2)) | → | mark(sel1(X1, X2)) |
| quote(mark(X)) | → | mark(quote(X)) | | proper(dbl(X)) | → | dbl(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(dbls(X)) | → | dbls(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(indx(X1, X2)) | → | indx(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(dbl1(X)) | → | dbl1(proper(X)) | | proper(01) | → | ok(01) |
| proper(s1(X)) | → | s1(proper(X)) | | proper(sel1(X1, X2)) | → | sel1(proper(X1), proper(X2)) |
| proper(quote(X)) | → | quote(proper(X)) | | dbl(ok(X)) | → | ok(dbl(X)) |
| s(ok(X)) | → | ok(s(X)) | | dbls(ok(X)) | → | ok(dbls(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| indx(ok(X1), ok(X2)) | → | ok(indx(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| dbl1(ok(X)) | → | ok(dbl1(X)) | | s1(ok(X)) | → | ok(s1(X)) |
| sel1(ok(X1), ok(X2)) | → | ok(sel1(X1, X2)) | | quote(ok(X)) | → | ok(quote(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(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, ok, proper, sel, top, nil, cons
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
- mark(x): x + 2
- nil: 0
- ok(x): 0
- proper(x): 0
- quote(x): 0
- s(x): 0
- s1(x): 0
- sel(x,y): 0
- sel1(x,y): 0
- sel1#(x,y): y + x + 1
- top(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:
| sel1#(X1, mark(X2)) | → | sel1#(X1, X2) |
Problem 10: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| proper#(sel1(X1, X2)) | → | proper#(X1) | | proper#(cons(X1, X2)) | → | proper#(X1) |
| proper#(cons(X1, X2)) | → | proper#(X2) | | proper#(dbl(X)) | → | proper#(X) |
| proper#(s1(X)) | → | proper#(X) | | proper#(indx(X1, X2)) | → | proper#(X2) |
| proper#(sel(X1, X2)) | → | proper#(X1) | | proper#(s(X)) | → | proper#(X) |
| proper#(sel1(X1, X2)) | → | proper#(X2) | | proper#(dbl1(X)) | → | proper#(X) |
| proper#(dbls(X)) | → | proper#(X) | | proper#(quote(X)) | → | proper#(X) |
| proper#(sel(X1, X2)) | → | proper#(X2) | | proper#(indx(X1, X2)) | → | proper#(X1) |
| proper#(from(X)) | → | proper#(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)) | | active(dbl(X)) | → | dbl(active(X)) |
| active(dbls(X)) | → | dbls(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(indx(X1, X2)) | → | indx(active(X1), X2) |
| active(dbl1(X)) | → | dbl1(active(X)) | | active(s1(X)) | → | s1(active(X)) |
| active(sel1(X1, X2)) | → | sel1(active(X1), X2) | | active(sel1(X1, X2)) | → | sel1(X1, active(X2)) |
| active(quote(X)) | → | quote(active(X)) | | dbl(mark(X)) | → | mark(dbl(X)) |
| dbls(mark(X)) | → | mark(dbls(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | indx(mark(X1), X2) | → | mark(indx(X1, X2)) |
| dbl1(mark(X)) | → | mark(dbl1(X)) | | s1(mark(X)) | → | mark(s1(X)) |
| sel1(mark(X1), X2) | → | mark(sel1(X1, X2)) | | sel1(X1, mark(X2)) | → | mark(sel1(X1, X2)) |
| quote(mark(X)) | → | mark(quote(X)) | | proper(dbl(X)) | → | dbl(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(dbls(X)) | → | dbls(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(indx(X1, X2)) | → | indx(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(dbl1(X)) | → | dbl1(proper(X)) | | proper(01) | → | ok(01) |
| proper(s1(X)) | → | s1(proper(X)) | | proper(sel1(X1, X2)) | → | sel1(proper(X1), proper(X2)) |
| proper(quote(X)) | → | quote(proper(X)) | | dbl(ok(X)) | → | ok(dbl(X)) |
| s(ok(X)) | → | ok(s(X)) | | dbls(ok(X)) | → | ok(dbls(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| indx(ok(X1), ok(X2)) | → | ok(indx(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| dbl1(ok(X)) | → | ok(dbl1(X)) | | s1(ok(X)) | → | ok(s1(X)) |
| sel1(ok(X1), ok(X2)) | → | ok(sel1(X1, X2)) | | quote(ok(X)) | → | ok(quote(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(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, ok, proper, sel, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| proper#(sel1(X1, X2)) | → | proper#(X1) | | proper#(cons(X1, X2)) | → | proper#(X1) |
| proper#(cons(X1, X2)) | → | proper#(X2) | | proper#(dbl(X)) | → | proper#(X) |
| proper#(s1(X)) | → | proper#(X) | | proper#(indx(X1, X2)) | → | proper#(X2) |
| proper#(sel(X1, X2)) | → | proper#(X1) | | proper#(s(X)) | → | proper#(X) |
| proper#(dbl1(X)) | → | proper#(X) | | proper#(sel1(X1, X2)) | → | proper#(X2) |
| proper#(dbls(X)) | → | proper#(X) | | proper#(quote(X)) | → | proper#(X) |
| proper#(sel(X1, X2)) | → | proper#(X2) | | proper#(indx(X1, X2)) | → | proper#(X1) |
| proper#(from(X)) | → | proper#(X) |
Problem 11: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| active#(dbl1(X)) | → | active#(X) | | active#(sel(X1, X2)) | → | active#(X2) |
| active#(s1(X)) | → | active#(X) | | active#(sel1(X1, X2)) | → | active#(X2) |
| active#(indx(X1, X2)) | → | active#(X1) | | active#(sel(X1, X2)) | → | active#(X1) |
| active#(dbl(X)) | → | active#(X) | | active#(dbls(X)) | → | active#(X) |
| active#(sel1(X1, X2)) | → | active#(X1) | | active#(quote(X)) | → | active#(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)) | | active(dbl(X)) | → | dbl(active(X)) |
| active(dbls(X)) | → | dbls(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(indx(X1, X2)) | → | indx(active(X1), X2) |
| active(dbl1(X)) | → | dbl1(active(X)) | | active(s1(X)) | → | s1(active(X)) |
| active(sel1(X1, X2)) | → | sel1(active(X1), X2) | | active(sel1(X1, X2)) | → | sel1(X1, active(X2)) |
| active(quote(X)) | → | quote(active(X)) | | dbl(mark(X)) | → | mark(dbl(X)) |
| dbls(mark(X)) | → | mark(dbls(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | indx(mark(X1), X2) | → | mark(indx(X1, X2)) |
| dbl1(mark(X)) | → | mark(dbl1(X)) | | s1(mark(X)) | → | mark(s1(X)) |
| sel1(mark(X1), X2) | → | mark(sel1(X1, X2)) | | sel1(X1, mark(X2)) | → | mark(sel1(X1, X2)) |
| quote(mark(X)) | → | mark(quote(X)) | | proper(dbl(X)) | → | dbl(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(dbls(X)) | → | dbls(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(indx(X1, X2)) | → | indx(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(dbl1(X)) | → | dbl1(proper(X)) | | proper(01) | → | ok(01) |
| proper(s1(X)) | → | s1(proper(X)) | | proper(sel1(X1, X2)) | → | sel1(proper(X1), proper(X2)) |
| proper(quote(X)) | → | quote(proper(X)) | | dbl(ok(X)) | → | ok(dbl(X)) |
| s(ok(X)) | → | ok(s(X)) | | dbls(ok(X)) | → | ok(dbls(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| indx(ok(X1), ok(X2)) | → | ok(indx(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| dbl1(ok(X)) | → | ok(dbl1(X)) | | s1(ok(X)) | → | ok(s1(X)) |
| sel1(ok(X1), ok(X2)) | → | ok(sel1(X1, X2)) | | quote(ok(X)) | → | ok(quote(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(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, ok, proper, sel, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| active#(s1(X)) | → | active#(X) | | active#(dbl1(X)) | → | active#(X) |
| active#(sel(X1, X2)) | → | active#(X2) | | active#(sel1(X1, X2)) | → | active#(X2) |
| active#(sel(X1, X2)) | → | active#(X1) | | active#(indx(X1, X2)) | → | active#(X1) |
| active#(dbls(X)) | → | active#(X) | | active#(dbl(X)) | → | active#(X) |
| active#(sel1(X1, X2)) | → | active#(X1) | | active#(quote(X)) | → | active#(X) |
Problem 12: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| quote#(ok(X)) | → | quote#(X) | | quote#(mark(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)) | | active(dbl(X)) | → | dbl(active(X)) |
| active(dbls(X)) | → | dbls(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(indx(X1, X2)) | → | indx(active(X1), X2) |
| active(dbl1(X)) | → | dbl1(active(X)) | | active(s1(X)) | → | s1(active(X)) |
| active(sel1(X1, X2)) | → | sel1(active(X1), X2) | | active(sel1(X1, X2)) | → | sel1(X1, active(X2)) |
| active(quote(X)) | → | quote(active(X)) | | dbl(mark(X)) | → | mark(dbl(X)) |
| dbls(mark(X)) | → | mark(dbls(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | indx(mark(X1), X2) | → | mark(indx(X1, X2)) |
| dbl1(mark(X)) | → | mark(dbl1(X)) | | s1(mark(X)) | → | mark(s1(X)) |
| sel1(mark(X1), X2) | → | mark(sel1(X1, X2)) | | sel1(X1, mark(X2)) | → | mark(sel1(X1, X2)) |
| quote(mark(X)) | → | mark(quote(X)) | | proper(dbl(X)) | → | dbl(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(dbls(X)) | → | dbls(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(indx(X1, X2)) | → | indx(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(dbl1(X)) | → | dbl1(proper(X)) | | proper(01) | → | ok(01) |
| proper(s1(X)) | → | s1(proper(X)) | | proper(sel1(X1, X2)) | → | sel1(proper(X1), proper(X2)) |
| proper(quote(X)) | → | quote(proper(X)) | | dbl(ok(X)) | → | ok(dbl(X)) |
| s(ok(X)) | → | ok(s(X)) | | dbls(ok(X)) | → | ok(dbls(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| indx(ok(X1), ok(X2)) | → | ok(indx(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| dbl1(ok(X)) | → | ok(dbl1(X)) | | s1(ok(X)) | → | ok(s1(X)) |
| sel1(ok(X1), ok(X2)) | → | ok(sel1(X1, X2)) | | quote(ok(X)) | → | ok(quote(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(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, ok, proper, sel, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| quote#(ok(X)) | → | quote#(X) | | quote#(mark(X)) | → | quote#(X) |
Problem 13: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| sel#(mark(X1), X2) | → | sel#(X1, X2) | | sel#(ok(X1), ok(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)) | | active(dbl(X)) | → | dbl(active(X)) |
| active(dbls(X)) | → | dbls(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(indx(X1, X2)) | → | indx(active(X1), X2) |
| active(dbl1(X)) | → | dbl1(active(X)) | | active(s1(X)) | → | s1(active(X)) |
| active(sel1(X1, X2)) | → | sel1(active(X1), X2) | | active(sel1(X1, X2)) | → | sel1(X1, active(X2)) |
| active(quote(X)) | → | quote(active(X)) | | dbl(mark(X)) | → | mark(dbl(X)) |
| dbls(mark(X)) | → | mark(dbls(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | indx(mark(X1), X2) | → | mark(indx(X1, X2)) |
| dbl1(mark(X)) | → | mark(dbl1(X)) | | s1(mark(X)) | → | mark(s1(X)) |
| sel1(mark(X1), X2) | → | mark(sel1(X1, X2)) | | sel1(X1, mark(X2)) | → | mark(sel1(X1, X2)) |
| quote(mark(X)) | → | mark(quote(X)) | | proper(dbl(X)) | → | dbl(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(dbls(X)) | → | dbls(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(indx(X1, X2)) | → | indx(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(dbl1(X)) | → | dbl1(proper(X)) | | proper(01) | → | ok(01) |
| proper(s1(X)) | → | s1(proper(X)) | | proper(sel1(X1, X2)) | → | sel1(proper(X1), proper(X2)) |
| proper(quote(X)) | → | quote(proper(X)) | | dbl(ok(X)) | → | ok(dbl(X)) |
| s(ok(X)) | → | ok(s(X)) | | dbls(ok(X)) | → | ok(dbls(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| indx(ok(X1), ok(X2)) | → | ok(indx(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| dbl1(ok(X)) | → | ok(dbl1(X)) | | s1(ok(X)) | → | ok(s1(X)) |
| sel1(ok(X1), ok(X2)) | → | ok(sel1(X1, X2)) | | quote(ok(X)) | → | ok(quote(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(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, ok, proper, sel, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| sel#(mark(X1), X2) | → | sel#(X1, X2) | | sel#(ok(X1), ok(X2)) | → | sel#(X1, X2) |
Problem 17: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| 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)) | | active(dbl(X)) | → | dbl(active(X)) |
| active(dbls(X)) | → | dbls(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(indx(X1, X2)) | → | indx(active(X1), X2) |
| active(dbl1(X)) | → | dbl1(active(X)) | | active(s1(X)) | → | s1(active(X)) |
| active(sel1(X1, X2)) | → | sel1(active(X1), X2) | | active(sel1(X1, X2)) | → | sel1(X1, active(X2)) |
| active(quote(X)) | → | quote(active(X)) | | dbl(mark(X)) | → | mark(dbl(X)) |
| dbls(mark(X)) | → | mark(dbls(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | indx(mark(X1), X2) | → | mark(indx(X1, X2)) |
| dbl1(mark(X)) | → | mark(dbl1(X)) | | s1(mark(X)) | → | mark(s1(X)) |
| sel1(mark(X1), X2) | → | mark(sel1(X1, X2)) | | sel1(X1, mark(X2)) | → | mark(sel1(X1, X2)) |
| quote(mark(X)) | → | mark(quote(X)) | | proper(dbl(X)) | → | dbl(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(dbls(X)) | → | dbls(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(indx(X1, X2)) | → | indx(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(dbl1(X)) | → | dbl1(proper(X)) | | proper(01) | → | ok(01) |
| proper(s1(X)) | → | s1(proper(X)) | | proper(sel1(X1, X2)) | → | sel1(proper(X1), proper(X2)) |
| proper(quote(X)) | → | quote(proper(X)) | | dbl(ok(X)) | → | ok(dbl(X)) |
| s(ok(X)) | → | ok(s(X)) | | dbls(ok(X)) | → | ok(dbls(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| indx(ok(X1), ok(X2)) | → | ok(indx(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| dbl1(ok(X)) | → | ok(dbl1(X)) | | s1(ok(X)) | → | ok(s1(X)) |
| sel1(ok(X1), ok(X2)) | → | ok(sel1(X1, X2)) | | quote(ok(X)) | → | ok(quote(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(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, ok, proper, sel, top, nil, cons
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
- mark(x): x + 2
- nil: 0
- ok(x): 0
- proper(x): 0
- quote(x): 0
- s(x): 0
- s1(x): 0
- sel(x,y): 0
- sel#(x,y): y + x + 1
- sel1(x,y): 0
- top(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:
| sel#(X1, mark(X2)) | → | sel#(X1, X2) |
Problem 14: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| dbls#(ok(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)) | | active(dbl(X)) | → | dbl(active(X)) |
| active(dbls(X)) | → | dbls(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(indx(X1, X2)) | → | indx(active(X1), X2) |
| active(dbl1(X)) | → | dbl1(active(X)) | | active(s1(X)) | → | s1(active(X)) |
| active(sel1(X1, X2)) | → | sel1(active(X1), X2) | | active(sel1(X1, X2)) | → | sel1(X1, active(X2)) |
| active(quote(X)) | → | quote(active(X)) | | dbl(mark(X)) | → | mark(dbl(X)) |
| dbls(mark(X)) | → | mark(dbls(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | indx(mark(X1), X2) | → | mark(indx(X1, X2)) |
| dbl1(mark(X)) | → | mark(dbl1(X)) | | s1(mark(X)) | → | mark(s1(X)) |
| sel1(mark(X1), X2) | → | mark(sel1(X1, X2)) | | sel1(X1, mark(X2)) | → | mark(sel1(X1, X2)) |
| quote(mark(X)) | → | mark(quote(X)) | | proper(dbl(X)) | → | dbl(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(dbls(X)) | → | dbls(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(indx(X1, X2)) | → | indx(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(dbl1(X)) | → | dbl1(proper(X)) | | proper(01) | → | ok(01) |
| proper(s1(X)) | → | s1(proper(X)) | | proper(sel1(X1, X2)) | → | sel1(proper(X1), proper(X2)) |
| proper(quote(X)) | → | quote(proper(X)) | | dbl(ok(X)) | → | ok(dbl(X)) |
| s(ok(X)) | → | ok(s(X)) | | dbls(ok(X)) | → | ok(dbls(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| indx(ok(X1), ok(X2)) | → | ok(indx(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| dbl1(ok(X)) | → | ok(dbl1(X)) | | s1(ok(X)) | → | ok(s1(X)) |
| sel1(ok(X1), ok(X2)) | → | ok(sel1(X1, X2)) | | quote(ok(X)) | → | ok(quote(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(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, ok, proper, sel, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| dbls#(ok(X)) | → | dbls#(X) | | dbls#(mark(X)) | → | dbls#(X) |
Problem 15: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
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)) | | active(dbl(X)) | → | dbl(active(X)) |
| active(dbls(X)) | → | dbls(active(X)) | | active(sel(X1, X2)) | → | sel(active(X1), X2) |
| active(sel(X1, X2)) | → | sel(X1, active(X2)) | | active(indx(X1, X2)) | → | indx(active(X1), X2) |
| active(dbl1(X)) | → | dbl1(active(X)) | | active(s1(X)) | → | s1(active(X)) |
| active(sel1(X1, X2)) | → | sel1(active(X1), X2) | | active(sel1(X1, X2)) | → | sel1(X1, active(X2)) |
| active(quote(X)) | → | quote(active(X)) | | dbl(mark(X)) | → | mark(dbl(X)) |
| dbls(mark(X)) | → | mark(dbls(X)) | | sel(mark(X1), X2) | → | mark(sel(X1, X2)) |
| sel(X1, mark(X2)) | → | mark(sel(X1, X2)) | | indx(mark(X1), X2) | → | mark(indx(X1, X2)) |
| dbl1(mark(X)) | → | mark(dbl1(X)) | | s1(mark(X)) | → | mark(s1(X)) |
| sel1(mark(X1), X2) | → | mark(sel1(X1, X2)) | | sel1(X1, mark(X2)) | → | mark(sel1(X1, X2)) |
| quote(mark(X)) | → | mark(quote(X)) | | proper(dbl(X)) | → | dbl(proper(X)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(dbls(X)) | → | dbls(proper(X)) | | proper(nil) | → | ok(nil) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(sel(X1, X2)) | → | sel(proper(X1), proper(X2)) |
| proper(indx(X1, X2)) | → | indx(proper(X1), proper(X2)) | | proper(from(X)) | → | from(proper(X)) |
| proper(dbl1(X)) | → | dbl1(proper(X)) | | proper(01) | → | ok(01) |
| proper(s1(X)) | → | s1(proper(X)) | | proper(sel1(X1, X2)) | → | sel1(proper(X1), proper(X2)) |
| proper(quote(X)) | → | quote(proper(X)) | | dbl(ok(X)) | → | ok(dbl(X)) |
| s(ok(X)) | → | ok(s(X)) | | dbls(ok(X)) | → | ok(dbls(X)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | sel(ok(X1), ok(X2)) | → | ok(sel(X1, X2)) |
| indx(ok(X1), ok(X2)) | → | ok(indx(X1, X2)) | | from(ok(X)) | → | ok(from(X)) |
| dbl1(ok(X)) | → | ok(dbl1(X)) | | s1(ok(X)) | → | ok(s1(X)) |
| sel1(ok(X1), ok(X2)) | → | ok(sel1(X1, X2)) | | quote(ok(X)) | → | ok(quote(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(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, ok, proper, sel, cons, nil, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed: