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, 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))

On this Scc, a Narrowing SCC transformation can be performed.
 
As a result of transforming the rule 

   APPEND(l1, l2) -> IFAPPEND(l1, l2, is_empty(l1))
two new Dependency Pairs
are created:


   APPEND(cons(x', l'), l2) -> IFAPPEND(cons(x', l'), l2, false)
   APPEND(nil, l2) -> IFAPPEND(nil, l2, true)

The transformation is resulting in one subcycle:


SCC1.Nar1:

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

On this Scc, a Narrowing SCC transformation can be performed.
 
As a result of transforming the rule 

   IFAPPEND(l1, l2, false) -> APPEND(tl(l1), l2)
one new Dependency Pair
is created:


   IFAPPEND(cons(x', l'), l2, false) -> APPEND(l', l2)

The transformation is resulting in one subcycle:


SCC1.Nar1.Nar1:

IFAPPEND(cons(x', l'), l2, false) -> APPEND(l', l2)
APPEND(cons(x', l'), l2) -> IFAPPEND(cons(x', l'), l2, false)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(IFAPPEND(x_1, x_2, x_3)) = x_1 + x_2 + x_3
POL(false) = 0
POL(cons(x_1, x_2)) = x_1 + x_2
POL(APPEND(x_1, x_2)) = x_1 + x_2

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   tl(cons(x, l)) -> l
   is_empty(cons(x, l)) -> false
   is_empty(nil) -> true


 This transformation is resulting in one new subcycle:


SCC1.Nar1.Nar1.MRR1:

APPEND(cons(x', l'), l2) -> IFAPPEND(cons(x', l'), l2, false)
IFAPPEND(cons(x', l'), l2, false) -> APPEND(l', l2)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(IFAPPEND(x_1, x_2, x_3)) = x_1 + x_2 + x_3
POL(false) = 0
POL(APPEND(x_1, x_2)) = x_1 + x_2
POL(cons(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   IFAPPEND(cons(x', l'), l2, false) -> APPEND(l', l2)



 This transformation is resulting in no new subcycles.




Termination of R successfully shown.


Duration: 10.661 seconds.