MAYBE
Time: 0.008440
TRS:
 {f(t(), x, y) -> f(g(x, y), x, s y),
   g(s x, s y) -> g(x, y),
   g(s x, 0()) -> t()}
 DP:
  DP:
   {f#(t(), x, y) -> f#(g(x, y), x, s y),
    f#(t(), x, y) -> g#(x, y),
     g#(s x, s y) -> g#(x, y)}
  TRS:
  {f(t(), x, y) -> f(g(x, y), x, s y),
    g(s x, s y) -> g(x, y),
    g(s x, 0()) -> t()}
  UR:
   {g(s x, s y) -> g(x, y),
    g(s x, 0()) -> t(),
        a(z, w) -> z,
        a(z, w) -> w}
   EDG:
    {(g#(s x, s y) -> g#(x, y), g#(s x, s y) -> g#(x, y))
     (f#(t(), x, y) -> f#(g(x, y), x, s y), f#(t(), x, y) -> f#(g(x, y), x, s y))
     (f#(t(), x, y) -> f#(g(x, y), x, s y), f#(t(), x, y) -> g#(x, y))
     (f#(t(), x, y) -> g#(x, y), g#(s x, s y) -> g#(x, y))}
    EDG:
     {(g#(s x, s y) -> g#(x, y), g#(s x, s y) -> g#(x, y))
      (f#(t(), x, y) -> f#(g(x, y), x, s y), f#(t(), x, y) -> f#(g(x, y), x, s y))
      (f#(t(), x, y) -> f#(g(x, y), x, s y), f#(t(), x, y) -> g#(x, y))
      (f#(t(), x, y) -> g#(x, y), g#(s x, s y) -> g#(x, y))}
     EDG:
      {(g#(s x, s y) -> g#(x, y), g#(s x, s y) -> g#(x, y))
       (f#(t(), x, y) -> f#(g(x, y), x, s y), f#(t(), x, y) -> f#(g(x, y), x, s y))
       (f#(t(), x, y) -> f#(g(x, y), x, s y), f#(t(), x, y) -> g#(x, y))
       (f#(t(), x, y) -> g#(x, y), g#(s x, s y) -> g#(x, y))}
      EDG:
       {(g#(s x, s y) -> g#(x, y), g#(s x, s y) -> g#(x, y))
        (f#(t(), x, y) -> f#(g(x, y), x, s y), f#(t(), x, y) -> f#(g(x, y), x, s y))
        (f#(t(), x, y) -> f#(g(x, y), x, s y), f#(t(), x, y) -> g#(x, y))
        (f#(t(), x, y) -> g#(x, y), g#(s x, s y) -> g#(x, y))}
       STATUS:
        arrows: 0.555556
        SCCS (2):
         Scc:
          {f#(t(), x, y) -> f#(g(x, y), x, s y)}
         Scc:
          {g#(s x, s y) -> g#(x, y)}
         
         SCC (1):
          Strict:
           {f#(t(), x, y) -> f#(g(x, y), x, s y)}
          Weak:
          {f(t(), x, y) -> f(g(x, y), x, s y),
            g(s x, s y) -> g(x, y),
            g(s x, 0()) -> t()}
          Fail
         
         SCC (1):
          Strict:
           {g#(s x, s y) -> g#(x, y)}
          Weak:
          {f(t(), x, y) -> f(g(x, y), x, s y),
            g(s x, s y) -> g(x, y),
            g(s x, 0()) -> t()}
          POLY:
           Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
           Interpretation:
            [f](x0, x1, x2) = x0 + 1,
            
            [g](x0, x1) = 0,
            
            [s](x0) = x0 + 1,
            
            [t] = 1,
            
            [0] = 0,
            
            [g#](x0, x1) = x0
           Strict:
            g#(s x, s y) -> g#(x, y)
            1 + 0x + 1y >= 0 + 0x + 1y
           Weak:
            g(s x, 0()) -> t()
            0 + 0x >= 1
            g(s x, s y) -> g(x, y)
            0 + 0x + 0y >= 0 + 0x + 0y
            f(t(), x, y) -> f(g(x, y), x, s y)
            2 + 0x + 0y >= 1 + 0x + 0y
          Qed