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 ) |
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 |
a__U11#( tt , M , N ) | → | a__U12#( tt , M , N ) |
a__U12#( tt , M , N ) | → | a__plus#( mark( N ) , mark( M ) ) |
The dependency pairs are split into 0 component(s).