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