Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

i#( :( x , y ) ) → :#( y , x )
:#( :( x , y ) , z ) → :#( x , :( z , i( y ) ) )
:#( :( x , y ) , z ) → :#( z , i( y ) )
:#( :( x , y ) , z ) → i#( y )
:#( e , x ) → i#( x )
:#( x , :( y , i( x ) ) ) → i#( y )
:#( x , :( y , :( i( x ) , z ) ) ) → :#( i( z ) , y )
:#( x , :( y , :( i( x ) , z ) ) ) → i#( z )
:#( i( x ) , :( y , x ) ) → i#( y )
:#( i( x ) , :( y , :( x , z ) ) ) → :#( i( z ) , y )
:#( i( x ) , :( y , :( x , z ) ) ) → i#( z )

1.1: reduction pair processor

Using the following reduction pair

Linear polynomial interpretation over the naturals
[e] = 2
[i (x1) ] = x1
[i# (x1) ] = 2 x1 + 3
[:# (x1, x2) ] = 2 x1 + 2 x2
[: (x1, x2) ] = x1 + x2 + 2
[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 , :( z , i( y ) ) )

1.1.1: reduction pair processor

Using the following reduction pair

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