YES ---- CR(R) ---- Hot decreasingness. R: g(f(a())) -> f(g(f(a()))) g(f(a())) -> f(f(a())) f(f(a())) -> f(a()) C: g(f(a())) -> f(f(a())) f(f(a())) -> f(a()) Label: [g(f(a())) -> f(g(f(a())))] = 0