YES
Time: 0.000673
TRS:
 {   r1(empty(), a) -> a,
  r1(cons(x, k), a) -> r1(k, cons(x, a)),
             rev ls -> r1(ls, empty())}
 RUF:
  Strict:
   {   r1(empty(), a) -> a,
    r1(cons(x, k), a) -> r1(k, cons(x, a))}
  Weak:
   {}
  RUF:
   Strict:
    {r1(cons(x, k), a) -> r1(k, cons(x, a))}
   Weak:
    {}
   DP:
    DP:
     {r1#(cons(x, k), a) -> r1#(k, cons(x, a))}
    TRS:
    {r1(cons(x, k), a) -> r1(k, cons(x, a))}
    EDG:
     {(r1#(cons(x, k), a) -> r1#(k, cons(x, a)), r1#(cons(x, k), a) -> r1#(k, cons(x, a)))}
     SCCS (1):
      Scc:
       {r1#(cons(x, k), a) -> r1#(k, cons(x, a))}
      SCC (1):
       Strict:
        {r1#(cons(x, k), a) -> r1#(k, cons(x, a))}
       Weak:
       {r1(cons(x, k), a) -> r1(k, cons(x, a))}
       SPSC:
        Simple Projection:
         pi(r1#) = 0
        Strict:
         {}
        Qed