YES # parallel critical pair closing system (Shintani and Hirokawa 2022) Consider the left-linear TRS R: nats() -> :(0(),inc(nats())) inc(:(x,y)) -> :(s(x),inc(y)) inc(tl(nats())) -> tl(inc(nats())) hd(:(x,y)) -> x tl(:(x,y)) -> y d(:(x,y)) -> :(x,:(x,d(y))) Let C be the following subset of R: 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 follows from that of C. # parallel critical pair closing system (Shintani and Hirokawa 2022) Consider the left-linear TRS R: 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 TRS R is left-linear and all parallel critical pairs are joinable by C. Therefore, the confluence of R follows from that of C. # emptiness The empty TRS is confluent.