(VAR l l1 l2 x y z )
(RULES 
        0(#) -> #
        +(x, #) -> x
        +(#, x) -> x
        +(0(x), 0(y)) -> 0(+(x, y))
        +(0(x), 1(y)) -> 1(+(x, y))
        +(1(x), 0(y)) -> 1(+(x, y))
        +(1(x), 1(y)) -> 0(+(+(x, y), 1(#)))
        +(+(x, y), z) -> +(x, +(y, z))
        *(#, x) -> #
        *(0(x), y) -> 0(*(x, y))
        *(1(x), y) -> +(0(*(x, y)), y)
        *(*(x, y), z) -> *(x, *(y, z))
        *(x, +(y, z)) -> +(*(x, y), *(x, 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) -> 1(#)
        prod(cons(x, l)) -> *(x, prod(l))
        prod(app(l1, l2)) -> *(prod(l1), prod(l2))
        
)