YES
Time: 0.003106
TRS:
 {              s a() -> a(),
                s s x -> x,
            s f(x, y) -> f(s y, s x),
            s g(x, y) -> g(s x, s y),
            f(x, a()) -> x,
            f(a(), y) -> y,
  f(g(x, y), g(u, v)) -> g(f(x, u), f(y, v)),
          g(a(), a()) -> a()}
 DP:
  DP:
   {          s# f(x, y) -> s# x,
              s# f(x, y) -> s# y,
              s# f(x, y) -> f#(s y, s x),
              s# g(x, y) -> s# x,
              s# g(x, y) -> s# y,
              s# g(x, y) -> g#(s x, s y),
    f#(g(x, y), g(u, v)) -> f#(x, u),
    f#(g(x, y), g(u, v)) -> f#(y, v),
    f#(g(x, y), g(u, v)) -> g#(f(x, u), f(y, v))}
  TRS:
  {              s a() -> a(),
                 s s x -> x,
             s f(x, y) -> f(s y, s x),
             s g(x, y) -> g(s x, s y),
             f(x, a()) -> x,
             f(a(), y) -> y,
   f(g(x, y), g(u, v)) -> g(f(x, u), f(y, v)),
           g(a(), a()) -> a()}
  EDG:
   {(s# g(x, y) -> s# x, s# g(x, y) -> g#(s x, s y))
    (s# g(x, y) -> s# x, s# g(x, y) -> s# y)
    (s# g(x, y) -> s# x, s# g(x, y) -> s# x)
    (s# g(x, y) -> s# x, s# f(x, y) -> f#(s y, s x))
    (s# g(x, y) -> s# x, s# f(x, y) -> s# y)
    (s# g(x, y) -> s# x, s# f(x, y) -> s# x)
    (f#(g(x, y), g(u, v)) -> f#(x, u), f#(g(x, y), g(u, v)) -> g#(f(x, u), f(y, v)))
    (f#(g(x, y), g(u, v)) -> f#(x, u), f#(g(x, y), g(u, v)) -> f#(y, v))
    (f#(g(x, y), g(u, v)) -> f#(x, u), f#(g(x, y), g(u, v)) -> f#(x, u))
    (s# g(x, y) -> s# y, s# g(x, y) -> g#(s x, s y))
    (s# g(x, y) -> s# y, s# g(x, y) -> s# y)
    (s# g(x, y) -> s# y, s# g(x, y) -> s# x)
    (s# g(x, y) -> s# y, s# f(x, y) -> f#(s y, s x))
    (s# g(x, y) -> s# y, s# f(x, y) -> s# y)
    (s# g(x, y) -> s# y, s# f(x, y) -> s# x)
    (s# f(x, y) -> f#(s y, s x), f#(g(x, y), g(u, v)) -> g#(f(x, u), f(y, v)))
    (s# f(x, y) -> f#(s y, s x), f#(g(x, y), g(u, v)) -> f#(y, v))
    (s# f(x, y) -> f#(s y, s x), f#(g(x, y), g(u, v)) -> f#(x, u))
    (s# f(x, y) -> s# y, s# f(x, y) -> s# x)
    (s# f(x, y) -> s# y, s# f(x, y) -> s# y)
    (s# f(x, y) -> s# y, s# f(x, y) -> f#(s y, s x))
    (s# f(x, y) -> s# y, s# g(x, y) -> s# x)
    (s# f(x, y) -> s# y, s# g(x, y) -> s# y)
    (s# f(x, y) -> s# y, s# g(x, y) -> g#(s x, s y))
    (f#(g(x, y), g(u, v)) -> f#(y, v), f#(g(x, y), g(u, v)) -> f#(x, u))
    (f#(g(x, y), g(u, v)) -> f#(y, v), f#(g(x, y), g(u, v)) -> f#(y, v))
    (f#(g(x, y), g(u, v)) -> f#(y, v), f#(g(x, y), g(u, v)) -> g#(f(x, u), f(y, v)))
    (s# f(x, y) -> s# x, s# f(x, y) -> s# x)
    (s# f(x, y) -> s# x, s# f(x, y) -> s# y)
    (s# f(x, y) -> s# x, s# f(x, y) -> f#(s y, s x))
    (s# f(x, y) -> s# x, s# g(x, y) -> s# x)
    (s# f(x, y) -> s# x, s# g(x, y) -> s# y)
    (s# f(x, y) -> s# x, s# g(x, y) -> g#(s x, s y))}
   SCCS (2):
    Scc:
     {f#(g(x, y), g(u, v)) -> f#(x, u),
      f#(g(x, y), g(u, v)) -> f#(y, v)}
    Scc:
     {s# f(x, y) -> s# x,
      s# f(x, y) -> s# y,
      s# g(x, y) -> s# x,
      s# g(x, y) -> s# y}
    SCC (2):
     Strict:
      {f#(g(x, y), g(u, v)) -> f#(x, u),
       f#(g(x, y), g(u, v)) -> f#(y, v)}
     Weak:
     {              s a() -> a(),
                    s s x -> x,
                s f(x, y) -> f(s y, s x),
                s g(x, y) -> g(s x, s y),
                f(x, a()) -> x,
                f(a(), y) -> y,
      f(g(x, y), g(u, v)) -> g(f(x, u), f(y, v)),
              g(a(), a()) -> a()}
     SPSC:
      Simple Projection:
       pi(f#) = 1
      Strict:
       {f#(g(x, y), g(u, v)) -> f#(x, u)}
      EDG:
       {(f#(g(x, y), g(u, v)) -> f#(x, u), f#(g(x, y), g(u, v)) -> f#(x, u))}
       SCCS (1):
        Scc:
         {f#(g(x, y), g(u, v)) -> f#(x, u)}
        SCC (1):
         Strict:
          {f#(g(x, y), g(u, v)) -> f#(x, u)}
         Weak:
         {              s a() -> a(),
                        s s x -> x,
                    s f(x, y) -> f(s y, s x),
                    s g(x, y) -> g(s x, s y),
                    f(x, a()) -> x,
                    f(a(), y) -> y,
          f(g(x, y), g(u, v)) -> g(f(x, u), f(y, v)),
                  g(a(), a()) -> a()}
         SPSC:
          Simple Projection:
           pi(f#) = 1
          Strict:
           {}
          Qed
    SCC (4):
     Strict:
      {s# f(x, y) -> s# x,
       s# f(x, y) -> s# y,
       s# g(x, y) -> s# x,
       s# g(x, y) -> s# y}
     Weak:
     {              s a() -> a(),
                    s s x -> x,
                s f(x, y) -> f(s y, s x),
                s g(x, y) -> g(s x, s y),
                f(x, a()) -> x,
                f(a(), y) -> y,
      f(g(x, y), g(u, v)) -> g(f(x, u), f(y, v)),
              g(a(), a()) -> a()}
     SPSC:
      Simple Projection:
       pi(s#) = 0
      Strict:
       {s# f(x, y) -> s# x,
        s# f(x, y) -> s# y,
        s# g(x, y) -> s# y}
      EDG:
       {(s# f(x, y) -> s# y, s# g(x, y) -> s# y)
        (s# f(x, y) -> s# y, s# f(x, y) -> s# y)
        (s# f(x, y) -> s# y, s# f(x, y) -> s# x)
        (s# g(x, y) -> s# y, s# f(x, y) -> s# x)
        (s# g(x, y) -> s# y, s# f(x, y) -> s# y)
        (s# g(x, y) -> s# y, s# g(x, y) -> s# y)
        (s# f(x, y) -> s# x, s# f(x, y) -> s# x)
        (s# f(x, y) -> s# x, s# f(x, y) -> s# y)
        (s# f(x, y) -> s# x, s# g(x, y) -> s# y)}
       SCCS (1):
        Scc:
         {s# f(x, y) -> s# x,
          s# f(x, y) -> s# y,
          s# g(x, y) -> s# y}
        SCC (3):
         Strict:
          {s# f(x, y) -> s# x,
           s# f(x, y) -> s# y,
           s# g(x, y) -> s# y}
         Weak:
         {              s a() -> a(),
                        s s x -> x,
                    s f(x, y) -> f(s y, s x),
                    s g(x, y) -> g(s x, s y),
                    f(x, a()) -> x,
                    f(a(), y) -> y,
          f(g(x, y), g(u, v)) -> g(f(x, u), f(y, v)),
                  g(a(), a()) -> a()}
         SPSC:
          Simple Projection:
           pi(s#) = 0
          Strict:
           {s# f(x, y) -> s# x,
            s# g(x, y) -> s# y}
          EDG:
           {(s# g(x, y) -> s# y, s# g(x, y) -> s# y)
            (s# g(x, y) -> s# y, s# f(x, y) -> s# x)
            (s# f(x, y) -> s# x, s# f(x, y) -> s# x)
            (s# f(x, y) -> s# x, s# g(x, y) -> s# y)}
           SCCS (1):
            Scc:
             {s# f(x, y) -> s# x,
              s# g(x, y) -> s# y}
            SCC (2):
             Strict:
              {s# f(x, y) -> s# x,
               s# g(x, y) -> s# y}
             Weak:
             {              s a() -> a(),
                            s s x -> x,
                        s f(x, y) -> f(s y, s x),
                        s g(x, y) -> g(s x, s y),
                        f(x, a()) -> x,
                        f(a(), y) -> y,
              f(g(x, y), g(u, v)) -> g(f(x, u), f(y, v)),
                      g(a(), a()) -> a()}
             SPSC:
              Simple Projection:
               pi(s#) = 0
              Strict:
               {s# g(x, y) -> s# y}
              EDG:
               {(s# g(x, y) -> s# y, s# g(x, y) -> s# y)}
               SCCS (1):
                Scc:
                 {s# g(x, y) -> s# y}
                SCC (1):
                 Strict:
                  {s# g(x, y) -> s# y}
                 Weak:
                 {              s a() -> a(),
                                s s x -> x,
                            s f(x, y) -> f(s y, s x),
                            s g(x, y) -> g(s x, s y),
                            f(x, a()) -> x,
                            f(a(), y) -> y,
                  f(g(x, y), g(u, v)) -> g(f(x, u), f(y, v)),
                          g(a(), a()) -> a()}
                 SPSC:
                  Simple Projection:
                   pi(s#) = 0
                  Strict:
                   {}
                  Qed