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: ?2(e', x) -> x ?1(e, x) -> ?2(x, x) f(x) -> ?1(x, x) g(d, x, x) -> A h(x, x) -> g(x, x, f(k)) c -> e' a -> c a -> d b -> c b -> d c -> e c -> l k -> l k -> m d -> m DP Processor: DPs: ?1#(e(),x) -> ?2#(x,x) f#(x) -> ?1#(x,x) h#(x,x) -> k#() h#(x,x) -> f#(k()) h#(x,x) -> g#(x,x,f(k())) a#() -> c#() a#() -> d#() b#() -> c#() b#() -> d#() TRS: ?2(e'(),x) -> x ?1(e(),x) -> ?2(x,x) f(x) -> ?1(x,x) g(d(),x,x) -> A() h(x,x) -> g(x,x,f(k())) c() -> e'() a() -> c() a() -> d() b() -> c() b() -> d() c() -> e() c() -> l() k() -> l() k() -> m() d() -> m() TDG Processor: DPs: ?1#(e(),x) -> ?2#(x,x) f#(x) -> ?1#(x,x) h#(x,x) -> k#() h#(x,x) -> f#(k()) h#(x,x) -> g#(x,x,f(k())) a#() -> c#() a#() -> d#() b#() -> c#() b#() -> d#() TRS: ?2(e'(),x) -> x ?1(e(),x) -> ?2(x,x) f(x) -> ?1(x,x) g(d(),x,x) -> A() h(x,x) -> g(x,x,f(k())) c() -> e'() a() -> c() a() -> d() b() -> c() b() -> d() c() -> e() c() -> l() k() -> l() k() -> m() d() -> m() graph: h#(x,x) -> f#(k()) -> f#(x) -> ?1#(x,x) f#(x) -> ?1#(x,x) -> ?1#(e(),x) -> ?2#(x,x) SCC Processor: #sccs: 0 #rules: 0 #arcs: 2/81