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)) -> cons(x, l)
   append(l1, l2) -> ifappend(l1, l2, is_empty(l1))
   ifappend(l1, l2, true) -> l2
   ifappend(l1, l2, false) -> cons(hd(l1), append(tl(l1), 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, is_empty(l1))
   APPEND(l1, l2) -> IS_EMPTY(l1)
   IFAPPEND(l1, l2, false) -> HD(l1)
   IFAPPEND(l1, l2, false) -> APPEND(tl(l1), l2)
   IFAPPEND(l1, l2, false) -> TL(l1)

Furthermore, R contains one SCC.


SCC1:

IFAPPEND(l1, l2, false) -> APPEND(tl(l1), l2)
APPEND(l1, l2) -> IFAPPEND(l1, l2, is_empty(l1))

Found an infinite P-chain over R:
P = IFAPPEND(l1, l2, false) -> APPEND(tl(l1), l2)
APPEND(l1, l2) -> IFAPPEND(l1, l2, is_empty(l1))
R = [tl(cons(x, l)) -> cons(x, l), is_empty(cons(x, l)) -> false, is_empty(nil) -> true]
s = IFAPPEND(cons(x'''', l''''), l2''', false) evaluates to t = IFAPPEND(cons(x'''', l''''), l2''', false)
Thus, s starts an infinite reduction.


Non-Termination of R could be shown.

Duration: 0.860 seconds.