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_1h_1(cons_1(0_0, tail_0(M_1)))tail_1(cons_2(x, s))s
tail_1(cons_3(x, s))stail_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))stail_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_0cons_3(x, s)garbage_collection_0
cons_4(x, s)garbage_collection_0cons_5(x, s)garbage_collection_0
cons_6(x, s)garbage_collection_0cons_7(x, s)garbage_collection_0
cons_8(x, s)garbage_collection_0cons_9(x, s)garbage_collection_0
cons_10(x, s)garbage_collection_0cons_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_1h_1(cons_1(0_0, tail_0(M_1)))tail_1(cons_2(x, s))s
tail_1(cons_3(x, s))stail_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))stail_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_0cons_3(x, s)garbage_collection_0
cons_4(x, s)garbage_collection_0cons_5(x, s)garbage_collection_0
cons_6(x, s)garbage_collection_0cons_7(x, s)garbage_collection_0
cons_8(x, s)garbage_collection_0cons_9(x, s)garbage_collection_0
cons_10(x, s)garbage_collection_0cons_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_1h_1(cons_1(0_0, tail_0(M_1)))tail_1(cons_2(x, s))s
tail_1(cons_3(x, s))stail_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))stail_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_0cons_3(x, s)garbage_collection_0
cons_4(x, s)garbage_collection_0cons_5(x, s)garbage_collection_0
cons_6(x, s)garbage_collection_0cons_7(x, s)garbage_collection_0
cons_8(x, s)garbage_collection_0cons_9(x, s)garbage_collection_0
cons_10(x, s)garbage_collection_0cons_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_1h_1(cons_1(0_0, tail_0(M_1)))tail_1(cons_2(x, s))s
tail_1(cons_3(x, s))stail_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))stail_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_0cons_3(x, s)garbage_collection_0
cons_4(x, s)garbage_collection_0cons_5(x, s)garbage_collection_0
cons_6(x, s)garbage_collection_0cons_7(x, s)garbage_collection_0
cons_8(x, s)garbage_collection_0cons_9(x, s)garbage_collection_0
cons_10(x, s)garbage_collection_0cons_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

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_1h_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_0tail_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_0cons_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_0tail_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))scons_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))scons_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_0tail_0(tail_1(cons_5(x, s)))tail_1(s)
tail_1(cons_9(x, s))stail_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_1h_1(cons_1(0_0, tail_0(M_1)))tail_1(cons_2(x, s))s
tail_1(cons_3(x, s))stail_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))stail_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_0cons_3(x, s)garbage_collection_0
cons_4(x, s)garbage_collection_0cons_5(x, s)garbage_collection_0
cons_6(x, s)garbage_collection_0cons_7(x, s)garbage_collection_0
cons_8(x, s)garbage_collection_0cons_9(x, s)garbage_collection_0
cons_10(x, s)garbage_collection_0cons_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

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_1h_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_0tail_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_0cons_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_0tail_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))scons_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))scons_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_0tail_0(tail_1(cons_5(x, s)))tail_1(s)
tail_1(cons_9(x, s))stail_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_1h_1(cons_1(0_0, tail_0(M_1)))tail_1(cons_2(x, s))s
tail_1(cons_3(x, s))stail_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))stail_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_0cons_3(x, s)garbage_collection_0
cons_4(x, s)garbage_collection_0cons_5(x, s)garbage_collection_0
cons_6(x, s)garbage_collection_0cons_7(x, s)garbage_collection_0
cons_8(x, s)garbage_collection_0cons_9(x, s)garbage_collection_0
cons_10(x, s)garbage_collection_0cons_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

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_1h_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_0tail_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_0cons_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_0tail_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))scons_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))scons_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_0tail_0(tail_1(cons_5(x, s)))tail_1(s)
tail_1(cons_9(x, s))stail_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_1h_1(cons_1(0_0, tail_0(M_1)))tail_1(cons_2(x, s))s
tail_1(cons_3(x, s))stail_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))stail_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_0cons_3(x, s)garbage_collection_0
cons_4(x, s)garbage_collection_0cons_5(x, s)garbage_collection_0
cons_6(x, s)garbage_collection_0cons_7(x, s)garbage_collection_0
cons_8(x, s)garbage_collection_0cons_9(x, s)garbage_collection_0
cons_10(x, s)garbage_collection_0cons_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_1h_1(cons_1(0_0, tail_0(M_1)))tail_1(cons_2(x, s))s
tail_1(cons_3(x, s))stail_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))stail_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_0cons_3(x, s)garbage_collection_0
cons_4(x, s)garbage_collection_0cons_5(x, s)garbage_collection_0
cons_6(x, s)garbage_collection_0cons_7(x, s)garbage_collection_0
cons_8(x, s)garbage_collection_0cons_9(x, s)garbage_collection_0
cons_10(x, s)garbage_collection_0cons_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

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_1h_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_0tail_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_0cons_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_0tail_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))scons_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))scons_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_0tail_0(tail_1(cons_5(x, s)))tail_1(s)
tail_1(cons_9(x, s))stail_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_1h_1(cons_1(0_0, tail_0(M_1)))tail_1(cons_2(x, s))s
tail_1(cons_3(x, s))stail_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))stail_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_0cons_3(x, s)garbage_collection_0
cons_4(x, s)garbage_collection_0cons_5(x, s)garbage_collection_0
cons_6(x, s)garbage_collection_0cons_7(x, s)garbage_collection_0
cons_8(x, s)garbage_collection_0cons_9(x, s)garbage_collection_0
cons_10(x, s)garbage_collection_0cons_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

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_1h_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_0tail_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_0cons_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_0tail_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))scons_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))scons_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_0tail_0(tail_1(cons_5(x, s)))tail_1(s)
tail_1(cons_9(x, s))stail_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_1h_1(cons_1(0_0, tail_0(M_1)))tail_1(cons_2(x, s))s
tail_1(cons_3(x, s))stail_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))stail_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_0cons_3(x, s)garbage_collection_0
cons_4(x, s)garbage_collection_0cons_5(x, s)garbage_collection_0
cons_6(x, s)garbage_collection_0cons_7(x, s)garbage_collection_0
cons_8(x, s)garbage_collection_0cons_9(x, s)garbage_collection_0
cons_10(x, s)garbage_collection_0cons_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

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_1h_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_0tail_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_0cons_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_0tail_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))scons_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))scons_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_0tail_0(tail_1(cons_5(x, s)))tail_1(s)
tail_1(cons_9(x, s))stail_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_1h_1(cons_1(0_0, tail_0(M_1)))tail_1(cons_2(x, s))s
tail_1(cons_3(x, s))stail_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))stail_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_0cons_3(x, s)garbage_collection_0
cons_4(x, s)garbage_collection_0cons_5(x, s)garbage_collection_0
cons_6(x, s)garbage_collection_0cons_7(x, s)garbage_collection_0
cons_8(x, s)garbage_collection_0cons_9(x, s)garbage_collection_0
cons_10(x, s)garbage_collection_0cons_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

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_1h_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_0tail_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_0cons_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_0tail_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))scons_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))scons_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_0tail_0(tail_1(cons_5(x, s)))tail_1(s)
tail_1(cons_9(x, s))stail_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_1h_1(cons_1(0_0, tail_0(M_1)))tail_1(cons_2(x, s))s
tail_1(cons_3(x, s))stail_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))stail_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_0cons_3(x, s)garbage_collection_0
cons_4(x, s)garbage_collection_0cons_5(x, s)garbage_collection_0
cons_6(x, s)garbage_collection_0cons_7(x, s)garbage_collection_0
cons_8(x, s)garbage_collection_0cons_9(x, s)garbage_collection_0
cons_10(x, s)garbage_collection_0cons_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

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_1h_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_0tail_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_0cons_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_0tail_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))scons_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))scons_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_0tail_0(tail_1(cons_5(x, s)))tail_1(s)
tail_1(cons_9(x, s))stail_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_1h_1(cons_1(0_0, tail_0(M_1)))tail_1(cons_2(x, s))s
tail_1(cons_3(x, s))stail_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))stail_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_0cons_3(x, s)garbage_collection_0
cons_4(x, s)garbage_collection_0cons_5(x, s)garbage_collection_0
cons_6(x, s)garbage_collection_0cons_7(x, s)garbage_collection_0
cons_8(x, s)garbage_collection_0cons_9(x, s)garbage_collection_0
cons_10(x, s)garbage_collection_0cons_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

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_1h_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_0tail_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_0cons_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_0tail_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))scons_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))scons_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_0tail_0(tail_1(cons_5(x, s)))tail_1(s)
tail_1(cons_9(x, s))stail_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_1h_1(cons_1(0_0, tail_0(M_1)))tail_1(cons_2(x, s))s
tail_1(cons_3(x, s))stail_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))stail_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_0cons_3(x, s)garbage_collection_0
cons_4(x, s)garbage_collection_0cons_5(x, s)garbage_collection_0
cons_6(x, s)garbage_collection_0cons_7(x, s)garbage_collection_0
cons_8(x, s)garbage_collection_0cons_9(x, s)garbage_collection_0
cons_10(x, s)garbage_collection_0cons_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

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_1h_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_0tail_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_0cons_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_0tail_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))scons_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))scons_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_0tail_0(tail_1(cons_5(x, s)))tail_1(s)
tail_1(cons_9(x, s))stail_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_1h_1(cons_1(0_0, tail_0(M_1)))tail_1(cons_2(x, s))s
tail_1(cons_3(x, s))stail_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))stail_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_0cons_3(x, s)garbage_collection_0
cons_4(x, s)garbage_collection_0cons_5(x, s)garbage_collection_0
cons_6(x, s)garbage_collection_0cons_7(x, s)garbage_collection_0
cons_8(x, s)garbage_collection_0cons_9(x, s)garbage_collection_0
cons_10(x, s)garbage_collection_0cons_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

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_1h_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_0tail_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_0cons_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_0tail_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))scons_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))scons_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_0tail_0(tail_1(cons_5(x, s)))tail_1(s)
tail_1(cons_9(x, s))stail_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_1h_1(cons_1(0_0, tail_0(M_1)))tail_1(cons_2(x, s))s
tail_1(cons_3(x, s))stail_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))stail_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_0cons_3(x, s)garbage_collection_0
cons_4(x, s)garbage_collection_0cons_5(x, s)garbage_collection_0
cons_6(x, s)garbage_collection_0cons_7(x, s)garbage_collection_0
cons_8(x, s)garbage_collection_0cons_9(x, s)garbage_collection_0
cons_10(x, s)garbage_collection_0cons_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

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_1h_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_0tail_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_0cons_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_0tail_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))scons_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))scons_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_0tail_0(tail_1(cons_5(x, s)))tail_1(s)
tail_1(cons_9(x, s))stail_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))))