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 -> b ?1(b, x) -> A f(x) -> ?1(x, x) g(x, x) -> h(x) h(x) -> i(x) DP Processor: DPs: f#(x) -> ?1#(x,x) g#(x,x) -> h#(x) TRS: a() -> b() ?1(b(),x) -> A() f(x) -> ?1(x,x) g(x,x) -> h(x) h(x) -> i(x) TDG Processor: DPs: f#(x) -> ?1#(x,x) g#(x,x) -> h#(x) TRS: a() -> b() ?1(b(),x) -> A() f(x) -> ?1(x,x) g(x,x) -> h(x) h(x) -> i(x) graph: Qed