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