MAYBE
Time: 0.009103
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:
   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)}
   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}
   EDG:
    {(f#(s x, y) -> double# y, double# x -> g#(d(), x))
     (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))
     (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))
     (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 (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}
      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}
      SPSC:
       Simple Projection:
        pi(g#) = 1
       Strict:
        {}
       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}
      SPSC:
       Simple Projection:
        pi(g#) = 1
       Strict:
        {}
       Qed