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