YES # Parallel rule labeling (Zankl et al. 2015). Consider the left-linear TRS R: a(c(x)) -> b(a(x)) a(c(x)) -> a(c(x)) a(a(x)) -> a(b(x)) b(b(x)) -> a(c(x)) c(c(x)) -> c(a(x)) c(b(x)) -> a(c(x)) a(b(x)) -> a(c(x)) a(c(x)) -> a(c(x)) All parallel critical peaks (except C's) are decreasing wrt rule labeling: phi(a(c(x)) -> b(a(x))) = 4 phi(a(c(x)) -> a(c(x))) = 1 phi(a(a(x)) -> a(b(x))) = 3 phi(b(b(x)) -> a(c(x))) = 7 phi(c(c(x)) -> c(a(x))) = 9 phi(c(b(x)) -> a(c(x))) = 10 phi(a(b(x)) -> a(c(x))) = 1 phi(a(c(x)) -> a(c(x))) = 0 psi(a(c(x)) -> b(a(x))) = 6 psi(a(c(x)) -> a(c(x))) = 1 psi(a(a(x)) -> a(b(x))) = 8 psi(b(b(x)) -> a(c(x))) = 11 psi(c(c(x)) -> c(a(x))) = 2 psi(c(b(x)) -> a(c(x))) = 5 psi(a(b(x)) -> a(c(x))) = 6 psi(a(c(x)) -> a(c(x))) = 0