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: f(x) -> e f(x) -> d h(x, x) -> A h(x, y) -> x h(x, y) -> y f(x) -> x DP Processor: DPs: TRS: f(x) -> e() f(x) -> d() h(x,x) -> A() h(x,y) -> x h(x,y) -> y f(x) -> x Qed