YES Proof: This system is quasi-decreasing. 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: F(x, y) -> G(x) F(x, y) -> x a -> b G(x) -> x F(x, y) -> x F(x, y) -> y DP Processor: DPs: F#(x,y) -> G#(x) TRS: F(x,y) -> G(x) F(x,y) -> x a() -> b() G(x) -> x F(x,y) -> y TDG Processor: DPs: F#(x,y) -> G#(x) TRS: F(x,y) -> G(x) F(x,y) -> x a() -> b() G(x) -> x F(x,y) -> y graph: Qed