Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

-#( -( neg( x ) , neg( x ) ) , -( neg( y ) , neg( y ) ) ) → -#( -( x , y ) , -( x , y ) )
-#( -( neg( x ) , neg( x ) ) , -( neg( y ) , neg( y ) ) ) → -#( x , y )
-#( -( neg( x ) , neg( x ) ) , -( neg( y ) , neg( y ) ) ) → -#( x , y )

1.1: reduction pair processor

Using the following reduction pair

Linear polynomial interpretation over the naturals
[neg (x1) ] = x1 + 3
[- (x1, x2) ] = 3 x1 + 3 x2 + 3
[-# (x1, x2) ] = 3 x1 + 3 x2
[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.