YES
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:
  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)}
  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))}
   SCCS:
    Scc:
     {ifappend#(l1, l2, cons(x, l)) -> append#(l, l2),
                    append#(l1, l2) -> ifappend#(l1, l2, l1)}
    SCC:
     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)}
     SPSC:
      Simple Projection:
       pi(append#) = 0, pi(ifappend#) = 2
      Strict:
       {append#(l1, l2) -> ifappend#(l1, l2, l1)}
      EDG:
       {}
       SCCS:
        
        Qed