Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

a__U11#( tt , M , N ) → a__U12#( tt , M , N )
a__U12#( tt , M , N ) → a__plus#( mark( N ) , mark( M ) )
a__U12#( tt , M , N ) → mark#( N )
a__U12#( tt , M , N ) → mark#( M )
a__plus#( N , 0 ) → mark#( N )
a__plus#( N , s( M ) ) → a__U11#( tt , M , N )
mark#( U11( X1 , X2 , X3 ) ) → a__U11#( mark( X1 ) , X2 , X3 )
mark#( U11( X1 , X2 , X3 ) ) → mark#( X1 )
mark#( U12( X1 , X2 , X3 ) ) → a__U12#( mark( X1 ) , X2 , X3 )
mark#( U12( X1 , X2 , X3 ) ) → mark#( X1 )
mark#( plus( X1 , X2 ) ) → a__plus#( mark( X1 ) , mark( X2 ) )
mark#( plus( X1 , X2 ) ) → mark#( X1 )
mark#( plus( X1 , X2 ) ) → mark#( X2 )
mark#( s( X ) ) → mark#( X )

1.1: reduction pair processor

Using the following reduction pair

Linear polynomial interpretation over the naturals
[U11 (x1, x2, x3) ] = x1 + 2 x2 + 2 x3 + 3
[mark (x1) ] = x1
[mark# (x1) ] = 2 x1
[a__plus (x1, x2) ] = 2 x1 + 2 x2 + 1
[0] = 3
[tt] = 1
[a__U11# (x1, x2, x3) ] = 2 x1 + 2 x2 + 1
[a__U11 (x1, x2, x3) ] = x1 + 2 x2 + 2 x3 + 3
[plus (x1, x2) ] = 2 x1 + 2 x2 + 1
[a__U12 (x1, x2, x3) ] = 3 x1 + 2 x2 + 2 x3 + 1
[a__U12# (x1, x2, x3) ] = 2 x1 + 2 x2 + 1
[s (x1) ] = x1 + 2
[U12 (x1, x2, x3) ] = 3 x1 + 2 x2 + 2 x3 + 1
[a__plus# (x1, x2) ] = 2 x1 + 2 x2 + 1
[f(x1, ..., xn)] = x1 + ... + xn + 1 for all other symbols f of arity n

one remains with the following pair(s).

a__U11#( tt , M , N ) → a__U12#( tt , M , N )
a__U12#( tt , M , N ) → a__plus#( mark( N ) , mark( M ) )

1.1.1: dependency graph processor

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