Termination proof

1: switching to dependency pairs

__#( __( X , Y ) , Z )	→	__#( X , __( Y , Z ) )
__#( __( X , Y ) , Z )	→	__#( Y , Z )
and#( tt , X )	→	activate#( X )
isList#( V )	→	isNeList#( activate( V ) )
isList#( V )	→	activate#( V )
isList#( n____( V1 , V2 ) )	→	and#( isList( activate( V1 ) ) , n__isList( activate( V2 ) ) )
isList#( n____( V1 , V2 ) )	→	isList#( activate( V1 ) )
isList#( n____( V1 , V2 ) )	→	activate#( V1 )
isList#( n____( V1 , V2 ) )	→	activate#( V2 )
isNeList#( V )	→	isQid#( activate( V ) )
isNeList#( V )	→	activate#( V )
isNeList#( n____( V1 , V2 ) )	→	and#( isList( activate( V1 ) ) , n__isNeList( activate( V2 ) ) )
isNeList#( n____( V1 , V2 ) )	→	isList#( activate( V1 ) )
isNeList#( n____( V1 , V2 ) )	→	activate#( V1 )
isNeList#( n____( V1 , V2 ) )	→	activate#( V2 )
isNeList#( n____( V1 , V2 ) )	→	and#( isNeList( activate( V1 ) ) , n__isList( activate( V2 ) ) )
isNeList#( n____( V1 , V2 ) )	→	isNeList#( activate( V1 ) )
isNeList#( n____( V1 , V2 ) )	→	activate#( V1 )
isNeList#( n____( V1 , V2 ) )	→	activate#( V2 )
isNePal#( V )	→	isQid#( activate( V ) )
isNePal#( V )	→	activate#( V )
isNePal#( n____( I , __( P , I ) ) )	→	and#( isQid( activate( I ) ) , n__isPal( activate( P ) ) )
isNePal#( n____( I , __( P , I ) ) )	→	isQid#( activate( I ) )
isNePal#( n____( I , __( P , I ) ) )	→	activate#( I )
isNePal#( n____( I , __( P , I ) ) )	→	activate#( P )
isPal#( V )	→	isNePal#( activate( V ) )
isPal#( V )	→	activate#( V )
activate#( n__nil )	→	nil#
activate#( n____( X1 , X2 ) )	→	__#( X1 , X2 )
activate#( n__isList( X ) )	→	isList#( X )
activate#( n__isNeList( X ) )	→	isNeList#( X )
activate#( n__isPal( X ) )	→	isPal#( X )
activate#( n__a )	→	a#
activate#( n__e )	→	e#
activate#( n__i )	→	i#
activate#( n__o )	→	o#
activate#( n__u )	→	u#

1.1: dependency graph processor

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

• The 1st component contains the pair(s)

  activate#( n__isList( X ) )	→	isList#( X )
  isList#( V )	→	isNeList#( activate( V ) )
  isNeList#( V )	→	activate#( V )
  activate#( n__isNeList( X ) )	→	isNeList#( X )
  isNeList#( n____( V1 , V2 ) )	→	and#( isList( activate( V1 ) ) , n__isNeList( activate( V2 ) ) )
  and#( tt , X )	→	activate#( X )
  activate#( n__isPal( X ) )	→	isPal#( X )
  isPal#( V )	→	isNePal#( activate( V ) )
  isNePal#( V )	→	activate#( V )
  isNePal#( n____( I , __( P , I ) ) )	→	and#( isQid( activate( I ) ) , n__isPal( activate( P ) ) )
  isNePal#( n____( I , __( P , I ) ) )	→	activate#( I )
  isNePal#( n____( I , __( P , I ) ) )	→	activate#( P )
  isPal#( V )	→	activate#( V )
  isNeList#( n____( V1 , V2 ) )	→	isList#( activate( V1 ) )
  isList#( V )	→	activate#( V )
  isList#( n____( V1 , V2 ) )	→	and#( isList( activate( V1 ) ) , n__isList( activate( V2 ) ) )
  isList#( n____( V1 , V2 ) )	→	isList#( activate( V1 ) )
  isList#( n____( V1 , V2 ) )	→	activate#( V1 )
  isList#( n____( V1 , V2 ) )	→	activate#( V2 )
  isNeList#( n____( V1 , V2 ) )	→	activate#( V1 )
  isNeList#( n____( V1 , V2 ) )	→	activate#( V2 )
  isNeList#( n____( V1 , V2 ) )	→	and#( isNeList( activate( V1 ) ) , n__isList( activate( V2 ) ) )
  isNeList#( n____( V1 , V2 ) )	→	isNeList#( activate( V1 ) )

  1.1.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [isList# (x1) ]	=	2 x1 + 2
  [__ (x1, x2) ]	=	x1 + x2 + 2
  [a]	=	0
  [isNePal (x1) ]	=	x1 + 1
  [isPal# (x1) ]	=	2 x1 + 2
  [i]	=	0
  [activate (x1) ]	=	x1
  [n__isList (x1) ]	=	x1 + 2
  [and (x1, x2) ]	=	x1 + x2
  [u]	=	0
  [n__o]	=	0
  [isNeList (x1) ]	=	x1 + 2
  [isPal (x1) ]	=	x1 + 1
  [n____ (x1, x2) ]	=	x1 + x2 + 2
  [isList (x1) ]	=	x1 + 2
  [and# (x1, x2) ]	=	2 x1
  [n__e]	=	0
  [n__nil]	=	0
  [n__isPal (x1) ]	=	x1 + 1
  [nil]	=	0
  [tt]	=	0
  [o]	=	0
  [e]	=	0
  [n__a]	=	0
  [n__i]	=	0
  [isNeList# (x1) ]	=	2 x1 + 2
  [activate# (x1) ]	=	2 x1
  [isNePal# (x1) ]	=	2 x1 + 1
  [isQid (x1) ]	=	0
  [n__isNeList (x1) ]	=	x1 + 2
  [n__u]	=	0
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  isList#( V )	→	isNeList#( activate( V ) )
  and#( tt , X )	→	activate#( X )
  activate#( n__isPal( X ) )	→	isPal#( X )

  1.1.1.1: dependency graph processor

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

• The 2nd component contains the pair(s)

  __#( __( X , Y ) , Z )	→	__#( Y , Z )
  __#( __( X , Y ) , Z )	→	__#( X , __( Y , Z ) )

  1.1.2: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [a]	=	2
  [__ (x1, x2) ]	=	x1 + x2 + 1
  [isNePal (x1) ]	=	0
  [__# (x1, x2) ]	=	x1
  [i]	=	0
  [activate (x1) ]	=	x1
  [n__isList (x1) ]	=	0
  [and (x1, x2) ]	=	x1
  [u]	=	0
  [n__o]	=	0
  [isNeList (x1) ]	=	0
  [isPal (x1) ]	=	0
  [n____ (x1, x2) ]	=	x1 + x2 + 1
  [isList (x1) ]	=	0
  [n__e]	=	0
  [n__nil]	=	0
  [n__isPal (x1) ]	=	0
  [nil]	=	0
  [tt]	=	0
  [o]	=	0
  [e]	=	0
  [n__a]	=	2
  [n__i]	=	0
  [n__u]	=	0
  [n__isNeList (x1) ]	=	0
  [isQid (x1) ]	=	0
  [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.