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