YES ---- CR(R) ---- Rule Labeling [van Oostrom, RTA 2008]. R: f(f(a())) -> f(f(f(a()))) f(f(a())) -> f(a()) Label: [f(f(a())) -> f(f(f(a())))] = 1 [f(f(a())) -> f(a())] = 0