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

The program

(COMMENT 

  Claude Marché

  Sum and product of a list of integers

  Peano notation

)

(VAR l  y  x)
(RULES

+(x,0) -> x 
+(0,x) -> x 
+(s(x),s(y)) -> s(s(+(x,y))) 
*(x,0) -> 0 
*(0,x) -> 0 
*(s(x),s(y)) -> s(+(*(x,y),+(x,y))) 
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