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: u -> a w -> a v -> b w -> b G -> D G -> u DP Processor: DPs: G#() -> u#() TRS: u() -> a() w() -> a() v() -> b() w() -> b() G() -> D() G() -> u() TDG Processor: DPs: G#() -> u#() TRS: u() -> a() w() -> a() v() -> b() w() -> b() G() -> D() G() -> u() graph: Qed