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