YES
(VAR x_0 y l1_2 l2_1 x l a_4 l_3 l' l1 l2 l_5 a)
(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)))
)

Proving termination of rewriting for quick:

-> Dependency pairs:
nF_append(l1_2,l2_1) -> nF_match_0(l1_2,l2_1,l1_2)
nF_match_0(l1_2,l2_1,Cons(x,l)) -> nF_append(l,l2_1)
nF_part(a_4,l_3) -> nF_match_1(a_4,l_3,l_3)
nF_match_1(a_4,l_3,Cons(x,l')) -> nF_match_2(x,l',a_4,l_3,part(a_4,l'))
nF_match_1(a_4,l_3,Cons(x,l')) -> nF_part(a_4,l')
nF_match_2(x,l',a_4,l_3,Pair(l1,l2)) -> nF_match_3(l1,l2,x,l',a_4,l_3,test(a_4,x))
nF_match_2(x,l',a_4,l_3,Pair(l1,l2)) -> nF_test(a_4,x)
nF_quick(l_5) -> nF_match_4(l_5,l_5)
nF_match_4(l_5,Cons(a,l')) -> nF_match_5(a,l',l_5,part(a,l'))
nF_match_4(l_5,Cons(a,l')) -> nF_part(a,l')
nF_match_5(a,l',l_5,Pair(l1,l2)) -> nF_append(quick(l1),Cons(a,quick(l2)))
nF_match_5(a,l',l_5,Pair(l1,l2)) -> nF_quick(l1)
nF_match_5(a,l',l_5,Pair(l1,l2)) -> nF_quick(l2)

-> Proof of termination for quick_1_1:
-> -> Dependency pairs in cycle:
nF_quick(l_5) -> nF_match_4(l_5,l_5)
nF_match_5(a,l',l_5,Pair(l1,l2)) -> nF_quick(l2)
nF_match_4(l_5,Cons(a,l')) -> nF_match_5(a,l',l_5,part(a,l'))
nF_match_5(a,l',l_5,Pair(l1,l2)) -> nF_quick(l1)

UsableRules:
test(x_0,y) -> True
test(x_0,y) -> False
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))

Polynomial Interpretation:

[test](X1,X2) = 0
[True] = 0
[False] = 0
[append](X1,X2) = 0
[match_0](X1,X2,X3) = 0
[Nil] = 0
[Cons](X1,X2) = X2 + 1
[part](X1,X2) = X2
[match_1](X1,X2,X3) = X3
[Pair](X1,X2) = X1 + X2
[match_2](X1,X2,X3,X4,X5) = X5 + 1
[match_3](X1,X2,X3,X4,X5,X6,X7) = X1 + X2 + 1
[quick](X) = 0
[match_4](X1,X2) = 0
[match_5](X1,X2,X3,X4) = 0
[nF_quick](X) = X
[nF_match_5](X1,X2,X3,X4) = X4 + 1
[nF_match_4](X1,X2) = X2

TIME: 7.0201e-2

-> -> Dependency pairs in cycle:
nF_quick(l_5) -> nF_match_4(l_5,l_5)
nF_match_5(a,l',l_5,Pair(l1,l2)) -> nF_quick(l2)
nF_match_4(l_5,Cons(a,l')) -> nF_match_5(a,l',l_5,part(a,l'))

UsableRules:
test(x_0,y) -> True
test(x_0,y) -> False
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))

Polynomial Interpretation:

[test](X1,X2) = 0
[True] = 0
[False] = 0
[append](X1,X2) = 0
[match_0](X1,X2,X3) = 0
[Nil] = 0
[Cons](X1,X2) = X2 + 1
[part](X1,X2) = X2
[match_1](X1,X2,X3) = X3
[Pair](X1,X2) = X1 + X2
[match_2](X1,X2,X3,X4,X5) = X5 + 1
[match_3](X1,X2,X3,X4,X5,X6,X7) = X1 + X2 + 1
[quick](X) = 0
[match_4](X1,X2) = 0
[match_5](X1,X2,X3,X4) = 0
[nF_quick](X) = X
[nF_match_5](X1,X2,X3,X4) = X4
[nF_match_4](X1,X2) = X2

TIME: 5.9693e-2


-> Proof of termination for quick_1_2:
-> -> Dependency pairs in cycle:
nF_part(a_4,l_3) -> nF_match_1(a_4,l_3,l_3)
nF_match_1(a_4,l_3,Cons(x,l')) -> nF_part(a_4,l')

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for quick_1_3:
-> -> Dependency pairs in cycle:
nF_append(l1_2,l2_1) -> nF_match_0(l1_2,l2_1,l1_2)
nF_match_0(l1_2,l2_1,Cons(x,l)) -> nF_append(l,l2_1)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.