YES
Time: 0.027241
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)}
   STATUS:
    arrows: 0.000000
    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}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [++](x0, x1) = x0 + x1 + 1,
        
        [rev](x0) = x0 + 1,
        
        [a] = 1,
        
        [b] = 1,
        
        [rev#](x0) = x0
       Strict:
        rev# ++(x, x) -> rev# x
        1 + 2x >= 0 + 1x
        rev# ++(x, y) -> rev# x
        1 + 1y + 1x >= 0 + 1x
        rev# ++(x, y) -> rev# y
        1 + 1y + 1x >= 0 + 1y
       Weak:
        rev ++(x, x) -> rev x
        2 + 2x >= 1 + 1x
        rev ++(x, y) -> ++(rev y, rev x)
        2 + 1y + 1x >= 3 + 1y + 1x
        rev b() -> b()
        2 >= 1
        rev a() -> a()
        2 >= 1
      Qed