YES Problem: W(B(x)) -> W(x) B(I(x)) -> J(x) W(I(x)) -> W(J(x)) Proof: Church Rosser Transformation Processor (kb): W(B(x)) -> W(x) B(I(x)) -> J(x) W(I(x)) -> W(J(x)) critical peaks: joinable Matrix Interpretation Processor: dim=1 interpretation: [W](x0) = 4x0 + 3, [J](x0) = x0, [B](x0) = x0, [I](x0) = 2x0 + 4 orientation: W(B(x)) = 4x + 3 >= 4x + 3 = W(x) B(I(x)) = 2x + 4 >= x = J(x) W(I(x)) = 8x + 19 >= 4x + 3 = W(J(x)) problem: W(B(x)) -> W(x) Matrix Interpretation Processor: dim=1 interpretation: [W](x0) = x0, [B](x0) = x0 + 3 orientation: W(B(x)) = x + 3 >= x = W(x) problem: Qed