MAYBE

Problem:
 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))

Proof:
 DP Processor:
  DPs:
   append#(l1,l2) -> is_empty#(l1)
   append#(l1,l2) -> ifappend#(l1,l2,is_empty(l1))
   ifappend#(l1,l2,false()) -> tl#(l1)
   ifappend#(l1,l2,false()) -> append#(tl(l1),l2)
   ifappend#(l1,l2,false()) -> hd#(l1)
  TRS:
   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))
  Open