YES Proof: This system is quasi-decreasing. By \cite{O02}, p. 214, Proposition 7.2.50. This system is of type 3 or smaller. This system is deterministic. System R transformed to U(R). 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 ?1(h(f(x)), x) -> g(x) f(x) -> ?1(d, x) DP Processor: DPs: h#(f(a())) -> c#() h#(x) -> j#(x) c#() -> a#() c#() -> f#(a()) c#() -> j#(f(a())) f#(x) -> ?1#(d(),x) TRS: h(f(a())) -> c() h(x) -> j(x) c() -> j(f(a())) a() -> b() c() -> d() j(g(b())) -> d() ?1(h(f(x)),x) -> g(x) f(x) -> ?1(d(),x) TDG Processor: DPs: h#(f(a())) -> c#() h#(x) -> j#(x) c#() -> a#() c#() -> f#(a()) c#() -> j#(f(a())) f#(x) -> ?1#(d(),x) TRS: h(f(a())) -> c() h(x) -> j(x) c() -> j(f(a())) a() -> b() c() -> d() j(g(b())) -> d() ?1(h(f(x)),x) -> g(x) f(x) -> ?1(d(),x) graph: c#() -> f#(a()) -> f#(x) -> ?1#(d(),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