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