Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

f#( g( X ) ) → f#( f( X ) )

f#( g( X ) ) → f#( X )

1.1: reduction pair processor

Using the following reduction pair

Linear polynomial interpretation over the naturals

[h (x₁) ] = 0

[f (x₁) ] = x₁

[f# (x₁) ] = 2 x₁

[g (x₁) ] = 2 x₁ + 2

[f(x₁, ..., x_n)] = x₁ + ... + x_n + 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.

[h (x₁) ]	=	0
[f (x₁) ]	=	x₁
[f# (x₁) ]	=	2 x₁
[g (x₁) ]	=	2 x₁ + 2
[f(x₁, ..., x_n)]	=	x₁ + ... + x_n + 1	for all other symbols f of arity n