YES Proof: This system is confluent. By \cite{ALS94}, Theorem 4.1. This system is of type 3 or smaller. This system is strongly deterministic. There are no critical pairs. By \cite{A14}, Theorem 11.5.9. This system is of type 3 or smaller. This system is deterministic. System R transformed to V(R) + Emb. Call external tool: ttt2 - trs 30 Input: a -> c b -> c f(x) -> x f(x) -> a f(x) -> x DP Processor: DPs: f#(x) -> a#() TRS: a() -> c() b() -> c() f(x) -> x f(x) -> a() TDG Processor: DPs: f#(x) -> a#() TRS: a() -> c() b() -> c() f(x) -> x f(x) -> a() graph: Qed This system is deterministic. This system is not weakly left-linear. This system is not normal. This system is oriented. This system is of type 3 or smaller. This system is not right-stable. This system is conditional.