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