YES
exiting with thread!
(VAR x y z )
(RULES 
        +(+(x,y),z) -> +(x,+(y,z))
        f(+(x,y)) -> +(f(x),f(y))
        
)