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: a -> t(c) a -> t(d) ?1(t(z), x, y) -> z f(x, y) -> ?1(x, x, y) g(x, x) -> h(x, x) DP Processor: DPs: f#(x,y) -> ?1#(x,x,y) TRS: a() -> t(c()) a() -> t(d()) ?1(t(z),x,y) -> z f(x,y) -> ?1(x,x,y) g(x,x) -> h(x,x) TDG Processor: DPs: f#(x,y) -> ?1#(x,x,y) TRS: a() -> t(c()) a() -> t(d()) ?1(t(z),x,y) -> z f(x,y) -> ?1(x,x,y) g(x,x) -> h(x,x) graph: Qed