(VAR l x y ) (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)) )