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:
    f14(x,y) -> x
    f14(x,y) -> y
   TDG Processor:
    DPs:
     append#(l1,l2) -> ifappend#(l1,l2,l1)
     ifappend#(l1,l2,cons(x,l)) -> append#(l,l2)
    TRS:
     f14(x,y) -> x
     f14(x,y) -> y
    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)
    Restore Modifier:
     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))
     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))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [ifappend#](x0, x1, x2) = x2 + 1,
        
        [append#](x0, x1) = x0 + 1,
        
        [ifappend](x0, x1, x2) = x1 + x2,
        
        [append](x0, x1) = x0 + x1,
        
        [tl](x0) = x0,
        
        [hd](x0) = x0,
        
        [false] = 0,
        
        [cons](x0, x1) = x0 + x1 + 1,
        
        [true] = 0,
        
        [is_empty](x0) = 0,
        
        [nil] = 0
       orientation:
        ifappend#(l1,l2,cons(x,l)) = l + x + 2 >= l + 1 = append#(l,l2)
        
        append#(l1,l2) = l1 + 1 >= l1 + 1 = ifappend#(l1,l2,l1)
        
        is_empty(nil()) = 0 >= 0 = true()
        
        is_empty(cons(x,l)) = 0 >= 0 = false()
        
        hd(cons(x,l)) = l + x + 1 >= x = x
        
        tl(cons(x,l)) = l + x + 1 >= l = l
        
        append(l1,l2) = l1 + l2 >= l1 + l2 = ifappend(l1,l2,l1)
        
        ifappend(l1,l2,nil()) = l2 >= l2 = l2
        
        ifappend(l1,l2,cons(x,l)) = l + l2 + x + 1 >= l + l2 + x + 1 = cons(x,append(l,l2))
       problem:
        DPs:
         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))
       Matrix Interpretation Processor:
        dimension: 1
        interpretation:
         [ifappend#](x0, x1, x2) = 0,
         
         [append#](x0, x1) = 1,
         
         [ifappend](x0, x1, x2) = x1 + x2,
         
         [append](x0, x1) = x0 + x1,
         
         [tl](x0) = x0,
         
         [hd](x0) = x0,
         
         [false] = 0,
         
         [cons](x0, x1) = x0 + x1,
         
         [true] = 0,
         
         [is_empty](x0) = 0,
         
         [nil] = 0
        orientation:
         append#(l1,l2) = 1 >= 0 = ifappend#(l1,l2,l1)
         
         is_empty(nil()) = 0 >= 0 = true()
         
         is_empty(cons(x,l)) = 0 >= 0 = false()
         
         hd(cons(x,l)) = l + x >= x = x
         
         tl(cons(x,l)) = l + x >= l = l
         
         append(l1,l2) = l1 + l2 >= l1 + l2 = ifappend(l1,l2,l1)
         
         ifappend(l1,l2,nil()) = l2 >= l2 = l2
         
         ifappend(l1,l2,cons(x,l)) = l + l2 + x >= l + l2 + x = 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