(VAR l l1 l2 x y z )
(STRATEGY INNERMOST)
(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))
        
)