Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

+#( x , +( y , z ) ) → +#( +( x , y ) , z )
+#( x , +( y , z ) ) → +#( x , y )
+#( *( x , y ) , +( x , z ) ) → +#( y , z )
+#( *( x , y ) , +( *( x , z ) , u ) ) → +#( *( x , +( y , z ) ) , u )
+#( *( x , y ) , +( *( x , z ) , u ) ) → +#( y , z )

1.1: reduction pair processor

Using the following reduction pair

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

one remains with the following pair(s).

+#( x , +( y , z ) ) → +#( +( x , y ) , z )

1.1.1: reduction pair processor

Using the following reduction pair

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

All dependency pairs have been removed.