YES
Time: 0.024237
TRS:
 {f(a(), y) -> f(y, g y),
      g a() -> b(),
      g b() -> b()}
 DP:
  DP:
   {f#(a(), y) -> f#(y, g y),
    f#(a(), y) -> g# y}
  TRS:
  {f(a(), y) -> f(y, g y),
       g a() -> b(),
       g b() -> b()}
  UR:
   {  g a() -> b(),
      g b() -> b(),
    c(x, z) -> x,
    c(x, z) -> z}
   EDG:
    {(f#(a(), y) -> f#(y, g y), f#(a(), y) -> f#(y, g y))
     (f#(a(), y) -> f#(y, g y), f#(a(), y) -> g# y)}
    STATUS:
     arrows: 0.500000
     SCCS (1):
      Scc:
       {f#(a(), y) -> f#(y, g y)}
      
      SCC (1):
       Strict:
        {f#(a(), y) -> f#(y, g y)}
       Weak:
       {f(a(), y) -> f(y, g y),
            g a() -> b(),
            g b() -> b()}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [f](x0, x1) = x0 + 1,
         
         [g](x0) = 0,
         
         [a] = 1,
         
         [b] = 0,
         
         [f#](x0, x1) = x0 + x1
        Strict:
         f#(a(), y) -> f#(y, g y)
         1 + 1y >= 0 + 1y
        Weak:
         g b() -> b()
         0 >= 0
         g a() -> b()
         0 >= 0
         f(a(), y) -> f(y, g y)
         2 + 0y >= 1 + 1y
       Qed