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: f(x, x') -> g(x', x') f(x, x') -> x' f(x, x') -> x h(x, x', x'') -> c h(x, x', x'') -> x'' h(x, x', x'') -> x' h(x, x', x'') -> x h(x, y, z) -> x h(x, y, z) -> y h(x, y, z) -> z g(x, y) -> x g(x, y) -> y f(x, y) -> x f(x, y) -> y DP Processor: DPs: f#(x,x') -> g#(x',x') TRS: f(x,x') -> g(x',x') f(x,x') -> x' f(x,x') -> x h(x,x',x'') -> c() h(x,x',x'') -> x'' h(x,x',x'') -> x' h(x,x',x'') -> x h(x,y,z) -> x h(x,y,z) -> y h(x,y,z) -> z g(x,y) -> x g(x,y) -> y f(x,y) -> x f(x,y) -> y TDG Processor: DPs: f#(x,x') -> g#(x',x') TRS: f(x,x') -> g(x',x') f(x,x') -> x' f(x,x') -> x h(x,x',x'') -> c() h(x,x',x'') -> x'' h(x,x',x'') -> x' h(x,x',x'') -> x h(x,y,z) -> x h(x,y,z) -> y h(x,y,z) -> z g(x,y) -> x g(x,y) -> y f(x,y) -> x f(x,y) -> y graph: Qed This system is deterministic. This system is not weakly left-linear. This system is not normal. This system is oriented. This system is of type 3 or smaller. This system is not right-stable. This system is conditional.