Term Rewriting System R:

   [x_0, y, l1_2, l2_1, x, l, a_4, l_3, l', l1, l2, l_5, a]
   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)))

Termination of R to be shown.


R contains the following Dependency Pairs: 


   MATCH_0(l1_2, l2_1, Cons(x, l)) -> APPEND(l, l2_1)
   MATCH_1(a_4, l_3, Cons(x, l')) -> MATCH_2(x, l', a_4, l_3, part(a_4, l'))
   MATCH_1(a_4, l_3, Cons(x, l')) -> 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_2(x, l', a_4, l_3, Pair(l1, l2)) -> TEST(a_4, x)
   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)
   QUICK(l_5) -> MATCH_4(l_5, l_5)
   MATCH_4(l_5, Cons(a, l')) -> MATCH_5(a, l', l_5, part(a, l'))
   MATCH_4(l_5, Cons(a, l')) -> PART(a, l')
   MATCH_5(a, l', l_5, Pair(l1, l2)) -> APPEND(quick(l1), Cons(a, quick(l2)))
   MATCH_5(a, l', l_5, Pair(l1, l2)) -> QUICK(l1)
   MATCH_5(a, l', l_5, Pair(l1, l2)) -> QUICK(l2)

Furthermore, R contains three SCCs.


SCC1:

APPEND(l1_2, l2_1) -> MATCH_0(l1_2, l2_1, l1_2)
MATCH_0(l1_2, l2_1, Cons(x, l)) -> APPEND(l, l2_1)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

No rules need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
POL(MATCH_0(x_1, x_2, x_3)) = x_3
POL(Cons(x_1, x_2)) = 1 + x_1 + x_2
POL(APPEND(x_1, x_2)) = 1 + x_1

 resulting in no subcycles.


SCC2:

PART(a_4, l_3) -> MATCH_1(a_4, l_3, l_3)
MATCH_1(a_4, l_3, Cons(x, l')) -> PART(a_4, l')

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

No rules need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
POL(Cons(x_1, x_2)) = 1 + x_1 + x_2
POL(PART(x_1, x_2)) = 1 + x_2
POL(MATCH_1(x_1, x_2, x_3)) = x_3

 resulting in no subcycles.


SCC3:

MATCH_5(a, l', l_5, Pair(l1, l2)) -> QUICK(l2)
MATCH_5(a, l', l_5, Pair(l1, l2)) -> QUICK(l1)
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)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   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_1(a_4, l_3, Nil) -> Pair(Nil, Nil)
   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_3(l1, l2, x, l', a_4, l_3, False) -> Pair(Cons(x, l1), l2)


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(match_3(x_1, x_2, x_3, x_4, x_5, x_6, x_7)) = 1 + x_1 + x_2
POL(MATCH_4(x_1, x_2)) = x_2
POL(False) = 0
POL(match_2(x_1, x_2, x_3, x_4, x_5)) = 1 + x_5
POL(Pair(x_1, x_2)) = x_1 + x_2
POL(Cons(x_1, x_2)) = 1 + x_2
POL(MATCH_5(x_1, x_2, x_3, x_4)) = 1 + x_4
POL(test(x_1, x_2)) = 0
POL(match_1(x_1, x_2, x_3)) = x_3
POL(Nil) = 0
POL(QUICK(x_1)) = x_1
POL(part(x_1, x_2)) = x_2
POL(True) = 0

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 1.118 seconds.