Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

a#( b( a( x ) ) ) → a#( b( x ) )

1.1: reduction pair processor

Using the following reduction pair

Linear polynomial interpretation over the naturals

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

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

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

[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.

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