Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

plus#( s( X ) , plus( Y , Z ) ) → plus#( X , plus( s( s( Y ) ) , Z ) )
plus#( s( X ) , plus( Y , Z ) ) → plus#( s( s( Y ) ) , Z )
plus#( s( X1 ) , plus( X2 , plus( X3 , X4 ) ) ) → plus#( X1 , plus( X3 , plus( X2 , X4 ) ) )
plus#( s( X1 ) , plus( X2 , plus( X3 , X4 ) ) ) → plus#( X3 , plus( X2 , X4 ) )
plus#( s( X1 ) , plus( X2 , plus( X3 , X4 ) ) ) → plus#( X2 , X4 )

1.1: reduction pair processor

Using the following reduction pair

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

one remains with the following pair(s).

plus#( s( X ) , plus( Y , Z ) ) → plus#( X , plus( s( s( Y ) ) , Z ) )
plus#( s( X1 ) , plus( X2 , plus( X3 , X4 ) ) ) → plus#( X1 , plus( X3 , plus( X2 , X4 ) ) )

1.1.1: reduction pair processor

Using the following reduction pair

Linear polynomial interpretation over the naturals
[plus (x1, x2) ] = 0
[s (x1) ] = 2 x1 + 1
[plus# (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.