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