MAYBE
Time: 0.025881
TRS:
 {    g(x, 0()) -> 0(),
    g(d(), s x) -> s s g(d(), x),
  g(h(), s 0()) -> 0(),
  g(h(), s s x) -> s g(h(), x),
       double x -> g(d(), x),
         half x -> g(h(), x),
      f(s x, y) -> f(half s x, double y),
    f(s 0(), y) -> y,
           id x -> f(x, s 0())}
 DP:
  DP:
   {  g#(d(), s x) -> g#(d(), x),
    g#(h(), s s x) -> g#(h(), x),
         double# x -> g#(d(), x),
           half# x -> g#(h(), x),
        f#(s x, y) -> double# y,
        f#(s x, y) -> half# s x,
        f#(s x, y) -> f#(half s x, double y),
             id# x -> f#(x, s 0())}
  TRS:
  {    g(x, 0()) -> 0(),
     g(d(), s x) -> s s g(d(), x),
   g(h(), s 0()) -> 0(),
   g(h(), s s x) -> s g(h(), x),
        double x -> g(d(), x),
          half x -> g(h(), x),
       f(s x, y) -> f(half s x, double y),
     f(s 0(), y) -> y,
            id x -> f(x, s 0())}
  UR:
   {    g(x, 0()) -> 0(),
      g(d(), s x) -> s s g(d(), x),
    g(h(), s 0()) -> 0(),
    g(h(), s s x) -> s g(h(), x),
         double x -> g(d(), x),
           half x -> g(h(), x)}
   EDG:
    {(g#(h(), s s x) -> g#(h(), x), g#(h(), s s x) -> g#(h(), x))
     (half# x -> g#(h(), x), g#(h(), s s x) -> g#(h(), x))
     (f#(s x, y) -> half# s x, half# x -> g#(h(), x))
     (f#(s x, y) -> f#(half s x, double y), f#(s x, y) -> f#(half s x, double y))
     (f#(s x, y) -> f#(half s x, double y), f#(s x, y) -> half# s x)
     (f#(s x, y) -> f#(half s x, double y), f#(s x, y) -> double# y)
     (f#(s x, y) -> double# y, double# x -> g#(d(), x))
     (id# x -> f#(x, s 0()), f#(s x, y) -> double# y)
     (id# x -> f#(x, s 0()), f#(s x, y) -> half# s x)
     (id# x -> f#(x, s 0()), f#(s x, y) -> f#(half s x, double y))
     (double# x -> g#(d(), x), g#(d(), s x) -> g#(d(), x))
     (g#(d(), s x) -> g#(d(), x), g#(d(), s x) -> g#(d(), x))}
    STATUS:
     arrows: 0.812500
     SCCS (3):
      Scc:
       {f#(s x, y) -> f#(half s x, double y)}
      Scc:
       {g#(h(), s s x) -> g#(h(), x)}
      Scc:
       {g#(d(), s x) -> g#(d(), x)}
      
      
      SCC (1):
       Strict:
        {f#(s x, y) -> f#(half s x, double y)}
       Weak:
       {    g(x, 0()) -> 0(),
          g(d(), s x) -> s s g(d(), x),
        g(h(), s 0()) -> 0(),
        g(h(), s s x) -> s g(h(), x),
             double x -> g(d(), x),
               half x -> g(h(), x),
            f(s x, y) -> f(half s x, double y),
          f(s 0(), y) -> y,
                 id x -> f(x, s 0())}
       Fail
      
      
      
      
      SCC (1):
       Strict:
        {g#(h(), s s x) -> g#(h(), x)}
       Weak:
       {    g(x, 0()) -> 0(),
          g(d(), s x) -> s s g(d(), x),
        g(h(), s 0()) -> 0(),
        g(h(), s s x) -> s g(h(), x),
             double x -> g(d(), x),
               half x -> g(h(), x),
            f(s x, y) -> f(half s x, double y),
          f(s 0(), y) -> y,
                 id x -> f(x, s 0())}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [g](x0, x1) = x0 + x1 + 1,
         
         [f](x0, x1) = x0,
         
         [s](x0) = x0 + 1,
         
         [double](x0) = 0,
         
         [half](x0) = x0 + 1,
         
         [id](x0) = 0,
         
         [0] = 1,
         
         [d] = 1,
         
         [h] = 1,
         
         [g#](x0, x1) = x0
        Strict:
         g#(h(), s s x) -> g#(h(), x)
         2 + 1x >= 0 + 1x
        Weak:
         id x -> f(x, s 0())
         0 + 0x >= 0 + 1x
         f(s 0(), y) -> y
         2 + 0y >= 1y
         f(s x, y) -> f(half s x, double y)
         1 + 1x + 0y >= 2 + 1x + 0y
         half x -> g(h(), x)
         1 + 1x >= 2 + 1x
         double x -> g(d(), x)
         0 + 0x >= 2 + 1x
         g(h(), s s x) -> s g(h(), x)
         4 + 1x >= 3 + 1x
         g(h(), s 0()) -> 0()
         4 >= 1
         g(d(), s x) -> s s g(d(), x)
         3 + 1x >= 4 + 1x
         g(x, 0()) -> 0()
         2 + 1x >= 1
       Qed
     SCC (1):
      Strict:
       {g#(d(), s x) -> g#(d(), x)}
      Weak:
      {    g(x, 0()) -> 0(),
         g(d(), s x) -> s s g(d(), x),
       g(h(), s 0()) -> 0(),
       g(h(), s s x) -> s g(h(), x),
            double x -> g(d(), x),
              half x -> g(h(), x),
           f(s x, y) -> f(half s x, double y),
         f(s 0(), y) -> y,
                id x -> f(x, s 0())}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [g](x0, x1) = x0 + x1 + 1,
        
        [f](x0, x1) = x0 + 1,
        
        [s](x0) = x0 + 1,
        
        [double](x0) = 0,
        
        [half](x0) = x0,
        
        [id](x0) = 0,
        
        [0] = 1,
        
        [d] = 1,
        
        [h] = 0,
        
        [g#](x0, x1) = x0 + 1
       Strict:
        g#(d(), s x) -> g#(d(), x)
        2 + 1x >= 1 + 1x
       Weak:
        id x -> f(x, s 0())
        0 + 0x >= 1 + 1x
        f(s 0(), y) -> y
        3 + 0y >= 1y
        f(s x, y) -> f(half s x, double y)
        2 + 1x + 0y >= 2 + 1x + 0y
        half x -> g(h(), x)
        0 + 1x >= 1 + 1x
        double x -> g(d(), x)
        0 + 0x >= 2 + 1x
        g(h(), s s x) -> s g(h(), x)
        3 + 1x >= 2 + 1x
        g(h(), s 0()) -> 0()
        3 >= 1
        g(d(), s x) -> s s g(d(), x)
        3 + 1x >= 4 + 1x
        g(x, 0()) -> 0()
        2 + 1x >= 1
      Qed