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,l1)
 ifappend(l1,l2,nil()) -> l2
 ifappend(l1,l2,cons(x,l)) -> cons(x,append(l,l2))

Proof:
 DP Processor:
  DPs:
   append#(l1,l2) -> ifappend#(l1,l2,l1)
   ifappend#(l1,l2,cons(x,l)) -> append#(l,l2)
  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,l1)
   ifappend(l1,l2,nil()) -> l2
   ifappend(l1,l2,cons(x,l)) -> cons(x,append(l,l2))
  CDG Processor:
   DPs:
    append#(l1,l2) -> ifappend#(l1,l2,l1)
    ifappend#(l1,l2,cons(x,l)) -> append#(l,l2)
   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,l1)
    ifappend(l1,l2,nil()) -> l2
    ifappend(l1,l2,cons(x,l)) -> cons(x,append(l,l2))
   graph:
    ifappend#(l1,l2,cons(x,l)) -> append#(l,l2) ->
    append#(l1,l2) -> ifappend#(l1,l2,l1)
    append#(l1,l2) -> ifappend#(l1,l2,l1) -> ifappend#(l1,l2,cons(x,l)) -> append#(l,l2)
   SCC Processor:
    #sccs: 1
    #rules: 2
    #arcs: 2/4
    DPs:
     ifappend#(l1,l2,cons(x,l)) -> append#(l,l2)
     append#(l1,l2) -> ifappend#(l1,l2,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,l1)
     ifappend(l1,l2,nil()) -> l2
     ifappend(l1,l2,cons(x,l)) -> cons(x,append(l,l2))
    Open