MAYBE 0.07/0.18 MAYBE 0.07/0.18 0.07/0.18 Problem: 0.07/0.18 plus(x,y) -> plusIter(x,y,0()) 0.07/0.18 plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z) 0.07/0.18 ifPlus(true(),x,y,z) -> y 0.07/0.18 ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z)) 0.07/0.18 le(s(x),0()) -> false() 0.07/0.18 le(0(),y) -> true() 0.07/0.18 le(s(x),s(y)) -> le(x,y) 0.07/0.18 sum(xs) -> sumIter(xs,0()) 0.07/0.18 sumIter(xs,x) -> ifSum(isempty(xs),xs,x,plus(x,head(xs))) 0.07/0.18 ifSum(true(),xs,x,y) -> x 0.07/0.18 ifSum(false(),xs,x,y) -> sumIter(tail(xs),y) 0.07/0.18 isempty(nil()) -> true() 0.07/0.18 isempty(cons(x,xs)) -> false() 0.07/0.18 head(nil()) -> error() 0.07/0.18 head(cons(x,xs)) -> x 0.07/0.18 tail(nil()) -> nil() 0.07/0.18 tail(cons(x,xs)) -> xs 0.07/0.18 a() -> b() 0.07/0.18 a() -> c() 0.07/0.18 0.07/0.18 Proof: 0.07/0.18 Open 0.07/0.19 EOF