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 -> c a -> d ?2(x, x) -> x ?1(c, x) -> ?2(d, x) f(x) -> ?1(x, x) DP Processor: DPs: ?1#(c(),x) -> ?2#(d(),x) f#(x) -> ?1#(x,x) TRS: a() -> c() a() -> d() ?2(x,x) -> x ?1(c(),x) -> ?2(d(),x) f(x) -> ?1(x,x) TDG Processor: DPs: ?1#(c(),x) -> ?2#(d(),x) f#(x) -> ?1#(x,x) TRS: a() -> c() a() -> d() ?2(x,x) -> x ?1(c(),x) -> ?2(d(),x) f(x) -> ?1(x,x) graph: f#(x) -> ?1#(x,x) -> ?1#(c(),x) -> ?2#(d(),x) SCC Processor: #sccs: 0 #rules: 0 #arcs: 1/4