YES
Time: 0.006699
TRS:
 {f(s 0(), g x) -> f(x, g x),
          g s x -> g x}
 DP:
  DP:
   {f#(s 0(), g x) -> f#(x, g x),
            g# s x -> g# x}
  TRS:
  {f(s 0(), g x) -> f(x, g x),
           g s x -> g x}
  EDG:
   {(g# s x -> g# x, g# s x -> g# x)
    (f#(s 0(), g x) -> f#(x, g x), f#(s 0(), g x) -> f#(x, g x))}
   EDG:
    {(g# s x -> g# x, g# s x -> g# x)}
    EDG:
     {(g# s x -> g# x, g# s x -> g# x)}
     EDG:
      {(g# s x -> g# x, g# s x -> g# x)}
      STATUS:
       arrows: 0.750000
       SCCS (1):
        Scc:
         {g# s x -> g# x}
        
        SCC (1):
         Strict:
          {g# s x -> g# x}
         Weak:
         {f(s 0(), g x) -> f(x, g x),
                  g s x -> g x}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [f](x0, x1) = x0 + x1 + 1,
           
           [g](x0) = x0 + 1,
           
           [s](x0) = x0 + 1,
           
           [0] = 1,
           
           [g#](x0) = x0
          Strict:
           g# s x -> g# x
           1 + 1x >= 0 + 1x
          Weak:
           g s x -> g x
           2 + 1x >= 1 + 1x
           f(s 0(), g x) -> f(x, g x)
           4 + 1x >= 2 + 2x
         Qed