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