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(l, x) -> e f(x) -> ?1(d, x) h(x, x) -> A sorted: (order) 0:?1(l(),x) -> e() f(x) -> ?1(d(),x) 1:h(x,x) -> A() ----- sorts [0>1, 1>2, 1>5, 1>9, 3>4, 3>8, 5>6, 5>7, 9>10] sort attachment (non-strict) ?1 : 5 x 9 -> 1 l : 7 e : 2 f : 10 -> 0 d : 6 h : 8 x 8 -> 3 A : 4 ----- 0:?1(l(),x) -> e() f(x) -> ?1(d(),x) Church Rosser Transformation Processor: strict: ?1(l(),x) -> e() f(x) -> ?1(d(),x) weak: critical peaks: 0 Closedness Processor (*strongly -- <=7 steps*): strict: weak: Qed 1:h(x,x) -> A() Church Rosser Transformation Processor (kb): h(x,x) -> A() critical peaks: joinable Matrix Interpretation Processor: dim=1 interpretation: [h](x0, x1) = x0 + 2x1 + 4, [A] = 0 orientation: h(x,x) = 3x + 4 >= 0 = A() problem: Qed