YES
Time: 0.024646
TRS:
 {              is_empty nil() -> true(),
           is_empty cons(x, l) -> false(),
                 hd cons(x, l) -> x,
                 tl cons(x, l) -> l,
       ifappend(l1, l2, nil()) -> l2,
  ifappend(l1, l2, cons(x, l)) -> cons(x, append(l, l2)),
                append(l1, l2) -> ifappend(l1, l2, l1)}
 DP:
  DP:
   {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,
        ifappend(l1, l2, nil()) -> l2,
   ifappend(l1, l2, cons(x, l)) -> cons(x, append(l, l2)),
                 append(l1, l2) -> ifappend(l1, l2, l1)}
  UR:
   {a(y, z) -> y,
    a(y, z) -> z}
   EDG:
    {(append#(l1, l2) -> ifappend#(l1, l2, l1), ifappend#(l1, l2, cons(x, l)) -> append#(l, l2))
     (ifappend#(l1, l2, cons(x, l)) -> append#(l, l2), append#(l1, l2) -> ifappend#(l1, l2, l1))}
    STATUS:
     arrows: 0.500000
     SCCS (1):
      Scc:
       {ifappend#(l1, l2, cons(x, l)) -> append#(l, l2),
                      append#(l1, l2) -> ifappend#(l1, l2, l1)}
      
      SCC (2):
       Strict:
        {ifappend#(l1, l2, cons(x, l)) -> append#(l, l2),
                       append#(l1, l2) -> ifappend#(l1, l2, l1)}
       Weak:
       {              is_empty nil() -> true(),
                 is_empty cons(x, l) -> false(),
                       hd cons(x, l) -> x,
                       tl cons(x, l) -> l,
             ifappend(l1, l2, nil()) -> l2,
        ifappend(l1, l2, cons(x, l)) -> cons(x, append(l, l2)),
                      append(l1, l2) -> ifappend(l1, l2, l1)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [ifappend](x0, x1, x2) = x0 + 1,
         
         [cons](x0, x1) = x0 + 1,
         
         [append](x0, x1) = 1,
         
         [is_empty](x0) = x0 + 1,
         
         [hd](x0) = x0 + 1,
         
         [tl](x0) = x0 + 1,
         
         [true] = 0,
         
         [nil] = 1,
         
         [false] = 0,
         
         [ifappend#](x0, x1, x2) = x0,
         
         [append#](x0, x1) = x0 + 1
        Strict:
         append#(l1, l2) -> ifappend#(l1, l2, l1)
         1 + 1l1 + 0l2 >= 0 + 1l1 + 0l2
         ifappend#(l1, l2, cons(x, l)) -> append#(l, l2)
         1 + 0x + 1l + 0l1 + 0l2 >= 1 + 1l + 0l2
        Weak:
         append(l1, l2) -> ifappend(l1, l2, l1)
         1 + 0l1 + 0l2 >= 1 + 1l1 + 0l2
         ifappend(l1, l2, cons(x, l)) -> cons(x, append(l, l2))
         2 + 0x + 1l + 0l1 + 0l2 >= 2 + 0x + 0l + 0l2
         ifappend(l1, l2, nil()) -> l2
         2 + 0l1 + 0l2 >= 1l2
         tl cons(x, l) -> l
         2 + 0x + 1l >= 1l
         hd cons(x, l) -> x
         2 + 0x + 1l >= 1x
         is_empty cons(x, l) -> false()
         2 + 0x + 1l >= 0
         is_empty nil() -> true()
         2 >= 0
       SCCS (0):