YES
Time: 0.000994
TRS:
 {   g(empty(), d) -> d,
  g(cons(x, k), d) -> g(k, cons(x, d)),
     f(a, empty()) -> g(a, empty()),
  f(a, cons(x, k)) -> f(cons(x, a), k)}
 DP:
  DP:
   {g#(cons(x, k), d) -> g#(k, cons(x, d)),
       f#(a, empty()) -> g#(a, empty()),
    f#(a, cons(x, k)) -> f#(cons(x, a), k)}
  TRS:
  {   g(empty(), d) -> d,
   g(cons(x, k), d) -> g(k, cons(x, d)),
      f(a, empty()) -> g(a, empty()),
   f(a, cons(x, k)) -> f(cons(x, a), k)}
  EDG:
   {(g#(cons(x, k), d) -> g#(k, cons(x, d)), g#(cons(x, k), d) -> g#(k, cons(x, d)))
    (f#(a, empty()) -> g#(a, empty()), g#(cons(x, k), d) -> g#(k, cons(x, d)))
    (f#(a, cons(x, k)) -> f#(cons(x, a), k), f#(a, empty()) -> g#(a, empty()))
    (f#(a, cons(x, k)) -> f#(cons(x, a), k), f#(a, cons(x, k)) -> f#(cons(x, a), k))}
   SCCS (2):
    Scc:
     {f#(a, cons(x, k)) -> f#(cons(x, a), k)}
    Scc:
     {g#(cons(x, k), d) -> g#(k, cons(x, d))}
    SCC (1):
     Strict:
      {f#(a, cons(x, k)) -> f#(cons(x, a), k)}
     Weak:
     {   g(empty(), d) -> d,
      g(cons(x, k), d) -> g(k, cons(x, d)),
         f(a, empty()) -> g(a, empty()),
      f(a, cons(x, k)) -> f(cons(x, a), k)}
     SPSC:
      Simple Projection:
       pi(f#) = 1
      Strict:
       {}
      Qed
    SCC (1):
     Strict:
      {g#(cons(x, k), d) -> g#(k, cons(x, d))}
     Weak:
     {   g(empty(), d) -> d,
      g(cons(x, k), d) -> g(k, cons(x, d)),
         f(a, empty()) -> g(a, empty()),
      f(a, cons(x, k)) -> f(cons(x, a), k)}
     SPSC:
      Simple Projection:
       pi(g#) = 0
      Strict:
       {}
      Qed