MAYBE
Time: 0.005391
TRS:
 {             prodIter(xs, x) -> ifProd(isempty xs, xs, x),
                       prod xs -> prodIter(xs, s 0()),
         ifProd(true(), xs, x) -> x,
        ifProd(false(), xs, x) -> prodIter(tail xs, times(x, head xs)),
                 isempty nil() -> true(),
           isempty cons(x, xs) -> false(),
                    tail nil() -> nil(),
              tail cons(x, xs) -> xs,
                   times(x, y) -> timesIter(x, y, 0(), 0()),
                    head nil() -> error(),
              head cons(x, xs) -> x,
                  plus(s x, y) -> s plus(x, y),
                  plus(0(), y) -> y,
         timesIter(x, y, z, u) -> ifTimes(ge(u, x), x, y, z, u),
   ifTimes(true(), x, y, z, u) -> z,
  ifTimes(false(), x, y, z, u) -> timesIter(x, y, plus(y, z), s u),
                    ge(x, 0()) -> true(),
                  ge(s x, s y) -> ge(x, y),
                  ge(0(), s y) -> false(),
                           a() -> b(),
                           a() -> c()}
 DP:
  DP:
   {             prodIter#(xs, x) -> ifProd#(isempty xs, xs, x),
                 prodIter#(xs, x) -> isempty# xs,
                         prod# xs -> prodIter#(xs, s 0()),
          ifProd#(false(), xs, x) -> prodIter#(tail xs, times(x, head xs)),
          ifProd#(false(), xs, x) -> tail# xs,
          ifProd#(false(), xs, x) -> times#(x, head xs),
          ifProd#(false(), xs, x) -> head# xs,
                     times#(x, y) -> timesIter#(x, y, 0(), 0()),
                    plus#(s x, y) -> plus#(x, y),
           timesIter#(x, y, z, u) -> ifTimes#(ge(u, x), x, y, z, u),
           timesIter#(x, y, z, u) -> ge#(u, x),
    ifTimes#(false(), x, y, z, u) -> plus#(y, z),
    ifTimes#(false(), x, y, z, u) -> timesIter#(x, y, plus(y, z), s u),
                    ge#(s x, s y) -> ge#(x, y)}
  TRS:
  {             prodIter(xs, x) -> ifProd(isempty xs, xs, x),
                        prod xs -> prodIter(xs, s 0()),
          ifProd(true(), xs, x) -> x,
         ifProd(false(), xs, x) -> prodIter(tail xs, times(x, head xs)),
                  isempty nil() -> true(),
            isempty cons(x, xs) -> false(),
                     tail nil() -> nil(),
               tail cons(x, xs) -> xs,
                    times(x, y) -> timesIter(x, y, 0(), 0()),
                     head nil() -> error(),
               head cons(x, xs) -> x,
                   plus(s x, y) -> s plus(x, y),
                   plus(0(), y) -> y,
          timesIter(x, y, z, u) -> ifTimes(ge(u, x), x, y, z, u),
    ifTimes(true(), x, y, z, u) -> z,
   ifTimes(false(), x, y, z, u) -> timesIter(x, y, plus(y, z), s u),
                     ge(x, 0()) -> true(),
                   ge(s x, s y) -> ge(x, y),
                   ge(0(), s y) -> false(),
                            a() -> b(),
                            a() -> c()}
  EDG:
   {(timesIter#(x, y, z, u) -> ifTimes#(ge(u, x), x, y, z, u), ifTimes#(false(), x, y, z, u) -> timesIter#(x, y, plus(y, z), s u))
    (timesIter#(x, y, z, u) -> ifTimes#(ge(u, x), x, y, z, u), ifTimes#(false(), x, y, z, u) -> plus#(y, z))
    (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
    (ifProd#(false(), xs, x) -> prodIter#(tail xs, times(x, head xs)), prodIter#(xs, x) -> isempty# xs)
    (ifProd#(false(), xs, x) -> prodIter#(tail xs, times(x, head xs)), prodIter#(xs, x) -> ifProd#(isempty xs, xs, x))
    (ifProd#(false(), xs, x) -> times#(x, head xs), times#(x, y) -> timesIter#(x, y, 0(), 0()))
    (ifTimes#(false(), x, y, z, u) -> timesIter#(x, y, plus(y, z), s u), timesIter#(x, y, z, u) -> ge#(u, x))
    (ifTimes#(false(), x, y, z, u) -> timesIter#(x, y, plus(y, z), s u), timesIter#(x, y, z, u) -> ifTimes#(ge(u, x), x, y, z, u))
    (prodIter#(xs, x) -> ifProd#(isempty xs, xs, x), ifProd#(false(), xs, x) -> prodIter#(tail xs, times(x, head xs)))
    (prodIter#(xs, x) -> ifProd#(isempty xs, xs, x), ifProd#(false(), xs, x) -> tail# xs)
    (prodIter#(xs, x) -> ifProd#(isempty xs, xs, x), ifProd#(false(), xs, x) -> times#(x, head xs))
    (prodIter#(xs, x) -> ifProd#(isempty xs, xs, x), ifProd#(false(), xs, x) -> head# xs)
    (times#(x, y) -> timesIter#(x, y, 0(), 0()), timesIter#(x, y, z, u) -> ifTimes#(ge(u, x), x, y, z, u))
    (times#(x, y) -> timesIter#(x, y, 0(), 0()), timesIter#(x, y, z, u) -> ge#(u, x))
    (ifTimes#(false(), x, y, z, u) -> plus#(y, z), plus#(s x, y) -> plus#(x, y))
    (ge#(s x, s y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y))
    (timesIter#(x, y, z, u) -> ge#(u, x), ge#(s x, s y) -> ge#(x, y))
    (prod# xs -> prodIter#(xs, s 0()), prodIter#(xs, x) -> ifProd#(isempty xs, xs, x))
    (prod# xs -> prodIter#(xs, s 0()), prodIter#(xs, x) -> isempty# xs)}
   STATUS:
    arrows: 0.903061
    SCCS (4):
     Scc:
      {       prodIter#(xs, x) -> ifProd#(isempty xs, xs, x),
       ifProd#(false(), xs, x) -> prodIter#(tail xs, times(x, head xs))}
     Scc:
      {       timesIter#(x, y, z, u) -> ifTimes#(ge(u, x), x, y, z, u),
       ifTimes#(false(), x, y, z, u) -> timesIter#(x, y, plus(y, z), s u)}
     Scc:
      {ge#(s x, s y) -> ge#(x, y)}
     Scc:
      {plus#(s x, y) -> plus#(x, y)}
     
     
     SCC (2):
      Strict:
       {       prodIter#(xs, x) -> ifProd#(isempty xs, xs, x),
        ifProd#(false(), xs, x) -> prodIter#(tail xs, times(x, head xs))}
      Weak:
      {             prodIter(xs, x) -> ifProd(isempty xs, xs, x),
                            prod xs -> prodIter(xs, s 0()),
              ifProd(true(), xs, x) -> x,
             ifProd(false(), xs, x) -> prodIter(tail xs, times(x, head xs)),
                      isempty nil() -> true(),
                isempty cons(x, xs) -> false(),
                         tail nil() -> nil(),
                   tail cons(x, xs) -> xs,
                        times(x, y) -> timesIter(x, y, 0(), 0()),
                         head nil() -> error(),
                   head cons(x, xs) -> x,
                       plus(s x, y) -> s plus(x, y),
                       plus(0(), y) -> y,
              timesIter(x, y, z, u) -> ifTimes(ge(u, x), x, y, z, u),
        ifTimes(true(), x, y, z, u) -> z,
       ifTimes(false(), x, y, z, u) -> timesIter(x, y, plus(y, z), s u),
                         ge(x, 0()) -> true(),
                       ge(s x, s y) -> ge(x, y),
                       ge(0(), s y) -> false(),
                                a() -> b(),
                                a() -> c()}
      Open
     
     
     
     SCC (2):
      Strict:
       {       timesIter#(x, y, z, u) -> ifTimes#(ge(u, x), x, y, z, u),
        ifTimes#(false(), x, y, z, u) -> timesIter#(x, y, plus(y, z), s u)}
      Weak:
      {             prodIter(xs, x) -> ifProd(isempty xs, xs, x),
                            prod xs -> prodIter(xs, s 0()),
              ifProd(true(), xs, x) -> x,
             ifProd(false(), xs, x) -> prodIter(tail xs, times(x, head xs)),
                      isempty nil() -> true(),
                isempty cons(x, xs) -> false(),
                         tail nil() -> nil(),
                   tail cons(x, xs) -> xs,
                        times(x, y) -> timesIter(x, y, 0(), 0()),
                         head nil() -> error(),
                   head cons(x, xs) -> x,
                       plus(s x, y) -> s plus(x, y),
                       plus(0(), y) -> y,
              timesIter(x, y, z, u) -> ifTimes(ge(u, x), x, y, z, u),
        ifTimes(true(), x, y, z, u) -> z,
       ifTimes(false(), x, y, z, u) -> timesIter(x, y, plus(y, z), s u),
                         ge(x, 0()) -> true(),
                       ge(s x, s y) -> ge(x, y),
                       ge(0(), s y) -> false(),
                                a() -> b(),
                                a() -> c()}
      Open
     
     SCC (1):
      Strict:
       {ge#(s x, s y) -> ge#(x, y)}
      Weak:
      {             prodIter(xs, x) -> ifProd(isempty xs, xs, x),
                            prod xs -> prodIter(xs, s 0()),
              ifProd(true(), xs, x) -> x,
             ifProd(false(), xs, x) -> prodIter(tail xs, times(x, head xs)),
                      isempty nil() -> true(),
                isempty cons(x, xs) -> false(),
                         tail nil() -> nil(),
                   tail cons(x, xs) -> xs,
                        times(x, y) -> timesIter(x, y, 0(), 0()),
                         head nil() -> error(),
                   head cons(x, xs) -> x,
                       plus(s x, y) -> s plus(x, y),
                       plus(0(), y) -> y,
              timesIter(x, y, z, u) -> ifTimes(ge(u, x), x, y, z, u),
        ifTimes(true(), x, y, z, u) -> z,
       ifTimes(false(), x, y, z, u) -> timesIter(x, y, plus(y, z), s u),
                         ge(x, 0()) -> true(),
                       ge(s x, s y) -> ge(x, y),
                       ge(0(), s y) -> false(),
                                a() -> b(),
                                a() -> c()}
      Open
     
     SCC (1):
      Strict:
       {plus#(s x, y) -> plus#(x, y)}
      Weak:
      {             prodIter(xs, x) -> ifProd(isempty xs, xs, x),
                            prod xs -> prodIter(xs, s 0()),
              ifProd(true(), xs, x) -> x,
             ifProd(false(), xs, x) -> prodIter(tail xs, times(x, head xs)),
                      isempty nil() -> true(),
                isempty cons(x, xs) -> false(),
                         tail nil() -> nil(),
                   tail cons(x, xs) -> xs,
                        times(x, y) -> timesIter(x, y, 0(), 0()),
                         head nil() -> error(),
                   head cons(x, xs) -> x,
                       plus(s x, y) -> s plus(x, y),
                       plus(0(), y) -> y,
              timesIter(x, y, z, u) -> ifTimes(ge(u, x), x, y, z, u),
        ifTimes(true(), x, y, z, u) -> z,
       ifTimes(false(), x, y, z, u) -> timesIter(x, y, plus(y, z), s u),
                         ge(x, 0()) -> true(),
                       ge(s x, s y) -> ge(x, y),
                       ge(0(), s y) -> false(),
                                a() -> b(),
                                a() -> c()}
      Open