MAYBE
MAYBE
TRS:
 {
         plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z),
                plus(x, y) -> plusIter(x, y, 0()),
   ifPlus(true(), x, y, z) -> y,
  ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)),
                le(0(), y) -> true(),
             le(s(x), 0()) -> false(),
            le(s(x), s(y)) -> le(x, y),
            sumIter(xs, x) -> ifSum(isempty(xs), xs, x, plus(x, head(xs))),
                   sum(xs) -> sumIter(xs, 0()),
   ifSum(true(), xs, x, y) -> x,
  ifSum(false(), xs, x, y) -> sumIter(tail(xs), y),
            isempty(nil()) -> true(),
      isempty(cons(x, xs)) -> false(),
               head(nil()) -> error(),
         head(cons(x, xs)) -> x,
               tail(nil()) -> nil(),
         tail(cons(x, xs)) -> xs,
                       a() -> b(),
                       a() -> c()
 }
 DUP: We consider a duplicating system.
  Trs:
   {
           plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z),
                  plus(x, y) -> plusIter(x, y, 0()),
     ifPlus(true(), x, y, z) -> y,
    ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)),
                  le(0(), y) -> true(),
               le(s(x), 0()) -> false(),
              le(s(x), s(y)) -> le(x, y),
              sumIter(xs, x) -> ifSum(isempty(xs), xs, x, plus(x, head(xs))),
                     sum(xs) -> sumIter(xs, 0()),
     ifSum(true(), xs, x, y) -> x,
    ifSum(false(), xs, x, y) -> sumIter(tail(xs), y),
              isempty(nil()) -> true(),
        isempty(cons(x, xs)) -> false(),
                 head(nil()) -> error(),
           head(cons(x, xs)) -> x,
                 tail(nil()) -> nil(),
           tail(cons(x, xs)) -> xs,
                         a() -> b(),
                         a() -> c()
   }
  Fail