YES

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

C:


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