YES
exiting with thread!
(VAR x y z )
(RULES 
        +(+(x,y),z) -> +(x,+(y,z))
        +(x,0) -> x
        *(*(x,y),z) -> *(x,*(y,z))
        *(x,1) -> x
        exp(0) -> 1
        exp(+(x,y)) -> *(exp(x),exp(y))
        +(x,+(0,z)) -> +(x,z)
        *(x,*(1,z)) -> *(x,z)
        
)