MAYBE

Problem:
 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()

Proof:
 DP Processor:
  DPs:
   plus#(x,y) -> plusIter#(x,y,0())
   plusIter#(x,y,z) -> le#(x,z)
   plusIter#(x,y,z) -> ifPlus#(le(x,z),x,y,z)
   ifPlus#(false(),x,y,z) -> plusIter#(x,s(y),s(z))
   le#(s(x),s(y)) -> le#(x,y)
   sum#(xs) -> sumIter#(xs,0())
   sumIter#(xs,x) -> head#(xs)
   sumIter#(xs,x) -> plus#(x,head(xs))
   sumIter#(xs,x) -> isempty#(xs)
   sumIter#(xs,x) -> ifSum#(isempty(xs),xs,x,plus(x,head(xs)))
   ifSum#(false(),xs,x,y) -> tail#(xs)
   ifSum#(false(),xs,x,y) -> sumIter#(tail(xs),y)
  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()
  Usable Rule Processor:
   DPs:
    plus#(x,y) -> plusIter#(x,y,0())
    plusIter#(x,y,z) -> le#(x,z)
    plusIter#(x,y,z) -> ifPlus#(le(x,z),x,y,z)
    ifPlus#(false(),x,y,z) -> plusIter#(x,s(y),s(z))
    le#(s(x),s(y)) -> le#(x,y)
    sum#(xs) -> sumIter#(xs,0())
    sumIter#(xs,x) -> head#(xs)
    sumIter#(xs,x) -> plus#(x,head(xs))
    sumIter#(xs,x) -> isempty#(xs)
    sumIter#(xs,x) -> ifSum#(isempty(xs),xs,x,plus(x,head(xs)))
    ifSum#(false(),xs,x,y) -> tail#(xs)
    ifSum#(false(),xs,x,y) -> sumIter#(tail(xs),y)
   TRS:
    le(s(x),0()) -> false()
    le(0(),y) -> true()
    le(s(x),s(y)) -> le(x,y)
    head(nil()) -> error()
    head(cons(x,xs)) -> x
    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))
    isempty(nil()) -> true()
    isempty(cons(x,xs)) -> false()
    tail(nil()) -> nil()
    tail(cons(x,xs)) -> xs
   Open