NO
Rewrite Rules:
   [ mirror(leaf(?x)) -> leaf(?x),
     mirror(node(?x,?yt,?zt)) -> node(?x,mirror(?zt),mirror(?yt)),
     sum(leaf(?x)) -> ?x,
     sum(node(?x,?yt,?zt)) -> +(sum(?yt),sum(?zt)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     sum(mirror(?xt)) -> sum(?xt) ]
Apply Direct Methods...
Inner CPs:
   [ sum(leaf(?x)) = sum(leaf(?x)),
     sum(node(?x_1,mirror(?zt_1),mirror(?yt_1))) = sum(node(?x_1,?yt_1,?zt_1)) ]
Outer CPs:
   [  ]
not Overlay, check Termination...
Terminating, not WCR
Knuth & Bendix
Direct Methods: not CR

Final result: not CR
new/mirror.trs: Success(not CR)
(17 msec.)