Consider the TRS R consisting of the rewrite rules

1: test(x_0,y) -> True
2: test(x_0,y) -> False
3: append(l1_2,l2_1) -> match_0(l1_2,l2_1,l1_2)
4: match_0(l1_2,l2_1,Nil) -> l2_1
5: match_0(l1_2,l2_1,Cons(x,l)) -> Cons(x,append(l,l2_1))
6: part(a_4,l_3) -> match_1(a_4,l_3,l_3)
7: match_1(a_4,l_3,Nil) -> Pair(Nil,Nil)
8: match_1(a_4,l_3,Cons(x,l')) -> match_2(x,l',a_4,l_3,part(a_4,l'))
9: 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))
10: match_3(l1,l2,x,l',a_4,l_3,False) -> Pair(Cons(x,l1),l2)
11: match_3(l1,l2,x,l',a_4,l_3,True) -> Pair(l1,Cons(x,l2))
12: quick(l_5) -> match_4(l_5,l_5)
13: match_4(l_5,Nil) -> Nil
14: match_4(l_5,Cons(a,l')) -> match_5(a,l',l_5,part(a,l'))
15: match_5(a,l',l_5,Pair(l1,l2)) -> append(quick(l1),Cons(a,quick(l2)))

There are 13 dependency pairs:

16: APPEND(l1_2,l2_1) -> MATCH_0(l1_2,l2_1,l1_2)
17: MATCH_0(l1_2,l2_1,Cons(x,l)) -> APPEND(l,l2_1)
18: PART(a_4,l_3) -> MATCH_1(a_4,l_3,l_3)
19: MATCH_1(a_4,l_3,Cons(x,l')) -> MATCH_2(x,l',a_4,l_3,part(a_4,l'))
20: MATCH_1(a_4,l_3,Cons(x,l')) -> PART(a_4,l')
21: 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))
22: MATCH_2(x,l',a_4,l_3,Pair(l1,l2)) -> TEST(a_4,x)
23: QUICK(l_5) -> MATCH_4(l_5,l_5)
24: MATCH_4(l_5,Cons(a,l')) -> MATCH_5(a,l',l_5,part(a,l'))
25: MATCH_4(l_5,Cons(a,l')) -> PART(a,l')
26: MATCH_5(a,l',l_5,Pair(l1,l2)) -> APPEND(quick(l1),Cons(a,quick(l2)))
27: MATCH_5(a,l',l_5,Pair(l1,l2)) -> QUICK(l1)
28: MATCH_5(a,l',l_5,Pair(l1,l2)) -> QUICK(l2)

The approximated dependency graph contains 3 SCCs:
{16,17},
{18,20}
and {23,24,27,28}.

- Consider the SCC {16,17}.
There are no usable rules.
By taking the polynomial interpretation
[Cons](x,y) = [APPEND](x,y) = x + y + 1
and [MATCH_0](x,y,z) = y + z + 1,
rule 16
is weakly decreasing and
rule 17
is strictly decreasing.

- Consider the SCC {18,20}.
There are no usable rules.
By taking the polynomial interpretation
[Cons](x,y) = [PART](x,y) = x + y + 1
and [MATCH_1](x,y,z) = x + z + 1,
rule 18
is weakly decreasing and
rule 20
is strictly decreasing.

- Consider the SCC {23,24,27,28}.
The usable rules are {1,2,6-11}.
By taking the polynomial interpretation
[Nil] = 0,
[False] = [True] = [test](x,y) = 1,
[MATCH_5](x,y,z,w) = w + 1,
[QUICK](x) = x + 1,
[match_2](x,y,z,w,v) = x + v + 1,
[Cons](x,y) = [Pair](x,y) = [part](x,y) = x + y + 1,
[match_3](x,y,z,w,v,u,t) = x + y + z + t + 1,
[match_1](x,y,z) = x + z + 1
and [MATCH_4](x,y) = y + 1,
the rules in {1,2,6-11,23,24}
are weakly decreasing and
the rules in {27,28}
are strictly decreasing.

Hence the TRS is terminating.