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