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