Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

p#( m , n , s( r ) ) → p#( m , r , n )
p#( m , s( n ) , 0 ) → p#( 0 , n , m )

1.1: reduction pair processor

Using the following reduction pair

Linear polynomial interpretation over the naturals
[s (x1) ] = x1 + 3
[0] = 1
[p (x1, x2, x3) ] = 2 x1 + x2 + x3
[p# (x1, x2, x3) ] = 3 x1 + 2 x2 + 2 x3
[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: P is empty

All dependency pairs have been removed.