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))
  Usable Rule Processor:
   DPs:
    append#(l1,l2) -> ifappend#(l1,l2,l1)
    ifappend#(l1,l2,cons(x,l)) -> append#(l,l2)
   TRS:
    
   Arctic Interpretation Processor:
    dimension: 1
    usable rules:
     
    interpretation:
     [ifappend#](x0, x1, x2) = -16x0 + -8x2 + 0,
     
     [append#](x0, x1) = -4x0 + 2,
     
     [cons](x0, x1) = x0 + 8x1 + 11
    orientation:
     append#(l1,l2) = -4l1 + 2 >= -8l1 + 0 = ifappend#(l1,l2,l1)
     
     ifappend#(l1,l2,cons(x,l)) = l + -16l1 + -8x + 3 >= -4l + 2 = append#(l,l2)
    problem:
     DPs:
      
     TRS:
      
    Qed