(COMMENT Claude Marché Sum and product of a list of integers Peano notation, + and * are associative ) (VAR l z y x) (RULES +(x,0) -> x +(0,x) -> x +(s(x),s(y)) -> s(s(+(x,y))) +(+(x,y),z) -> +(x,+(y,z)) *(x,0) -> 0 *(0,x) -> 0 *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) *(*(x,y),z) -> *(x,*(y,z)) sum(nil) -> 0 sum(cons(x,l)) -> +(x,sum(l)) prod(nil) -> s(0) prod(cons(x,l)) -> *(x,prod(l)) )