TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60000 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (146ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (40ms), PolynomialLinearRange4iUR (2251ms), DependencyGraph (40ms), PolynomialLinearRange8NegiUR (29998ms), DependencyGraph (timeout), ReductionPairSAT (2227ms), DependencyGraph (29ms), SizeChangePrinciple (timeout)].
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| a__sel#(0, cons(X, Y)) | → | mark#(X) | | mark#(dbls(X)) | → | mark#(X) |
| mark#(sel(X1, X2)) | → | a__sel#(mark(X1), mark(X2)) | | a__sel#(s(X), cons(Y, Z)) | → | mark#(Z) |
| mark#(sel(X1, X2)) | → | mark#(X2) | | a__sel#(s(X), cons(Y, Z)) | → | a__sel#(mark(X), mark(Z)) |
| mark#(indx(X1, X2)) | → | mark#(X1) | | mark#(sel(X1, X2)) | → | mark#(X1) |
| mark#(dbl(X)) | → | mark#(X) | | a__sel#(s(X), cons(Y, Z)) | → | mark#(X) |
Rewrite Rules
| a__dbl(0) | → | 0 | | a__dbl(s(X)) | → | s(s(dbl(X))) |
| a__dbls(nil) | → | nil | | a__dbls(cons(X, Y)) | → | cons(dbl(X), dbls(Y)) |
| a__sel(0, cons(X, Y)) | → | mark(X) | | a__sel(s(X), cons(Y, Z)) | → | a__sel(mark(X), mark(Z)) |
| a__indx(nil, X) | → | nil | | a__indx(cons(X, Y), Z) | → | cons(sel(X, Z), indx(Y, Z)) |
| a__from(X) | → | cons(X, from(s(X))) | | mark(dbl(X)) | → | a__dbl(mark(X)) |
| mark(dbls(X)) | → | a__dbls(mark(X)) | | mark(sel(X1, X2)) | → | a__sel(mark(X1), mark(X2)) |
| mark(indx(X1, X2)) | → | a__indx(mark(X1), X2) | | mark(from(X)) | → | a__from(X) |
| mark(0) | → | 0 | | mark(s(X)) | → | s(X) |
| mark(nil) | → | nil | | mark(cons(X1, X2)) | → | cons(X1, X2) |
| a__dbl(X) | → | dbl(X) | | a__dbls(X) | → | dbls(X) |
| a__sel(X1, X2) | → | sel(X1, X2) | | a__indx(X1, X2) | → | indx(X1, X2) |
| a__from(X) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: dbl, mark, from, dbls, 0, a__dbl, s, indx, a__dbls, a__sel, a__indx, sel, a__from, nil, cons
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a__sel#(0, cons(X, Y)) | → | mark#(X) | | mark#(dbls(X)) | → | mark#(X) |
| a__sel#(s(X), cons(Y, Z)) | → | mark#(Z) | | a__sel#(s(X), cons(Y, Z)) | → | a__sel#(mark(X), mark(Z)) |
| mark#(from(X)) | → | a__from#(X) | | mark#(dbl(X)) | → | a__dbl#(mark(X)) |
| mark#(indx(X1, X2)) | → | mark#(X1) | | mark#(dbl(X)) | → | mark#(X) |
| mark#(indx(X1, X2)) | → | a__indx#(mark(X1), X2) | | mark#(sel(X1, X2)) | → | a__sel#(mark(X1), mark(X2)) |
| mark#(sel(X1, X2)) | → | mark#(X2) | | mark#(dbls(X)) | → | a__dbls#(mark(X)) |
| mark#(sel(X1, X2)) | → | mark#(X1) | | a__sel#(s(X), cons(Y, Z)) | → | mark#(X) |
Rewrite Rules
| a__dbl(0) | → | 0 | | a__dbl(s(X)) | → | s(s(dbl(X))) |
| a__dbls(nil) | → | nil | | a__dbls(cons(X, Y)) | → | cons(dbl(X), dbls(Y)) |
| a__sel(0, cons(X, Y)) | → | mark(X) | | a__sel(s(X), cons(Y, Z)) | → | a__sel(mark(X), mark(Z)) |
| a__indx(nil, X) | → | nil | | a__indx(cons(X, Y), Z) | → | cons(sel(X, Z), indx(Y, Z)) |
| a__from(X) | → | cons(X, from(s(X))) | | mark(dbl(X)) | → | a__dbl(mark(X)) |
| mark(dbls(X)) | → | a__dbls(mark(X)) | | mark(sel(X1, X2)) | → | a__sel(mark(X1), mark(X2)) |
| mark(indx(X1, X2)) | → | a__indx(mark(X1), X2) | | mark(from(X)) | → | a__from(X) |
| mark(0) | → | 0 | | mark(s(X)) | → | s(X) |
| mark(nil) | → | nil | | mark(cons(X1, X2)) | → | cons(X1, X2) |
| a__dbl(X) | → | dbl(X) | | a__dbls(X) | → | dbls(X) |
| a__sel(X1, X2) | → | sel(X1, X2) | | a__indx(X1, X2) | → | indx(X1, X2) |
| a__from(X) | → | from(X) |
Original Signature
Termination of terms over the following signature is verified: dbl, mark, from, dbls, 0, a__dbl, s, indx, a__dbls, a__sel, a__indx, sel, a__from, cons, nil
Strategy
The following SCCs where found
| a__sel#(0, cons(X, Y)) → mark#(X) | mark#(dbls(X)) → mark#(X) |
| mark#(sel(X1, X2)) → a__sel#(mark(X1), mark(X2)) | a__sel#(s(X), cons(Y, Z)) → mark#(Z) |
| a__sel#(s(X), cons(Y, Z)) → a__sel#(mark(X), mark(Z)) | mark#(sel(X1, X2)) → mark#(X2) |
| mark#(indx(X1, X2)) → mark#(X1) | mark#(sel(X1, X2)) → mark#(X1) |
| a__sel#(s(X), cons(Y, Z)) → mark#(X) | mark#(dbl(X)) → mark#(X) |