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