MAYBE
TRS:
 {      le(s(x), s(y)) -> le(x, y),
         le(s(x), 0()) -> false(),
            le(0(), y) -> true(),
          double(s(x)) -> s(s(double(x))),
           double(0()) -> 0(),
             log(s(x)) -> loop(s(x), s(0()), 0()),
              log(0()) -> logError(),
      loop(x, s(y), z) -> if(le(x, s(y)), x, s(y), z),
  if(false(), x, y, z) -> loop(x, double(y), s(z)),
   if(true(), x, y, z) -> z}
 DP:
  Strict:
   {      le#(s(x), s(y)) -> le#(x, y),
            double#(s(x)) -> double#(x),
               log#(s(x)) -> loop#(s(x), s(0()), 0()),
        loop#(x, s(y), z) -> le#(x, s(y)),
        loop#(x, s(y), z) -> if#(le(x, s(y)), x, s(y), z),
    if#(false(), x, y, z) -> double#(y),
    if#(false(), x, y, z) -> loop#(x, double(y), s(z))}
  Weak:
  {      le(s(x), s(y)) -> le(x, y),
          le(s(x), 0()) -> false(),
             le(0(), y) -> true(),
           double(s(x)) -> s(s(double(x))),
            double(0()) -> 0(),
              log(s(x)) -> loop(s(x), s(0()), 0()),
               log(0()) -> logError(),
       loop(x, s(y), z) -> if(le(x, s(y)), x, s(y), z),
   if(false(), x, y, z) -> loop(x, double(y), s(z)),
    if(true(), x, y, z) -> z}
  EDG:
   {(loop#(x, s(y), z) -> le#(x, s(y)), le#(s(x), s(y)) -> le#(x, y))
    (if#(false(), x, y, z) -> loop#(x, double(y), s(z)), loop#(x, s(y), z) -> if#(le(x, s(y)), x, s(y), z))
    (if#(false(), x, y, z) -> loop#(x, double(y), s(z)), loop#(x, s(y), z) -> le#(x, s(y)))
    (log#(s(x)) -> loop#(s(x), s(0()), 0()), loop#(x, s(y), z) -> if#(le(x, s(y)), x, s(y), z))
    (log#(s(x)) -> loop#(s(x), s(0()), 0()), loop#(x, s(y), z) -> le#(x, s(y)))
    (loop#(x, s(y), z) -> if#(le(x, s(y)), x, s(y), z), if#(false(), x, y, z) -> double#(y))
    (loop#(x, s(y), z) -> if#(le(x, s(y)), x, s(y), z), if#(false(), x, y, z) -> loop#(x, double(y), s(z)))
    (double#(s(x)) -> double#(x), double#(s(x)) -> double#(x))
    (if#(false(), x, y, z) -> double#(y), double#(s(x)) -> double#(x))
    (le#(s(x), s(y)) -> le#(x, y), le#(s(x), s(y)) -> le#(x, y))}
   SCCS:
    Scc:
     {    loop#(x, s(y), z) -> if#(le(x, s(y)), x, s(y), z),
      if#(false(), x, y, z) -> loop#(x, double(y), s(z))}
    Scc:
     {double#(s(x)) -> double#(x)}
    Scc:
     {le#(s(x), s(y)) -> le#(x, y)}
    SCC:
     Strict:
      {    loop#(x, s(y), z) -> if#(le(x, s(y)), x, s(y), z),
       if#(false(), x, y, z) -> loop#(x, double(y), s(z))}
     Weak:
     {      le(s(x), s(y)) -> le(x, y),
             le(s(x), 0()) -> false(),
                le(0(), y) -> true(),
              double(s(x)) -> s(s(double(x))),
               double(0()) -> 0(),
                 log(s(x)) -> loop(s(x), s(0()), 0()),
                  log(0()) -> logError(),
          loop(x, s(y), z) -> if(le(x, s(y)), x, s(y), z),
      if(false(), x, y, z) -> loop(x, double(y), s(z)),
       if(true(), x, y, z) -> z}
     Fail
    SCC:
     Strict:
      {double#(s(x)) -> double#(x)}
     Weak:
     {      le(s(x), s(y)) -> le(x, y),
             le(s(x), 0()) -> false(),
                le(0(), y) -> true(),
              double(s(x)) -> s(s(double(x))),
               double(0()) -> 0(),
                 log(s(x)) -> loop(s(x), s(0()), 0()),
                  log(0()) -> logError(),
          loop(x, s(y), z) -> if(le(x, s(y)), x, s(y), z),
      if(false(), x, y, z) -> loop(x, double(y), s(z)),
       if(true(), x, y, z) -> z}
     SPSC:
      Simple Projection:
       pi(double#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {le#(s(x), s(y)) -> le#(x, y)}
     Weak:
     {      le(s(x), s(y)) -> le(x, y),
             le(s(x), 0()) -> false(),
                le(0(), y) -> true(),
              double(s(x)) -> s(s(double(x))),
               double(0()) -> 0(),
                 log(s(x)) -> loop(s(x), s(0()), 0()),
                  log(0()) -> logError(),
          loop(x, s(y), z) -> if(le(x, s(y)), x, s(y), z),
      if(false(), x, y, z) -> loop(x, double(y), s(z)),
       if(true(), x, y, z) -> z}
     SPSC:
      Simple Projection:
       pi(le#) = 0
      Strict:
       {}
      Qed