YES # Parallel rule labeling (Zankl et al. 2015). Consider the left-linear TRS R: +(0(),y) -> y +(s(0()),y) -> s(y) +(s(s(x)),y) -> s(s(+(y,x))) All parallel critical peaks (except C's) are decreasing wrt rule labeling: phi(+(0(),y) -> y) = 1 phi(+(s(0()),y) -> s(y)) = 1 phi(+(s(s(x)),y) -> s(s(+(y,x)))) = 1 psi(+(0(),y) -> y) = 1 psi(+(s(0()),y) -> s(y)) = 1 psi(+(s(s(x)),y) -> s(s(+(y,x)))) = 1