(COMMENT variant of AG01 3.17, prod([x,..,z]) = x*...*z ) (VAR k l x y b) (RULES car(cons(x,l)) -> x cddr(nil) -> nil cddr(cons(x,nil)) -> nil cddr(cons(x,cons(y,l))) -> l cadr(cons(x,cons(y,l))) -> y isZero(0) -> true isZero(s(x)) -> false plus(x,y) -> ifplus(isZero(x),x,y) ifplus(true,x,y) -> y ifplus(false,x,y) -> s(plus(p(x),y)) times(x,y) -> iftimes(isZero(x),x,y) iftimes(true,x,y) -> 0 iftimes(false,x,y) -> plus(y,times(p(x),y)) p(s(x)) -> x p(0) -> 0 shorter(nil,y) -> true shorter(cons(x,l),0) -> false shorter(cons(x,l),s(y)) -> shorter(l,y) prod(l) -> if(shorter(l,0),shorter(l,s(0)),l) if(true,b,l) -> s(0) if(false,b,l) -> if2(b,l) if2(true,l) -> car(l) if2(false,l) -> prod(cons(times(car(l),cadr(l)),cddr(l))) )