TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60097 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (2361ms).
| Problem 2 was processed with processor PolynomialLinearRange4 (1481ms).
| | Problem 4 was processed with processor PolynomialLinearRange4 (901ms).
| | | Problem 6 was processed with processor PolynomialLinearRange4 (667ms).
| | | | Problem 8 was processed with processor DependencyGraph (60ms).
| | | | | Problem 10 remains open; application of the following processors failed [PolynomialLinearRange4 (976ms), DependencyGraph (17ms), PolynomialLinearRange4 (962ms), DependencyGraph (17ms), PolynomialLinearRange4 (962ms), DependencyGraph (16ms), PolynomialLinearRange4 (984ms), DependencyGraph (17ms), PolynomialLinearRange4 (958ms), DependencyGraph (16ms), PolynomialLinearRange4 (980ms), DependencyGraph (15ms), PolynomialLinearRange4 (962ms), DependencyGraph (23ms), ReductionPairSAT (105ms), DependencyGraph (14ms)].
| Problem 3 was processed with processor PolynomialLinearRange4 (992ms).
| | Problem 5 was processed with processor PolynomialLinearRange4 (731ms).
| | | Problem 7 was processed with processor PolynomialLinearRange4 (1052ms).
| | | | Problem 9 was processed with processor PolynomialLinearRange4 (1199ms).
| | | | | Problem 11 was processed with processor PolynomialLinearRange4 (1687ms).
| | | | | | Problem 12 was processed with processor PolynomialLinearRange4 (991ms).
| | | | | | | Problem 13 was processed with processor PolynomialLinearRange4 (954ms).
| | | | | | | | Problem 14 was processed with processor PolynomialLinearRange4 (1078ms).
| | | | | | | | | Problem 15 was processed with processor PolynomialLinearRange4 (1080ms).
| | | | | | | | | | Problem 16 remains open; application of the following processors failed [DependencyGraph (8ms), PolynomialLinearRange4 (1897ms), DependencyGraph (8ms), ReductionPairSAT (30039ms), DependencyGraph (34ms), SizeChangePrinciple (timeout)].
The following open problems remain:
Open Dependency Pair Problem 16
Dependency Pairs
*top*_0#(h_1(cons_8(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0#(h_1(cons_10(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0#(h_1(cons_2(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0#(h_1(cons_1(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0#(h_1(cons_6(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0#(h_1(cons_1(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) |
Rewrite Rules
M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) | | tail_1(cons_2(x, s)) | → | s |
tail_1(cons_3(x, s)) | → | s | | tail_1(cons_4(x, s)) | → | s |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) | | *top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) |
tail_1(cons_7(x, s)) | → | s | | tail_1(cons_8(x, s)) | → | s |
tail_1(cons_9(x, s)) | → | s | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
*top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_1(cons_1(x, s)) | → | s |
*top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) | | *top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_2(x, s) | → | garbage_collection_0 | | cons_3(x, s) | → | garbage_collection_0 |
cons_4(x, s) | → | garbage_collection_0 | | cons_5(x, s) | → | garbage_collection_0 |
cons_6(x, s) | → | garbage_collection_0 | | cons_7(x, s) | → | garbage_collection_0 |
cons_8(x, s) | → | garbage_collection_0 | | cons_9(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | cons_11(x, s) | → | garbage_collection_0 |
cons_1(x, s) | → | garbage_collection_0 |
Original Signature
Termination of terms over the following signature is verified: garbage_collection_0, cons_3, cons_2, cons_5, cons_4, h_0, cons_1, h_1, 0_0, cons_7, tail_1, cons_11, cons_6, cons_9, cons_10, tail_0, cons_8, 1_0, *top*_0, M_1
Open Dependency Pair Problem 10
Dependency Pairs
T(cons_1(x_1, x_2)) | → | T(x_2) | | T(h_0(s)) | → | h_0#(s) |
T(cons_10(x_1, x_2)) | → | T(x_2) | | T(cons_6(x_1, x_2)) | → | T(x_2) |
T(tail_0(x_1)) | → | T(x_1) | | T(h_1(x_1)) | → | T(x_1) |
h_0#(tail_1(cons_1(x, s))) | → | T(s) | | h_0#(tail_1(cons_1(x, s))) | → | h_0#(s) |
T(h_0(x_1)) | → | T(x_1) |
Rewrite Rules
M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) | | tail_1(cons_2(x, s)) | → | s |
tail_1(cons_3(x, s)) | → | s | | tail_1(cons_4(x, s)) | → | s |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) | | *top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) |
tail_1(cons_7(x, s)) | → | s | | tail_1(cons_8(x, s)) | → | s |
tail_1(cons_9(x, s)) | → | s | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
*top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_1(cons_1(x, s)) | → | s |
*top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) | | *top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_2(x, s) | → | garbage_collection_0 | | cons_3(x, s) | → | garbage_collection_0 |
cons_4(x, s) | → | garbage_collection_0 | | cons_5(x, s) | → | garbage_collection_0 |
cons_6(x, s) | → | garbage_collection_0 | | cons_7(x, s) | → | garbage_collection_0 |
cons_8(x, s) | → | garbage_collection_0 | | cons_9(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | cons_11(x, s) | → | garbage_collection_0 |
cons_1(x, s) | → | garbage_collection_0 |
Original Signature
Termination of terms over the following signature is verified: garbage_collection_0, cons_3, cons_2, cons_5, cons_4, h_0, cons_1, h_1, 0_0, cons_7, tail_1, cons_11, cons_6, cons_9, cons_10, tail_0, cons_8, 1_0, *top*_0, M_1
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
*top*_0#(h_1(cons_1(1_0, s))) | → | cons_10#(1_0, cons_1(0_0, h_0(s))) | | *top*_0#(h_1(cons_3(0_0, s))) | → | cons_6#(0_0, cons_1(1_0, h_0(s))) |
*top*_0#(h_1(cons_9(1_0, s))) | → | cons_10#(1_0, cons_1(0_0, h_0(s))) | | *top*_0#(h_1(cons_7(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0#(h_1(cons_9(1_0, s))) | → | tail_1#(cons_10(1_0, cons_1(0_0, h_0(s)))) | | T(cons_6(0_0, cons_7(1_0, h_1(s)))) | → | cons_6#(0_0, cons_7(1_0, h_1(s))) |
*top*_0#(tail_1(cons_10(x, s))) | → | *top*_0#(s) | | tail_0#(h_1(cons_8(1_0, s))) | → | tail_1#(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0#(h_1(cons_7(1_0, s))) | → | cons_10#(1_0, cons_1(0_0, h_0(s))) | | *top*_0#(h_1(cons_2(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) |
T(tail_0(M_1)) | → | tail_0#(M_1) | | *top*_0#(tail_1(cons_10(x, s))) | → | T(s) |
T(cons_2(0_0, h_1(s))) | → | cons_2#(0_0, h_1(s)) | | *top*_0#(h_1(cons_4(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0#(tail_1(cons_5(x, s))) | → | tail_1#(s) | | *top*_0#(tail_1(cons_5(x, s))) | → | *top*_0#(s) |
T(cons_6(0_0, cons_1(1_0, h_0(s)))) | → | cons_6#(0_0, cons_1(1_0, h_0(s))) | | *top*_0#(h_1(cons_1(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0#(tail_1(cons_10(x, s))) | → | tail_1#(s) | | *top*_0#(h_1(cons_11(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_3(0_0, h_1(s)))) |
tail_0#(h_1(cons_11(1_0, s))) | → | tail_1#(cons_10(1_0, cons_3(0_0, h_1(s)))) | | T(cons_10(1_0, cons_1(0_0, h_0(s)))) | → | cons_10#(1_0, cons_1(0_0, h_0(s))) |
T(cons_1(x_1, x_2)) | → | T(x_2) | | *top*_0#(h_1(cons_10(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_2(0_0, h_1(s)))) |
tail_0#(h_1(cons_7(1_0, s))) | → | tail_1#(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0#(tail_1(cons_6(x, s))) | → | T(s) |
T(tail_0(x_1)) | → | T(x_1) | | *top*_0#(h_1(cons_1(0_0, s))) | → | cons_6#(0_0, cons_1(1_0, h_0(s))) |
T(cons_7(1_0, h_1(s))) | → | cons_7#(1_0, h_1(s)) | | T(cons_1(1_0, h_0(s))) | → | cons_1#(1_0, h_0(s)) |
*top*_0#(h_1(cons_8(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0#(h_1(cons_2(0_0, s))) | → | cons_6#(0_0, cons_1(1_0, h_0(s))) |
tail_0#(h_1(cons_10(1_0, s))) | → | tail_1#(cons_10(1_0, cons_2(0_0, h_1(s)))) | | tail_1#(cons_2(x, s)) | → | T(s) |
tail_0#(h_1(cons_2(0_0, s))) | → | tail_1#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0#(tail_1(cons_11(x, s))) | → | T(s) |
T(cons_10(1_0, cons_3(0_0, h_1(s)))) | → | cons_10#(1_0, cons_3(0_0, h_1(s))) | | tail_0#(h_1(cons_5(0_0, s))) | → | tail_1#(cons_6(0_0, cons_7(1_0, h_1(s)))) |
T(h_0(x_1)) | → | T(x_1) | | h_0#(tail_1(cons_1(x, s))) | → | h_0#(s) |
T(h_0(s)) | → | h_0#(s) | | tail_0#(h_1(cons_4(0_0, s))) | → | tail_1#(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0#(h_1(cons_8(1_0, s))) | → | cons_10#(1_0, cons_1(0_0, h_0(s))) | | T(cons_1(0_0, tail_0(M_1))) | → | cons_1#(0_0, tail_0(M_1)) |
T(cons_10(x_1, x_2)) | → | T(x_2) | | tail_1#(cons_4(x, s)) | → | T(s) |
T(cons_6(x_1, x_2)) | → | T(x_2) | | T(cons_3(0_0, h_1(s))) | → | cons_3#(0_0, h_1(s)) |
T(h_1(x_1)) | → | T(x_1) | | tail_1#(cons_9(x, s)) | → | T(s) |
tail_1#(cons_7(x, s)) | → | T(s) | | tail_1#(cons_3(x, s)) | → | T(s) |
T(cons_8(1_0, h_1(s))) | → | cons_8#(1_0, h_1(s)) | | *top*_0#(h_1(cons_4(0_0, s))) | → | cons_6#(0_0, cons_1(1_0, h_0(s))) |
*top*_0#(h_1(cons_3(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | T(cons_10(1_0, cons_2(0_0, h_1(s)))) | → | cons_10#(1_0, cons_2(0_0, h_1(s))) |
T(cons_1(0_0, h_0(s))) | → | cons_1#(0_0, h_0(s)) | | *top*_0#(h_1(cons_6(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_8(1_0, h_1(s)))) |
h_0#(tail_1(cons_1(x, s))) | → | T(s) | | *top*_0#(h_1(cons_6(0_0, s))) | → | cons_6#(0_0, cons_8(1_0, h_1(s))) |
tail_0#(tail_1(cons_11(x, s))) | → | tail_1#(s) | | *top*_0#(tail_1(cons_5(x, s))) | → | T(s) |
tail_1#(cons_8(x, s)) | → | T(s) | | *top*_0#(tail_1(cons_11(x, s))) | → | *top*_0#(s) |
*top*_0#(h_1(cons_5(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_7(1_0, h_1(s)))) | | *top*_0#(h_1(cons_1(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0#(h_1(cons_3(0_0, s))) | → | tail_1#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | T(cons_6(0_0, cons_8(1_0, h_1(s)))) | → | cons_6#(0_0, cons_8(1_0, h_1(s))) |
*top*_0#(tail_1(cons_1(x, s))) | → | *top*_0#(s) | | *top*_0#(h_1(cons_9(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0#(h_1(cons_6(0_0, s))) | → | tail_1#(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0#(h_1(cons_10(1_0, s))) | → | cons_10#(1_0, cons_2(0_0, h_1(s))) |
T(M_1) | → | M_1# | | *top*_0#(h_1(cons_5(0_0, s))) | → | cons_6#(0_0, cons_7(1_0, h_1(s))) |
tail_0#(h_1(cons_1(1_0, s))) | → | tail_1#(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0#(tail_1(cons_6(x, s))) | → | tail_1#(s) |
*top*_0#(tail_1(cons_1(x, s))) | → | T(s) | | tail_1#(cons_1(x, s)) | → | T(s) |
*top*_0#(h_1(cons_11(1_0, s))) | → | cons_10#(1_0, cons_3(0_0, h_1(s))) | | *top*_0#(tail_1(cons_6(x, s))) | → | *top*_0#(s) |
tail_0#(h_1(cons_1(0_0, s))) | → | tail_1#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0#(tail_1(cons_1(x, s))) | → | tail_1#(s) |
Rewrite Rules
M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) | | tail_1(cons_2(x, s)) | → | s |
tail_1(cons_3(x, s)) | → | s | | tail_1(cons_4(x, s)) | → | s |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) | | *top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) |
tail_1(cons_7(x, s)) | → | s | | tail_1(cons_8(x, s)) | → | s |
tail_1(cons_9(x, s)) | → | s | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
*top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_1(cons_1(x, s)) | → | s |
*top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) | | *top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_2(x, s) | → | garbage_collection_0 | | cons_3(x, s) | → | garbage_collection_0 |
cons_4(x, s) | → | garbage_collection_0 | | cons_5(x, s) | → | garbage_collection_0 |
cons_6(x, s) | → | garbage_collection_0 | | cons_7(x, s) | → | garbage_collection_0 |
cons_8(x, s) | → | garbage_collection_0 | | cons_9(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | cons_11(x, s) | → | garbage_collection_0 |
cons_1(x, s) | → | garbage_collection_0 |
Original Signature
Termination of terms over the following signature is verified: garbage_collection_0, cons_3, cons_2, cons_5, cons_4, h_0, cons_1, h_1, 0_0, cons_7, tail_1, cons_11, cons_6, cons_9, cons_10, tail_0, cons_8, 1_0, *top*_0, M_1
Strategy
Context-sensitive strategy:
μ(cons_3) = μ(garbage_collection_0) = μ(cons_2) = μ(cons_5) = μ(M_1#) = μ(cons_1#) = μ(cons_5#) = μ(cons_4) = μ(cons_3#) = μ(cons_1) = μ(h_1) = μ(cons_7#) = μ(cons_7) = μ(tail_1) = μ(cons_11) = μ(cons_6) = μ(cons_9#) = μ(cons_9) = μ(cons_10) = μ(cons_8) = μ(T) = μ(1_0) = μ(cons_2#) = μ(tail_1#) = μ(cons_11#) = μ(cons_4#) = μ(cons_6#) = μ(cons_8#) = μ(0_0) = μ(M_1) = μ(cons_10#) = ∅
μ(h_0) = μ(tail_0) = μ(*top*_0#) = μ(h_0#) = μ(*top*_0) = μ(tail_0#) = {1}
The following SCCs where found
*top*_0#(tail_1(cons_11(x, s))) → *top*_0#(s) | *top*_0#(h_1(cons_5(0_0, s))) → *top*_0#(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0#(h_1(cons_10(1_0, s))) → *top*_0#(cons_10(1_0, cons_2(0_0, h_1(s)))) | *top*_0#(h_1(cons_1(1_0, s))) → *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0#(tail_1(cons_1(x, s))) → *top*_0#(s) | *top*_0#(h_1(cons_9(1_0, s))) → *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0#(h_1(cons_7(1_0, s))) → *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) | *top*_0#(tail_1(cons_10(x, s))) → *top*_0#(s) |
*top*_0#(h_1(cons_8(1_0, s))) → *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) | *top*_0#(h_1(cons_2(0_0, s))) → *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0#(h_1(cons_3(0_0, s))) → *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | *top*_0#(tail_1(cons_5(x, s))) → *top*_0#(s) |
*top*_0#(h_1(cons_4(0_0, s))) → *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | *top*_0#(h_1(cons_6(0_0, s))) → *top*_0#(cons_6(0_0, cons_8(1_0, h_1(s)))) |
*top*_0#(h_1(cons_1(0_0, s))) → *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | *top*_0#(tail_1(cons_6(x, s))) → *top*_0#(s) |
*top*_0#(h_1(cons_11(1_0, s))) → *top*_0#(cons_10(1_0, cons_3(0_0, h_1(s)))) |
T(h_0(s)) → h_0#(s) | T(cons_1(x_1, x_2)) → T(x_2) |
tail_1#(cons_8(x, s)) → T(s) | tail_1#(cons_4(x, s)) → T(s) |
T(cons_10(x_1, x_2)) → T(x_2) | T(tail_0(x_1)) → T(x_1) |
T(cons_6(x_1, x_2)) → T(x_2) | T(h_1(x_1)) → T(x_1) |
tail_1#(cons_9(x, s)) → T(s) | tail_1#(cons_7(x, s)) → T(s) |
tail_1#(cons_3(x, s)) → T(s) | T(tail_0(M_1)) → tail_0#(M_1) |
tail_1#(cons_2(x, s)) → T(s) | tail_0#(tail_1(cons_5(x, s))) → tail_1#(s) |
tail_0#(tail_1(cons_6(x, s))) → tail_1#(s) | tail_1#(cons_1(x, s)) → T(s) |
h_0#(tail_1(cons_1(x, s))) → T(s) | tail_0#(tail_1(cons_1(x, s))) → tail_1#(s) |
tail_0#(tail_1(cons_10(x, s))) → tail_1#(s) | T(h_0(x_1)) → T(x_1) |
h_0#(tail_1(cons_1(x, s))) → h_0#(s) | tail_0#(tail_1(cons_11(x, s))) → tail_1#(s) |
Problem 2: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
T(cons_1(x_1, x_2)) | → | T(x_2) | | T(h_0(s)) | → | h_0#(s) |
tail_1#(cons_8(x, s)) | → | T(s) | | T(cons_10(x_1, x_2)) | → | T(x_2) |
tail_1#(cons_4(x, s)) | → | T(s) | | T(cons_6(x_1, x_2)) | → | T(x_2) |
T(tail_0(x_1)) | → | T(x_1) | | T(h_1(x_1)) | → | T(x_1) |
tail_1#(cons_9(x, s)) | → | T(s) | | tail_1#(cons_3(x, s)) | → | T(s) |
tail_1#(cons_7(x, s)) | → | T(s) | | T(tail_0(M_1)) | → | tail_0#(M_1) |
tail_1#(cons_2(x, s)) | → | T(s) | | tail_0#(tail_1(cons_5(x, s))) | → | tail_1#(s) |
tail_0#(tail_1(cons_6(x, s))) | → | tail_1#(s) | | tail_1#(cons_1(x, s)) | → | T(s) |
h_0#(tail_1(cons_1(x, s))) | → | T(s) | | tail_0#(tail_1(cons_1(x, s))) | → | tail_1#(s) |
tail_0#(tail_1(cons_10(x, s))) | → | tail_1#(s) | | T(h_0(x_1)) | → | T(x_1) |
h_0#(tail_1(cons_1(x, s))) | → | h_0#(s) | | tail_0#(tail_1(cons_11(x, s))) | → | tail_1#(s) |
Rewrite Rules
M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) | | tail_1(cons_2(x, s)) | → | s |
tail_1(cons_3(x, s)) | → | s | | tail_1(cons_4(x, s)) | → | s |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) | | *top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) |
tail_1(cons_7(x, s)) | → | s | | tail_1(cons_8(x, s)) | → | s |
tail_1(cons_9(x, s)) | → | s | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
*top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_1(cons_1(x, s)) | → | s |
*top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) | | *top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_2(x, s) | → | garbage_collection_0 | | cons_3(x, s) | → | garbage_collection_0 |
cons_4(x, s) | → | garbage_collection_0 | | cons_5(x, s) | → | garbage_collection_0 |
cons_6(x, s) | → | garbage_collection_0 | | cons_7(x, s) | → | garbage_collection_0 |
cons_8(x, s) | → | garbage_collection_0 | | cons_9(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | cons_11(x, s) | → | garbage_collection_0 |
cons_1(x, s) | → | garbage_collection_0 |
Original Signature
Termination of terms over the following signature is verified: garbage_collection_0, cons_3, cons_2, cons_5, cons_4, h_0, cons_1, h_1, 0_0, cons_7, tail_1, cons_11, cons_6, cons_9, cons_10, tail_0, cons_8, 1_0, *top*_0, M_1
Strategy
Context-sensitive strategy:
μ(garbage_collection_0) = μ(cons_3) = μ(cons_2) = μ(M_1#) = μ(cons_5) = μ(cons_4) = μ(cons_5#) = μ(cons_1#) = μ(cons_3#) = μ(cons_1) = μ(h_1) = μ(cons_7#) = μ(cons_7) = μ(tail_1) = μ(cons_11) = μ(cons_6) = μ(cons_9#) = μ(cons_9) = μ(cons_10) = μ(cons_8) = μ(T) = μ(1_0) = μ(tail_1#) = μ(cons_2#) = μ(cons_11#) = μ(cons_4#) = μ(cons_6#) = μ(cons_8#) = μ(0_0) = μ(M_1) = μ(cons_10#) = ∅
μ(h_0) = μ(tail_0) = μ(*top*_0#) = μ(h_0#) = μ(*top*_0) = μ(tail_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 1
- 0_0: 0
- 1_0: 0
- M_1: 0
- T(x): 0
- cons_1(x,y): y
- cons_10(x,y): y
- cons_11(x,y): y + x
- cons_2(x,y): y
- cons_3(x,y): 2y
- cons_4(x,y): y + x + 2
- cons_5(x,y): y + 3x
- cons_6(x,y): y
- cons_7(x,y): y
- cons_8(x,y): y
- cons_9(x,y): 2y + 2
- garbage_collection_0: 0
- h_0(x): 0
- h_0#(x): 0
- h_1(x): 0
- tail_0(x): 2x
- tail_0#(x): 2x
- tail_1(x): x
- tail_1#(x): x
Standard Usable rules
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_2(x, s)) | → | s |
*top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_2(x, s) | → | garbage_collection_0 |
cons_3(x, s) | → | garbage_collection_0 | | *top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_1(cons_8(x, s)) | → | s |
cons_5(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_1(x, s) | → | garbage_collection_0 | | cons_4(x, s) | → | garbage_collection_0 |
h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_3(x, s)) | → | s |
*top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_7(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_1(cons_1(x, s)) | → | s | | cons_9(x, s) | → | garbage_collection_0 |
tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_1(cons_4(x, s)) | → | s | | cons_11(x, s) | → | garbage_collection_0 |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | tail_1(cons_7(x, s)) | → | s |
h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_6(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) | | tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_8(x, s) | → | garbage_collection_0 | | tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) |
tail_1(cons_9(x, s)) | → | s | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
tail_1#(cons_4(x, s)) | → | T(s) | | tail_1#(cons_9(x, s)) | → | T(s) |
Problem 4: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
T(cons_1(x_1, x_2)) | → | T(x_2) | | T(h_0(s)) | → | h_0#(s) |
tail_1#(cons_8(x, s)) | → | T(s) | | T(cons_10(x_1, x_2)) | → | T(x_2) |
T(cons_6(x_1, x_2)) | → | T(x_2) | | T(tail_0(x_1)) | → | T(x_1) |
T(h_1(x_1)) | → | T(x_1) | | tail_1#(cons_3(x, s)) | → | T(s) |
tail_1#(cons_7(x, s)) | → | T(s) | | T(tail_0(M_1)) | → | tail_0#(M_1) |
tail_1#(cons_2(x, s)) | → | T(s) | | tail_0#(tail_1(cons_5(x, s))) | → | tail_1#(s) |
tail_0#(tail_1(cons_6(x, s))) | → | tail_1#(s) | | tail_1#(cons_1(x, s)) | → | T(s) |
h_0#(tail_1(cons_1(x, s))) | → | T(s) | | tail_0#(tail_1(cons_10(x, s))) | → | tail_1#(s) |
tail_0#(tail_1(cons_1(x, s))) | → | tail_1#(s) | | tail_0#(tail_1(cons_11(x, s))) | → | tail_1#(s) |
h_0#(tail_1(cons_1(x, s))) | → | h_0#(s) | | T(h_0(x_1)) | → | T(x_1) |
Rewrite Rules
M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) | | tail_1(cons_2(x, s)) | → | s |
tail_1(cons_3(x, s)) | → | s | | tail_1(cons_4(x, s)) | → | s |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) | | *top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) |
tail_1(cons_7(x, s)) | → | s | | tail_1(cons_8(x, s)) | → | s |
tail_1(cons_9(x, s)) | → | s | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
*top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_1(cons_1(x, s)) | → | s |
*top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) | | *top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_2(x, s) | → | garbage_collection_0 | | cons_3(x, s) | → | garbage_collection_0 |
cons_4(x, s) | → | garbage_collection_0 | | cons_5(x, s) | → | garbage_collection_0 |
cons_6(x, s) | → | garbage_collection_0 | | cons_7(x, s) | → | garbage_collection_0 |
cons_8(x, s) | → | garbage_collection_0 | | cons_9(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | cons_11(x, s) | → | garbage_collection_0 |
cons_1(x, s) | → | garbage_collection_0 |
Original Signature
Termination of terms over the following signature is verified: garbage_collection_0, cons_3, cons_2, cons_5, cons_4, h_0, cons_1, h_1, 0_0, cons_7, tail_1, cons_11, cons_6, cons_10, cons_9, cons_8, tail_0, 1_0, *top*_0, M_1
Strategy
Context-sensitive strategy:
μ(cons_3) = μ(garbage_collection_0) = μ(cons_2) = μ(cons_5) = μ(M_1#) = μ(cons_1#) = μ(cons_5#) = μ(cons_4) = μ(cons_3#) = μ(cons_1) = μ(h_1) = μ(cons_7#) = μ(cons_7) = μ(tail_1) = μ(cons_11) = μ(cons_6) = μ(cons_9#) = μ(cons_9) = μ(cons_10) = μ(cons_8) = μ(T) = μ(1_0) = μ(cons_2#) = μ(tail_1#) = μ(cons_11#) = μ(cons_4#) = μ(cons_6#) = μ(cons_8#) = μ(0_0) = μ(M_1) = μ(cons_10#) = ∅
μ(h_0) = μ(tail_0) = μ(*top*_0#) = μ(h_0#) = μ(*top*_0) = μ(tail_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 1
- 0_0: 0
- 1_0: 0
- M_1: 0
- T(x): 0
- cons_1(x,y): 2y
- cons_10(x,y): 2y
- cons_11(x,y): y
- cons_2(x,y): 2y
- cons_3(x,y): 2y
- cons_4(x,y): 2y + 3x
- cons_5(x,y): 2y + 1
- cons_6(x,y): y
- cons_7(x,y): 2y
- cons_8(x,y): y
- cons_9(x,y): y + 1
- garbage_collection_0: 0
- h_0(x): 0
- h_0#(x): 0
- h_1(x): 0
- tail_0(x): 2x
- tail_0#(x): 2x
- tail_1(x): x
- tail_1#(x): 0
Standard Usable rules
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_2(x, s)) | → | s |
*top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_2(x, s) | → | garbage_collection_0 |
cons_3(x, s) | → | garbage_collection_0 | | *top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_1(cons_8(x, s)) | → | s |
cons_5(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_1(x, s) | → | garbage_collection_0 | | cons_4(x, s) | → | garbage_collection_0 |
h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_3(x, s)) | → | s |
*top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_7(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_1(cons_1(x, s)) | → | s | | cons_9(x, s) | → | garbage_collection_0 |
tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_1(cons_4(x, s)) | → | s | | cons_11(x, s) | → | garbage_collection_0 |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | tail_1(cons_7(x, s)) | → | s |
h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_6(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) | | tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_8(x, s) | → | garbage_collection_0 | | tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) |
tail_1(cons_9(x, s)) | → | s | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
tail_0#(tail_1(cons_5(x, s))) | → | tail_1#(s) |
Problem 6: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
T(cons_1(x_1, x_2)) | → | T(x_2) | | T(h_0(s)) | → | h_0#(s) |
tail_1#(cons_8(x, s)) | → | T(s) | | T(cons_10(x_1, x_2)) | → | T(x_2) |
T(cons_6(x_1, x_2)) | → | T(x_2) | | T(tail_0(x_1)) | → | T(x_1) |
T(h_1(x_1)) | → | T(x_1) | | tail_1#(cons_3(x, s)) | → | T(s) |
tail_1#(cons_7(x, s)) | → | T(s) | | T(tail_0(M_1)) | → | tail_0#(M_1) |
tail_1#(cons_2(x, s)) | → | T(s) | | tail_0#(tail_1(cons_6(x, s))) | → | tail_1#(s) |
tail_1#(cons_1(x, s)) | → | T(s) | | h_0#(tail_1(cons_1(x, s))) | → | T(s) |
tail_0#(tail_1(cons_1(x, s))) | → | tail_1#(s) | | tail_0#(tail_1(cons_10(x, s))) | → | tail_1#(s) |
T(h_0(x_1)) | → | T(x_1) | | h_0#(tail_1(cons_1(x, s))) | → | h_0#(s) |
tail_0#(tail_1(cons_11(x, s))) | → | tail_1#(s) |
Rewrite Rules
M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) | | tail_1(cons_2(x, s)) | → | s |
tail_1(cons_3(x, s)) | → | s | | tail_1(cons_4(x, s)) | → | s |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) | | *top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) |
tail_1(cons_7(x, s)) | → | s | | tail_1(cons_8(x, s)) | → | s |
tail_1(cons_9(x, s)) | → | s | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
*top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_1(cons_1(x, s)) | → | s |
*top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) | | *top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_2(x, s) | → | garbage_collection_0 | | cons_3(x, s) | → | garbage_collection_0 |
cons_4(x, s) | → | garbage_collection_0 | | cons_5(x, s) | → | garbage_collection_0 |
cons_6(x, s) | → | garbage_collection_0 | | cons_7(x, s) | → | garbage_collection_0 |
cons_8(x, s) | → | garbage_collection_0 | | cons_9(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | cons_11(x, s) | → | garbage_collection_0 |
cons_1(x, s) | → | garbage_collection_0 |
Original Signature
Termination of terms over the following signature is verified: garbage_collection_0, cons_3, cons_2, cons_5, cons_4, h_0, cons_1, h_1, 0_0, cons_7, tail_1, cons_11, cons_6, cons_9, cons_10, tail_0, cons_8, 1_0, *top*_0, M_1
Strategy
Context-sensitive strategy:
μ(garbage_collection_0) = μ(cons_3) = μ(cons_2) = μ(M_1#) = μ(cons_5) = μ(cons_4) = μ(cons_5#) = μ(cons_1#) = μ(cons_3#) = μ(cons_1) = μ(h_1) = μ(cons_7#) = μ(cons_7) = μ(tail_1) = μ(cons_11) = μ(cons_6) = μ(cons_9#) = μ(cons_9) = μ(cons_10) = μ(cons_8) = μ(T) = μ(1_0) = μ(tail_1#) = μ(cons_2#) = μ(cons_11#) = μ(cons_4#) = μ(cons_6#) = μ(cons_8#) = μ(0_0) = μ(M_1) = μ(cons_10#) = ∅
μ(h_0) = μ(tail_0) = μ(*top*_0#) = μ(h_0#) = μ(*top*_0) = μ(tail_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 1
- 0_0: 0
- 1_0: 0
- M_1: 0
- T(x): 2
- cons_1(x,y): y + 3x
- cons_10(x,y): y + 3x
- cons_11(x,y): y + 2x
- cons_2(x,y): 3y
- cons_3(x,y): 2y + x
- cons_4(x,y): 2y + 1
- cons_5(x,y): y
- cons_6(x,y): 2y + x
- cons_7(x,y): 3y
- cons_8(x,y): y
- cons_9(x,y): y + 1
- garbage_collection_0: 0
- h_0(x): 0
- h_0#(x): 2
- h_1(x): 0
- tail_0(x): x + 2
- tail_0#(x): 2x
- tail_1(x): 2x + 1
- tail_1#(x): 2
Standard Usable rules
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_2(x, s)) | → | s |
*top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_2(x, s) | → | garbage_collection_0 |
cons_3(x, s) | → | garbage_collection_0 | | *top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_1(cons_8(x, s)) | → | s |
cons_5(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_1(x, s) | → | garbage_collection_0 | | cons_4(x, s) | → | garbage_collection_0 |
h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_3(x, s)) | → | s |
*top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_7(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_1(cons_1(x, s)) | → | s | | cons_9(x, s) | → | garbage_collection_0 |
tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_1(cons_4(x, s)) | → | s | | cons_11(x, s) | → | garbage_collection_0 |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | tail_1(cons_7(x, s)) | → | s |
h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_6(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) | | tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_8(x, s) | → | garbage_collection_0 | | tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) |
tail_1(cons_9(x, s)) | → | s | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
T(tail_0(M_1)) | → | tail_0#(M_1) |
Problem 8: DependencyGraph
Dependency Pair Problem
Dependency Pairs
T(cons_1(x_1, x_2)) | → | T(x_2) | | T(h_0(s)) | → | h_0#(s) |
tail_1#(cons_8(x, s)) | → | T(s) | | T(cons_10(x_1, x_2)) | → | T(x_2) |
T(cons_6(x_1, x_2)) | → | T(x_2) | | T(tail_0(x_1)) | → | T(x_1) |
T(h_1(x_1)) | → | T(x_1) | | tail_1#(cons_3(x, s)) | → | T(s) |
tail_1#(cons_7(x, s)) | → | T(s) | | tail_1#(cons_2(x, s)) | → | T(s) |
tail_0#(tail_1(cons_6(x, s))) | → | tail_1#(s) | | tail_1#(cons_1(x, s)) | → | T(s) |
h_0#(tail_1(cons_1(x, s))) | → | T(s) | | tail_0#(tail_1(cons_10(x, s))) | → | tail_1#(s) |
tail_0#(tail_1(cons_1(x, s))) | → | tail_1#(s) | | tail_0#(tail_1(cons_11(x, s))) | → | tail_1#(s) |
h_0#(tail_1(cons_1(x, s))) | → | h_0#(s) | | T(h_0(x_1)) | → | T(x_1) |
Rewrite Rules
M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) | | tail_1(cons_2(x, s)) | → | s |
tail_1(cons_3(x, s)) | → | s | | tail_1(cons_4(x, s)) | → | s |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) | | *top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) |
tail_1(cons_7(x, s)) | → | s | | tail_1(cons_8(x, s)) | → | s |
tail_1(cons_9(x, s)) | → | s | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
*top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_1(cons_1(x, s)) | → | s |
*top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) | | *top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_2(x, s) | → | garbage_collection_0 | | cons_3(x, s) | → | garbage_collection_0 |
cons_4(x, s) | → | garbage_collection_0 | | cons_5(x, s) | → | garbage_collection_0 |
cons_6(x, s) | → | garbage_collection_0 | | cons_7(x, s) | → | garbage_collection_0 |
cons_8(x, s) | → | garbage_collection_0 | | cons_9(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | cons_11(x, s) | → | garbage_collection_0 |
cons_1(x, s) | → | garbage_collection_0 |
Original Signature
Termination of terms over the following signature is verified: garbage_collection_0, cons_3, cons_2, cons_5, cons_4, h_0, cons_1, h_1, 0_0, cons_7, tail_1, cons_11, cons_6, cons_10, cons_9, cons_8, tail_0, 1_0, *top*_0, M_1
Strategy
Context-sensitive strategy:
μ(cons_3) = μ(garbage_collection_0) = μ(cons_2) = μ(cons_5) = μ(M_1#) = μ(cons_1#) = μ(cons_5#) = μ(cons_4) = μ(cons_3#) = μ(cons_1) = μ(h_1) = μ(cons_7#) = μ(cons_7) = μ(tail_1) = μ(cons_11) = μ(cons_6) = μ(cons_9#) = μ(cons_9) = μ(cons_10) = μ(cons_8) = μ(T) = μ(1_0) = μ(cons_2#) = μ(tail_1#) = μ(cons_11#) = μ(cons_4#) = μ(cons_6#) = μ(cons_8#) = μ(0_0) = μ(M_1) = μ(cons_10#) = ∅
μ(h_0) = μ(tail_0) = μ(*top*_0#) = μ(h_0#) = μ(*top*_0) = μ(tail_0#) = {1}
The following SCCs where found
T(h_0(s)) → h_0#(s) | T(cons_1(x_1, x_2)) → T(x_2) |
T(cons_10(x_1, x_2)) → T(x_2) | T(tail_0(x_1)) → T(x_1) |
T(cons_6(x_1, x_2)) → T(x_2) | T(h_1(x_1)) → T(x_1) |
h_0#(tail_1(cons_1(x, s))) → T(s) | T(h_0(x_1)) → T(x_1) |
h_0#(tail_1(cons_1(x, s))) → h_0#(s) |
Problem 3: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
*top*_0#(tail_1(cons_11(x, s))) | → | *top*_0#(s) | | *top*_0#(h_1(cons_10(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0#(h_1(cons_5(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_7(1_0, h_1(s)))) | | *top*_0#(h_1(cons_1(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0#(tail_1(cons_1(x, s))) | → | *top*_0#(s) | | *top*_0#(h_1(cons_7(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0#(h_1(cons_9(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0#(tail_1(cons_10(x, s))) | → | *top*_0#(s) |
*top*_0#(h_1(cons_8(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0#(h_1(cons_2(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0#(h_1(cons_3(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0#(h_1(cons_4(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0#(tail_1(cons_5(x, s))) | → | *top*_0#(s) | | *top*_0#(h_1(cons_6(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_8(1_0, h_1(s)))) |
*top*_0#(h_1(cons_1(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0#(tail_1(cons_6(x, s))) | → | *top*_0#(s) |
*top*_0#(h_1(cons_11(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_3(0_0, h_1(s)))) |
Rewrite Rules
M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) | | tail_1(cons_2(x, s)) | → | s |
tail_1(cons_3(x, s)) | → | s | | tail_1(cons_4(x, s)) | → | s |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) | | *top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) |
tail_1(cons_7(x, s)) | → | s | | tail_1(cons_8(x, s)) | → | s |
tail_1(cons_9(x, s)) | → | s | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
*top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_1(cons_1(x, s)) | → | s |
*top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) | | *top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_2(x, s) | → | garbage_collection_0 | | cons_3(x, s) | → | garbage_collection_0 |
cons_4(x, s) | → | garbage_collection_0 | | cons_5(x, s) | → | garbage_collection_0 |
cons_6(x, s) | → | garbage_collection_0 | | cons_7(x, s) | → | garbage_collection_0 |
cons_8(x, s) | → | garbage_collection_0 | | cons_9(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | cons_11(x, s) | → | garbage_collection_0 |
cons_1(x, s) | → | garbage_collection_0 |
Original Signature
Termination of terms over the following signature is verified: garbage_collection_0, cons_3, cons_2, cons_5, cons_4, h_0, cons_1, h_1, 0_0, cons_7, tail_1, cons_11, cons_6, cons_9, cons_10, tail_0, cons_8, 1_0, *top*_0, M_1
Strategy
Context-sensitive strategy:
μ(garbage_collection_0) = μ(cons_3) = μ(cons_2) = μ(M_1#) = μ(cons_5) = μ(cons_4) = μ(cons_5#) = μ(cons_1#) = μ(cons_3#) = μ(cons_1) = μ(h_1) = μ(cons_7#) = μ(cons_7) = μ(tail_1) = μ(cons_11) = μ(cons_6) = μ(cons_9#) = μ(cons_9) = μ(cons_10) = μ(cons_8) = μ(T) = μ(1_0) = μ(tail_1#) = μ(cons_2#) = μ(cons_11#) = μ(cons_4#) = μ(cons_6#) = μ(cons_8#) = μ(0_0) = μ(M_1) = μ(cons_10#) = ∅
μ(h_0) = μ(tail_0) = μ(*top*_0#) = μ(h_0#) = μ(*top*_0) = μ(tail_0#) = {1}
Polynomial Interpretation
- *top*_0(x): x + 1
- *top*_0#(x): 2x
- 0_0: 0
- 1_0: 0
- M_1: 0
- cons_1(x,y): 2y
- cons_10(x,y): y
- cons_11(x,y): y + 3x
- cons_2(x,y): 2y
- cons_3(x,y): 2y
- cons_4(x,y): y
- cons_5(x,y): y + 1
- cons_6(x,y): 2y
- cons_7(x,y): 2y
- cons_8(x,y): y + 3x
- cons_9(x,y): y
- garbage_collection_0: 0
- h_0(x): 0
- h_1(x): 0
- tail_0(x): 2x
- tail_1(x): x
Standard Usable rules
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_2(x, s)) | → | s |
*top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_2(x, s) | → | garbage_collection_0 |
cons_3(x, s) | → | garbage_collection_0 | | *top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_1(cons_8(x, s)) | → | s |
cons_5(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_1(x, s) | → | garbage_collection_0 | | cons_4(x, s) | → | garbage_collection_0 |
h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_3(x, s)) | → | s |
*top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_7(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_1(cons_1(x, s)) | → | s | | cons_9(x, s) | → | garbage_collection_0 |
tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_1(cons_4(x, s)) | → | s | | cons_11(x, s) | → | garbage_collection_0 |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | tail_1(cons_7(x, s)) | → | s |
h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_6(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) | | tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_8(x, s) | → | garbage_collection_0 | | tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) |
tail_1(cons_9(x, s)) | → | s | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
*top*_0#(tail_1(cons_5(x, s))) | → | *top*_0#(s) |
Problem 5: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
*top*_0#(tail_1(cons_11(x, s))) | → | *top*_0#(s) | | *top*_0#(h_1(cons_10(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0#(h_1(cons_5(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_7(1_0, h_1(s)))) | | *top*_0#(h_1(cons_1(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0#(tail_1(cons_1(x, s))) | → | *top*_0#(s) | | *top*_0#(h_1(cons_7(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0#(h_1(cons_9(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0#(tail_1(cons_10(x, s))) | → | *top*_0#(s) |
*top*_0#(h_1(cons_8(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0#(h_1(cons_2(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0#(h_1(cons_3(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0#(h_1(cons_4(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0#(h_1(cons_6(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0#(tail_1(cons_6(x, s))) | → | *top*_0#(s) |
*top*_0#(h_1(cons_1(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0#(h_1(cons_11(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_3(0_0, h_1(s)))) |
Rewrite Rules
M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) | | tail_1(cons_2(x, s)) | → | s |
tail_1(cons_3(x, s)) | → | s | | tail_1(cons_4(x, s)) | → | s |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) | | *top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) |
tail_1(cons_7(x, s)) | → | s | | tail_1(cons_8(x, s)) | → | s |
tail_1(cons_9(x, s)) | → | s | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
*top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_1(cons_1(x, s)) | → | s |
*top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) | | *top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_2(x, s) | → | garbage_collection_0 | | cons_3(x, s) | → | garbage_collection_0 |
cons_4(x, s) | → | garbage_collection_0 | | cons_5(x, s) | → | garbage_collection_0 |
cons_6(x, s) | → | garbage_collection_0 | | cons_7(x, s) | → | garbage_collection_0 |
cons_8(x, s) | → | garbage_collection_0 | | cons_9(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | cons_11(x, s) | → | garbage_collection_0 |
cons_1(x, s) | → | garbage_collection_0 |
Original Signature
Termination of terms over the following signature is verified: garbage_collection_0, cons_3, cons_2, cons_5, cons_4, h_0, cons_1, h_1, 0_0, cons_7, tail_1, cons_11, cons_6, cons_10, cons_9, cons_8, tail_0, 1_0, *top*_0, M_1
Strategy
Context-sensitive strategy:
μ(cons_3) = μ(garbage_collection_0) = μ(cons_2) = μ(cons_5) = μ(M_1#) = μ(cons_1#) = μ(cons_5#) = μ(cons_4) = μ(cons_3#) = μ(cons_1) = μ(h_1) = μ(cons_7#) = μ(cons_7) = μ(tail_1) = μ(cons_11) = μ(cons_6) = μ(cons_9#) = μ(cons_9) = μ(cons_10) = μ(cons_8) = μ(T) = μ(1_0) = μ(cons_2#) = μ(tail_1#) = μ(cons_11#) = μ(cons_4#) = μ(cons_6#) = μ(cons_8#) = μ(0_0) = μ(M_1) = μ(cons_10#) = ∅
μ(h_0) = μ(tail_0) = μ(*top*_0#) = μ(h_0#) = μ(*top*_0) = μ(tail_0#) = {1}
Polynomial Interpretation
- *top*_0(x): x + 1
- *top*_0#(x): 2x
- 0_0: 0
- 1_0: 0
- M_1: 0
- cons_1(x,y): 2y
- cons_10(x,y): 2y
- cons_11(x,y): y + 1
- cons_2(x,y): 2y
- cons_3(x,y): y
- cons_4(x,y): y
- cons_5(x,y): y + 1
- cons_6(x,y): y
- cons_7(x,y): y
- cons_8(x,y): 2y
- cons_9(x,y): y
- garbage_collection_0: 0
- h_0(x): 0
- h_1(x): 0
- tail_0(x): x
- tail_1(x): x
Standard Usable rules
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_2(x, s)) | → | s |
*top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_2(x, s) | → | garbage_collection_0 |
cons_3(x, s) | → | garbage_collection_0 | | *top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_1(cons_8(x, s)) | → | s |
cons_5(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_1(x, s) | → | garbage_collection_0 | | cons_4(x, s) | → | garbage_collection_0 |
h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_3(x, s)) | → | s |
*top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_7(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_1(cons_1(x, s)) | → | s | | cons_9(x, s) | → | garbage_collection_0 |
tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_1(cons_4(x, s)) | → | s | | cons_11(x, s) | → | garbage_collection_0 |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | tail_1(cons_7(x, s)) | → | s |
h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_6(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) | | tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_8(x, s) | → | garbage_collection_0 | | tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) |
tail_1(cons_9(x, s)) | → | s | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
*top*_0#(tail_1(cons_11(x, s))) | → | *top*_0#(s) |
Problem 7: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
*top*_0#(h_1(cons_10(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_2(0_0, h_1(s)))) | | *top*_0#(h_1(cons_5(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0#(h_1(cons_1(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0#(tail_1(cons_1(x, s))) | → | *top*_0#(s) |
*top*_0#(h_1(cons_7(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0#(h_1(cons_9(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0#(tail_1(cons_10(x, s))) | → | *top*_0#(s) | | *top*_0#(h_1(cons_8(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0#(h_1(cons_2(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0#(h_1(cons_3(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0#(h_1(cons_4(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0#(h_1(cons_6(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_8(1_0, h_1(s)))) |
*top*_0#(h_1(cons_1(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0#(tail_1(cons_6(x, s))) | → | *top*_0#(s) |
*top*_0#(h_1(cons_11(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_3(0_0, h_1(s)))) |
Rewrite Rules
M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) | | tail_1(cons_2(x, s)) | → | s |
tail_1(cons_3(x, s)) | → | s | | tail_1(cons_4(x, s)) | → | s |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) | | *top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) |
tail_1(cons_7(x, s)) | → | s | | tail_1(cons_8(x, s)) | → | s |
tail_1(cons_9(x, s)) | → | s | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
*top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_1(cons_1(x, s)) | → | s |
*top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) | | *top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_2(x, s) | → | garbage_collection_0 | | cons_3(x, s) | → | garbage_collection_0 |
cons_4(x, s) | → | garbage_collection_0 | | cons_5(x, s) | → | garbage_collection_0 |
cons_6(x, s) | → | garbage_collection_0 | | cons_7(x, s) | → | garbage_collection_0 |
cons_8(x, s) | → | garbage_collection_0 | | cons_9(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | cons_11(x, s) | → | garbage_collection_0 |
cons_1(x, s) | → | garbage_collection_0 |
Original Signature
Termination of terms over the following signature is verified: garbage_collection_0, cons_3, cons_2, cons_5, cons_4, h_0, cons_1, h_1, 0_0, cons_7, tail_1, cons_11, cons_6, cons_9, cons_10, tail_0, cons_8, 1_0, *top*_0, M_1
Strategy
Context-sensitive strategy:
μ(garbage_collection_0) = μ(cons_3) = μ(cons_2) = μ(M_1#) = μ(cons_5) = μ(cons_4) = μ(cons_5#) = μ(cons_1#) = μ(cons_3#) = μ(cons_1) = μ(h_1) = μ(cons_7#) = μ(cons_7) = μ(tail_1) = μ(cons_11) = μ(cons_6) = μ(cons_9#) = μ(cons_9) = μ(cons_10) = μ(cons_8) = μ(T) = μ(1_0) = μ(tail_1#) = μ(cons_2#) = μ(cons_11#) = μ(cons_4#) = μ(cons_6#) = μ(cons_8#) = μ(0_0) = μ(M_1) = μ(cons_10#) = ∅
μ(h_0) = μ(tail_0) = μ(*top*_0#) = μ(h_0#) = μ(*top*_0) = μ(tail_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 0
- *top*_0#(x): 2x
- 0_0: 0
- 1_0: 0
- M_1: 0
- cons_1(x,y): 2y
- cons_10(x,y): 2y
- cons_11(x,y): 2y
- cons_2(x,y): 2y
- cons_3(x,y): y
- cons_4(x,y): 3y + 3x
- cons_5(x,y): y + 1
- cons_6(x,y): 2y
- cons_7(x,y): y + x
- cons_8(x,y): y + 3x
- cons_9(x,y): y
- garbage_collection_0: 0
- h_0(x): 0
- h_1(x): 0
- tail_0(x): x + 1
- tail_1(x): x + 1
Standard Usable rules
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_2(x, s)) | → | s |
*top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_2(x, s) | → | garbage_collection_0 |
cons_3(x, s) | → | garbage_collection_0 | | *top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_1(cons_8(x, s)) | → | s |
cons_5(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_1(x, s) | → | garbage_collection_0 | | cons_4(x, s) | → | garbage_collection_0 |
h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_3(x, s)) | → | s |
*top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_7(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_1(cons_1(x, s)) | → | s | | cons_9(x, s) | → | garbage_collection_0 |
tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_1(cons_4(x, s)) | → | s | | cons_11(x, s) | → | garbage_collection_0 |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | tail_1(cons_7(x, s)) | → | s |
h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_6(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) | | tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_8(x, s) | → | garbage_collection_0 | | tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) |
tail_1(cons_9(x, s)) | → | s | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
*top*_0#(tail_1(cons_1(x, s))) | → | *top*_0#(s) | | *top*_0#(tail_1(cons_10(x, s))) | → | *top*_0#(s) |
*top*_0#(tail_1(cons_6(x, s))) | → | *top*_0#(s) |
Problem 9: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
*top*_0#(h_1(cons_8(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0#(h_1(cons_2(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0#(h_1(cons_5(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_7(1_0, h_1(s)))) | | *top*_0#(h_1(cons_10(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0#(h_1(cons_1(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0#(h_1(cons_3(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0#(h_1(cons_9(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0#(h_1(cons_7(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0#(h_1(cons_4(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0#(h_1(cons_6(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_8(1_0, h_1(s)))) |
*top*_0#(h_1(cons_1(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0#(h_1(cons_11(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_3(0_0, h_1(s)))) |
Rewrite Rules
M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) | | tail_1(cons_2(x, s)) | → | s |
tail_1(cons_3(x, s)) | → | s | | tail_1(cons_4(x, s)) | → | s |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) | | *top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) |
tail_1(cons_7(x, s)) | → | s | | tail_1(cons_8(x, s)) | → | s |
tail_1(cons_9(x, s)) | → | s | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
*top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_1(cons_1(x, s)) | → | s |
*top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) | | *top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_2(x, s) | → | garbage_collection_0 | | cons_3(x, s) | → | garbage_collection_0 |
cons_4(x, s) | → | garbage_collection_0 | | cons_5(x, s) | → | garbage_collection_0 |
cons_6(x, s) | → | garbage_collection_0 | | cons_7(x, s) | → | garbage_collection_0 |
cons_8(x, s) | → | garbage_collection_0 | | cons_9(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | cons_11(x, s) | → | garbage_collection_0 |
cons_1(x, s) | → | garbage_collection_0 |
Original Signature
Termination of terms over the following signature is verified: garbage_collection_0, cons_3, cons_2, cons_5, cons_4, h_0, cons_1, h_1, 0_0, cons_7, tail_1, cons_11, cons_6, cons_10, cons_9, cons_8, tail_0, 1_0, *top*_0, M_1
Strategy
Context-sensitive strategy:
μ(cons_3) = μ(garbage_collection_0) = μ(cons_2) = μ(cons_5) = μ(M_1#) = μ(cons_1#) = μ(cons_5#) = μ(cons_4) = μ(cons_3#) = μ(cons_1) = μ(h_1) = μ(cons_7#) = μ(cons_7) = μ(tail_1) = μ(cons_11) = μ(cons_6) = μ(cons_9#) = μ(cons_9) = μ(cons_10) = μ(cons_8) = μ(T) = μ(1_0) = μ(cons_2#) = μ(tail_1#) = μ(cons_11#) = μ(cons_4#) = μ(cons_6#) = μ(cons_8#) = μ(0_0) = μ(M_1) = μ(cons_10#) = ∅
μ(h_0) = μ(tail_0) = μ(*top*_0#) = μ(h_0#) = μ(*top*_0) = μ(tail_0#) = {1}
Polynomial Interpretation
- *top*_0(x): x + 1
- *top*_0#(x): 2x + 1
- 0_0: 0
- 1_0: 0
- M_1: 0
- cons_1(x,y): y
- cons_10(x,y): y
- cons_11(x,y): y
- cons_2(x,y): y
- cons_3(x,y): y
- cons_4(x,y): y
- cons_5(x,y): y + 1
- cons_6(x,y): y
- cons_7(x,y): y
- cons_8(x,y): y
- cons_9(x,y): 2y
- garbage_collection_0: 0
- h_0(x): x
- h_1(x): x
- tail_0(x): x
- tail_1(x): x
Standard Usable rules
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_2(x, s)) | → | s |
*top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_2(x, s) | → | garbage_collection_0 |
cons_3(x, s) | → | garbage_collection_0 | | *top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_1(cons_8(x, s)) | → | s |
cons_5(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_1(x, s) | → | garbage_collection_0 | | cons_4(x, s) | → | garbage_collection_0 |
h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_3(x, s)) | → | s |
*top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_7(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_1(cons_1(x, s)) | → | s | | cons_9(x, s) | → | garbage_collection_0 |
tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_1(cons_4(x, s)) | → | s | | cons_11(x, s) | → | garbage_collection_0 |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | tail_1(cons_7(x, s)) | → | s |
h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_6(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) | | tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_8(x, s) | → | garbage_collection_0 | | tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) |
tail_1(cons_9(x, s)) | → | s | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
*top*_0#(h_1(cons_5(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_7(1_0, h_1(s)))) |
Problem 11: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
*top*_0#(h_1(cons_8(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0#(h_1(cons_10(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0#(h_1(cons_2(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0#(h_1(cons_1(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0#(h_1(cons_3(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0#(h_1(cons_7(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0#(h_1(cons_9(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0#(h_1(cons_4(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0#(h_1(cons_6(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0#(h_1(cons_1(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0#(h_1(cons_11(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_3(0_0, h_1(s)))) |
Rewrite Rules
M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) | | tail_1(cons_2(x, s)) | → | s |
tail_1(cons_3(x, s)) | → | s | | tail_1(cons_4(x, s)) | → | s |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) | | *top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) |
tail_1(cons_7(x, s)) | → | s | | tail_1(cons_8(x, s)) | → | s |
tail_1(cons_9(x, s)) | → | s | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
*top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_1(cons_1(x, s)) | → | s |
*top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) | | *top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_2(x, s) | → | garbage_collection_0 | | cons_3(x, s) | → | garbage_collection_0 |
cons_4(x, s) | → | garbage_collection_0 | | cons_5(x, s) | → | garbage_collection_0 |
cons_6(x, s) | → | garbage_collection_0 | | cons_7(x, s) | → | garbage_collection_0 |
cons_8(x, s) | → | garbage_collection_0 | | cons_9(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | cons_11(x, s) | → | garbage_collection_0 |
cons_1(x, s) | → | garbage_collection_0 |
Original Signature
Termination of terms over the following signature is verified: garbage_collection_0, cons_3, cons_2, cons_5, cons_4, h_0, cons_1, h_1, 0_0, cons_7, tail_1, cons_11, cons_6, cons_9, cons_10, tail_0, cons_8, 1_0, *top*_0, M_1
Strategy
Context-sensitive strategy:
μ(garbage_collection_0) = μ(cons_3) = μ(cons_2) = μ(M_1#) = μ(cons_5) = μ(cons_4) = μ(cons_5#) = μ(cons_1#) = μ(cons_3#) = μ(cons_1) = μ(h_1) = μ(cons_7#) = μ(cons_7) = μ(tail_1) = μ(cons_11) = μ(cons_6) = μ(cons_9#) = μ(cons_9) = μ(cons_10) = μ(cons_8) = μ(T) = μ(1_0) = μ(tail_1#) = μ(cons_2#) = μ(cons_11#) = μ(cons_4#) = μ(cons_6#) = μ(cons_8#) = μ(0_0) = μ(M_1) = μ(cons_10#) = ∅
μ(h_0) = μ(tail_0) = μ(*top*_0#) = μ(h_0#) = μ(*top*_0) = μ(tail_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 0
- *top*_0#(x): 2x
- 0_0: 0
- 1_0: 0
- M_1: 0
- cons_1(x,y): y
- cons_10(x,y): y
- cons_11(x,y): 2y + 2x
- cons_2(x,y): y
- cons_3(x,y): 2y
- cons_4(x,y): y
- cons_5(x,y): y + 2x + 1
- cons_6(x,y): y
- cons_7(x,y): y + 1
- cons_8(x,y): y
- cons_9(x,y): 2y
- garbage_collection_0: 0
- h_0(x): x
- h_1(x): x
- tail_0(x): 2x
- tail_1(x): x
Standard Usable rules
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_2(x, s)) | → | s |
*top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_2(x, s) | → | garbage_collection_0 |
cons_3(x, s) | → | garbage_collection_0 | | *top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_1(cons_8(x, s)) | → | s |
cons_5(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_1(x, s) | → | garbage_collection_0 | | cons_4(x, s) | → | garbage_collection_0 |
h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_3(x, s)) | → | s |
*top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_7(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_1(cons_1(x, s)) | → | s | | cons_9(x, s) | → | garbage_collection_0 |
tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_1(cons_4(x, s)) | → | s | | cons_11(x, s) | → | garbage_collection_0 |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | tail_1(cons_7(x, s)) | → | s |
h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_6(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) | | tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_8(x, s) | → | garbage_collection_0 | | tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) |
tail_1(cons_9(x, s)) | → | s | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
*top*_0#(h_1(cons_7(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) |
Problem 12: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
*top*_0#(h_1(cons_8(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0#(h_1(cons_2(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0#(h_1(cons_10(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_2(0_0, h_1(s)))) | | *top*_0#(h_1(cons_1(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0#(h_1(cons_3(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0#(h_1(cons_9(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0#(h_1(cons_4(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0#(h_1(cons_6(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_8(1_0, h_1(s)))) |
*top*_0#(h_1(cons_1(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0#(h_1(cons_11(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_3(0_0, h_1(s)))) |
Rewrite Rules
M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) | | tail_1(cons_2(x, s)) | → | s |
tail_1(cons_3(x, s)) | → | s | | tail_1(cons_4(x, s)) | → | s |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) | | *top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) |
tail_1(cons_7(x, s)) | → | s | | tail_1(cons_8(x, s)) | → | s |
tail_1(cons_9(x, s)) | → | s | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
*top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_1(cons_1(x, s)) | → | s |
*top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) | | *top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_2(x, s) | → | garbage_collection_0 | | cons_3(x, s) | → | garbage_collection_0 |
cons_4(x, s) | → | garbage_collection_0 | | cons_5(x, s) | → | garbage_collection_0 |
cons_6(x, s) | → | garbage_collection_0 | | cons_7(x, s) | → | garbage_collection_0 |
cons_8(x, s) | → | garbage_collection_0 | | cons_9(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | cons_11(x, s) | → | garbage_collection_0 |
cons_1(x, s) | → | garbage_collection_0 |
Original Signature
Termination of terms over the following signature is verified: garbage_collection_0, cons_3, cons_2, cons_5, cons_4, h_0, cons_1, h_1, 0_0, cons_7, tail_1, cons_11, cons_6, cons_10, cons_9, cons_8, tail_0, 1_0, *top*_0, M_1
Strategy
Context-sensitive strategy:
μ(cons_3) = μ(garbage_collection_0) = μ(cons_2) = μ(cons_5) = μ(M_1#) = μ(cons_1#) = μ(cons_5#) = μ(cons_4) = μ(cons_3#) = μ(cons_1) = μ(h_1) = μ(cons_7#) = μ(cons_7) = μ(tail_1) = μ(cons_11) = μ(cons_6) = μ(cons_9#) = μ(cons_9) = μ(cons_10) = μ(cons_8) = μ(T) = μ(1_0) = μ(cons_2#) = μ(tail_1#) = μ(cons_11#) = μ(cons_4#) = μ(cons_6#) = μ(cons_8#) = μ(0_0) = μ(M_1) = μ(cons_10#) = ∅
μ(h_0) = μ(tail_0) = μ(*top*_0#) = μ(h_0#) = μ(*top*_0) = μ(tail_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 0
- *top*_0#(x): 2x
- 0_0: 0
- 1_0: 0
- M_1: 0
- cons_1(x,y): y
- cons_10(x,y): y
- cons_11(x,y): 2y
- cons_2(x,y): y
- cons_3(x,y): y
- cons_4(x,y): y
- cons_5(x,y): 3y
- cons_6(x,y): y
- cons_7(x,y): y
- cons_8(x,y): y
- cons_9(x,y): 2y + 1
- garbage_collection_0: 0
- h_0(x): x
- h_1(x): x
- tail_0(x): 2x
- tail_1(x): 2x
Standard Usable rules
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_2(x, s)) | → | s |
*top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_2(x, s) | → | garbage_collection_0 |
cons_3(x, s) | → | garbage_collection_0 | | *top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_1(cons_8(x, s)) | → | s |
cons_5(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_1(x, s) | → | garbage_collection_0 | | cons_4(x, s) | → | garbage_collection_0 |
h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_3(x, s)) | → | s |
*top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_7(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_1(cons_1(x, s)) | → | s | | cons_9(x, s) | → | garbage_collection_0 |
tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_1(cons_4(x, s)) | → | s | | cons_11(x, s) | → | garbage_collection_0 |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | tail_1(cons_7(x, s)) | → | s |
h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_6(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) | | tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_8(x, s) | → | garbage_collection_0 | | tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) |
tail_1(cons_9(x, s)) | → | s | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
*top*_0#(h_1(cons_9(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) |
Problem 13: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
*top*_0#(h_1(cons_8(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0#(h_1(cons_10(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0#(h_1(cons_2(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0#(h_1(cons_1(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0#(h_1(cons_3(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0#(h_1(cons_4(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0#(h_1(cons_6(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0#(h_1(cons_1(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0#(h_1(cons_11(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_3(0_0, h_1(s)))) |
Rewrite Rules
M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) | | tail_1(cons_2(x, s)) | → | s |
tail_1(cons_3(x, s)) | → | s | | tail_1(cons_4(x, s)) | → | s |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) | | *top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) |
tail_1(cons_7(x, s)) | → | s | | tail_1(cons_8(x, s)) | → | s |
tail_1(cons_9(x, s)) | → | s | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
*top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_1(cons_1(x, s)) | → | s |
*top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) | | *top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_2(x, s) | → | garbage_collection_0 | | cons_3(x, s) | → | garbage_collection_0 |
cons_4(x, s) | → | garbage_collection_0 | | cons_5(x, s) | → | garbage_collection_0 |
cons_6(x, s) | → | garbage_collection_0 | | cons_7(x, s) | → | garbage_collection_0 |
cons_8(x, s) | → | garbage_collection_0 | | cons_9(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | cons_11(x, s) | → | garbage_collection_0 |
cons_1(x, s) | → | garbage_collection_0 |
Original Signature
Termination of terms over the following signature is verified: garbage_collection_0, cons_3, cons_2, cons_5, cons_4, h_0, cons_1, h_1, 0_0, cons_7, tail_1, cons_11, cons_6, cons_9, cons_10, tail_0, cons_8, 1_0, *top*_0, M_1
Strategy
Context-sensitive strategy:
μ(garbage_collection_0) = μ(cons_3) = μ(cons_2) = μ(M_1#) = μ(cons_5) = μ(cons_4) = μ(cons_5#) = μ(cons_1#) = μ(cons_3#) = μ(cons_1) = μ(h_1) = μ(cons_7#) = μ(cons_7) = μ(tail_1) = μ(cons_11) = μ(cons_6) = μ(cons_9#) = μ(cons_9) = μ(cons_10) = μ(cons_8) = μ(T) = μ(1_0) = μ(tail_1#) = μ(cons_2#) = μ(cons_11#) = μ(cons_4#) = μ(cons_6#) = μ(cons_8#) = μ(0_0) = μ(M_1) = μ(cons_10#) = ∅
μ(h_0) = μ(tail_0) = μ(*top*_0#) = μ(h_0#) = μ(*top*_0) = μ(tail_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 0
- *top*_0#(x): 2x
- 0_0: 0
- 1_0: 0
- M_1: 0
- cons_1(x,y): y
- cons_10(x,y): y
- cons_11(x,y): 2y + x
- cons_2(x,y): y
- cons_3(x,y): y
- cons_4(x,y): y + 1
- cons_5(x,y): y
- cons_6(x,y): y
- cons_7(x,y): y
- cons_8(x,y): y
- cons_9(x,y): y
- garbage_collection_0: 0
- h_0(x): x
- h_1(x): x
- tail_0(x): 2x
- tail_1(x): 2x
Standard Usable rules
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_2(x, s)) | → | s |
*top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_2(x, s) | → | garbage_collection_0 |
cons_3(x, s) | → | garbage_collection_0 | | *top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_1(cons_8(x, s)) | → | s |
cons_5(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_1(x, s) | → | garbage_collection_0 | | cons_4(x, s) | → | garbage_collection_0 |
h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_3(x, s)) | → | s |
*top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_7(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_1(cons_1(x, s)) | → | s | | cons_9(x, s) | → | garbage_collection_0 |
tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_1(cons_4(x, s)) | → | s | | cons_11(x, s) | → | garbage_collection_0 |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | tail_1(cons_7(x, s)) | → | s |
h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_6(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) | | tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_8(x, s) | → | garbage_collection_0 | | tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) |
tail_1(cons_9(x, s)) | → | s | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
*top*_0#(h_1(cons_4(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) |
Problem 14: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
*top*_0#(h_1(cons_8(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0#(h_1(cons_2(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0#(h_1(cons_10(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_2(0_0, h_1(s)))) | | *top*_0#(h_1(cons_1(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0#(h_1(cons_3(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0#(h_1(cons_6(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_8(1_0, h_1(s)))) |
*top*_0#(h_1(cons_1(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0#(h_1(cons_11(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_3(0_0, h_1(s)))) |
Rewrite Rules
M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) | | tail_1(cons_2(x, s)) | → | s |
tail_1(cons_3(x, s)) | → | s | | tail_1(cons_4(x, s)) | → | s |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) | | *top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) |
tail_1(cons_7(x, s)) | → | s | | tail_1(cons_8(x, s)) | → | s |
tail_1(cons_9(x, s)) | → | s | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
*top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_1(cons_1(x, s)) | → | s |
*top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) | | *top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_2(x, s) | → | garbage_collection_0 | | cons_3(x, s) | → | garbage_collection_0 |
cons_4(x, s) | → | garbage_collection_0 | | cons_5(x, s) | → | garbage_collection_0 |
cons_6(x, s) | → | garbage_collection_0 | | cons_7(x, s) | → | garbage_collection_0 |
cons_8(x, s) | → | garbage_collection_0 | | cons_9(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | cons_11(x, s) | → | garbage_collection_0 |
cons_1(x, s) | → | garbage_collection_0 |
Original Signature
Termination of terms over the following signature is verified: garbage_collection_0, cons_3, cons_2, cons_5, cons_4, h_0, cons_1, h_1, 0_0, cons_7, tail_1, cons_11, cons_6, cons_10, cons_9, cons_8, tail_0, 1_0, *top*_0, M_1
Strategy
Context-sensitive strategy:
μ(cons_3) = μ(garbage_collection_0) = μ(cons_2) = μ(cons_5) = μ(M_1#) = μ(cons_1#) = μ(cons_5#) = μ(cons_4) = μ(cons_3#) = μ(cons_1) = μ(h_1) = μ(cons_7#) = μ(cons_7) = μ(tail_1) = μ(cons_11) = μ(cons_6) = μ(cons_9#) = μ(cons_9) = μ(cons_10) = μ(cons_8) = μ(T) = μ(1_0) = μ(cons_2#) = μ(tail_1#) = μ(cons_11#) = μ(cons_4#) = μ(cons_6#) = μ(cons_8#) = μ(0_0) = μ(M_1) = μ(cons_10#) = ∅
μ(h_0) = μ(tail_0) = μ(*top*_0#) = μ(h_0#) = μ(*top*_0) = μ(tail_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 1
- *top*_0#(x): x
- 0_0: 0
- 1_0: 0
- M_1: 1
- cons_1(x,y): y
- cons_10(x,y): y
- cons_11(x,y): y + 2
- cons_2(x,y): y
- cons_3(x,y): y + 2
- cons_4(x,y): y + 3
- cons_5(x,y): y
- cons_6(x,y): y
- cons_7(x,y): y
- cons_8(x,y): y
- cons_9(x,y): y
- garbage_collection_0: 0
- h_0(x): x
- h_1(x): x
- tail_0(x): x
- tail_1(x): x
Standard Usable rules
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_2(x, s)) | → | s |
*top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_2(x, s) | → | garbage_collection_0 |
cons_3(x, s) | → | garbage_collection_0 | | *top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_1(cons_8(x, s)) | → | s |
cons_5(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_1(x, s) | → | garbage_collection_0 | | cons_4(x, s) | → | garbage_collection_0 |
h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_3(x, s)) | → | s |
*top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_7(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_1(cons_1(x, s)) | → | s | | cons_9(x, s) | → | garbage_collection_0 |
tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_1(cons_4(x, s)) | → | s | | cons_11(x, s) | → | garbage_collection_0 |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | tail_1(cons_7(x, s)) | → | s |
h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_6(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) | | tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_8(x, s) | → | garbage_collection_0 | | tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) |
tail_1(cons_9(x, s)) | → | s | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
*top*_0#(h_1(cons_3(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) |
Problem 15: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
*top*_0#(h_1(cons_8(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0#(h_1(cons_10(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0#(h_1(cons_2(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0#(h_1(cons_1(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0#(h_1(cons_6(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0#(h_1(cons_1(0_0, s))) | → | *top*_0#(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0#(h_1(cons_11(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_3(0_0, h_1(s)))) |
Rewrite Rules
M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) | | tail_1(cons_2(x, s)) | → | s |
tail_1(cons_3(x, s)) | → | s | | tail_1(cons_4(x, s)) | → | s |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) | | *top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) |
tail_1(cons_7(x, s)) | → | s | | tail_1(cons_8(x, s)) | → | s |
tail_1(cons_9(x, s)) | → | s | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
*top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_1(cons_1(x, s)) | → | s |
*top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) | | *top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_2(x, s) | → | garbage_collection_0 | | cons_3(x, s) | → | garbage_collection_0 |
cons_4(x, s) | → | garbage_collection_0 | | cons_5(x, s) | → | garbage_collection_0 |
cons_6(x, s) | → | garbage_collection_0 | | cons_7(x, s) | → | garbage_collection_0 |
cons_8(x, s) | → | garbage_collection_0 | | cons_9(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | cons_11(x, s) | → | garbage_collection_0 |
cons_1(x, s) | → | garbage_collection_0 |
Original Signature
Termination of terms over the following signature is verified: garbage_collection_0, cons_3, cons_2, cons_5, cons_4, h_0, cons_1, h_1, 0_0, cons_7, tail_1, cons_11, cons_6, cons_9, cons_10, tail_0, cons_8, 1_0, *top*_0, M_1
Strategy
Context-sensitive strategy:
μ(garbage_collection_0) = μ(cons_3) = μ(cons_2) = μ(M_1#) = μ(cons_5) = μ(cons_4) = μ(cons_5#) = μ(cons_1#) = μ(cons_3#) = μ(cons_1) = μ(h_1) = μ(cons_7#) = μ(cons_7) = μ(tail_1) = μ(cons_11) = μ(cons_6) = μ(cons_9#) = μ(cons_9) = μ(cons_10) = μ(cons_8) = μ(T) = μ(1_0) = μ(tail_1#) = μ(cons_2#) = μ(cons_11#) = μ(cons_4#) = μ(cons_6#) = μ(cons_8#) = μ(0_0) = μ(M_1) = μ(cons_10#) = ∅
μ(h_0) = μ(tail_0) = μ(*top*_0#) = μ(h_0#) = μ(*top*_0) = μ(tail_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 1
- *top*_0#(x): 2x
- 0_0: 0
- 1_0: 0
- M_1: 0
- cons_1(x,y): y
- cons_10(x,y): y
- cons_11(x,y): 2y + 3x + 1
- cons_2(x,y): y
- cons_3(x,y): 2y
- cons_4(x,y): y
- cons_5(x,y): y + 1
- cons_6(x,y): y
- cons_7(x,y): y
- cons_8(x,y): y
- cons_9(x,y): y
- garbage_collection_0: 0
- h_0(x): x
- h_1(x): x
- tail_0(x): 2x
- tail_1(x): x
Standard Usable rules
h_0(h_1(cons_3(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | *top*_0(h_1(cons_1(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
h_0(h_1(cons_1(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_2(x, s)) | → | s |
*top*_0(h_1(cons_1(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_2(x, s) | → | garbage_collection_0 |
cons_3(x, s) | → | garbage_collection_0 | | *top*_0(tail_1(cons_1(x, s))) | → | *top*_0(s) |
tail_0(h_1(cons_2(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | h_0(h_1(cons_10(1_0, s))) | → | h_1(cons_10(1_0, cons_2(0_0, h_1(s)))) |
*top*_0(h_1(cons_7(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | M_1 | → | h_1(cons_1(0_0, tail_0(M_1))) |
h_0(tail_1(cons_6(x, s))) | → | h_1(s) | | tail_1(cons_8(x, s)) | → | s |
cons_5(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_9(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
cons_1(x, s) | → | garbage_collection_0 | | cons_4(x, s) | → | garbage_collection_0 |
h_0(h_1(cons_9(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(h_1(cons_10(1_0, s))) | → | *top*_0(cons_10(1_0, cons_2(0_0, h_1(s)))) |
h_0(h_1(cons_5(0_0, s))) | → | h_1(cons_6(0_0, cons_7(1_0, h_1(s)))) | | tail_0(h_1(cons_1(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
*top*_0(h_1(cons_4(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_1(cons_3(x, s)) | → | s |
*top*_0(h_1(cons_8(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_6(0_0, s))) | → | h_1(cons_6(0_0, cons_8(1_0, h_1(s)))) |
tail_0(h_1(cons_6(0_0, s))) | → | tail_1(cons_6(0_0, cons_8(1_0, h_1(s)))) | | *top*_0(h_1(cons_3(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(h_1(cons_3(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) | | tail_0(h_1(cons_1(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_7(x, s) | → | garbage_collection_0 | | tail_0(h_1(cons_7(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
h_0(h_1(cons_1(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | *top*_0(tail_1(cons_10(x, s))) | → | *top*_0(s) |
h_0(tail_1(cons_10(x, s))) | → | h_1(s) | | h_0(tail_1(cons_1(x, s))) | → | h_0(s) |
tail_1(cons_1(x, s)) | → | s | | cons_9(x, s) | → | garbage_collection_0 |
tail_0(h_1(cons_10(1_0, s))) | → | tail_1(cons_10(1_0, cons_2(0_0, h_1(s)))) | | h_0(h_1(cons_4(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_1(cons_4(x, s)) | → | s | | cons_11(x, s) | → | garbage_collection_0 |
*top*_0(tail_1(cons_5(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_11(x, s))) | → | h_1(s) |
tail_0(tail_1(cons_6(x, s))) | → | tail_1(s) | | h_0(h_1(cons_11(1_0, s))) | → | h_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
*top*_0(h_1(cons_9(1_0, s))) | → | *top*_0(cons_10(1_0, cons_1(0_0, h_0(s)))) | | tail_0(h_1(cons_8(1_0, s))) | → | tail_1(cons_10(1_0, cons_1(0_0, h_0(s)))) |
tail_0(tail_1(cons_11(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_2(0_0, s))) | → | *top*_0(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_1(x, s))) | → | tail_1(s) | | tail_0(h_1(cons_4(0_0, s))) | → | tail_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
tail_0(tail_1(cons_10(x, s))) | → | tail_1(s) | | *top*_0(h_1(cons_6(0_0, s))) | → | *top*_0(cons_6(0_0, cons_8(1_0, h_1(s)))) |
*top*_0(tail_1(cons_11(x, s))) | → | *top*_0(s) | | h_0(tail_1(cons_5(x, s))) | → | h_1(s) |
*top*_0(h_1(cons_11(1_0, s))) | → | *top*_0(cons_10(1_0, cons_3(0_0, h_1(s)))) | | tail_1(cons_7(x, s)) | → | s |
h_0(h_1(cons_7(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | cons_6(x, s) | → | garbage_collection_0 |
cons_10(x, s) | → | garbage_collection_0 | | *top*_0(h_1(cons_5(0_0, s))) | → | *top*_0(cons_6(0_0, cons_7(1_0, h_1(s)))) |
*top*_0(tail_1(cons_6(x, s))) | → | *top*_0(s) | | tail_0(h_1(cons_11(1_0, s))) | → | tail_1(cons_10(1_0, cons_3(0_0, h_1(s)))) |
h_0(h_1(cons_8(1_0, s))) | → | h_1(cons_10(1_0, cons_1(0_0, h_0(s)))) | | h_0(h_1(cons_2(0_0, s))) | → | h_1(cons_6(0_0, cons_1(1_0, h_0(s)))) |
cons_8(x, s) | → | garbage_collection_0 | | tail_0(tail_1(cons_5(x, s))) | → | tail_1(s) |
tail_1(cons_9(x, s)) | → | s | | tail_0(h_1(cons_5(0_0, s))) | → | tail_1(cons_6(0_0, cons_7(1_0, h_1(s)))) |
h_0(tail_1(cons_1(x, s))) | → | h_1(s) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
*top*_0#(h_1(cons_11(1_0, s))) | → | *top*_0#(cons_10(1_0, cons_3(0_0, h_1(s)))) |