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,
                 mapIter(xs, ys) -> ifmap(isempty(xs), xs, ys),
                      maplog(xs) -> mapIter(xs, nil()),
          ifmap(false(), xs, ys) -> mapIter(droplast(xs), cons(log(last(xs)), ys)),
           ifmap(true(), xs, ys) -> ys,
                  isempty(nil()) -> true(),
            isempty(cons(x, xs)) -> false(),
                 droplast(nil()) -> nil(),
        droplast(cons(x, nil())) -> nil(),
  droplast(cons(x, cons(y, xs))) -> cons(x, droplast(cons(y, xs))),
                     last(nil()) -> error(),
            last(cons(x, nil())) -> x,
      last(cons(x, cons(y, xs))) -> last(cons(y, xs)),
                             a() -> b(),
                             a() -> c()}
 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)),
                   mapIter#(xs, ys) -> ifmap#(isempty(xs), xs, ys),
                   mapIter#(xs, ys) -> isempty#(xs),
                        maplog#(xs) -> mapIter#(xs, nil()),
            ifmap#(false(), xs, ys) -> log#(last(xs)),
            ifmap#(false(), xs, ys) -> mapIter#(droplast(xs), cons(log(last(xs)), ys)),
            ifmap#(false(), xs, ys) -> droplast#(xs),
            ifmap#(false(), xs, ys) -> last#(xs),
    droplast#(cons(x, cons(y, xs))) -> droplast#(cons(y, xs)),
        last#(cons(x, cons(y, xs))) -> last#(cons(y, xs))}
  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,
                  mapIter(xs, ys) -> ifmap(isempty(xs), xs, ys),
                       maplog(xs) -> mapIter(xs, nil()),
           ifmap(false(), xs, ys) -> mapIter(droplast(xs), cons(log(last(xs)), ys)),
            ifmap(true(), xs, ys) -> ys,
                   isempty(nil()) -> true(),
             isempty(cons(x, xs)) -> false(),
                  droplast(nil()) -> nil(),
         droplast(cons(x, nil())) -> nil(),
   droplast(cons(x, cons(y, xs))) -> cons(x, droplast(cons(y, xs))),
                      last(nil()) -> error(),
             last(cons(x, nil())) -> x,
       last(cons(x, cons(y, xs))) -> last(cons(y, xs)),
                              a() -> b(),
                              a() -> c()}
  EDG:
   {(ifmap#(false(), xs, ys) -> log#(last(xs)), log#(s(x)) -> loop#(s(x), s(0()), 0()))
    (droplast#(cons(x, cons(y, xs))) -> droplast#(cons(y, xs)), droplast#(cons(x, cons(y, xs))) -> droplast#(cons(y, xs)))
    (mapIter#(xs, ys) -> ifmap#(isempty(xs), xs, ys), ifmap#(false(), xs, ys) -> last#(xs))
    (mapIter#(xs, ys) -> ifmap#(isempty(xs), xs, ys), ifmap#(false(), xs, ys) -> droplast#(xs))
    (mapIter#(xs, ys) -> ifmap#(isempty(xs), xs, ys), ifmap#(false(), xs, ys) -> mapIter#(droplast(xs), cons(log(last(xs)), ys)))
    (mapIter#(xs, ys) -> ifmap#(isempty(xs), xs, ys), ifmap#(false(), xs, ys) -> log#(last(xs)))
    (le#(s(x), s(y)) -> le#(x, 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)))
    (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) -> if#(le(x, s(y)), x, s(y), z), if#(false(), x, y, z) -> double#(y))
    (ifmap#(false(), xs, ys) -> droplast#(xs), droplast#(cons(x, cons(y, xs))) -> droplast#(cons(y, xs)))
    (double#(s(x)) -> double#(x), double#(s(x)) -> double#(x))
    (ifmap#(false(), xs, ys) -> last#(xs), last#(cons(x, cons(y, xs))) -> last#(cons(y, xs)))
    (ifmap#(false(), xs, ys) -> mapIter#(droplast(xs), cons(log(last(xs)), ys)), mapIter#(xs, ys) -> ifmap#(isempty(xs), xs, ys))
    (ifmap#(false(), xs, ys) -> mapIter#(droplast(xs), cons(log(last(xs)), ys)), mapIter#(xs, ys) -> isempty#(xs))
    (log#(s(x)) -> loop#(s(x), s(0()), 0()), 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))
    (loop#(x, s(y), z) -> le#(x, s(y)), le#(s(x), s(y)) -> le#(x, y))
    (last#(cons(x, cons(y, xs))) -> last#(cons(y, xs)), last#(cons(x, cons(y, xs))) -> last#(cons(y, xs)))
    (if#(false(), x, y, z) -> double#(y), double#(s(x)) -> double#(x))
    (maplog#(xs) -> mapIter#(xs, nil()), mapIter#(xs, ys) -> ifmap#(isempty(xs), xs, ys))
    (maplog#(xs) -> mapIter#(xs, nil()), mapIter#(xs, ys) -> isempty#(xs))}
   SCCS:
    Scc:
     {last#(cons(x, cons(y, xs))) -> last#(cons(y, xs))}
    Scc:
     {droplast#(cons(x, cons(y, xs))) -> droplast#(cons(y, xs))}
    Scc:
     {       mapIter#(xs, ys) -> ifmap#(isempty(xs), xs, ys),
      ifmap#(false(), xs, ys) -> mapIter#(droplast(xs), cons(log(last(xs)), ys))}
    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:
      {last#(cons(x, cons(y, xs))) -> last#(cons(y, xs))}
     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,
                     mapIter(xs, ys) -> ifmap(isempty(xs), xs, ys),
                          maplog(xs) -> mapIter(xs, nil()),
              ifmap(false(), xs, ys) -> mapIter(droplast(xs), cons(log(last(xs)), ys)),
               ifmap(true(), xs, ys) -> ys,
                      isempty(nil()) -> true(),
                isempty(cons(x, xs)) -> false(),
                     droplast(nil()) -> nil(),
            droplast(cons(x, nil())) -> nil(),
      droplast(cons(x, cons(y, xs))) -> cons(x, droplast(cons(y, xs))),
                         last(nil()) -> error(),
                last(cons(x, nil())) -> x,
          last(cons(x, cons(y, xs))) -> last(cons(y, xs)),
                                 a() -> b(),
                                 a() -> c()}
     SPSC:
      Simple Projection:
       pi(last#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {droplast#(cons(x, cons(y, xs))) -> droplast#(cons(y, xs))}
     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,
                     mapIter(xs, ys) -> ifmap(isempty(xs), xs, ys),
                          maplog(xs) -> mapIter(xs, nil()),
              ifmap(false(), xs, ys) -> mapIter(droplast(xs), cons(log(last(xs)), ys)),
               ifmap(true(), xs, ys) -> ys,
                      isempty(nil()) -> true(),
                isempty(cons(x, xs)) -> false(),
                     droplast(nil()) -> nil(),
            droplast(cons(x, nil())) -> nil(),
      droplast(cons(x, cons(y, xs))) -> cons(x, droplast(cons(y, xs))),
                         last(nil()) -> error(),
                last(cons(x, nil())) -> x,
          last(cons(x, cons(y, xs))) -> last(cons(y, xs)),
                                 a() -> b(),
                                 a() -> c()}
     SPSC:
      Simple Projection:
       pi(droplast#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {       mapIter#(xs, ys) -> ifmap#(isempty(xs), xs, ys),
       ifmap#(false(), xs, ys) -> mapIter#(droplast(xs), cons(log(last(xs)), ys))}
     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,
                     mapIter(xs, ys) -> ifmap(isempty(xs), xs, ys),
                          maplog(xs) -> mapIter(xs, nil()),
              ifmap(false(), xs, ys) -> mapIter(droplast(xs), cons(log(last(xs)), ys)),
               ifmap(true(), xs, ys) -> ys,
                      isempty(nil()) -> true(),
                isempty(cons(x, xs)) -> false(),
                     droplast(nil()) -> nil(),
            droplast(cons(x, nil())) -> nil(),
      droplast(cons(x, cons(y, xs))) -> cons(x, droplast(cons(y, xs))),
                         last(nil()) -> error(),
                last(cons(x, nil())) -> x,
          last(cons(x, cons(y, xs))) -> last(cons(y, xs)),
                                 a() -> b(),
                                 a() -> c()}
     Fail
    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,
                     mapIter(xs, ys) -> ifmap(isempty(xs), xs, ys),
                          maplog(xs) -> mapIter(xs, nil()),
              ifmap(false(), xs, ys) -> mapIter(droplast(xs), cons(log(last(xs)), ys)),
               ifmap(true(), xs, ys) -> ys,
                      isempty(nil()) -> true(),
                isempty(cons(x, xs)) -> false(),
                     droplast(nil()) -> nil(),
            droplast(cons(x, nil())) -> nil(),
      droplast(cons(x, cons(y, xs))) -> cons(x, droplast(cons(y, xs))),
                         last(nil()) -> error(),
                last(cons(x, nil())) -> x,
          last(cons(x, cons(y, xs))) -> last(cons(y, xs)),
                                 a() -> b(),
                                 a() -> c()}
     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,
                     mapIter(xs, ys) -> ifmap(isempty(xs), xs, ys),
                          maplog(xs) -> mapIter(xs, nil()),
              ifmap(false(), xs, ys) -> mapIter(droplast(xs), cons(log(last(xs)), ys)),
               ifmap(true(), xs, ys) -> ys,
                      isempty(nil()) -> true(),
                isempty(cons(x, xs)) -> false(),
                     droplast(nil()) -> nil(),
            droplast(cons(x, nil())) -> nil(),
      droplast(cons(x, cons(y, xs))) -> cons(x, droplast(cons(y, xs))),
                         last(nil()) -> error(),
                last(cons(x, nil())) -> x,
          last(cons(x, cons(y, xs))) -> last(cons(y, xs)),
                                 a() -> b(),
                                 a() -> c()}
     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,
                     mapIter(xs, ys) -> ifmap(isempty(xs), xs, ys),
                          maplog(xs) -> mapIter(xs, nil()),
              ifmap(false(), xs, ys) -> mapIter(droplast(xs), cons(log(last(xs)), ys)),
               ifmap(true(), xs, ys) -> ys,
                      isempty(nil()) -> true(),
                isempty(cons(x, xs)) -> false(),
                     droplast(nil()) -> nil(),
            droplast(cons(x, nil())) -> nil(),
      droplast(cons(x, cons(y, xs))) -> cons(x, droplast(cons(y, xs))),
                         last(nil()) -> error(),
                last(cons(x, nil())) -> x,
          last(cons(x, cons(y, xs))) -> last(cons(y, xs)),
                                 a() -> b(),
                                 a() -> c()}
     SPSC:
      Simple Projection:
       pi(le#) = 0
      Strict:
       {}
      Qed