Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

a__first#( s( X ) , cons( Y , Z ) ) → mark#( Y )
a__from#( X ) → mark#( X )
mark#( first( X1 , X2 ) ) → a__first#( mark( X1 ) , mark( X2 ) )
mark#( first( X1 , X2 ) ) → mark#( X1 )
mark#( first( X1 , X2 ) ) → mark#( X2 )
mark#( from( X ) ) → a__from#( mark( X ) )
mark#( from( X ) ) → mark#( X )
mark#( s( X ) ) → mark#( X )
mark#( cons( X1 , X2 ) ) → mark#( X1 )

1.1: reduction pair processor

Using the following reduction pair

Linear polynomial interpretation over the naturals
[from (x1) ] = 2 x1 + 2
[mark (x1) ] = 2 x1
[first (x1, x2) ] = x1 + 2 x2 + 1
[a__first (x1, x2) ] = x1 + 2 x2 + 1
[mark# (x1) ] = 2 x1
[a__from (x1) ] = 2 x1 + 3
[a__first# (x1, x2) ] = 2 x1 + 1
[s (x1) ] = 2 x1 + 3
[a__from# (x1) ] = 2 x1 + 3
[0] = 0
[nil] = 0
[cons (x1, x2) ] = x1 + 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: P is empty

All dependency pairs have been removed.