YES # orthogonality Consider the left-linear TRS R: F(x,y) -> c(A()) G(x) -> x h(x) -> c(x) The left-linear and non-overlapping TRS is confluent