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