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