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