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