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