YES Proof: This system is confluent. By \cite{GNG13}, Theorem 9. This system is deterministic. This system is weakly left-linear. System R transformed to optimized U(R). This system is not orthogonal. Call external tool: csi - trs 30 Input: ?1(y, x, y, z) -> G(z) F(x, y, z) -> ?1(x, x, y, z) G(A) -> F(A, B, A) e(x) -> f(x, x) f(x, y) -> x sorted: (order) 0:?1(y,x,y,z) -> G(z) F(x,y,z) -> ?1(x,x,y,z) G(A()) -> F(A(),B(),A()) 1:e(x) -> f(x,x) f(x,y) -> x ----- sorts [0>2, 0>4, 2>3, 2>5, 4>5] sort attachment (strict) ?1 : 2 x 2 x 2 x 4 -> 0 G : 4 -> 0 F : 2 x 2 x 4 -> 0 A : 5 B : 3 e : 1 -> 1 f : 1 x 1 -> 1 ----- 0:?1(y,x,y,z) -> G(z) F(x,y,z) -> ?1(x,x,y,z) G(A()) -> F(A(),B(),A()) Church Rosser Transformation Processor (kb): ?1(y,x,y,z) -> G(z) F(x,y,z) -> ?1(x,x,y,z) G(A()) -> F(A(),B(),A()) critical peaks: joinable DP Processor: DPs: ?1#(y,x,y,z) -> G#(z) F#(x,y,z) -> ?1#(x,x,y,z) G#(A()) -> F#(A(),B(),A()) TRS: ?1(y,x,y,z) -> G(z) F(x,y,z) -> ?1(x,x,y,z) G(A()) -> F(A(),B(),A()) EDG Processor: DPs: ?1#(y,x,y,z) -> G#(z) F#(x,y,z) -> ?1#(x,x,y,z) G#(A()) -> F#(A(),B(),A()) TRS: ?1(y,x,y,z) -> G(z) F(x,y,z) -> ?1(x,x,y,z) G(A()) -> F(A(),B(),A()) graph: F#(x,y,z) -> ?1#(x,x,y,z) -> ?1#(y,x,y,z) -> G#(z) G#(A()) -> F#(A(),B(),A()) -> F#(x,y,z) -> ?1#(x,x,y,z) ?1#(y,x,y,z) -> G#(z) -> G#(A()) -> F#(A(),B(),A()) Bounds Processor: bound: 0 enrichment: top-dp automaton: final states: {8} transitions: B0() -> 10* A0() -> 9* F{#,0}(9,10,9) -> 8* ?1{#,0}(9,9,10,9) -> 8* problem: DPs: ?1#(y,x,y,z) -> G#(z) F#(x,y,z) -> ?1#(x,x,y,z) TRS: ?1(y,x,y,z) -> G(z) F(x,y,z) -> ?1(x,x,y,z) G(A()) -> F(A(),B(),A()) SCC Processor: #sccs: 0 #rules: 0 #arcs: 3/4 1:e(x) -> f(x,x) f(x,y) -> x Church Rosser Transformation Processor (kb): e(x) -> f(x,x) f(x,y) -> x critical peaks: joinable Matrix Interpretation Processor: dim=1 interpretation: [e](x0) = 3x0 + 4, [f](x0, x1) = x0 + 2x1 orientation: e(x) = 3x + 4 >= 3x = f(x,x) f(x,y) = x + 2y >= x = x problem: f(x,y) -> x Matrix Interpretation Processor: dim=1 interpretation: [f](x0, x1) = 4x0 + 2x1 + 4 orientation: f(x,y) = 4x + 2y + 4 >= x = x problem: Qed