YES Proof: This system is quasi-decreasing. By \cite{O02}, p. 214, Proposition 7.2.50. This system is of type 3 or smaller. This system is deterministic. System R transformed to U(R). Call external tool: ttt2 - trs 30 Input: u -> a w -> a v -> b w -> b ?1(v) -> D G -> ?1(u) DP Processor: DPs: G#() -> u#() G#() -> ?1#(u()) TRS: u() -> a() w() -> a() v() -> b() w() -> b() ?1(v()) -> D() G() -> ?1(u()) TDG Processor: DPs: G#() -> u#() G#() -> ?1#(u()) TRS: u() -> a() w() -> a() v() -> b() w() -> b() ?1(v()) -> D() G() -> ?1(u()) graph: Qed