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: ?1(l, x) -> e f(x) -> ?1(d, x) h(x, x) -> A DP Processor: DPs: f#(x) -> ?1#(d(),x) TRS: ?1(l(),x) -> e() f(x) -> ?1(d(),x) h(x,x) -> A() TDG Processor: DPs: f#(x) -> ?1#(d(),x) TRS: ?1(l(),x) -> e() f(x) -> ?1(d(),x) h(x,x) -> A() graph: Qed