YES ---- CR(R) ---- Hot decreasingness. R: +(x,y) -> +(y,x) C: Label: [+(x,y) -> +(y,x)] = 0