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: h(f(a)) -> c h(x) -> j(x) c -> j(f(a)) a -> b c -> d j(g(b)) -> d f(x) -> g(x) f(x) -> d h(x) -> x j(x) -> x g(x) -> x f(x) -> x DP Processor: DPs: h#(f(a())) -> c#() h#(x) -> j#(x) c#() -> a#() c#() -> f#(a()) c#() -> j#(f(a())) f#(x) -> g#(x) TRS: h(f(a())) -> c() h(x) -> j(x) c() -> j(f(a())) a() -> b() c() -> d() j(g(b())) -> d() f(x) -> g(x) f(x) -> d() h(x) -> x j(x) -> x g(x) -> x f(x) -> x TDG Processor: DPs: h#(f(a())) -> c#() h#(x) -> j#(x) c#() -> a#() c#() -> f#(a()) c#() -> j#(f(a())) f#(x) -> g#(x) TRS: h(f(a())) -> c() h(x) -> j(x) c() -> j(f(a())) a() -> b() c() -> d() j(g(b())) -> d() f(x) -> g(x) f(x) -> d() h(x) -> x j(x) -> x g(x) -> x f(x) -> x graph: c#() -> f#(a()) -> f#(x) -> g#(x) h#(f(a())) -> c#() -> c#() -> j#(f(a())) h#(f(a())) -> c#() -> c#() -> f#(a()) h#(f(a())) -> c#() -> c#() -> a#() SCC Processor: #sccs: 0 #rules: 0 #arcs: 4/36