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()}
 DP:
  Strict:
   {       plusIter#(x, y, z) -> ifPlus#(le(x, z), x, y, z),
           plusIter#(x, y, z) -> le#(x, z),
                  plus#(x, y) -> plusIter#(x, y, 0()),
    ifPlus#(false(), x, y, z) -> plusIter#(x, s(y), s(z)),
              le#(s(x), s(y)) -> le#(x, y),
              sumIter#(xs, x) -> plus#(x, head(xs)),
              sumIter#(xs, x) -> ifSum#(isempty(xs), xs, x, plus(x, head(xs))),
              sumIter#(xs, x) -> isempty#(xs),
              sumIter#(xs, x) -> head#(xs),
                     sum#(xs) -> sumIter#(xs, 0()),
    ifSum#(false(), xs, x, y) -> sumIter#(tail(xs), y),
    ifSum#(false(), xs, x, y) -> tail#(xs)}
  Weak:
  {       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()}
  EDG:
   {(sumIter#(xs, x) -> ifSum#(isempty(xs), xs, x, plus(x, head(xs))), ifSum#(false(), xs, x, y) -> tail#(xs))
    (sumIter#(xs, x) -> ifSum#(isempty(xs), xs, x, plus(x, head(xs))), ifSum#(false(), xs, x, y) -> sumIter#(tail(xs), y))
    (plusIter#(x, y, z) -> ifPlus#(le(x, z), x, y, z), ifPlus#(false(), x, y, z) -> plusIter#(x, s(y), s(z)))
    (plus#(x, y) -> plusIter#(x, y, 0()), plusIter#(x, y, z) -> le#(x, z))
    (plus#(x, y) -> plusIter#(x, y, 0()), plusIter#(x, y, z) -> ifPlus#(le(x, z), x, y, z))
    (le#(s(x), s(y)) -> le#(x, y), le#(s(x), s(y)) -> le#(x, y))
    (ifSum#(false(), xs, x, y) -> sumIter#(tail(xs), y), sumIter#(xs, x) -> head#(xs))
    (ifSum#(false(), xs, x, y) -> sumIter#(tail(xs), y), sumIter#(xs, x) -> isempty#(xs))
    (ifSum#(false(), xs, x, y) -> sumIter#(tail(xs), y), sumIter#(xs, x) -> ifSum#(isempty(xs), xs, x, plus(x, head(xs))))
    (ifSum#(false(), xs, x, y) -> sumIter#(tail(xs), y), sumIter#(xs, x) -> plus#(x, head(xs)))
    (sum#(xs) -> sumIter#(xs, 0()), sumIter#(xs, x) -> plus#(x, head(xs)))
    (sum#(xs) -> sumIter#(xs, 0()), sumIter#(xs, x) -> ifSum#(isempty(xs), xs, x, plus(x, head(xs))))
    (sum#(xs) -> sumIter#(xs, 0()), sumIter#(xs, x) -> isempty#(xs))
    (sum#(xs) -> sumIter#(xs, 0()), sumIter#(xs, x) -> head#(xs))
    (ifPlus#(false(), x, y, z) -> plusIter#(x, s(y), s(z)), plusIter#(x, y, z) -> ifPlus#(le(x, z), x, y, z))
    (ifPlus#(false(), x, y, z) -> plusIter#(x, s(y), s(z)), plusIter#(x, y, z) -> le#(x, z))
    (plusIter#(x, y, z) -> le#(x, z), le#(s(x), s(y)) -> le#(x, y))
    (sumIter#(xs, x) -> plus#(x, head(xs)), plus#(x, y) -> plusIter#(x, y, 0()))}
   SCCS:
    Scc:
     {          sumIter#(xs, x) -> ifSum#(isempty(xs), xs, x, plus(x, head(xs))),
      ifSum#(false(), xs, x, y) -> sumIter#(tail(xs), y)}
    Scc:
     {le#(s(x), s(y)) -> le#(x, y)}
    Scc:
     {       plusIter#(x, y, z) -> ifPlus#(le(x, z), x, y, z),
      ifPlus#(false(), x, y, z) -> plusIter#(x, s(y), s(z))}
    SCC:
     Strict:
      {          sumIter#(xs, x) -> ifSum#(isempty(xs), xs, x, plus(x, head(xs))),
       ifSum#(false(), xs, x, y) -> sumIter#(tail(xs), y)}
     Weak:
     {       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
    SCC:
     Strict:
      {le#(s(x), s(y)) -> le#(x, y)}
     Weak:
     {       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()}
     SPSC:
      Simple Projection:
       pi(le#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {       plusIter#(x, y, z) -> ifPlus#(le(x, z), x, y, z),
       ifPlus#(false(), x, y, z) -> plusIter#(x, s(y), s(z))}
     Weak:
     {       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