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: ?2(h(x), x, y) -> c(x, y) ?1(y, x) -> ?2(y, x, y) f(x) -> ?1(g(x), x) a -> b g(a) -> h(b) DP Processor: DPs: ?1#(y,x) -> ?2#(y,x,y) f#(x) -> g#(x) f#(x) -> ?1#(g(x),x) TRS: ?2(h(x),x,y) -> c(x,y) ?1(y,x) -> ?2(y,x,y) f(x) -> ?1(g(x),x) a() -> b() g(a()) -> h(b()) TDG Processor: DPs: ?1#(y,x) -> ?2#(y,x,y) f#(x) -> g#(x) f#(x) -> ?1#(g(x),x) TRS: ?2(h(x),x,y) -> c(x,y) ?1(y,x) -> ?2(y,x,y) f(x) -> ?1(g(x),x) a() -> b() g(a()) -> h(b()) graph: f#(x) -> ?1#(g(x),x) -> ?1#(y,x) -> ?2#(y,x,y) SCC Processor: #sccs: 0 #rules: 0 #arcs: 1/9