TRS:
 {                    prod(xs) -> prodIter(xs, s(0())),
               prodIter(xs, x) -> ifProd(isempty(xs), xs, x),
         ifProd(true(), xs, x) -> x,
        ifProd(false(), xs, x) -> prodIter(tail(xs), times(x, head(xs))),
                  plus(0(), y) -> y,
                 plus(s(x), y) -> s(plus(x, y)),
                   times(x, y) -> timesIter(x, y, 0(), 0()),
         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)),
                isempty(nil()) -> true(),
          isempty(cons(x, xs)) -> false(),
                   head(nil()) -> error(),
             head(cons(x, xs)) -> x,
                   tail(nil()) -> nil(),
             tail(cons(x, xs)) -> xs,
                    ge(x, 0()) -> true(),
                 ge(0(), s(y)) -> false(),
                ge(s(x), s(y)) -> ge(x, y),
                           a() -> b(),
                           a() -> c()}
 Fail