YES

---- CR(R)
---- Hot decreasingness.
R:
f(a()) -> f(f(a()))
f(x) -> f(a())

C:


Label:
[f(a()) -> f(f(a()))] = 0
[f(x) -> f(a())] = 0