/home/nowonder/forschung/aprove/TPDB05/TRS/Cime/list-sum-prod-assoc.trs

The program

(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)) 

)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend