Termination proof

1: switching to dependency pairs

foldf#( x , cons( y , z ) )	→	f#( foldf( x , z ) , y )
foldf#( x , cons( y , z ) )	→	foldf#( x , z )
f#( t , x )	→	f'#( t , g( x ) )
f#( t , x )	→	g#( x )
f'#( triple( a , b , c ) , B )	→	f#( triple( a , b , c ) , A )
f'#( triple( a , b , c ) , A )	→	f''#( foldf( triple( cons( A , a ) , nil , c ) , b ) )
f'#( triple( a , b , c ) , A )	→	foldf#( triple( cons( A , a ) , nil , c ) , b )
f''#( triple( a , b , c ) )	→	foldf#( triple( a , b , nil ) , c )

1.1: dependency graph processor

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

• The 1st component contains the pair(s)

  f#( t , x )	→	f'#( t , g( x ) )
  f'#( triple( a , b , c ) , B )	→	f#( triple( a , b , c ) , A )
  f'#( triple( a , b , c ) , A )	→	f''#( foldf( triple( cons( A , a ) , nil , c ) , b ) )
  f''#( triple( a , b , c ) )	→	foldf#( triple( a , b , nil ) , c )
  foldf#( x , cons( y , z ) )	→	f#( foldf( x , z ) , y )
  foldf#( x , cons( y , z ) )	→	foldf#( x , z )
  f'#( triple( a , b , c ) , A )	→	foldf#( triple( cons( A , a ) , nil , c ) , b )

  1.1.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [triple (x1, x2, x3) ]	=	x1 + x2
  [f''# (x1) ]	=	2 x1
  [f'' (x1) ]	=	x1 + 1
  [f# (x1, x2) ]	=	2 x1
  [f'# (x1, x2) ]	=	2 x1
  [nil]	=	0
  [g (x1) ]	=	0
  [cons (x1, x2) ]	=	x1 + x2 + 2
  [C]	=	0
  [f' (x1, x2) ]	=	x1 + 2
  [A]	=	0
  [f (x1, x2) ]	=	x1 + x2 + 2
  [foldf# (x1, x2) ]	=	2 x1 + 2 x2
  [foldf (x1, x2) ]	=	x1 + x2
  [B]	=	0
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  f#( t , x )	→	f'#( t , g( x ) )
  f'#( triple( a , b , c ) , B )	→	f#( triple( a , b , c ) , A )
  f'#( triple( a , b , c ) , A )	→	f''#( foldf( triple( cons( A , a ) , nil , c ) , b ) )
  f''#( triple( a , b , c ) )	→	foldf#( triple( a , b , nil ) , c )
  f'#( triple( a , b , c ) , A )	→	foldf#( triple( cons( A , a ) , nil , c ) , b )

  1.1.1.1: dependency graph processor

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

  • The 1st component contains the pair(s)

    f'#( triple( a , b , c ) , B )	→	f#( triple( a , b , c ) , A )
    f#( t , x )	→	f'#( t , g( x ) )

    1.1.1.1.1: reduction pair processor

    Using the following reduction pair

    Linear polynomial interpretation over the naturals

    [triple (x1, x2, x3) ]	=	0
    [f# (x1, x2) ]	=	2 x1
    [f'' (x1) ]	=	0
    [f'# (x1, x2) ]	=	2 x1
    [nil]	=	0
    [g (x1) ]	=	x1
    [cons (x1, x2) ]	=	0
    [C]	=	1
    [f' (x1, x2) ]	=	0
    [A]	=	0
    [f (x1, x2) ]	=	x1
    [foldf (x1, x2) ]	=	2 x1
    [B]	=	1
    [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

    one remains with the following pair(s).

    f#( t , x )

    →

    f'#( t , g( x ) )

    1.1.1.1.1.1: dependency graph processor

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