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