Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

append#( l1 , l2 ) → ifappend#( l1 , l2 , l1 )
ifappend#( l1 , l2 , cons( x , l ) ) → append#( l , l2 )

1.1: reduction pair processor

Using the following reduction pair

Linear polynomial interpretation over the naturals
[append# (x1, x2) ] = x1
[true] = 2
[append (x1, x2) ] = x1 + x2
[false] = 2
[is_empty (x1) ] = 2 x1 + 1
[hd (x1) ] = x1
[tl (x1) ] = x1
[ifappend# (x1, x2, x3) ] = x1
[nil] = 2
[cons (x1, x2) ] = x1 + x2 + 1
[ifappend (x1, x2, x3) ] = x1 + x2
[f(x1, ..., xn)] = x1 + ... + xn + 1 for all other symbols f of arity n

one remains with the following pair(s).

append#( l1 , l2 ) → ifappend#( l1 , l2 , l1 )

1.1.1: dependency graph processor

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