MAYBE
Time: 0.010308
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:
  DP:
   {                 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)}
  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()}
  UR:
   {                 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,
                    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),
                          d(w, v) -> w,
                          d(w, v) -> v}
   EDG:
    {(ifmap#(false(), xs, ys) -> log# last xs, log# s x -> loop#(s x, s 0(), 0()))
     (maplog# xs -> mapIter#(xs, nil()), mapIter#(xs, ys) -> isempty# xs)
     (maplog# xs -> mapIter#(xs, nil()), mapIter#(xs, ys) -> ifmap#(isempty xs, xs, ys))
     (last# cons(x, cons(y, xs)) -> last# cons(y, xs), last# cons(x, cons(y, xs)) -> last# cons(y, xs))
     (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))
     (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))
     (ifmap#(false(), xs, ys) -> mapIter#(droplast xs, cons(log last xs, ys)), mapIter#(xs, ys) -> isempty# 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) -> last# xs, last# cons(x, cons(y, xs)) -> last# cons(y, xs))
     (ifmap#(false(), xs, ys) -> droplast# xs, droplast# cons(x, cons(y, xs)) -> droplast# cons(y, xs))
     (mapIter#(xs, ys) -> ifmap#(isempty xs, xs, ys), ifmap#(false(), xs, ys) -> log# last 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) -> droplast# xs)
     (mapIter#(xs, ys) -> ifmap#(isempty xs, xs, ys), ifmap#(false(), xs, ys) -> last# xs)
     (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))
     (loop#(x, s y, z) -> le#(x, s y), le#(s x, s y) -> le#(x, y))
     (if#(false(), x, y, z) -> double# y, double# s x -> double# x)
     (droplast# cons(x, cons(y, xs)) -> droplast# cons(y, xs), droplast# cons(x, cons(y, xs)) -> droplast# cons(y, xs))
     (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
     (double# s x -> double# x, double# s x -> double# x)}
    STATUS:
     arrows: 0.910156
     SCCS (6):
      Scc:
       {       mapIter#(xs, ys) -> ifmap#(isempty xs, xs, ys),
        ifmap#(false(), xs, ys) -> mapIter#(droplast xs, cons(log last xs, ys))}
      Scc:
       {last# cons(x, cons(y, xs)) -> last# cons(y, xs)}
      Scc:
       {droplast# cons(x, cons(y, xs)) -> droplast# cons(y, xs)}
      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:
       {le#(s x, s y) -> le#(x, y)}
      Scc:
       {double# s x -> double# x}
      
      
      SCC (2):
       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()}
       Open
      
      SCC (1):
       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()}
       Open
      
      SCC (1):
       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()}
       Open
      
      
      
      SCC (2):
       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()}
       Open
      
      
      SCC (1):
       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()}
       Open
      SCC (1):
       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()}
       Open