Term Rewriting System R:

   [x, l, l1, l2]
   is_empty(nil) -> true
   is_empty(cons(x, l)) -> false
   hd(cons(x, l)) -> x
   tl(cons(x, l)) -> l
   append(l1, l2) -> ifappend(l1, l2, l1)
   ifappend(l1, l2, nil) -> l2
   ifappend(l1, l2, cons(x, l)) -> cons(x, append(l, l2))

Termination of R to be shown.


This program has no overlaps, so it is sufficient to show innermost termination. 


R contains the following Dependency Pairs: 


   APPEND(l1, l2) -> IFAPPEND(l1, l2, l1)
   IFAPPEND(l1, l2, cons(x, l)) -> APPEND(l, l2)

Furthermore, R contains one SCC.


SCC1:

IFAPPEND(l1, l2, cons(x, l)) -> APPEND(l, l2)
APPEND(l1, l2) -> IFAPPEND(l1, l2, l1)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

No rules need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
POL(IFAPPEND(x_1, x_2, x_3)) = x_3
POL(cons(x_1, x_2)) = 1 + x_1 + x_2
POL(APPEND(x_1, x_2)) = x_1

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 0.553 seconds.