Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

f#( 0 , 1 , x ) → f#( s( x ) , x , x )
f#( x , y , s( z ) ) → f#( 0 , 1 , z )

1.1: reduction pair processor

Using the following reduction pair

Linear polynomial interpretation over the naturals
[f (x1, x2, x3) ] = x1
[1] = 0
[0] = 0
[s (x1) ] = 2 x1 + 1
[f# (x1, x2, x3) ] = x1
[f(x1, ..., xn)] = x1 + ... + xn + 1 for all other symbols f of arity n

one remains with the following pair(s).

f#( 0 , 1 , x ) → f#( s( x ) , x , x )

1.1.1: dependency graph processor

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