YES # orthogonality Consider the left-linear TRS R: b() -> c() a() -> a() The left-linear and non-overlapping TRS is confluent