YES

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))
  TDG 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)
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [ifappend#](x0, x1, x2) = 2x2,
     
     [append#](x0, x1) = 2x0 + 1/2,
     
     [ifappend](x0, x1, x2) = x1 + 3x2,
     
     [append](x0, x1) = 3x0 + x1 + 3,
     
     [tl](x0) = 2x0,
     
     [hd](x0) = 2x0 + 1,
     
     [false] = 0,
     
     [cons](x0, x1) = 2x0 + x1 + 3/2,
     
     [true] = 2,
     
     [is_empty](x0) = 2x0 + 2,
     
     [nil] = 0
    orientation:
     append#(l1,l2) = 2l1 + 1/2 >= 2l1 = ifappend#(l1,l2,l1)
     
     ifappend#(l1,l2,cons(x,l)) = 2l + 4x + 3 >= 2l + 1/2 = append#(l,l2)
     
     is_empty(nil()) = 2 >= 2 = true()
     
     is_empty(cons(x,l)) = 2l + 4x + 5 >= 0 = false()
     
     hd(cons(x,l)) = 2l + 4x + 4 >= x = x
     
     tl(cons(x,l)) = 2l + 4x + 3 >= l = l
     
     append(l1,l2) = 3l1 + l2 + 3 >= 3l1 + l2 = ifappend(l1,l2,l1)
     
     ifappend(l1,l2,nil()) = l2 >= l2 = l2
     
     ifappend(l1,l2,cons(x,l)) = 3l + l2 + 6x + 9/2 >= 3l + l2 + 2x + 9/2 = cons(x,append(l,l2))
    problem:
     DPs:
      
     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))
    Qed