MAYBE
MAYBE
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()
 }
 DUP: We consider a duplicating system.
  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()
   }
  Fail