Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

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

1.1: reduction pair processor

Using the following reduction pair

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

one remains with the following pair(s).

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

1.1.1: dependency graph processor

The dependency pairs are split into 0 component(s).