YES # Parallel rule labeling (Zankl et al. 2015). Consider the left-linear TRS 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()) All parallel critical peaks (except C's) are decreasing wrt rule labeling: phi(a() -> c()) = 2 phi(b() -> c()) = 3 phi(f(a(),b()) -> d()) = 5 phi(f(x,c()) -> f(c(),c())) = 1 phi(f(c(),x) -> f(c(),c())) = 2 phi(d() -> f(a(),c())) = 5 phi(d() -> f(c(),b())) = 5 psi(a() -> c()) = 4 psi(b() -> c()) = 4 psi(f(a(),b()) -> d()) = 6 psi(f(x,c()) -> f(c(),c())) = 1 psi(f(c(),x) -> f(c(),c())) = 1 psi(d() -> f(a(),c())) = 4 psi(d() -> f(c(),b())) = 4