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