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: a -> c a -> d b -> c b -> d c -> e c -> k d -> k ?1(e, x) -> x f(x) -> ?1(x, x) ?2(B, x) -> C g(x, x) -> ?2(A, x) h(x) -> i(x, x) DP Processor: DPs: a#() -> c#() a#() -> d#() b#() -> c#() b#() -> d#() f#(x) -> ?1#(x,x) g#(x,x) -> ?2#(A(),x) TRS: a() -> c() a() -> d() b() -> c() b() -> d() c() -> e() c() -> k() d() -> k() ?1(e(),x) -> x f(x) -> ?1(x,x) ?2(B(),x) -> C() g(x,x) -> ?2(A(),x) h(x) -> i(x,x) TDG Processor: DPs: a#() -> c#() a#() -> d#() b#() -> c#() b#() -> d#() f#(x) -> ?1#(x,x) g#(x,x) -> ?2#(A(),x) TRS: a() -> c() a() -> d() b() -> c() b() -> d() c() -> e() c() -> k() d() -> k() ?1(e(),x) -> x f(x) -> ?1(x,x) ?2(B(),x) -> C() g(x,x) -> ?2(A(),x) h(x) -> i(x,x) graph: Qed