Problem: H(H(x)) -> K(x) H(K(x)) -> K(H(x)) Proof: Church Rosser Transformation Processor (kb): H(H(x)) -> K(x) H(K(x)) -> K(H(x)) critical peaks: joinable Matrix Interpretation Processor: dim=3 interpretation: [1 1 0] [0] [K](x0) = [0 0 0]x0 + [1] [0 0 0] [1], [1 1 0] [0] [H](x0) = [0 0 0]x0 + [1] [0 1 0] [0] orientation: [1 1 0] [1] [1 1 0] [0] H(H(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = K(x) [0 0 0] [1] [0 0 0] [1] [1 1 0] [1] [1 1 0] [1] H(K(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = K(H(x)) [0 0 0] [1] [0 0 0] [1] problem: H(K(x)) -> K(H(x)) Matrix Interpretation Processor: dim=3 interpretation: [1 0 0] [0] [K](x0) = [0 0 1]x0 + [0] [0 0 1] [1], [1 0 1] [H](x0) = [0 0 1]x0 [0 0 1] orientation: [1 0 1] [1] [1 0 1] [0] H(K(x)) = [0 0 1]x + [1] >= [0 0 1]x + [0] = K(H(x)) [0 0 1] [1] [0 0 1] [1] problem: Qed