TRS:
 {              plus(x, y) -> plusIter(x, y, 0()),
         plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z),
   ifPlus(true(), x, y, z) -> y,
  ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)),
             le(s(x), 0()) -> false(),
                le(0(), y) -> true(),
            le(s(x), s(y)) -> le(x, y),
                   sum(xs) -> sumIter(xs, 0()),
            sumIter(xs, x) -> ifSum(isempty(xs), xs, x, plus(x, head(xs))),
   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