Termination proof

1: switching to dependency pairs

active#( __( __( X , Y ) , Z ) )	→	__#( X , __( Y , Z ) )
active#( __( __( X , Y ) , Z ) )	→	__#( Y , Z )
active#( U21( tt , V2 ) )	→	U22#( isList( V2 ) )
active#( U21( tt , V2 ) )	→	isList#( V2 )
active#( U41( tt , V2 ) )	→	U42#( isNeList( V2 ) )
active#( U41( tt , V2 ) )	→	isNeList#( V2 )
active#( U51( tt , V2 ) )	→	U52#( isList( V2 ) )
active#( U51( tt , V2 ) )	→	isList#( V2 )
active#( U71( tt , P ) )	→	U72#( isPal( P ) )
active#( U71( tt , P ) )	→	isPal#( P )
active#( isList( V ) )	→	U11#( isNeList( V ) )
active#( isList( V ) )	→	isNeList#( V )
active#( isList( __( V1 , V2 ) ) )	→	U21#( isList( V1 ) , V2 )
active#( isList( __( V1 , V2 ) ) )	→	isList#( V1 )
active#( isNeList( V ) )	→	U31#( isQid( V ) )
active#( isNeList( V ) )	→	isQid#( V )
active#( isNeList( __( V1 , V2 ) ) )	→	U41#( isList( V1 ) , V2 )
active#( isNeList( __( V1 , V2 ) ) )	→	isList#( V1 )
active#( isNeList( __( V1 , V2 ) ) )	→	U51#( isNeList( V1 ) , V2 )
active#( isNeList( __( V1 , V2 ) ) )	→	isNeList#( V1 )
active#( isNePal( V ) )	→	U61#( isQid( V ) )
active#( isNePal( V ) )	→	isQid#( V )
active#( isNePal( __( I , __( P , I ) ) ) )	→	U71#( isQid( I ) , P )
active#( isNePal( __( I , __( P , I ) ) ) )	→	isQid#( I )
active#( isPal( V ) )	→	U81#( isNePal( V ) )
active#( isPal( V ) )	→	isNePal#( V )
active#( __( X1 , X2 ) )	→	__#( active( X1 ) , X2 )
active#( __( X1 , X2 ) )	→	active#( X1 )
active#( __( X1 , X2 ) )	→	__#( X1 , active( X2 ) )
active#( __( X1 , X2 ) )	→	active#( X2 )
active#( U11( X ) )	→	U11#( active( X ) )
active#( U11( X ) )	→	active#( X )
active#( U21( X1 , X2 ) )	→	U21#( active( X1 ) , X2 )
active#( U21( X1 , X2 ) )	→	active#( X1 )
active#( U22( X ) )	→	U22#( active( X ) )
active#( U22( X ) )	→	active#( X )
active#( U31( X ) )	→	U31#( active( X ) )
active#( U31( X ) )	→	active#( X )
active#( U41( X1 , X2 ) )	→	U41#( active( X1 ) , X2 )
active#( U41( X1 , X2 ) )	→	active#( X1 )
active#( U42( X ) )	→	U42#( active( X ) )
active#( U42( X ) )	→	active#( X )
active#( U51( X1 , X2 ) )	→	U51#( active( X1 ) , X2 )
active#( U51( X1 , X2 ) )	→	active#( X1 )
active#( U52( X ) )	→	U52#( active( X ) )
active#( U52( X ) )	→	active#( X )
active#( U61( X ) )	→	U61#( active( X ) )
active#( U61( X ) )	→	active#( X )
active#( U71( X1 , X2 ) )	→	U71#( active( X1 ) , X2 )
active#( U71( X1 , X2 ) )	→	active#( X1 )
active#( U72( X ) )	→	U72#( active( X ) )
active#( U72( X ) )	→	active#( X )
active#( U81( X ) )	→	U81#( active( X ) )
active#( U81( X ) )	→	active#( X )
__#( mark( X1 ) , X2 )	→	__#( X1 , X2 )
__#( X1 , mark( X2 ) )	→	__#( X1 , X2 )
U11#( mark( X ) )	→	U11#( X )
U21#( mark( X1 ) , X2 )	→	U21#( X1 , X2 )
U22#( mark( X ) )	→	U22#( X )
U31#( mark( X ) )	→	U31#( X )
U41#( mark( X1 ) , X2 )	→	U41#( X1 , X2 )
U42#( mark( X ) )	→	U42#( X )
U51#( mark( X1 ) , X2 )	→	U51#( X1 , X2 )
U52#( mark( X ) )	→	U52#( X )
U61#( mark( X ) )	→	U61#( X )
U71#( mark( X1 ) , X2 )	→	U71#( X1 , X2 )
U72#( mark( X ) )	→	U72#( X )
U81#( mark( X ) )	→	U81#( X )
proper#( __( X1 , X2 ) )	→	__#( proper( X1 ) , proper( X2 ) )
proper#( __( X1 , X2 ) )	→	proper#( X1 )
proper#( __( X1 , X2 ) )	→	proper#( X2 )
proper#( U11( X ) )	→	U11#( proper( X ) )
proper#( U11( X ) )	→	proper#( X )
proper#( U21( X1 , X2 ) )	→	U21#( proper( X1 ) , proper( X2 ) )
proper#( U21( X1 , X2 ) )	→	proper#( X1 )
proper#( U21( X1 , X2 ) )	→	proper#( X2 )
proper#( U22( X ) )	→	U22#( proper( X ) )
proper#( U22( X ) )	→	proper#( X )
proper#( isList( X ) )	→	isList#( proper( X ) )
proper#( isList( X ) )	→	proper#( X )
proper#( U31( X ) )	→	U31#( proper( X ) )
proper#( U31( X ) )	→	proper#( X )
proper#( U41( X1 , X2 ) )	→	U41#( proper( X1 ) , proper( X2 ) )
proper#( U41( X1 , X2 ) )	→	proper#( X1 )
proper#( U41( X1 , X2 ) )	→	proper#( X2 )
proper#( U42( X ) )	→	U42#( proper( X ) )
proper#( U42( X ) )	→	proper#( X )
proper#( isNeList( X ) )	→	isNeList#( proper( X ) )
proper#( isNeList( X ) )	→	proper#( X )
proper#( U51( X1 , X2 ) )	→	U51#( proper( X1 ) , proper( X2 ) )
proper#( U51( X1 , X2 ) )	→	proper#( X1 )
proper#( U51( X1 , X2 ) )	→	proper#( X2 )
proper#( U52( X ) )	→	U52#( proper( X ) )
proper#( U52( X ) )	→	proper#( X )
proper#( U61( X ) )	→	U61#( proper( X ) )
proper#( U61( X ) )	→	proper#( X )
proper#( U71( X1 , X2 ) )	→	U71#( proper( X1 ) , proper( X2 ) )
proper#( U71( X1 , X2 ) )	→	proper#( X1 )
proper#( U71( X1 , X2 ) )	→	proper#( X2 )
proper#( U72( X ) )	→	U72#( proper( X ) )
proper#( U72( X ) )	→	proper#( X )
proper#( isPal( X ) )	→	isPal#( proper( X ) )
proper#( isPal( X ) )	→	proper#( X )
proper#( U81( X ) )	→	U81#( proper( X ) )
proper#( U81( X ) )	→	proper#( X )
proper#( isQid( X ) )	→	isQid#( proper( X ) )
proper#( isQid( X ) )	→	proper#( X )
proper#( isNePal( X ) )	→	isNePal#( proper( X ) )
proper#( isNePal( X ) )	→	proper#( X )
__#( ok( X1 ) , ok( X2 ) )	→	__#( X1 , X2 )
U11#( ok( X ) )	→	U11#( X )
U21#( ok( X1 ) , ok( X2 ) )	→	U21#( X1 , X2 )
U22#( ok( X ) )	→	U22#( X )
isList#( ok( X ) )	→	isList#( X )
U31#( ok( X ) )	→	U31#( X )
U41#( ok( X1 ) , ok( X2 ) )	→	U41#( X1 , X2 )
U42#( ok( X ) )	→	U42#( X )
isNeList#( ok( X ) )	→	isNeList#( X )
U51#( ok( X1 ) , ok( X2 ) )	→	U51#( X1 , X2 )
U52#( ok( X ) )	→	U52#( X )
U61#( ok( X ) )	→	U61#( X )
U71#( ok( X1 ) , ok( X2 ) )	→	U71#( X1 , X2 )
U72#( ok( X ) )	→	U72#( X )
isPal#( ok( X ) )	→	isPal#( X )
U81#( ok( X ) )	→	U81#( X )
isQid#( ok( X ) )	→	isQid#( X )
isNePal#( ok( X ) )	→	isNePal#( X )
top#( mark( X ) )	→	top#( proper( X ) )
top#( mark( X ) )	→	proper#( X )
top#( ok( X ) )	→	top#( active( X ) )
top#( ok( X ) )	→	active#( X )

1.1: dependency graph processor

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

• The 1st component contains the pair(s)

  top#( ok( X ) )	→	top#( active( X ) )
  top#( mark( X ) )	→	top#( proper( X ) )

  1.1.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	x1 + 1
  [__ (x1, x2) ]	=	3 x1 + x2 + 2
  [a]	=	3
  [isNePal (x1) ]	=	2 x1 + 1
  [U22 (x1) ]	=	x1 + 1
  [i]	=	3
  [U72 (x1) ]	=	x1 + 2
  [U21 (x1, x2) ]	=	2 x1 + 3 x2 + 1
  [u]	=	3
  [U71 (x1, x2) ]	=	3 x1 + 2 x2 + 2
  [isNeList (x1) ]	=	3 x1 + 1
  [U52 (x1) ]	=	x1 + 2
  [isPal (x1) ]	=	2 x1 + 3
  [U11 (x1) ]	=	x1 + 1
  [top# (x1) ]	=	x1
  [isList (x1) ]	=	3 x1 + 3
  [top (x1) ]	=	0
  [mark (x1) ]	=	x1 + 1
  [U41 (x1, x2) ]	=	x1 + 3 x2 + 3
  [U61 (x1) ]	=	2 x1
  [active (x1) ]	=	x1
  [U31 (x1) ]	=	2 x1
  [U51 (x1, x2) ]	=	2 x1 + 3 x2 + 2
  [nil]	=	0
  [tt]	=	2
  [o]	=	3
  [e]	=	3
  [isQid (x1) ]	=	x1
  [ok (x1) ]	=	x1
  [U42 (x1) ]	=	x1 + 2
  [proper (x1) ]	=	x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  top#( ok( X ) )

  →

  top#( active( X ) )

  1.1.1.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	x1
  [a]	=	2
  [__ (x1, x2) ]	=	x1
  [isNePal (x1) ]	=	2 x1
  [U22 (x1) ]	=	2 x1
  [i]	=	2
  [U72 (x1) ]	=	2 x1
  [U21 (x1, x2) ]	=	3 x1 + 3 x2 + 2
  [u]	=	2
  [U71 (x1, x2) ]	=	3 x1
  [isNeList (x1) ]	=	x1
  [U52 (x1) ]	=	2 x1
  [isPal (x1) ]	=	2 x1
  [U11 (x1) ]	=	2 x1 + 2
  [top# (x1) ]	=	x1
  [isList (x1) ]	=	3 x1 + 2
  [top (x1) ]	=	0
  [mark (x1) ]	=	0
  [U41 (x1, x2) ]	=	2 x1 + 3 x2 + 1
  [U61 (x1) ]	=	2 x1
  [active (x1) ]	=	x1
  [U31 (x1) ]	=	2 x1
  [U51 (x1, x2) ]	=	3 x1 + 3
  [nil]	=	2
  [tt]	=	2
  [o]	=	2
  [e]	=	2
  [isQid (x1) ]	=	x1 + 1
  [ok (x1) ]	=	x1 + 1
  [U42 (x1) ]	=	x1
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.1.1.1: P is empty

  All dependency pairs have been removed.

• The 2nd component contains the pair(s)

  active#( __( X1 , X2 ) )	→	active#( X2 )
  active#( __( X1 , X2 ) )	→	active#( X1 )
  active#( U11( X ) )	→	active#( X )
  active#( U21( X1 , X2 ) )	→	active#( X1 )
  active#( U22( X ) )	→	active#( X )
  active#( U31( X ) )	→	active#( X )
  active#( U41( X1 , X2 ) )	→	active#( X1 )
  active#( U42( X ) )	→	active#( X )
  active#( U51( X1 , X2 ) )	→	active#( X1 )
  active#( U52( X ) )	→	active#( X )
  active#( U61( X ) )	→	active#( X )
  active#( U71( X1 , X2 ) )	→	active#( X1 )
  active#( U72( X ) )	→	active#( X )
  active#( U81( X ) )	→	active#( X )

  1.1.2: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	x1 + 1
  [a]	=	0
  [__ (x1, x2) ]	=	2 x1 + x2 + 3
  [isNePal (x1) ]	=	0
  [U22 (x1) ]	=	2 x1 + 3
  [i]	=	0
  [U21 (x1, x2) ]	=	2 x1 + 1
  [U72 (x1) ]	=	2 x1 + 3
  [u]	=	0
  [U71 (x1, x2) ]	=	2 x1 + 1
  [isNeList (x1) ]	=	3
  [U52 (x1) ]	=	2 x1 + 1
  [isPal (x1) ]	=	0
  [U11 (x1) ]	=	2 x1 + 1
  [isList (x1) ]	=	x1 + 3
  [top (x1) ]	=	0
  [mark (x1) ]	=	0
  [active# (x1) ]	=	2 x1
  [U61 (x1) ]	=	x1 + 3
  [U41 (x1, x2) ]	=	x1 + 3
  [active (x1) ]	=	3 x1
  [U31 (x1) ]	=	x1 + 3
  [U51 (x1, x2) ]	=	x1 + 3
  [nil]	=	0
  [tt]	=	2
  [o]	=	0
  [e]	=	1
  [isQid (x1) ]	=	2
  [ok (x1) ]	=	0
  [U42 (x1) ]	=	2 x1 + 3
  [proper (x1) ]	=	2 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)

  proper#( __( X1 , X2 ) )	→	proper#( X2 )
  proper#( __( X1 , X2 ) )	→	proper#( X1 )
  proper#( U11( X ) )	→	proper#( X )
  proper#( U21( X1 , X2 ) )	→	proper#( X1 )
  proper#( U21( X1 , X2 ) )	→	proper#( X2 )
  proper#( U22( X ) )	→	proper#( X )
  proper#( isList( X ) )	→	proper#( X )
  proper#( U31( X ) )	→	proper#( X )
  proper#( U41( X1 , X2 ) )	→	proper#( X1 )
  proper#( U41( X1 , X2 ) )	→	proper#( X2 )
  proper#( U42( X ) )	→	proper#( X )
  proper#( isNeList( X ) )	→	proper#( X )
  proper#( U51( X1 , X2 ) )	→	proper#( X1 )
  proper#( U51( X1 , X2 ) )	→	proper#( X2 )
  proper#( U52( X ) )	→	proper#( X )
  proper#( U61( X ) )	→	proper#( X )
  proper#( U71( X1 , X2 ) )	→	proper#( X1 )
  proper#( U71( X1 , X2 ) )	→	proper#( X2 )
  proper#( U72( X ) )	→	proper#( X )
  proper#( isPal( X ) )	→	proper#( X )
  proper#( U81( X ) )	→	proper#( X )
  proper#( isQid( X ) )	→	proper#( X )
  proper#( isNePal( X ) )	→	proper#( X )

  1.1.3: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	x1 + 3
  [a]	=	2
  [__ (x1, x2) ]	=	x1 + 2 x2
  [isNePal (x1) ]	=	x1 + 3
  [U22 (x1) ]	=	2 x1 + 3
  [i]	=	2
  [U72 (x1) ]	=	x1 + 1
  [U21 (x1, x2) ]	=	2 x1 + 3 x2
  [u]	=	0
  [U71 (x1, x2) ]	=	2 x1 + x2 + 2
  [isNeList (x1) ]	=	2 x1 + 1
  [U52 (x1) ]	=	2 x1 + 3
  [isPal (x1) ]	=	x1 + 3
  [U11 (x1) ]	=	x1
  [isList (x1) ]	=	2 x1
  [top (x1) ]	=	0
  [mark (x1) ]	=	0
  [U61 (x1) ]	=	x1 + 3
  [U41 (x1, x2) ]	=	x1 + 2 x2 + 1
  [active (x1) ]	=	2 x1
  [U31 (x1) ]	=	2 x1 + 3
  [U51 (x1, x2) ]	=	x1 + x2 + 3
  [nil]	=	2
  [tt]	=	0
  [o]	=	2
  [e]	=	2
  [proper# (x1) ]	=	2 x1
  [isQid (x1) ]	=	x1 + 1
  [ok (x1) ]	=	0
  [U42 (x1) ]	=	2 x1 + 3
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  proper#( __( X1 , X2 ) )	→	proper#( X2 )
  proper#( __( X1 , X2 ) )	→	proper#( X1 )
  proper#( U11( X ) )	→	proper#( X )
  proper#( U21( X1 , X2 ) )	→	proper#( X1 )
  proper#( U21( X1 , X2 ) )	→	proper#( X2 )
  proper#( isList( X ) )	→	proper#( X )

  1.1.3.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	1
  [a]	=	2
  [__ (x1, x2) ]	=	2 x1 + 2 x2
  [isNePal (x1) ]	=	x1 + 2
  [U22 (x1) ]	=	3
  [i]	=	2
  [U72 (x1) ]	=	0
  [U21 (x1, x2) ]	=	x1 + 2 x2 + 1
  [u]	=	2
  [U71 (x1, x2) ]	=	3 x1
  [isNeList (x1) ]	=	2 x1 + 3
  [U52 (x1) ]	=	3
  [isPal (x1) ]	=	x1 + 2
  [U11 (x1) ]	=	2 x1
  [isList (x1) ]	=	2 x1 + 3
  [top (x1) ]	=	0
  [mark (x1) ]	=	0
  [U41 (x1, x2) ]	=	3 x1
  [U61 (x1) ]	=	0
  [active (x1) ]	=	2 x1
  [U31 (x1) ]	=	2
  [U51 (x1, x2) ]	=	3
  [nil]	=	1
  [tt]	=	0
  [o]	=	2
  [e]	=	2
  [proper# (x1) ]	=	x1
  [isQid (x1) ]	=	2 x1 + 1
  [ok (x1) ]	=	0
  [U42 (x1) ]	=	3
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  proper#( __( X1 , X2 ) )	→	proper#( X2 )
  proper#( __( X1 , X2 ) )	→	proper#( X1 )
  proper#( U11( X ) )	→	proper#( X )

  1.1.3.1.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	2 x1 + 2
  [a]	=	2
  [__ (x1, x2) ]	=	2 x1 + 2 x2 + 3
  [isNePal (x1) ]	=	2 x1 + 2
  [U22 (x1) ]	=	2 x1 + 2
  [i]	=	2
  [U72 (x1) ]	=	x1 + 2
  [U21 (x1, x2) ]	=	3
  [u]	=	2
  [U71 (x1, x2) ]	=	3
  [isNeList (x1) ]	=	3 x1 + 2
  [U52 (x1) ]	=	2 x1 + 2
  [isPal (x1) ]	=	x1 + 2
  [U11 (x1) ]	=	3 x1
  [isList (x1) ]	=	3
  [top (x1) ]	=	0
  [mark (x1) ]	=	3
  [U41 (x1, x2) ]	=	3 x1 + 2 x2 + 1
  [U61 (x1) ]	=	2 x1 + 2
  [active (x1) ]	=	2 x1
  [U31 (x1) ]	=	2 x1 + 2
  [U51 (x1, x2) ]	=	3 x1 + 2 x2 + 1
  [nil]	=	2
  [tt]	=	1
  [o]	=	2
  [e]	=	2
  [proper# (x1) ]	=	x1
  [isQid (x1) ]	=	2 x1 + 2
  [ok (x1) ]	=	3
  [U42 (x1) ]	=	2 x1 + 2
  [proper (x1) ]	=	3 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  proper#( U11( X ) )

  →

  proper#( X )

  1.1.3.1.1.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	0
  [a]	=	3
  [__ (x1, x2) ]	=	x1
  [isNePal (x1) ]	=	0
  [U22 (x1) ]	=	0
  [i]	=	3
  [U72 (x1) ]	=	0
  [U21 (x1, x2) ]	=	x1 + 3 x2 + 3
  [u]	=	3
  [U71 (x1, x2) ]	=	0
  [isNeList (x1) ]	=	3
  [U52 (x1) ]	=	x1 + 1
  [isPal (x1) ]	=	3 x1
  [U11 (x1) ]	=	x1 + 1
  [isList (x1) ]	=	2 x1 + 3
  [top (x1) ]	=	0
  [mark (x1) ]	=	0
  [U41 (x1, x2) ]	=	x1 + 3 x2 + 3
  [U61 (x1) ]	=	x1 + 1
  [active (x1) ]	=	2 x1 + 1
  [U31 (x1) ]	=	x1 + 3
  [U51 (x1, x2) ]	=	3 x1
  [nil]	=	3
  [tt]	=	0
  [o]	=	3
  [e]	=	3
  [proper# (x1) ]	=	x1
  [isQid (x1) ]	=	3 x1
  [ok (x1) ]	=	0
  [U42 (x1) ]	=	x1 + 3
  [proper (x1) ]	=	x1
  [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.1.1.1: P is empty

  All dependency pairs have been removed.

• The 4th component contains the pair(s)

  __#( X1 , mark( X2 ) )	→	__#( X1 , X2 )
  __#( mark( X1 ) , X2 )	→	__#( X1 , X2 )
  __#( ok( X1 ) , ok( X2 ) )	→	__#( X1 , X2 )

  1.1.4: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	x1
  [a]	=	0
  [__ (x1, x2) ]	=	x1 + x2
  [isNePal (x1) ]	=	0
  [U22 (x1) ]	=	x1
  [__# (x1, x2) ]	=	x1
  [i]	=	0
  [U72 (x1) ]	=	x1
  [U21 (x1, x2) ]	=	x1
  [u]	=	0
  [U71 (x1, x2) ]	=	x1
  [isNeList (x1) ]	=	0
  [U52 (x1) ]	=	x1
  [isPal (x1) ]	=	0
  [U11 (x1) ]	=	x1
  [isList (x1) ]	=	0
  [top (x1) ]	=	0
  [mark (x1) ]	=	x1 + 1
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1
  [active (x1) ]	=	x1 + 1
  [U31 (x1) ]	=	x1
  [U51 (x1, x2) ]	=	x1
  [nil]	=	0
  [tt]	=	0
  [o]	=	0
  [e]	=	0
  [isQid (x1) ]	=	0
  [ok (x1) ]	=	2 x1
  [U42 (x1) ]	=	x1
  [proper (x1) ]	=	0
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  __#( X1 , mark( X2 ) )	→	__#( X1 , X2 )
  __#( ok( X1 ) , ok( X2 ) )	→	__#( X1 , X2 )

  1.1.4.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	2 x1
  [a]	=	2
  [__ (x1, x2) ]	=	3 x1 + 3 x2 + 2
  [isNePal (x1) ]	=	x1
  [U22 (x1) ]	=	2 x1 + 2
  [__# (x1, x2) ]	=	x1
  [i]	=	2
  [U72 (x1) ]	=	3 x1 + 3
  [U21 (x1, x2) ]	=	3 x1 + 3 x2 + 2
  [u]	=	2
  [U71 (x1, x2) ]	=	x1 + 3 x2 + 3
  [isNeList (x1) ]	=	2 x1 + 2
  [U52 (x1) ]	=	2 x1 + 2
  [isPal (x1) ]	=	x1 + 2
  [U11 (x1) ]	=	2 x1 + 2
  [isList (x1) ]	=	2 x1 + 2
  [top (x1) ]	=	0
  [mark (x1) ]	=	0
  [U41 (x1, x2) ]	=	3 x1 + 3 x2 + 2
  [U61 (x1) ]	=	2 x1
  [active (x1) ]	=	2 x1
  [U31 (x1) ]	=	2 x1 + 2
  [U51 (x1, x2) ]	=	3 x1 + 3 x2 + 2
  [nil]	=	1
  [tt]	=	2
  [o]	=	2
  [e]	=	2
  [isQid (x1) ]	=	2 x1
  [ok (x1) ]	=	x1 + 1
  [U42 (x1) ]	=	2 x1 + 2
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  __#( X1 , mark( X2 ) )

  →

  __#( X1 , X2 )

  1.1.4.1.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	2 x1
  [a]	=	2
  [__ (x1, x2) ]	=	3 x1 + 2 x2 + 1
  [isNePal (x1) ]	=	2 x1 + 2
  [U22 (x1) ]	=	2 x1 + 1
  [__# (x1, x2) ]	=	x1
  [i]	=	2
  [U72 (x1) ]	=	x1 + 3
  [U21 (x1, x2) ]	=	2 x1 + 3 x2
  [u]	=	2
  [U71 (x1, x2) ]	=	3 x1 + x2 + 1
  [isNeList (x1) ]	=	x1 + 2
  [U52 (x1) ]	=	3 x1 + 1
  [isPal (x1) ]	=	2 x1 + 3
  [U11 (x1) ]	=	x1 + 1
  [isList (x1) ]	=	2 x1 + 2
  [top (x1) ]	=	0
  [mark (x1) ]	=	x1 + 1
  [U41 (x1, x2) ]	=	2 x1 + 2 x2 + 1
  [U61 (x1) ]	=	2 x1
  [active (x1) ]	=	2 x1
  [U31 (x1) ]	=	x1
  [U51 (x1, x2) ]	=	2 x1 + 3 x2
  [nil]	=	0
  [tt]	=	2
  [o]	=	2
  [e]	=	2
  [isQid (x1) ]	=	2 x1
  [ok (x1) ]	=	0
  [U42 (x1) ]	=	3 x1 + 1
  [proper (x1) ]	=	x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.4.1.1.1: P is empty

  All dependency pairs have been removed.

• The 5th component contains the pair(s)

  U11#( ok( X ) )	→	U11#( X )
  U11#( mark( X ) )	→	U11#( X )

  1.1.5: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	x1
  [a]	=	0
  [__ (x1, x2) ]	=	x1 + 2 x2 + 2
  [isNePal (x1) ]	=	1
  [U22 (x1) ]	=	x1
  [i]	=	0
  [U11# (x1) ]	=	2 x1
  [U72 (x1) ]	=	x1 + 1
  [U21 (x1, x2) ]	=	x1
  [u]	=	0
  [U71 (x1, x2) ]	=	2 x1 + 1
  [isNeList (x1) ]	=	0
  [U52 (x1) ]	=	x1
  [isPal (x1) ]	=	1
  [U11 (x1) ]	=	x1
  [isList (x1) ]	=	0
  [top (x1) ]	=	0
  [mark (x1) ]	=	x1 + 1
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1 + 2
  [active (x1) ]	=	2 x1 + 1
  [U31 (x1) ]	=	x1
  [U51 (x1, x2) ]	=	x1
  [nil]	=	0
  [tt]	=	0
  [o]	=	2
  [e]	=	0
  [isQid (x1) ]	=	0
  [ok (x1) ]	=	x1
  [U42 (x1) ]	=	x1
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  U11#( ok( X ) )

  →

  U11#( X )

  1.1.5.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	2 x1
  [a]	=	1
  [__ (x1, x2) ]	=	2 x1
  [isNePal (x1) ]	=	2 x1
  [U22 (x1) ]	=	x1 + 3
  [i]	=	2
  [U11# (x1) ]	=	x1
  [U72 (x1) ]	=	x1
  [U21 (x1, x2) ]	=	2 x1
  [u]	=	1
  [U71 (x1, x2) ]	=	2 x1
  [isNeList (x1) ]	=	2 x1
  [U52 (x1) ]	=	2 x1
  [isPal (x1) ]	=	x1
  [U11 (x1) ]	=	x1 + 3
  [isList (x1) ]	=	2 x1 + 2
  [top (x1) ]	=	0
  [mark (x1) ]	=	0
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1
  [active (x1) ]	=	2 x1
  [U31 (x1) ]	=	2 x1 + 2
  [U51 (x1, x2) ]	=	x1
  [nil]	=	2
  [tt]	=	2
  [o]	=	1
  [e]	=	2
  [isQid (x1) ]	=	2 x1 + 2
  [ok (x1) ]	=	x1 + 1
  [U42 (x1) ]	=	2 x1 + 1
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.5.1.1: P is empty

  All dependency pairs have been removed.

• The 6th component contains the pair(s)

  U21#( ok( X1 ) , ok( X2 ) )	→	U21#( X1 , X2 )
  U21#( mark( X1 ) , X2 )	→	U21#( X1 , X2 )

  1.1.6: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	x1
  [a]	=	1
  [__ (x1, x2) ]	=	x1
  [isNePal (x1) ]	=	2 x1
  [U22 (x1) ]	=	x1
  [i]	=	1
  [U72 (x1) ]	=	2 x1
  [U21 (x1, x2) ]	=	2 x1
  [u]	=	3
  [U71 (x1, x2) ]	=	3 x1 + 3 x2 + 1
  [isNeList (x1) ]	=	x1
  [U52 (x1) ]	=	3 x1
  [isPal (x1) ]	=	x1
  [U11 (x1) ]	=	x1
  [isList (x1) ]	=	2 x1
  [top (x1) ]	=	0
  [U21# (x1, x2) ]	=	x1
  [mark (x1) ]	=	0
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1
  [active (x1) ]	=	x1
  [U31 (x1) ]	=	2 x1
  [U51 (x1, x2) ]	=	x1
  [nil]	=	2
  [tt]	=	3
  [o]	=	1
  [e]	=	1
  [isQid (x1) ]	=	2 x1
  [ok (x1) ]	=	2 x1 + 1
  [U42 (x1) ]	=	2 x1
  [proper (x1) ]	=	3 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  U21#( mark( X1 ) , X2 )

  →

  U21#( X1 , X2 )

  1.1.6.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	2 x1
  [a]	=	2
  [__ (x1, x2) ]	=	3 x1 + 2 x2 + 1
  [isNePal (x1) ]	=	2 x1 + 2
  [U22 (x1) ]	=	2 x1 + 1
  [i]	=	2
  [U72 (x1) ]	=	x1 + 3
  [U21 (x1, x2) ]	=	2 x1 + 3 x2
  [u]	=	2
  [U71 (x1, x2) ]	=	3 x1 + x2 + 1
  [isNeList (x1) ]	=	x1 + 2
  [U52 (x1) ]	=	3 x1 + 1
  [isPal (x1) ]	=	2 x1 + 3
  [U11 (x1) ]	=	x1 + 1
  [isList (x1) ]	=	2 x1 + 2
  [top (x1) ]	=	0
  [U21# (x1, x2) ]	=	x1
  [mark (x1) ]	=	x1 + 1
  [U41 (x1, x2) ]	=	2 x1 + 2 x2 + 1
  [U61 (x1) ]	=	2 x1
  [active (x1) ]	=	2 x1
  [U31 (x1) ]	=	x1
  [U51 (x1, x2) ]	=	2 x1 + 3 x2
  [nil]	=	0
  [tt]	=	2
  [o]	=	2
  [e]	=	2
  [isQid (x1) ]	=	2 x1
  [ok (x1) ]	=	0
  [U42 (x1) ]	=	3 x1 + 1
  [proper (x1) ]	=	x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.6.1.1: P is empty

  All dependency pairs have been removed.

• The 7th component contains the pair(s)

  U22#( ok( X ) )	→	U22#( X )
  U22#( mark( X ) )	→	U22#( X )

  1.1.7: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	x1
  [a]	=	0
  [__ (x1, x2) ]	=	x1 + 2 x2 + 2
  [isNePal (x1) ]	=	1
  [U22 (x1) ]	=	x1
  [i]	=	0
  [U72 (x1) ]	=	x1 + 1
  [U21 (x1, x2) ]	=	x1
  [u]	=	0
  [U71 (x1, x2) ]	=	2 x1 + 1
  [isNeList (x1) ]	=	0
  [U52 (x1) ]	=	x1
  [isPal (x1) ]	=	1
  [U11 (x1) ]	=	x1
  [isList (x1) ]	=	0
  [U22# (x1) ]	=	2 x1
  [top (x1) ]	=	0
  [mark (x1) ]	=	x1 + 1
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1 + 2
  [active (x1) ]	=	2 x1 + 1
  [U31 (x1) ]	=	x1
  [U51 (x1, x2) ]	=	x1
  [nil]	=	0
  [tt]	=	0
  [o]	=	2
  [e]	=	0
  [isQid (x1) ]	=	0
  [ok (x1) ]	=	x1
  [U42 (x1) ]	=	x1
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  U22#( ok( X ) )

  →

  U22#( X )

  1.1.7.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	2 x1
  [a]	=	1
  [__ (x1, x2) ]	=	2 x1
  [isNePal (x1) ]	=	2 x1
  [U22 (x1) ]	=	x1 + 3
  [i]	=	2
  [U72 (x1) ]	=	x1
  [U21 (x1, x2) ]	=	2 x1
  [u]	=	1
  [U71 (x1, x2) ]	=	2 x1
  [isNeList (x1) ]	=	2 x1
  [U52 (x1) ]	=	2 x1
  [isPal (x1) ]	=	x1
  [U11 (x1) ]	=	x1 + 3
  [isList (x1) ]	=	2 x1 + 2
  [U22# (x1) ]	=	x1
  [top (x1) ]	=	0
  [mark (x1) ]	=	0
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1
  [active (x1) ]	=	2 x1
  [U31 (x1) ]	=	2 x1 + 2
  [U51 (x1, x2) ]	=	x1
  [nil]	=	2
  [tt]	=	2
  [o]	=	1
  [e]	=	2
  [isQid (x1) ]	=	2 x1 + 2
  [ok (x1) ]	=	x1 + 1
  [U42 (x1) ]	=	2 x1 + 1
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.7.1.1: P is empty

  All dependency pairs have been removed.

• The 8th component contains the pair(s)

  U31#( ok( X ) )	→	U31#( X )
  U31#( mark( X ) )	→	U31#( X )

  1.1.8: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	x1
  [a]	=	0
  [__ (x1, x2) ]	=	x1 + 2 x2 + 2
  [isNePal (x1) ]	=	1
  [U22 (x1) ]	=	x1
  [i]	=	0
  [U72 (x1) ]	=	x1 + 1
  [U21 (x1, x2) ]	=	x1
  [u]	=	0
  [U71 (x1, x2) ]	=	2 x1 + 1
  [isNeList (x1) ]	=	0
  [U52 (x1) ]	=	x1
  [isPal (x1) ]	=	1
  [U11 (x1) ]	=	x1
  [isList (x1) ]	=	0
  [top (x1) ]	=	0
  [mark (x1) ]	=	x1 + 1
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1 + 2
  [active (x1) ]	=	2 x1 + 1
  [U31 (x1) ]	=	x1
  [U51 (x1, x2) ]	=	x1
  [nil]	=	0
  [tt]	=	0
  [U31# (x1) ]	=	2 x1
  [o]	=	2
  [e]	=	0
  [isQid (x1) ]	=	0
  [ok (x1) ]	=	x1
  [U42 (x1) ]	=	x1
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  U31#( ok( X ) )

  →

  U31#( X )

  1.1.8.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	2 x1
  [a]	=	1
  [__ (x1, x2) ]	=	2 x1
  [isNePal (x1) ]	=	2 x1
  [U22 (x1) ]	=	x1 + 3
  [i]	=	2
  [U72 (x1) ]	=	x1
  [U21 (x1, x2) ]	=	2 x1
  [u]	=	1
  [U71 (x1, x2) ]	=	2 x1
  [isNeList (x1) ]	=	2 x1
  [U52 (x1) ]	=	2 x1
  [isPal (x1) ]	=	x1
  [U11 (x1) ]	=	x1 + 3
  [isList (x1) ]	=	2 x1 + 2
  [top (x1) ]	=	0
  [mark (x1) ]	=	0
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1
  [active (x1) ]	=	2 x1
  [U31 (x1) ]	=	2 x1 + 2
  [U51 (x1, x2) ]	=	x1
  [nil]	=	2
  [tt]	=	2
  [U31# (x1) ]	=	x1
  [o]	=	1
  [e]	=	2
  [isQid (x1) ]	=	2 x1 + 2
  [ok (x1) ]	=	x1 + 1
  [U42 (x1) ]	=	2 x1 + 1
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.8.1.1: P is empty

  All dependency pairs have been removed.

• The 9th component contains the pair(s)

  U41#( ok( X1 ) , ok( X2 ) )	→	U41#( X1 , X2 )
  U41#( mark( X1 ) , X2 )	→	U41#( X1 , X2 )

  1.1.9: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	x1
  [a]	=	1
  [__ (x1, x2) ]	=	x1
  [isNePal (x1) ]	=	2 x1
  [U22 (x1) ]	=	x1
  [i]	=	1
  [U72 (x1) ]	=	2 x1
  [U21 (x1, x2) ]	=	2 x1
  [u]	=	3
  [U71 (x1, x2) ]	=	3 x1 + 3 x2 + 1
  [isNeList (x1) ]	=	x1
  [U52 (x1) ]	=	3 x1
  [isPal (x1) ]	=	x1
  [U11 (x1) ]	=	x1
  [isList (x1) ]	=	2 x1
  [top (x1) ]	=	0
  [mark (x1) ]	=	0
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1
  [active (x1) ]	=	x1
  [U41# (x1, x2) ]	=	x1
  [U31 (x1) ]	=	2 x1
  [U51 (x1, x2) ]	=	x1
  [nil]	=	2
  [tt]	=	3
  [o]	=	1
  [e]	=	1
  [isQid (x1) ]	=	2 x1
  [ok (x1) ]	=	2 x1 + 1
  [U42 (x1) ]	=	2 x1
  [proper (x1) ]	=	3 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  U41#( mark( X1 ) , X2 )

  →

  U41#( X1 , X2 )

  1.1.9.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	2 x1
  [a]	=	2
  [__ (x1, x2) ]	=	3 x1 + 2 x2 + 1
  [isNePal (x1) ]	=	2 x1 + 2
  [U22 (x1) ]	=	2 x1 + 1
  [i]	=	2
  [U72 (x1) ]	=	x1 + 3
  [U21 (x1, x2) ]	=	2 x1 + 3 x2
  [u]	=	2
  [U71 (x1, x2) ]	=	3 x1 + x2 + 1
  [isNeList (x1) ]	=	x1 + 2
  [U52 (x1) ]	=	3 x1 + 1
  [isPal (x1) ]	=	2 x1 + 3
  [U11 (x1) ]	=	x1 + 1
  [isList (x1) ]	=	2 x1 + 2
  [top (x1) ]	=	0
  [mark (x1) ]	=	x1 + 1
  [U41 (x1, x2) ]	=	2 x1 + 2 x2 + 1
  [U61 (x1) ]	=	2 x1
  [active (x1) ]	=	2 x1
  [U41# (x1, x2) ]	=	x1
  [U31 (x1) ]	=	x1
  [U51 (x1, x2) ]	=	2 x1 + 3 x2
  [nil]	=	0
  [tt]	=	2
  [o]	=	2
  [e]	=	2
  [isQid (x1) ]	=	2 x1
  [ok (x1) ]	=	0
  [U42 (x1) ]	=	3 x1 + 1
  [proper (x1) ]	=	x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.9.1.1: P is empty

  All dependency pairs have been removed.

• The 10th component contains the pair(s)

  U42#( ok( X ) )	→	U42#( X )
  U42#( mark( X ) )	→	U42#( X )

  1.1.10: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	x1
  [a]	=	0
  [__ (x1, x2) ]	=	x1 + 2 x2 + 2
  [isNePal (x1) ]	=	1
  [U22 (x1) ]	=	x1
  [i]	=	0
  [U72 (x1) ]	=	x1 + 1
  [U21 (x1, x2) ]	=	x1
  [u]	=	0
  [U71 (x1, x2) ]	=	2 x1 + 1
  [isNeList (x1) ]	=	0
  [U52 (x1) ]	=	x1
  [isPal (x1) ]	=	1
  [U11 (x1) ]	=	x1
  [isList (x1) ]	=	0
  [top (x1) ]	=	0
  [mark (x1) ]	=	x1 + 1
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1 + 2
  [active (x1) ]	=	2 x1 + 1
  [U31 (x1) ]	=	x1
  [U51 (x1, x2) ]	=	x1
  [nil]	=	0
  [tt]	=	0
  [o]	=	2
  [e]	=	0
  [U42# (x1) ]	=	2 x1
  [isQid (x1) ]	=	0
  [ok (x1) ]	=	x1
  [U42 (x1) ]	=	x1
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  U42#( ok( X ) )

  →

  U42#( X )

  1.1.10.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	2 x1
  [a]	=	1
  [__ (x1, x2) ]	=	2 x1
  [isNePal (x1) ]	=	2 x1
  [U22 (x1) ]	=	x1 + 3
  [i]	=	2
  [U72 (x1) ]	=	x1
  [U21 (x1, x2) ]	=	2 x1
  [u]	=	1
  [U71 (x1, x2) ]	=	2 x1
  [isNeList (x1) ]	=	2 x1
  [U52 (x1) ]	=	2 x1
  [isPal (x1) ]	=	x1
  [U11 (x1) ]	=	x1 + 3
  [isList (x1) ]	=	2 x1 + 2
  [top (x1) ]	=	0
  [mark (x1) ]	=	0
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1
  [active (x1) ]	=	2 x1
  [U31 (x1) ]	=	2 x1 + 2
  [U51 (x1, x2) ]	=	x1
  [nil]	=	2
  [tt]	=	2
  [o]	=	1
  [e]	=	2
  [U42# (x1) ]	=	x1
  [isQid (x1) ]	=	2 x1 + 2
  [ok (x1) ]	=	x1 + 1
  [U42 (x1) ]	=	2 x1 + 1
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.10.1.1: P is empty

  All dependency pairs have been removed.

• The 11th component contains the pair(s)

  U51#( ok( X1 ) , ok( X2 ) )	→	U51#( X1 , X2 )
  U51#( mark( X1 ) , X2 )	→	U51#( X1 , X2 )

  1.1.11: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	x1
  [a]	=	1
  [__ (x1, x2) ]	=	x1
  [isNePal (x1) ]	=	2 x1
  [U22 (x1) ]	=	x1
  [i]	=	1
  [U72 (x1) ]	=	2 x1
  [U21 (x1, x2) ]	=	2 x1
  [u]	=	3
  [U71 (x1, x2) ]	=	3 x1 + 3 x2 + 1
  [isNeList (x1) ]	=	x1
  [U52 (x1) ]	=	3 x1
  [isPal (x1) ]	=	x1
  [U11 (x1) ]	=	x1
  [isList (x1) ]	=	2 x1
  [top (x1) ]	=	0
  [mark (x1) ]	=	0
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1
  [active (x1) ]	=	x1
  [U31 (x1) ]	=	2 x1
  [U51 (x1, x2) ]	=	x1
  [nil]	=	2
  [tt]	=	3
  [o]	=	1
  [e]	=	1
  [U51# (x1, x2) ]	=	x1
  [isQid (x1) ]	=	2 x1
  [ok (x1) ]	=	2 x1 + 1
  [U42 (x1) ]	=	2 x1
  [proper (x1) ]	=	3 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  U51#( mark( X1 ) , X2 )

  →

  U51#( X1 , X2 )

  1.1.11.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	2 x1
  [a]	=	2
  [__ (x1, x2) ]	=	3 x1 + 2 x2 + 1
  [isNePal (x1) ]	=	2 x1 + 2
  [U22 (x1) ]	=	2 x1 + 1
  [i]	=	2
  [U72 (x1) ]	=	x1 + 3
  [U21 (x1, x2) ]	=	2 x1 + 3 x2
  [u]	=	2
  [U71 (x1, x2) ]	=	3 x1 + x2 + 1
  [isNeList (x1) ]	=	x1 + 2
  [U52 (x1) ]	=	3 x1 + 1
  [isPal (x1) ]	=	2 x1 + 3
  [U11 (x1) ]	=	x1 + 1
  [isList (x1) ]	=	2 x1 + 2
  [top (x1) ]	=	0
  [mark (x1) ]	=	x1 + 1
  [U41 (x1, x2) ]	=	2 x1 + 2 x2 + 1
  [U61 (x1) ]	=	2 x1
  [active (x1) ]	=	2 x1
  [U31 (x1) ]	=	x1
  [U51 (x1, x2) ]	=	2 x1 + 3 x2
  [nil]	=	0
  [tt]	=	2
  [o]	=	2
  [e]	=	2
  [U51# (x1, x2) ]	=	x1
  [isQid (x1) ]	=	2 x1
  [ok (x1) ]	=	0
  [U42 (x1) ]	=	3 x1 + 1
  [proper (x1) ]	=	x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.11.1.1: P is empty

  All dependency pairs have been removed.

• The 12th component contains the pair(s)

  U52#( ok( X ) )	→	U52#( X )
  U52#( mark( X ) )	→	U52#( X )

  1.1.12: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	x1
  [a]	=	0
  [__ (x1, x2) ]	=	x1 + 2 x2 + 2
  [isNePal (x1) ]	=	1
  [U22 (x1) ]	=	x1
  [i]	=	0
  [U72 (x1) ]	=	x1 + 1
  [U21 (x1, x2) ]	=	x1
  [u]	=	0
  [U71 (x1, x2) ]	=	2 x1 + 1
  [isNeList (x1) ]	=	0
  [U52 (x1) ]	=	x1
  [isPal (x1) ]	=	1
  [U11 (x1) ]	=	x1
  [isList (x1) ]	=	0
  [top (x1) ]	=	0
  [mark (x1) ]	=	x1 + 1
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1 + 2
  [active (x1) ]	=	2 x1 + 1
  [U31 (x1) ]	=	x1
  [U51 (x1, x2) ]	=	x1
  [nil]	=	0
  [tt]	=	0
  [U52# (x1) ]	=	2 x1
  [o]	=	2
  [e]	=	0
  [isQid (x1) ]	=	0
  [ok (x1) ]	=	x1
  [U42 (x1) ]	=	x1
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  U52#( ok( X ) )

  →

  U52#( X )

  1.1.12.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	2 x1
  [a]	=	1
  [__ (x1, x2) ]	=	2 x1
  [isNePal (x1) ]	=	2 x1
  [U22 (x1) ]	=	x1 + 3
  [i]	=	2
  [U72 (x1) ]	=	x1
  [U21 (x1, x2) ]	=	2 x1
  [u]	=	1
  [U71 (x1, x2) ]	=	2 x1
  [isNeList (x1) ]	=	2 x1
  [U52 (x1) ]	=	2 x1
  [isPal (x1) ]	=	x1
  [U11 (x1) ]	=	x1 + 3
  [isList (x1) ]	=	2 x1 + 2
  [top (x1) ]	=	0
  [mark (x1) ]	=	0
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1
  [active (x1) ]	=	2 x1
  [U31 (x1) ]	=	2 x1 + 2
  [U51 (x1, x2) ]	=	x1
  [nil]	=	2
  [tt]	=	2
  [U52# (x1) ]	=	x1
  [o]	=	1
  [e]	=	2
  [isQid (x1) ]	=	2 x1 + 2
  [ok (x1) ]	=	x1 + 1
  [U42 (x1) ]	=	2 x1 + 1
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.12.1.1: P is empty

  All dependency pairs have been removed.

• The 13th component contains the pair(s)

  U61#( ok( X ) )	→	U61#( X )
  U61#( mark( X ) )	→	U61#( X )

  1.1.13: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	x1
  [a]	=	0
  [__ (x1, x2) ]	=	x1 + 2 x2 + 2
  [isNePal (x1) ]	=	1
  [U22 (x1) ]	=	x1
  [i]	=	0
  [U72 (x1) ]	=	x1 + 1
  [U61# (x1) ]	=	2 x1
  [U21 (x1, x2) ]	=	x1
  [u]	=	0
  [U71 (x1, x2) ]	=	2 x1 + 1
  [isNeList (x1) ]	=	0
  [U52 (x1) ]	=	x1
  [isPal (x1) ]	=	1
  [U11 (x1) ]	=	x1
  [isList (x1) ]	=	0
  [top (x1) ]	=	0
  [mark (x1) ]	=	x1 + 1
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1 + 2
  [active (x1) ]	=	2 x1 + 1
  [U31 (x1) ]	=	x1
  [U51 (x1, x2) ]	=	x1
  [nil]	=	0
  [tt]	=	0
  [o]	=	2
  [e]	=	0
  [isQid (x1) ]	=	0
  [ok (x1) ]	=	x1
  [U42 (x1) ]	=	x1
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  U61#( ok( X ) )

  →

  U61#( X )

  1.1.13.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	2 x1
  [a]	=	1
  [__ (x1, x2) ]	=	2 x1
  [isNePal (x1) ]	=	2 x1
  [U22 (x1) ]	=	x1 + 3
  [i]	=	2
  [U72 (x1) ]	=	x1
  [U61# (x1) ]	=	x1
  [U21 (x1, x2) ]	=	2 x1
  [u]	=	1
  [U71 (x1, x2) ]	=	2 x1
  [isNeList (x1) ]	=	2 x1
  [U52 (x1) ]	=	2 x1
  [isPal (x1) ]	=	x1
  [U11 (x1) ]	=	x1 + 3
  [isList (x1) ]	=	2 x1 + 2
  [top (x1) ]	=	0
  [mark (x1) ]	=	0
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1
  [active (x1) ]	=	2 x1
  [U31 (x1) ]	=	2 x1 + 2
  [U51 (x1, x2) ]	=	x1
  [nil]	=	2
  [tt]	=	2
  [o]	=	1
  [e]	=	2
  [isQid (x1) ]	=	2 x1 + 2
  [ok (x1) ]	=	x1 + 1
  [U42 (x1) ]	=	2 x1 + 1
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.13.1.1: P is empty

  All dependency pairs have been removed.

• The 14th component contains the pair(s)

  U71#( ok( X1 ) , ok( X2 ) )	→	U71#( X1 , X2 )
  U71#( mark( X1 ) , X2 )	→	U71#( X1 , X2 )

  1.1.14: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	x1
  [a]	=	1
  [__ (x1, x2) ]	=	x1
  [isNePal (x1) ]	=	2 x1
  [U22 (x1) ]	=	x1
  [i]	=	1
  [U72 (x1) ]	=	2 x1
  [U21 (x1, x2) ]	=	2 x1
  [u]	=	3
  [U71 (x1, x2) ]	=	3 x1 + 3 x2 + 1
  [isNeList (x1) ]	=	x1
  [U52 (x1) ]	=	3 x1
  [isPal (x1) ]	=	x1
  [U11 (x1) ]	=	x1
  [isList (x1) ]	=	2 x1
  [top (x1) ]	=	0
  [mark (x1) ]	=	0
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1
  [active (x1) ]	=	x1
  [U31 (x1) ]	=	2 x1
  [U51 (x1, x2) ]	=	x1
  [nil]	=	2
  [tt]	=	3
  [o]	=	1
  [e]	=	1
  [isQid (x1) ]	=	2 x1
  [U71# (x1, x2) ]	=	x1
  [ok (x1) ]	=	2 x1 + 1
  [U42 (x1) ]	=	2 x1
  [proper (x1) ]	=	3 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  U71#( mark( X1 ) , X2 )

  →

  U71#( X1 , X2 )

  1.1.14.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	2 x1
  [a]	=	2
  [__ (x1, x2) ]	=	3 x1 + 2 x2 + 1
  [isNePal (x1) ]	=	2 x1 + 2
  [U22 (x1) ]	=	2 x1 + 1
  [i]	=	2
  [U72 (x1) ]	=	x1 + 3
  [U21 (x1, x2) ]	=	2 x1 + 3 x2
  [u]	=	2
  [U71 (x1, x2) ]	=	3 x1 + x2 + 1
  [isNeList (x1) ]	=	x1 + 2
  [U52 (x1) ]	=	3 x1 + 1
  [isPal (x1) ]	=	2 x1 + 3
  [U11 (x1) ]	=	x1 + 1
  [isList (x1) ]	=	2 x1 + 2
  [top (x1) ]	=	0
  [mark (x1) ]	=	x1 + 1
  [U41 (x1, x2) ]	=	2 x1 + 2 x2 + 1
  [U61 (x1) ]	=	2 x1
  [active (x1) ]	=	2 x1
  [U31 (x1) ]	=	x1
  [U51 (x1, x2) ]	=	2 x1 + 3 x2
  [nil]	=	0
  [tt]	=	2
  [o]	=	2
  [e]	=	2
  [isQid (x1) ]	=	2 x1
  [U71# (x1, x2) ]	=	x1
  [ok (x1) ]	=	0
  [U42 (x1) ]	=	3 x1 + 1
  [proper (x1) ]	=	x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.14.1.1: P is empty

  All dependency pairs have been removed.

• The 15th component contains the pair(s)

  U72#( ok( X ) )	→	U72#( X )
  U72#( mark( X ) )	→	U72#( X )

  1.1.15: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	x1
  [a]	=	0
  [__ (x1, x2) ]	=	x1 + 2 x2 + 2
  [isNePal (x1) ]	=	1
  [U22 (x1) ]	=	x1
  [i]	=	0
  [U72 (x1) ]	=	x1 + 1
  [U21 (x1, x2) ]	=	x1
  [u]	=	0
  [U71 (x1, x2) ]	=	2 x1 + 1
  [isNeList (x1) ]	=	0
  [U52 (x1) ]	=	x1
  [U72# (x1) ]	=	2 x1
  [isPal (x1) ]	=	1
  [U11 (x1) ]	=	x1
  [isList (x1) ]	=	0
  [top (x1) ]	=	0
  [mark (x1) ]	=	x1 + 1
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1 + 2
  [active (x1) ]	=	2 x1 + 1
  [U31 (x1) ]	=	x1
  [U51 (x1, x2) ]	=	x1
  [nil]	=	0
  [tt]	=	0
  [o]	=	2
  [e]	=	0
  [isQid (x1) ]	=	0
  [ok (x1) ]	=	x1
  [U42 (x1) ]	=	x1
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  U72#( ok( X ) )

  →

  U72#( X )

  1.1.15.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	2 x1
  [a]	=	1
  [__ (x1, x2) ]	=	2 x1
  [isNePal (x1) ]	=	2 x1
  [U22 (x1) ]	=	x1 + 3
  [i]	=	2
  [U72 (x1) ]	=	x1
  [U21 (x1, x2) ]	=	2 x1
  [u]	=	1
  [U71 (x1, x2) ]	=	2 x1
  [isNeList (x1) ]	=	2 x1
  [U52 (x1) ]	=	2 x1
  [U72# (x1) ]	=	x1
  [isPal (x1) ]	=	x1
  [U11 (x1) ]	=	x1 + 3
  [isList (x1) ]	=	2 x1 + 2
  [top (x1) ]	=	0
  [mark (x1) ]	=	0
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1
  [active (x1) ]	=	2 x1
  [U31 (x1) ]	=	2 x1 + 2
  [U51 (x1, x2) ]	=	x1
  [nil]	=	2
  [tt]	=	2
  [o]	=	1
  [e]	=	2
  [isQid (x1) ]	=	2 x1 + 2
  [ok (x1) ]	=	x1 + 1
  [U42 (x1) ]	=	2 x1 + 1
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.15.1.1: P is empty

  All dependency pairs have been removed.

• The 16th component contains the pair(s)

  U81#( ok( X ) )	→	U81#( X )
  U81#( mark( X ) )	→	U81#( X )

  1.1.16: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	x1
  [a]	=	0
  [__ (x1, x2) ]	=	x1 + 2 x2 + 2
  [isNePal (x1) ]	=	1
  [U22 (x1) ]	=	x1
  [i]	=	0
  [U72 (x1) ]	=	x1 + 1
  [U21 (x1, x2) ]	=	x1
  [u]	=	0
  [U71 (x1, x2) ]	=	2 x1 + 1
  [isNeList (x1) ]	=	0
  [U52 (x1) ]	=	x1
  [isPal (x1) ]	=	1
  [U11 (x1) ]	=	x1
  [U81# (x1) ]	=	2 x1
  [isList (x1) ]	=	0
  [top (x1) ]	=	0
  [mark (x1) ]	=	x1 + 1
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1 + 2
  [active (x1) ]	=	2 x1 + 1
  [U31 (x1) ]	=	x1
  [U51 (x1, x2) ]	=	x1
  [nil]	=	0
  [tt]	=	0
  [o]	=	2
  [e]	=	0
  [isQid (x1) ]	=	0
  [ok (x1) ]	=	x1
  [U42 (x1) ]	=	x1
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  U81#( ok( X ) )

  →

  U81#( X )

  1.1.16.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	2 x1
  [a]	=	1
  [__ (x1, x2) ]	=	2 x1
  [isNePal (x1) ]	=	2 x1
  [U22 (x1) ]	=	x1 + 3
  [i]	=	2
  [U72 (x1) ]	=	x1
  [U21 (x1, x2) ]	=	2 x1
  [u]	=	1
  [U71 (x1, x2) ]	=	2 x1
  [isNeList (x1) ]	=	2 x1
  [U52 (x1) ]	=	2 x1
  [isPal (x1) ]	=	x1
  [U11 (x1) ]	=	x1 + 3
  [U81# (x1) ]	=	x1
  [isList (x1) ]	=	2 x1 + 2
  [top (x1) ]	=	0
  [mark (x1) ]	=	0
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1
  [active (x1) ]	=	2 x1
  [U31 (x1) ]	=	2 x1 + 2
  [U51 (x1, x2) ]	=	x1
  [nil]	=	2
  [tt]	=	2
  [o]	=	1
  [e]	=	2
  [isQid (x1) ]	=	2 x1 + 2
  [ok (x1) ]	=	x1 + 1
  [U42 (x1) ]	=	2 x1 + 1
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.16.1.1: P is empty

  All dependency pairs have been removed.

• The 17th component contains the pair(s)

  isList#( ok( X ) )

  →

  isList#( X )

  1.1.17: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	2 x1
  [isList# (x1) ]	=	x1
  [a]	=	1
  [__ (x1, x2) ]	=	2 x1
  [isNePal (x1) ]	=	2 x1
  [U22 (x1) ]	=	x1 + 3
  [i]	=	2
  [U72 (x1) ]	=	x1
  [U21 (x1, x2) ]	=	2 x1
  [u]	=	1
  [U71 (x1, x2) ]	=	2 x1
  [isNeList (x1) ]	=	2 x1
  [U52 (x1) ]	=	2 x1
  [isPal (x1) ]	=	x1
  [U11 (x1) ]	=	x1 + 3
  [isList (x1) ]	=	2 x1 + 2
  [top (x1) ]	=	0
  [mark (x1) ]	=	0
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1
  [active (x1) ]	=	2 x1
  [U31 (x1) ]	=	2 x1 + 2
  [U51 (x1, x2) ]	=	x1
  [nil]	=	2
  [tt]	=	2
  [o]	=	1
  [e]	=	2
  [isQid (x1) ]	=	2 x1 + 2
  [ok (x1) ]	=	x1 + 1
  [U42 (x1) ]	=	2 x1 + 1
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.17.1: P is empty

  All dependency pairs have been removed.

• The 18th component contains the pair(s)

  isNeList#( ok( X ) )

  →

  isNeList#( X )

  1.1.18: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	2 x1
  [a]	=	1
  [__ (x1, x2) ]	=	2 x1
  [isNePal (x1) ]	=	2 x1
  [U22 (x1) ]	=	x1 + 3
  [i]	=	2
  [U72 (x1) ]	=	x1
  [U21 (x1, x2) ]	=	2 x1
  [u]	=	1
  [U71 (x1, x2) ]	=	2 x1
  [isNeList (x1) ]	=	2 x1
  [U52 (x1) ]	=	2 x1
  [isPal (x1) ]	=	x1
  [U11 (x1) ]	=	x1 + 3
  [isList (x1) ]	=	2 x1 + 2
  [top (x1) ]	=	0
  [mark (x1) ]	=	0
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1
  [active (x1) ]	=	2 x1
  [U31 (x1) ]	=	2 x1 + 2
  [U51 (x1, x2) ]	=	x1
  [nil]	=	2
  [tt]	=	2
  [o]	=	1
  [e]	=	2
  [isNeList# (x1) ]	=	x1
  [isQid (x1) ]	=	2 x1 + 2
  [ok (x1) ]	=	x1 + 1
  [U42 (x1) ]	=	2 x1 + 1
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.18.1: P is empty

  All dependency pairs have been removed.

• The 19th component contains the pair(s)

  isPal#( ok( X ) )

  →

  isPal#( X )

  1.1.19: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	2 x1
  [a]	=	1
  [__ (x1, x2) ]	=	2 x1
  [isNePal (x1) ]	=	2 x1
  [isPal# (x1) ]	=	x1
  [U22 (x1) ]	=	x1 + 3
  [i]	=	2
  [U72 (x1) ]	=	x1
  [U21 (x1, x2) ]	=	2 x1
  [u]	=	1
  [U71 (x1, x2) ]	=	2 x1
  [isNeList (x1) ]	=	2 x1
  [U52 (x1) ]	=	2 x1
  [isPal (x1) ]	=	x1
  [U11 (x1) ]	=	x1 + 3
  [isList (x1) ]	=	2 x1 + 2
  [top (x1) ]	=	0
  [mark (x1) ]	=	0
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1
  [active (x1) ]	=	2 x1
  [U31 (x1) ]	=	2 x1 + 2
  [U51 (x1, x2) ]	=	x1
  [nil]	=	2
  [tt]	=	2
  [o]	=	1
  [e]	=	2
  [isQid (x1) ]	=	2 x1 + 2
  [ok (x1) ]	=	x1 + 1
  [U42 (x1) ]	=	2 x1 + 1
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.19.1: P is empty

  All dependency pairs have been removed.

• The 20th component contains the pair(s)

  isQid#( ok( X ) )

  →

  isQid#( X )

  1.1.20: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	2 x1
  [a]	=	1
  [__ (x1, x2) ]	=	2 x1
  [isNePal (x1) ]	=	2 x1
  [U22 (x1) ]	=	x1 + 3
  [i]	=	2
  [U72 (x1) ]	=	x1
  [U21 (x1, x2) ]	=	2 x1
  [u]	=	1
  [U71 (x1, x2) ]	=	2 x1
  [isNeList (x1) ]	=	2 x1
  [U52 (x1) ]	=	2 x1
  [isPal (x1) ]	=	x1
  [U11 (x1) ]	=	x1 + 3
  [isList (x1) ]	=	2 x1 + 2
  [top (x1) ]	=	0
  [isQid# (x1) ]	=	x1
  [mark (x1) ]	=	0
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1
  [active (x1) ]	=	2 x1
  [U31 (x1) ]	=	2 x1 + 2
  [U51 (x1, x2) ]	=	x1
  [nil]	=	2
  [tt]	=	2
  [o]	=	1
  [e]	=	2
  [isQid (x1) ]	=	2 x1 + 2
  [ok (x1) ]	=	x1 + 1
  [U42 (x1) ]	=	2 x1 + 1
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.20.1: P is empty

  All dependency pairs have been removed.

• The 21th component contains the pair(s)

  isNePal#( ok( X ) )

  →

  isNePal#( X )

  1.1.21: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U81 (x1) ]	=	2 x1
  [a]	=	1
  [__ (x1, x2) ]	=	2 x1
  [isNePal (x1) ]	=	2 x1
  [U22 (x1) ]	=	x1 + 3
  [i]	=	2
  [U72 (x1) ]	=	x1
  [U21 (x1, x2) ]	=	2 x1
  [u]	=	1
  [U71 (x1, x2) ]	=	2 x1
  [isNeList (x1) ]	=	2 x1
  [U52 (x1) ]	=	2 x1
  [isPal (x1) ]	=	x1
  [U11 (x1) ]	=	x1 + 3
  [isList (x1) ]	=	2 x1 + 2
  [top (x1) ]	=	0
  [mark (x1) ]	=	0
  [U41 (x1, x2) ]	=	x1
  [U61 (x1) ]	=	x1
  [active (x1) ]	=	2 x1
  [U31 (x1) ]	=	2 x1 + 2
  [U51 (x1, x2) ]	=	x1
  [nil]	=	2
  [tt]	=	2
  [o]	=	1
  [e]	=	2
  [isNePal# (x1) ]	=	x1
  [isQid (x1) ]	=	2 x1 + 2
  [ok (x1) ]	=	x1 + 1
  [U42 (x1) ]	=	2 x1 + 1
  [proper (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.21.1: P is empty

  All dependency pairs have been removed.