MAYBE
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()))}
 RUF:
  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}
  Weak:
   {}
  DP:
   Strict:
    {   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))}
   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}
   EDG:
    {(f#(s(x), y) -> double#(y), double#(x) -> g#(d(), x))
     (g#(d(), s(x)) -> g#(d(), x), g#(d(), s(x)) -> g#(d(), x))
     (double#(x) -> g#(d(), x), g#(d(), s(x)) -> g#(d(), x))
     (half#(x) -> g#(h(), x), g#(h(), s(s(x))) -> g#(h(), x))
     (g#(h(), s(s(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) -> 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) -> f#(half(s(x)), double(y)))}
    SCCS:
     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:
      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}
      Fail
     SCC:
      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}
      SPSC:
       Simple Projection:
        pi(g#) = 1
       Strict:
        {}
       Qed
     SCC:
      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}
      SPSC:
       Simple Projection:
        pi(g#) = 1
       Strict:
        {}
       Qed