(COMMENT Claude Marché Sum and product of a list of integers Binary notation ) (VAR l y x) (RULES 0(#) -> # +(x,#) -> x +(#,x) -> x +(0(x),0(y)) -> 0(+(x,y)) +(0(x),1(y)) -> 1(+(x,y)) +(1(x),0(y)) -> 1(+(x,y)) +(1(x),1(y)) -> 0(+(+(x,y),1(#))) *(#,x) -> # *(0(x),y) -> 0(*(x,y)) *(1(x),y) -> +(0(*(x,y)),y) sum(nil) -> 0(#) sum(cons(x,l)) -> +(x,sum(l)) prod(nil) -> 1(#) prod(cons(x,l)) -> *(x,prod(l)) )