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