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)Truetest(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)Nilmatch_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)Truetest(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)Nilmatch_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:

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)Truetest(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)Nilmatch_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)Truetest(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)Nilmatch_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

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)Truetest(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)Nilmatch_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)Truetest(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)Nilmatch_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:

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)Truetest(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)Nilmatch_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!