Termination proof

1: switching to dependency pairs

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 )
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 , 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 )
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 )

1.1: dependency graph processor

The dependency pairs are split into 3 component(s).

• The 1st component contains the pair(s)

  match_5#( a , l' , l_5 , Pair( l1 , l2 ) )	→	quick#( l1 )
  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_5#( a , l' , l_5 , Pair( l1 , l2 ) )	→	quick#( l2 )

  1.1.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [Nil]	=	0
  [quick# (x1) ]	=	2 x1
  [part (x1, x2) ]	=	x1
  [False]	=	0
  [match_2 (x1, ..., x5) ]	=	x1 + 1
  [match_4 (x1, x2) ]	=	x1
  [quick (x1) ]	=	x1
  [match_3 (x1, ..., x7) ]	=	x1 + x2 + 1
  [Cons (x1, x2) ]	=	x1 + 1
  [test (x1, x2) ]	=	0
  [append (x1, x2) ]	=	x1 + x2
  [match_5# (x1, ..., x4) ]	=	2 x1
  [match_1 (x1, x2, x3) ]	=	x1
  [True]	=	0
  [match_4# (x1, x2) ]	=	2 x1
  [match_0 (x1, x2, x3) ]	=	x1 + x2
  [Pair (x1, x2) ]	=	x1 + x2
  [match_5 (x1, ..., x4) ]	=	x1 + 1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  match_5#( a , l' , l_5 , Pair( l1 , l2 ) )	→	quick#( l1 )
  quick#( l_5 )	→	match_4#( l_5 , l_5 )
  match_5#( a , l' , l_5 , Pair( l1 , l2 ) )	→	quick#( l2 )

  1.1.1.1: dependency graph processor

  The dependency pairs are split into 0 component(s).

• The 2nd component contains the pair(s)

  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 )

  1.1.2: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [Nil]	=	0
  [False]	=	1
  [part (x1, x2) ]	=	x1 + 1
  [match_2 (x1, ..., x5) ]	=	x1 + 2
  [match_4 (x1, x2) ]	=	x1
  [quick (x1) ]	=	x1
  [match_3 (x1, ..., x7) ]	=	x1 + x2 + 2 x3 + 1
  [Cons (x1, x2) ]	=	x1 + 2
  [append# (x1, x2) ]	=	x1 + 3
  [test (x1, x2) ]	=	1
  [append (x1, x2) ]	=	x1 + x2
  [match_1 (x1, x2, x3) ]	=	x1 + 1
  [True]	=	1
  [match_0 (x1, x2, x3) ]	=	x1 + x2
  [match_0# (x1, x2, x3) ]	=	x1 + 2
  [Pair (x1, x2) ]	=	x1 + x2 + 1
  [match_5 (x1, ..., x4) ]	=	x1 + 1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.2.1: P is empty

  All dependency pairs have been removed.

• The 3rd component contains the pair(s)

  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 )

  1.1.3: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [Nil]	=	0
  [False]	=	1
  [part (x1, x2) ]	=	x1 + 1
  [part# (x1, x2) ]	=	x1 + 3
  [match_2 (x1, ..., x5) ]	=	x1 + 2
  [match_4 (x1, x2) ]	=	x1
  [match_1# (x1, x2, x3) ]	=	x1 + 2
  [quick (x1) ]	=	x1
  [match_3 (x1, ..., x7) ]	=	x1 + x2 + 2 x3 + 1
  [Cons (x1, x2) ]	=	x1 + 2
  [test (x1, x2) ]	=	1
  [append (x1, x2) ]	=	x1 + x2
  [match_1 (x1, x2, x3) ]	=	x1 + 1
  [True]	=	1
  [match_0 (x1, x2, x3) ]	=	x1 + x2
  [Pair (x1, x2) ]	=	x1 + x2 + 1
  [match_5 (x1, ..., x4) ]	=	x1 + 1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.3.1: P is empty

  All dependency pairs have been removed.