(COMMENT 

  Claude Marché

  Sum and product of a list of integers, with append

  Peano notation, + and * are associative

)

(VAR l2  l1  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)) 
app(nil,l) -> l 
app(cons(x,l1),l2) -> cons(x,app(l1,l2)) 
sum(nil) -> 0 
sum(cons(x,l)) -> +(x,sum(l)) 
sum(app(l1,l2)) -> +(sum(l1),sum(l2)) 
prod(nil) -> s(0) 
prod(cons(x,l)) -> *(x,prod(l)) 
prod(app(l1,l2)) -> *(prod(l1),prod(l2)) 
)