YES
The TRS could be proven terminating. The proof took 542 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (111ms).
| – Problem 2 was processed with processor SubtermCriterion (21ms).
| | – Problem 5 was processed with processor DependencyGraph (21ms).
| – Problem 3 was processed with processor PolynomialLinearRange4iUR (231ms).
| | – Problem 7 was processed with processor DependencyGraph (3ms).
| – Problem 4 was processed with processor SubtermCriterion (1ms).
| | – Problem 6 was processed with processor DependencyGraph (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| match_2#(x, l', a_4, l_3, Pair(l1, l2)) | → | test#(a_4, x) | | match_1#(a_4, l_3, Cons(x, l')) | → | part#(a_4, l') |
| match_5#(a, l', l_5, Pair(l1, l2)) | → | quick#(l2) | | match_4#(l_5, Cons(a, l')) | → | part#(a, l') |
| match_0#(l1_2, l2_1, Cons(x, l)) | → | append#(l, l2_1) | | quick#(l_5) | → | match_4#(l_5, l_5) |
| match_5#(a, l', l_5, Pair(l1, l2)) | → | append#(quick(l1), Cons(a, quick(l2))) | | match_1#(a_4, l_3, Cons(x, l')) | → | match_2#(x, l', a_4, l_3, part(a_4, l')) |
| match_4#(l_5, Cons(a, l')) | → | match_5#(a, l', l_5, part(a, l')) | | match_2#(x, l', a_4, l_3, Pair(l1, l2)) | → | match_3#(l1, l2, x, l', a_4, l_3, test(a_4, x)) |
| match_5#(a, l', l_5, Pair(l1, l2)) | → | quick#(l1) | | part#(a_4, l_3) | → | match_1#(a_4, l_3, l_3) |
| append#(l1_2, l2_1) | → | match_0#(l1_2, l2_1, l1_2) |
Rewrite Rules
| test(x_0, y) | → | True | | test(x_0, y) | → | False |
| append(l1_2, l2_1) | → | match_0(l1_2, l2_1, l1_2) | | match_0(l1_2, l2_1, Nil) | → | l2_1 |
| match_0(l1_2, l2_1, Cons(x, l)) | → | Cons(x, append(l, l2_1)) | | part(a_4, l_3) | → | match_1(a_4, l_3, l_3) |
| match_1(a_4, l_3, Nil) | → | Pair(Nil, Nil) | | match_1(a_4, l_3, Cons(x, l')) | → | match_2(x, l', a_4, l_3, part(a_4, l')) |
| match_2(x, l', a_4, l_3, Pair(l1, l2)) | → | match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)) | | match_3(l1, l2, x, l', a_4, l_3, False) | → | Pair(Cons(x, l1), l2) |
| match_3(l1, l2, x, l', a_4, l_3, True) | → | Pair(l1, Cons(x, l2)) | | quick(l_5) | → | match_4(l_5, l_5) |
| match_4(l_5, Nil) | → | Nil | | match_4(l_5, Cons(a, l')) | → | match_5(a, l', l_5, part(a, l')) |
| match_5(a, l', l_5, Pair(l1, l2)) | → | append(quick(l1), Cons(a, quick(l2))) |
Original Signature
Termination of terms over the following signature is verified: append, match_1, test, match_0, Cons, Pair, match_5, quick, match_4, match_3, match_2, False, True, part, Nil
Strategy
The following SCCs where found
| match_5#(a, l', l_5, Pair(l1, l2)) → quick#(l2) | match_4#(l_5, Cons(a, l')) → match_5#(a, l', l_5, part(a, l')) |
| quick#(l_5) → match_4#(l_5, l_5) | match_5#(a, l', l_5, Pair(l1, l2)) → quick#(l1) |
| match_1#(a_4, l_3, Cons(x, l')) → part#(a_4, l') | part#(a_4, l_3) → match_1#(a_4, l_3, l_3) |
| match_0#(l1_2, l2_1, Cons(x, l)) → append#(l, l2_1) | append#(l1_2, l2_1) → match_0#(l1_2, l2_1, l1_2) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| match_0#(l1_2, l2_1, Cons(x, l)) | → | append#(l, l2_1) | | append#(l1_2, l2_1) | → | match_0#(l1_2, l2_1, l1_2) |
Rewrite Rules
| test(x_0, y) | → | True | | test(x_0, y) | → | False |
| append(l1_2, l2_1) | → | match_0(l1_2, l2_1, l1_2) | | match_0(l1_2, l2_1, Nil) | → | l2_1 |
| match_0(l1_2, l2_1, Cons(x, l)) | → | Cons(x, append(l, l2_1)) | | part(a_4, l_3) | → | match_1(a_4, l_3, l_3) |
| match_1(a_4, l_3, Nil) | → | Pair(Nil, Nil) | | match_1(a_4, l_3, Cons(x, l')) | → | match_2(x, l', a_4, l_3, part(a_4, l')) |
| match_2(x, l', a_4, l_3, Pair(l1, l2)) | → | match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)) | | match_3(l1, l2, x, l', a_4, l_3, False) | → | Pair(Cons(x, l1), l2) |
| match_3(l1, l2, x, l', a_4, l_3, True) | → | Pair(l1, Cons(x, l2)) | | quick(l_5) | → | match_4(l_5, l_5) |
| match_4(l_5, Nil) | → | Nil | | match_4(l_5, Cons(a, l')) | → | match_5(a, l', l_5, part(a, l')) |
| match_5(a, l', l_5, Pair(l1, l2)) | → | append(quick(l1), Cons(a, quick(l2))) |
Original Signature
Termination of terms over the following signature is verified: append, match_1, test, match_0, Cons, Pair, match_5, quick, match_4, match_3, match_2, False, True, part, Nil
Strategy
Projection
The following projection was used:
- π (match_0#): 3
- π (append#): 1
Thus, the following dependency pairs are removed:
| match_0#(l1_2, l2_1, Cons(x, l)) | → | append#(l, l2_1) |
Problem 5: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| append#(l1_2, l2_1) | → | match_0#(l1_2, l2_1, l1_2) |
Rewrite Rules
| test(x_0, y) | → | True | | test(x_0, y) | → | False |
| append(l1_2, l2_1) | → | match_0(l1_2, l2_1, l1_2) | | match_0(l1_2, l2_1, Nil) | → | l2_1 |
| match_0(l1_2, l2_1, Cons(x, l)) | → | Cons(x, append(l, l2_1)) | | part(a_4, l_3) | → | match_1(a_4, l_3, l_3) |
| match_1(a_4, l_3, Nil) | → | Pair(Nil, Nil) | | match_1(a_4, l_3, Cons(x, l')) | → | match_2(x, l', a_4, l_3, part(a_4, l')) |
| match_2(x, l', a_4, l_3, Pair(l1, l2)) | → | match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)) | | match_3(l1, l2, x, l', a_4, l_3, False) | → | Pair(Cons(x, l1), l2) |
| match_3(l1, l2, x, l', a_4, l_3, True) | → | Pair(l1, Cons(x, l2)) | | quick(l_5) | → | match_4(l_5, l_5) |
| match_4(l_5, Nil) | → | Nil | | match_4(l_5, Cons(a, l')) | → | match_5(a, l', l_5, part(a, l')) |
| match_5(a, l', l_5, Pair(l1, l2)) | → | append(quick(l1), Cons(a, quick(l2))) |
Original Signature
Termination of terms over the following signature is verified: append, match_1, test, match_0, Cons, Pair, match_5, quick, match_4, match_3, match_2, False, True, part, Nil
Strategy
There are no SCCs!
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| match_5#(a, l', l_5, Pair(l1, l2)) | → | quick#(l2) | | match_4#(l_5, Cons(a, l')) | → | match_5#(a, l', l_5, part(a, l')) |
| quick#(l_5) | → | match_4#(l_5, l_5) | | match_5#(a, l', l_5, Pair(l1, l2)) | → | quick#(l1) |
Rewrite Rules
| test(x_0, y) | → | True | | test(x_0, y) | → | False |
| append(l1_2, l2_1) | → | match_0(l1_2, l2_1, l1_2) | | match_0(l1_2, l2_1, Nil) | → | l2_1 |
| match_0(l1_2, l2_1, Cons(x, l)) | → | Cons(x, append(l, l2_1)) | | part(a_4, l_3) | → | match_1(a_4, l_3, l_3) |
| match_1(a_4, l_3, Nil) | → | Pair(Nil, Nil) | | match_1(a_4, l_3, Cons(x, l')) | → | match_2(x, l', a_4, l_3, part(a_4, l')) |
| match_2(x, l', a_4, l_3, Pair(l1, l2)) | → | match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)) | | match_3(l1, l2, x, l', a_4, l_3, False) | → | Pair(Cons(x, l1), l2) |
| match_3(l1, l2, x, l', a_4, l_3, True) | → | Pair(l1, Cons(x, l2)) | | quick(l_5) | → | match_4(l_5, l_5) |
| match_4(l_5, Nil) | → | Nil | | match_4(l_5, Cons(a, l')) | → | match_5(a, l', l_5, part(a, l')) |
| match_5(a, l', l_5, Pair(l1, l2)) | → | append(quick(l1), Cons(a, quick(l2))) |
Original Signature
Termination of terms over the following signature is verified: append, match_1, test, match_0, Cons, Pair, match_5, quick, match_4, match_3, match_2, False, True, part, Nil
Strategy
Polynomial Interpretation
- Cons(x,y): 3y + 1
- False: 0
- Nil: 0
- Pair(x,y): y + x
- True: 2
- append(x,y): 0
- match_0(x,y,z): 0
- match_1(x,y,z): 2z
- match_2(x1,x2,x3,x4,x5): 3x5 + 1
- match_3(x1,x2,x3,x4,x5,x6,x7): 3x2 + 3x1 + 1
- match_4(x,y): 0
- match_4#(x,y): 2y
- match_5(x1,x2,x3,x4): 0
- match_5#(x1,x2,x3,x4): 2x4
- part(x,y): 2y
- quick(x): 0
- quick#(x): 2x
- test(x,y): 3y + x
Improved Usable rules
| part(a_4, l_3) | → | match_1(a_4, l_3, l_3) | | match_1(a_4, l_3, Cons(x, l')) | → | match_2(x, l', a_4, l_3, part(a_4, l')) |
| match_2(x, l', a_4, l_3, Pair(l1, l2)) | → | match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)) | | match_3(l1, l2, x, l', a_4, l_3, True) | → | Pair(l1, Cons(x, l2)) |
| match_1(a_4, l_3, Nil) | → | Pair(Nil, Nil) | | match_3(l1, l2, x, l', a_4, l_3, False) | → | Pair(Cons(x, l1), l2) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| match_4#(l_5, Cons(a, l')) | → | match_5#(a, l', l_5, part(a, l')) |
Problem 7: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| match_5#(a, l', l_5, Pair(l1, l2)) | → | quick#(l2) | | match_5#(a, l', l_5, Pair(l1, l2)) | → | quick#(l1) |
| quick#(l_5) | → | match_4#(l_5, l_5) |
Rewrite Rules
| test(x_0, y) | → | True | | test(x_0, y) | → | False |
| append(l1_2, l2_1) | → | match_0(l1_2, l2_1, l1_2) | | match_0(l1_2, l2_1, Nil) | → | l2_1 |
| match_0(l1_2, l2_1, Cons(x, l)) | → | Cons(x, append(l, l2_1)) | | part(a_4, l_3) | → | match_1(a_4, l_3, l_3) |
| match_1(a_4, l_3, Nil) | → | Pair(Nil, Nil) | | match_1(a_4, l_3, Cons(x, l')) | → | match_2(x, l', a_4, l_3, part(a_4, l')) |
| match_2(x, l', a_4, l_3, Pair(l1, l2)) | → | match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)) | | match_3(l1, l2, x, l', a_4, l_3, False) | → | Pair(Cons(x, l1), l2) |
| match_3(l1, l2, x, l', a_4, l_3, True) | → | Pair(l1, Cons(x, l2)) | | quick(l_5) | → | match_4(l_5, l_5) |
| match_4(l_5, Nil) | → | Nil | | match_4(l_5, Cons(a, l')) | → | match_5(a, l', l_5, part(a, l')) |
| match_5(a, l', l_5, Pair(l1, l2)) | → | append(quick(l1), Cons(a, quick(l2))) |
Original Signature
Termination of terms over the following signature is verified: append, match_1, test, match_0, Cons, Pair, match_5, quick, match_4, match_3, match_2, False, True, part, Nil
Strategy
There are no SCCs!
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| match_1#(a_4, l_3, Cons(x, l')) | → | part#(a_4, l') | | part#(a_4, l_3) | → | match_1#(a_4, l_3, l_3) |
Rewrite Rules
| test(x_0, y) | → | True | | test(x_0, y) | → | False |
| append(l1_2, l2_1) | → | match_0(l1_2, l2_1, l1_2) | | match_0(l1_2, l2_1, Nil) | → | l2_1 |
| match_0(l1_2, l2_1, Cons(x, l)) | → | Cons(x, append(l, l2_1)) | | part(a_4, l_3) | → | match_1(a_4, l_3, l_3) |
| match_1(a_4, l_3, Nil) | → | Pair(Nil, Nil) | | match_1(a_4, l_3, Cons(x, l')) | → | match_2(x, l', a_4, l_3, part(a_4, l')) |
| match_2(x, l', a_4, l_3, Pair(l1, l2)) | → | match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)) | | match_3(l1, l2, x, l', a_4, l_3, False) | → | Pair(Cons(x, l1), l2) |
| match_3(l1, l2, x, l', a_4, l_3, True) | → | Pair(l1, Cons(x, l2)) | | quick(l_5) | → | match_4(l_5, l_5) |
| match_4(l_5, Nil) | → | Nil | | match_4(l_5, Cons(a, l')) | → | match_5(a, l', l_5, part(a, l')) |
| match_5(a, l', l_5, Pair(l1, l2)) | → | append(quick(l1), Cons(a, quick(l2))) |
Original Signature
Termination of terms over the following signature is verified: append, match_1, test, match_0, Cons, Pair, match_5, quick, match_4, match_3, match_2, False, True, part, Nil
Strategy
Projection
The following projection was used:
- π (match_1#): 3
- π (part#): 2
Thus, the following dependency pairs are removed:
| match_1#(a_4, l_3, Cons(x, l')) | → | part#(a_4, l') |
Problem 6: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| part#(a_4, l_3) | → | match_1#(a_4, l_3, l_3) |
Rewrite Rules
| test(x_0, y) | → | True | | test(x_0, y) | → | False |
| append(l1_2, l2_1) | → | match_0(l1_2, l2_1, l1_2) | | match_0(l1_2, l2_1, Nil) | → | l2_1 |
| match_0(l1_2, l2_1, Cons(x, l)) | → | Cons(x, append(l, l2_1)) | | part(a_4, l_3) | → | match_1(a_4, l_3, l_3) |
| match_1(a_4, l_3, Nil) | → | Pair(Nil, Nil) | | match_1(a_4, l_3, Cons(x, l')) | → | match_2(x, l', a_4, l_3, part(a_4, l')) |
| match_2(x, l', a_4, l_3, Pair(l1, l2)) | → | match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)) | | match_3(l1, l2, x, l', a_4, l_3, False) | → | Pair(Cons(x, l1), l2) |
| match_3(l1, l2, x, l', a_4, l_3, True) | → | Pair(l1, Cons(x, l2)) | | quick(l_5) | → | match_4(l_5, l_5) |
| match_4(l_5, Nil) | → | Nil | | match_4(l_5, Cons(a, l')) | → | match_5(a, l', l_5, part(a, l')) |
| match_5(a, l', l_5, Pair(l1, l2)) | → | append(quick(l1), Cons(a, quick(l2))) |
Original Signature
Termination of terms over the following signature is verified: append, match_1, test, match_0, Cons, Pair, match_5, quick, match_4, match_3, match_2, False, True, part, Nil
Strategy
There are no SCCs!