YES # parallel critical pair closing system (Shintani and Hirokawa 2022, Section 8 in LMCS 2023) Consider the left-linear TRS R: nats() -> :(0(),inc(nats())) inc(:(x,y)) -> :(s(x),inc(y)) hd(:(x,y)) -> x tl(:(x,y)) -> y inc(tl(nats())) -> tl(inc(nats())) Let C be the following subset of R: inc(tl(nats())) -> tl(inc(nats())) nats() -> :(0(),inc(nats())) inc(:(x,y)) -> :(s(x),inc(y)) tl(:(x,y)) -> y The TRS R is left-linear and all parallel critical pairs are joinable by C. Therefore, the confluence of R is equivalent to that of C. # Compositional parallel critical pair system (Shintani and Hirokawa 2022). Consider the left-linear TRS R: inc(tl(nats())) -> tl(inc(nats())) nats() -> :(0(),inc(nats())) inc(:(x,y)) -> :(s(x),inc(y)) tl(:(x,y)) -> y Let C be the following subset of R: (empty) The parallel critical pair system PCPS(R,C) is: inc(tl(nats())) -> inc(tl(:(0(),inc(nats())))) inc(tl(nats())) -> tl(inc(nats())) All pairs in PCP(R) are joinable and PCPS(R,C)/R is terminating. Therefore, the confluence of R follows from that of C. # emptiness The empty TRS is confluent.