Termination proof

1: switching to dependency pairs

foldB#( t , s( n ) )	→	f#( foldB( t , n ) , B )
foldB#( t , s( n ) )	→	foldB#( t , n )
foldC#( t , s( n ) )	→	f#( foldC( t , n ) , C )
foldC#( t , s( n ) )	→	foldC#( t , n )
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''#( foldB( triple( s( a ) , 0 , c ) , b ) )
f'#( triple( a , b , c ) , A )	→	foldB#( triple( s( a ) , 0 , c ) , b )
f''#( triple( a , b , c ) )	→	foldC#( triple( a , b , 0 ) , 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''#( foldB( triple( s( a ) , 0 , c ) , b ) )
  f''#( triple( a , b , c ) )	→	foldC#( triple( a , b , 0 ) , c )
  foldC#( t , s( n ) )	→	f#( foldC( t , n ) , C )
  foldC#( t , s( n ) )	→	foldC#( t , n )
  f'#( triple( a , b , c ) , A )	→	foldB#( triple( s( a ) , 0 , c ) , b )
  foldB#( t , s( n ) )	→	f#( foldB( t , n ) , B )
  foldB#( t , s( n ) )	→	foldB#( t , n )

  1.1.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [triple (x1, x2, x3) ]	=	2 x1
  [foldC (x1, x2) ]	=	x1
  [f''# (x1) ]	=	2 x1
  [foldC# (x1, x2) ]	=	2 x1
  [0]	=	0
  [f'' (x1) ]	=	2 x1
  [f# (x1, x2) ]	=	2 x1
  [f'# (x1, x2) ]	=	2 x1
  [g (x1) ]	=	0
  [C]	=	0
  [f' (x1, x2) ]	=	x1
  [foldB# (x1, x2) ]	=	2 x1 + 3 x2
  [foldB (x1, x2) ]	=	x1
  [A]	=	0
  [f (x1, x2) ]	=	x1 + 3 x2
  [s (x1) ]	=	x1 + 2
  [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''#( foldB( triple( s( a ) , 0 , c ) , b ) )
  f''#( triple( a , b , c ) )	→	foldC#( triple( a , b , 0 ) , c )
  foldC#( t , s( n ) )	→	f#( foldC( t , n ) , C )
  foldC#( t , s( n ) )	→	foldC#( t , n )
  f'#( triple( a , b , c ) , A )	→	foldB#( triple( s( a ) , 0 , 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 ) )
    f'#( triple( a , b , c ) , A )	→	f''#( foldB( triple( s( a ) , 0 , c ) , b ) )
    f''#( triple( a , b , c ) )	→	foldC#( triple( a , b , 0 ) , c )
    foldC#( t , s( n ) )	→	f#( foldC( t , n ) , C )
    foldC#( t , s( n ) )	→	foldC#( t , n )

    1.1.1.1.1: reduction pair processor

    Using the following reduction pair

    Linear polynomial interpretation over the naturals

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

    one remains with the following pair(s).

    f'#( triple( a , b , c ) , A )	→	f''#( foldB( triple( s( a ) , 0 , c ) , b ) )
    f''#( triple( a , b , c ) )	→	foldC#( triple( a , b , 0 ) , c )

    1.1.1.1.1.1: dependency graph processor

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