MAYBE

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

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)) -> 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))
  Usable Rule 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:
    f14(x,y) -> x
    f14(x,y) -> y
    is_empty(nil()) -> true()
    is_empty(cons(x,l)) -> false()
    tl(cons(x,l)) -> cons(x,l)
   ADG 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:
     f14(x,y) -> x
     f14(x,y) -> y
     is_empty(nil()) -> true()
     is_empty(cons(x,l)) -> false()
     tl(cons(x,l)) -> cons(x,l)
    graph:
     ifappend#(l1,l2,false()) -> append#(tl(l1),l2) ->
     append#(l1,l2) -> is_empty#(l1)
     ifappend#(l1,l2,false()) -> append#(tl(l1),l2) ->
     append#(l1,l2) -> ifappend#(l1,l2,is_empty(l1))
     append#(l1,l2) -> ifappend#(l1,l2,is_empty(l1)) ->
     ifappend#(l1,l2,false()) -> tl#(l1)
     append#(l1,l2) -> ifappend#(l1,l2,is_empty(l1)) ->
     ifappend#(l1,l2,false()) -> append#(tl(l1),l2)
     append#(l1,l2) -> ifappend#(l1,l2,is_empty(l1)) -> ifappend#(l1,l2,false()) -> hd#(l1)
    Restore Modifier:
     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)) -> 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))
     SCC Processor:
      #sccs: 1
      #rules: 2
      #arcs: 5/25
      DPs:
       ifappend#(l1,l2,false()) -> append#(tl(l1),l2)
       append#(l1,l2) -> ifappend#(l1,l2,is_empty(l1))
      TRS:
       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))
      Open