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