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