MAYBE

Problem:
 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()))

Proof:
 Complexity Transformation Processor:
  strict:
   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()))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [id](x0) = x0 + 1,
     
     [f](x0, x1) = x0 + x1,
     
     [half](x0) = x0,
     
     [double](x0) = x0,
     
     [h] = 0,
     
     [s](x0) = x0,
     
     [d] = 1,
     
     [g](x0, x1) = x0 + x1 + 1,
     
     [0] = 0
    orientation:
     g(x,0()) = x + 1 >= 0 = 0()
     
     g(d(),s(x)) = x + 2 >= x + 2 = s(s(g(d(),x)))
     
     g(h(),s(0())) = 1 >= 0 = 0()
     
     g(h(),s(s(x))) = x + 1 >= x + 1 = s(g(h(),x))
     
     double(x) = x >= x + 2 = g(d(),x)
     
     half(x) = x >= x + 1 = g(h(),x)
     
     f(s(x),y) = x + y >= x + y = f(half(s(x)),double(y))
     
     f(s(0()),y) = y >= y = y
     
     id(x) = x + 1 >= x = f(x,s(0()))
    problem:
     strict:
      g(d(),s(x)) -> s(s(g(d(),x)))
      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
     weak:
      g(x,0()) -> 0()
      g(h(),s(0())) -> 0()
      id(x) -> f(x,s(0()))
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [id](x0) = x0 + 1,
       
       [f](x0, x1) = x0 + x1,
       
       [half](x0) = x0 + 1,
       
       [double](x0) = x0 + 1,
       
       [h] = 0,
       
       [s](x0) = x0,
       
       [d] = 0,
       
       [g](x0, x1) = x0 + x1,
       
       [0] = 0
      orientation:
       g(d(),s(x)) = x >= x = s(s(g(d(),x)))
       
       g(h(),s(s(x))) = x >= x = s(g(h(),x))
       
       double(x) = x + 1 >= x = g(d(),x)
       
       half(x) = x + 1 >= x = g(h(),x)
       
       f(s(x),y) = x + y >= x + y + 2 = f(half(s(x)),double(y))
       
       f(s(0()),y) = y >= y = y
       
       g(x,0()) = x >= 0 = 0()
       
       g(h(),s(0())) = 0 >= 0 = 0()
       
       id(x) = x + 1 >= x = f(x,s(0()))
      problem:
       strict:
        g(d(),s(x)) -> s(s(g(d(),x)))
        g(h(),s(s(x))) -> s(g(h(),x))
        f(s(x),y) -> f(half(s(x)),double(y))
        f(s(0()),y) -> y
       weak:
        double(x) -> g(d(),x)
        half(x) -> g(h(),x)
        g(x,0()) -> 0()
        g(h(),s(0())) -> 0()
        id(x) -> f(x,s(0()))
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [id](x0) = x0 + 1,
         
         [f](x0, x1) = x0 + x1 + 1,
         
         [half](x0) = x0,
         
         [double](x0) = x0 + 1,
         
         [h] = 0,
         
         [s](x0) = x0,
         
         [d] = 1,
         
         [g](x0, x1) = x0 + x1,
         
         [0] = 0
        orientation:
         g(d(),s(x)) = x + 1 >= x + 1 = s(s(g(d(),x)))
         
         g(h(),s(s(x))) = x >= x = s(g(h(),x))
         
         f(s(x),y) = x + y + 1 >= x + y + 2 = f(half(s(x)),double(y))
         
         f(s(0()),y) = y + 1 >= y = y
         
         double(x) = x + 1 >= x + 1 = g(d(),x)
         
         half(x) = x >= x = g(h(),x)
         
         g(x,0()) = x >= 0 = 0()
         
         g(h(),s(0())) = 0 >= 0 = 0()
         
         id(x) = x + 1 >= x + 1 = f(x,s(0()))
        problem:
         strict:
          g(d(),s(x)) -> s(s(g(d(),x)))
          g(h(),s(s(x))) -> s(g(h(),x))
          f(s(x),y) -> f(half(s(x)),double(y))
         weak:
          f(s(0()),y) -> y
          double(x) -> g(d(),x)
          half(x) -> g(h(),x)
          g(x,0()) -> 0()
          g(h(),s(0())) -> 0()
          id(x) -> f(x,s(0()))
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [id](x0) = x0 + 1,
           
           [f](x0, x1) = x0 + x1,
           
           [half](x0) = x0 + 1,
           
           [double](x0) = x0,
           
           [h] = 0,
           
           [s](x0) = x0 + 1,
           
           [d] = 0,
           
           [g](x0, x1) = x0 + x1,
           
           [0] = 0
          orientation:
           g(d(),s(x)) = x + 1 >= x + 2 = s(s(g(d(),x)))
           
           g(h(),s(s(x))) = x + 2 >= x + 1 = s(g(h(),x))
           
           f(s(x),y) = x + y + 1 >= x + y + 2 = f(half(s(x)),double(y))
           
           f(s(0()),y) = y + 1 >= y = y
           
           double(x) = x >= x = g(d(),x)
           
           half(x) = x + 1 >= x = g(h(),x)
           
           g(x,0()) = x >= 0 = 0()
           
           g(h(),s(0())) = 1 >= 0 = 0()
           
           id(x) = x + 1 >= x + 1 = f(x,s(0()))
          problem:
           strict:
            g(d(),s(x)) -> s(s(g(d(),x)))
            f(s(x),y) -> f(half(s(x)),double(y))
           weak:
            g(h(),s(s(x))) -> s(g(h(),x))
            f(s(0()),y) -> y
            double(x) -> g(d(),x)
            half(x) -> g(h(),x)
            g(x,0()) -> 0()
            g(h(),s(0())) -> 0()
            id(x) -> f(x,s(0()))
          Open