Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

ackin#( s( X ) , s( Y ) ) → u21#( ackin( s( X ) , Y ) , X )
ackin#( s( X ) , s( Y ) ) → ackin#( s( X ) , Y )
u21#( ackout( X ) , Y ) → ackin#( Y , X )

1.1: reduction pair processor

Using the following reduction pair

Linear polynomial interpretation over the naturals
[u21# (x1, x2) ] = x1 + 3 x2 + 2
[u22 (x1) ] = 3 x1 + 1
[u21 (x1, x2) ] = 2 x1 + 1
[s (x1) ] = 3 x1 + 3
[ackout (x1) ] = 3 x1 + 2
[ackin# (x1, x2) ] = 2 x1 + 3 x2 + 3
[ackin (x1, x2) ] = x1 + 1
[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: P is empty

All dependency pairs have been removed.