YES Proof: This system is quasi-decreasing. By \cite{A14}, Theorem 11.5.9. This system is of type 3 or smaller. This system is deterministic. System R transformed to V(R) + Emb. Call external tool: ttt2 - trs 30 Input: f(x) -> g(x, h(a, x), h(a, h(a, x))) f(x) -> h(a, h(a, x)) f(x) -> h(a, x) h(a, a) -> i(b) h(a, b) -> i(c) h(b, b) -> i(d) h(x, y) -> x h(x, y) -> y g(x, y, z) -> x g(x, y, z) -> y g(x, y, z) -> z f(x) -> x i(x) -> x DP Processor: DPs: f#(x) -> h#(a(),h(a(),x)) f#(x) -> h#(a(),x) f#(x) -> g#(x,h(a(),x),h(a(),h(a(),x))) h#(a(),a()) -> i#(b()) h#(a(),b()) -> i#(c()) h#(b(),b()) -> i#(d()) TRS: f(x) -> g(x,h(a(),x),h(a(),h(a(),x))) f(x) -> h(a(),h(a(),x)) f(x) -> h(a(),x) h(a(),a()) -> i(b()) h(a(),b()) -> i(c()) h(b(),b()) -> i(d()) h(x,y) -> x h(x,y) -> y g(x,y,z) -> x g(x,y,z) -> y g(x,y,z) -> z f(x) -> x i(x) -> x TDG Processor: DPs: f#(x) -> h#(a(),h(a(),x)) f#(x) -> h#(a(),x) f#(x) -> g#(x,h(a(),x),h(a(),h(a(),x))) h#(a(),a()) -> i#(b()) h#(a(),b()) -> i#(c()) h#(b(),b()) -> i#(d()) TRS: f(x) -> g(x,h(a(),x),h(a(),h(a(),x))) f(x) -> h(a(),h(a(),x)) f(x) -> h(a(),x) h(a(),a()) -> i(b()) h(a(),b()) -> i(c()) h(b(),b()) -> i(d()) h(x,y) -> x h(x,y) -> y g(x,y,z) -> x g(x,y,z) -> y g(x,y,z) -> z f(x) -> x i(x) -> x graph: f#(x) -> h#(a(),h(a(),x)) -> h#(b(),b()) -> i#(d()) f#(x) -> h#(a(),h(a(),x)) -> h#(a(),b()) -> i#(c()) f#(x) -> h#(a(),h(a(),x)) -> h#(a(),a()) -> i#(b()) f#(x) -> h#(a(),x) -> h#(b(),b()) -> i#(d()) f#(x) -> h#(a(),x) -> h#(a(),b()) -> i#(c()) f#(x) -> h#(a(),x) -> h#(a(),a()) -> i#(b()) SCC Processor: #sccs: 0 #rules: 0 #arcs: 6/36