YES Proof: This system is confluent. By \cite{ALS94}, Theorem 4.1. This system is of type 3 or smaller. This system is strongly deterministic. There are no critical pairs. By \cite{A14}, Theorem 11.5.9. This system is of type 3 or smaller. This system is deterministic. System R transformed to V(R) + Emb. Call external tool: ttt2 - trs 30 Input: a -> b f(x) -> A f(x) -> x g(x, x) -> h(x) h(x) -> i(x) h(x) -> x g(x, y) -> x g(x, y) -> y f(x) -> x i(x) -> x DP Processor: DPs: g#(x,x) -> h#(x) h#(x) -> i#(x) TRS: a() -> b() f(x) -> A() f(x) -> x g(x,x) -> h(x) h(x) -> i(x) h(x) -> x g(x,y) -> x g(x,y) -> y i(x) -> x TDG Processor: DPs: g#(x,x) -> h#(x) h#(x) -> i#(x) TRS: a() -> b() f(x) -> A() f(x) -> x g(x,x) -> h(x) h(x) -> i(x) h(x) -> x g(x,y) -> x g(x,y) -> y i(x) -> x graph: g#(x,x) -> h#(x) -> h#(x) -> i#(x) SCC Processor: #sccs: 0 #rules: 0 #arcs: 1/4