MAYBE
Time: 0.007087
TRS:
 {f(g x, s 0()) -> f(g x, g x),
          g s x -> s g x,
          g 0() -> 0()}
 DP:
  DP:
   {f#(g x, s 0()) -> f#(g x, g x),
            g# s x -> g# x}
  TRS:
  {f(g x, s 0()) -> f(g x, g x),
           g s x -> s g x,
           g 0() -> 0()}
  EDG:
   {(g# s x -> g# x, g# s x -> g# x)
    (f#(g x, s 0()) -> f#(g x, g x), f#(g x, s 0()) -> f#(g x, g x))}
   STATUS:
    arrows: 0.500000
    SCCS (2):
     Scc:
      {g# s x -> g# x}
     Scc:
      {f#(g x, s 0()) -> f#(g x, g x)}
     
     SCC (1):
      Strict:
       {g# s x -> g# x}
      Weak:
      {f(g x, s 0()) -> f(g x, g x),
               g s x -> s g x,
               g 0() -> 0()}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [f](x0, x1) = 0,
        
        [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 0() -> 0()
        2 >= 1
        g s x -> s g x
        2 + 1x >= 2 + 1x
        f(g x, s 0()) -> f(g x, g x)
        0 + 0x >= 0 + 0x
      Qed
    SCC (1):
     Strict:
      {f#(g x, s 0()) -> f#(g x, g x)}
     Weak:
     {f(g x, s 0()) -> f(g x, g x),
              g s x -> s g x,
              g 0() -> 0()}
     Fail