Problem: H(I(x)) -> K(J(x)) J(x) -> K(J(x)) I(x) -> I(J(x)) J(x) -> J(K(J(x))) Proof: Church Rosser Transformation Processor (star): strict: weak: J(0)(x) -> J(0)(K(0)(J(0)(x))) I(0)(x) -> I(0)(J(0)(x)) J(0)(x) -> K(0)(J(0)(x)) H(0)(I(0)(x)) -> K(0)(J(0)(x)) critical peaks: 3 K(J(x)) <-1|[]- J(x) -3|[]-> J(K(J(x))) H(I(J(x))) <-2|0[]- H(I(x)) -0|[]-> K(J(x)) J(K(J(x))) <-3|[]- J(x) -1|[]-> K(J(x)) Matrix Interpretation Processor: dim=1, lab=right interpretation: [H(0)](x0) = x0, [I(0)](x0) = x0 + 2, [K(0)](x0) = x0, [J(0)](x0) = x0 orientation: J(0)(x) = x >= x = J(0)(K(0)(J(0)(x))) I(0)(x) = x + 2 >= x + 2 = I(0)(J(0)(x)) J(0)(x) = x >= x = K(0)(J(0)(x)) H(0)(I(0)(x)) = x + 2 >= x = K(0)(J(0)(x)) problem: strict: weak: J(0)(x) -> J(0)(K(0)(J(0)(x))) I(0)(x) -> I(0)(J(0)(x)) J(0)(x) -> K(0)(J(0)(x)) Shift Processor lab=left (dd): strict: J(x) -> K(J(x)) J(x) -> J(K(J(x))) K(J(x)) -> K(J(K(J(x)))) J(K(J(x))) -> K(J(K(J(x)))) H(I(x)) -> H(I(J(x))) H(I(x)) -> K(J(x)) H(I(J(x))) -> K(J(J(x))) K(J(J(x))) -> K(J(K(J(x)))) K(J(x)) -> K(J(K(J(x)))) H(I(J(x))) -> H(I(K(J(x)))) H(I(K(J(x)))) -> K(J(K(J(x)))) K(J(x)) -> K(J(K(J(x)))) J(x) -> J(K(J(x))) J(x) -> K(J(x)) J(K(J(x))) -> K(J(K(J(x)))) K(J(x)) -> K(J(K(J(x)))) weak: H(I(x)) -> K(J(x)) J(x) -> K(J(x)) I(x) -> I(J(x)) J(x) -> J(K(J(x))) Matrix Interpretation Processor: dim=1 interpretation: [K](x0) = x0, [J](x0) = x0, [H](x0) = 3x0, [I](x0) = x0 + 5 orientation: J(x) = x >= x = K(J(x)) J(x) = x >= x = J(K(J(x))) K(J(x)) = x >= x = K(J(K(J(x)))) J(K(J(x))) = x >= x = K(J(K(J(x)))) H(I(x)) = 3x + 15 >= 3x + 15 = H(I(J(x))) H(I(x)) = 3x + 15 >= x = K(J(x)) H(I(J(x))) = 3x + 15 >= x = K(J(J(x))) K(J(J(x))) = x >= x = K(J(K(J(x)))) K(J(x)) = x >= x = K(J(K(J(x)))) H(I(J(x))) = 3x + 15 >= 3x + 15 = H(I(K(J(x)))) H(I(K(J(x)))) = 3x + 15 >= x = K(J(K(J(x)))) K(J(x)) = x >= x = K(J(K(J(x)))) J(x) = x >= x = J(K(J(x))) J(x) = x >= x = K(J(x)) J(K(J(x))) = x >= x = K(J(K(J(x)))) K(J(x)) = x >= x = K(J(K(J(x)))) I(x) = x + 5 >= x + 5 = I(J(x)) problem: strict: J(x) -> K(J(x)) J(x) -> J(K(J(x))) K(J(x)) -> K(J(K(J(x)))) J(K(J(x))) -> K(J(K(J(x)))) H(I(x)) -> H(I(J(x))) K(J(J(x))) -> K(J(K(J(x)))) K(J(x)) -> K(J(K(J(x)))) H(I(J(x))) -> H(I(K(J(x)))) K(J(x)) -> K(J(K(J(x)))) J(x) -> J(K(J(x))) J(x) -> K(J(x)) J(K(J(x))) -> K(J(K(J(x)))) K(J(x)) -> K(J(K(J(x)))) weak: J(x) -> K(J(x)) I(x) -> I(J(x)) J(x) -> J(K(J(x))) Shift Processor (ldh) lab=left (force): strict: weak: Decreasing Processor: The following diagrams are decreasing: peak: K(J(x)) <-1|[1,0]- J(x) -3|[1,0]-> J(K(J(x))) joins: K(J(x)) -3|0[1,0]-> K(J(K(J(x)))) J(K(J(x))) -1|[1,0]-> K(J(K(J(x)))) peak: H(I(J(x))) <-2|0[1,0]- H(I(x)) -0|[1,0]-> K(J(x)) joins: H(I(J(x))) -0|[1,0]-> K(J(J(x))) -1|0,0[0,0]-> K(J(K(J(x)))) K(J(x)) -3|0[0,0]-> K(J(K(J(x)))) peak: J(K(J(x))) <-3|[1,0]- J(x) -1|[1,0]-> K(J(x)) joins: J(K(J(x))) -1|[1,0]-> K(J(K(J(x)))) K(J(x)) -3|0[1,0]-> K(J(K(J(x)))) Qed