MAYBE 0.08/0.19 MAYBE 0.08/0.19 0.08/0.19 Problem: 0.08/0.19 prod(xs) -> prodIter(xs,s(0())) 0.08/0.19 prodIter(xs,x) -> ifProd(isempty(xs),xs,x) 0.08/0.19 ifProd(true(),xs,x) -> x 0.08/0.19 ifProd(false(),xs,x) -> prodIter(tail(xs),times(x,head(xs))) 0.08/0.19 plus(0(),y) -> y 0.08/0.19 plus(s(x),y) -> s(plus(x,y)) 0.08/0.19 times(x,y) -> timesIter(x,y,0(),0()) 0.08/0.19 timesIter(x,y,z,u) -> ifTimes(ge(u,x),x,y,z,u) 0.08/0.19 ifTimes(true(),x,y,z,u) -> z 0.08/0.19 ifTimes(false(),x,y,z,u) -> timesIter(x,y,plus(y,z),s(u)) 0.08/0.19 isempty(nil()) -> true() 0.08/0.19 isempty(cons(x,xs)) -> false() 0.08/0.19 head(nil()) -> error() 0.08/0.19 head(cons(x,xs)) -> x 0.08/0.19 tail(nil()) -> nil() 0.08/0.19 tail(cons(x,xs)) -> xs 0.08/0.19 ge(x,0()) -> true() 0.08/0.19 ge(0(),s(y)) -> false() 0.08/0.19 ge(s(x),s(y)) -> ge(x,y) 0.08/0.19 a() -> b() 0.08/0.19 a() -> c() 0.08/0.19 0.08/0.19 Proof: 0.08/0.19 Open 0.08/0.19 EOF