YES
Time: 0.001456
TRS:
 {     rev a() -> a(),
       rev b() -> b(),
  rev ++(x, y) -> ++(rev y, rev x),
  rev ++(x, x) -> rev x}
 DP:
  DP:
   {rev# ++(x, y) -> rev# y,
    rev# ++(x, y) -> rev# x,
    rev# ++(x, x) -> rev# x}
  TRS:
  {     rev a() -> a(),
        rev b() -> b(),
   rev ++(x, y) -> ++(rev y, rev x),
   rev ++(x, x) -> rev x}
  EDG:
   {(rev# ++(x, x) -> rev# x, rev# ++(x, x) -> rev# x)
    (rev# ++(x, x) -> rev# x, rev# ++(x, y) -> rev# x)
    (rev# ++(x, x) -> rev# x, rev# ++(x, y) -> rev# y)
    (rev# ++(x, y) -> rev# y, rev# ++(x, y) -> rev# y)
    (rev# ++(x, y) -> rev# y, rev# ++(x, y) -> rev# x)
    (rev# ++(x, y) -> rev# y, rev# ++(x, x) -> rev# x)
    (rev# ++(x, y) -> rev# x, rev# ++(x, y) -> rev# y)
    (rev# ++(x, y) -> rev# x, rev# ++(x, y) -> rev# x)
    (rev# ++(x, y) -> rev# x, rev# ++(x, x) -> rev# x)}
   SCCS (1):
    Scc:
     {rev# ++(x, y) -> rev# y,
      rev# ++(x, y) -> rev# x,
      rev# ++(x, x) -> rev# x}
    SCC (3):
     Strict:
      {rev# ++(x, y) -> rev# y,
       rev# ++(x, y) -> rev# x,
       rev# ++(x, x) -> rev# x}
     Weak:
     {     rev a() -> a(),
           rev b() -> b(),
      rev ++(x, y) -> ++(rev y, rev x),
      rev ++(x, x) -> rev x}
     SPSC:
      Simple Projection:
       pi(rev#) = 0
      Strict:
       {rev# ++(x, y) -> rev# y,
        rev# ++(x, x) -> rev# x}
      EDG:
       {(rev# ++(x, y) -> rev# y, rev# ++(x, x) -> rev# x)
        (rev# ++(x, y) -> rev# y, rev# ++(x, y) -> rev# y)
        (rev# ++(x, x) -> rev# x, rev# ++(x, y) -> rev# y)
        (rev# ++(x, x) -> rev# x, rev# ++(x, x) -> rev# x)}
       SCCS (1):
        Scc:
         {rev# ++(x, y) -> rev# y,
          rev# ++(x, x) -> rev# x}
        SCC (2):
         Strict:
          {rev# ++(x, y) -> rev# y,
           rev# ++(x, x) -> rev# x}
         Weak:
         {     rev a() -> a(),
               rev b() -> b(),
          rev ++(x, y) -> ++(rev y, rev x),
          rev ++(x, x) -> rev x}
         SPSC:
          Simple Projection:
           pi(rev#) = 0
          Strict:
           {rev# ++(x, x) -> rev# x}
          EDG:
           {(rev# ++(x, x) -> rev# x, rev# ++(x, x) -> rev# x)}
           SCCS (1):
            Scc:
             {rev# ++(x, x) -> rev# x}
            SCC (1):
             Strict:
              {rev# ++(x, x) -> rev# x}
             Weak:
             {     rev a() -> a(),
                   rev b() -> b(),
              rev ++(x, y) -> ++(rev y, rev x),
              rev ++(x, x) -> rev x}
             SPSC:
              Simple Projection:
               pi(rev#) = 0
              Strict:
               {}
              Qed