MAYBE
Time: 0.004134
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:
  DP:
   {       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}
  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()}
  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))
    (ifPlus#(false(), x, y, z) -> plusIter#(x, s y, s z), plusIter#(x, y, z) -> le#(x, z))
    (ifPlus#(false(), x, y, z) -> plusIter#(x, s y, s z), plusIter#(x, y, z) -> ifPlus#(le(x, z), x, y, z))
    (ifSum#(false(), xs, x, y) -> sumIter#(tail xs, y), sumIter#(xs, x) -> plus#(x, head 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) -> isempty# xs)
    (ifSum#(false(), xs, x, y) -> sumIter#(tail xs, y), sumIter#(xs, x) -> head# xs)
    (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
    (plusIter#(x, y, z) -> le#(x, z), le#(s x, s y) -> le#(x, y))
    (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)
    (sumIter#(xs, x) -> plus#(x, head xs), plus#(x, y) -> plusIter#(x, y, 0()))}
   STATUS:
    arrows: 0.875000
    SCCS (3):
     Scc:
      {          sumIter#(xs, x) -> ifSum#(isempty xs, xs, x, plus(x, head xs)),
       ifSum#(false(), xs, x, y) -> sumIter#(tail xs, 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:
      {le#(s x, s y) -> le#(x, y)}
     
     
     SCC (2):
      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()}
      Open
     
     
     
     
     
     SCC (2):
      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()}
      Open
     
     SCC (1):
      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()}
      Open