Problem: F(D(x),y) -> F(D(x),G(G(y))) F(x,E(y)) -> F(G(x),E(y)) G(x) -> x H(I(x)) -> K(J(x)) J(x) -> K(J(x)) I(x) -> I(J(x)) J(x) -> J(K(J(x))) S(x,T(x)) -> T(x) Proof: sorted: (order) 0:F(D(x),y) -> F(D(x),G(G(y))) F(x,E(y)) -> F(G(x),E(y)) G(x) -> x 1:H(I(x)) -> K(J(x)) J(x) -> K(J(x)) I(x) -> I(J(x)) J(x) -> J(K(J(x))) 2:S(x,T(x)) -> T(x) ----- sorts [1>10, 2>4, 3>6, 4>5, 5>9, 6>7, 7>8, 10>11, 10>13, 11>12, 13>14] sort attachment (non-strict) F : 10 x 10 -> 1 D : 14 -> 13 G : 10 -> 10 E : 12 -> 11 H : 4 -> 2 I : 9 -> 5 K : 9 -> 9 J : 9 -> 9 S : 8 x 6 -> 3 T : 8 -> 7 ----- 0:F(D(x),y) -> F(D(x),G(G(y))) F(x,E(y)) -> F(G(x),E(y)) G(x) -> x Church Rosser Transformation Processor (star): strict: weak: G(0)(x) -> x F(0)(x) -> F(0)(G(0)(x)) F(1)(E(0)(y)) -> F(1)(E(0)(y)) F(0)(D(0)(x)) -> F(0)(D(0)(x)) F(1)(y) -> F(1)(G(0)(G(0)(y))) critical peaks: 2 F(D(x27),G(G(E(y)))) <-0|[]- F(D(x27),E(y)) -1|[]-> F(G(D(x27)),E(y)) F(G(D(x)),E(x30)) <-1|[]- F(D(x),E(x30)) -0|[]-> F(D(x),G(G(E(x30)))) Shift Processor lab=left (dd): strict: F(D(x27),E(y)) -> F(D(x27),G(G(E(y)))) F(D(x27),E(y)) -> F(G(D(x27)),E(y)) F(G(D(x27)),E(y)) -> F(D(x27),E(y)) F(D(x27),E(y)) -> F(D(x27),G(G(E(y)))) F(D(x27),G(G(E(y)))) -> F(D(x27),G(E(y))) F(D(x27),G(E(y))) -> F(D(x27),E(y)) F(G(D(x27)),E(y)) -> F(D(x27),E(y)) F(D(x),E(x30)) -> F(G(D(x)),E(x30)) F(D(x),E(x30)) -> F(D(x),G(G(E(x30)))) F(G(D(x)),E(x30)) -> F(D(x),E(x30)) F(D(x),G(G(E(x30)))) -> F(D(x),G(E(x30))) F(D(x),G(E(x30))) -> F(D(x),E(x30)) F(G(D(x)),E(x30)) -> F(D(x),E(x30)) F(D(x),E(x30)) -> F(D(x),G(G(E(x30)))) weak: F(D(x),y) -> F(D(x),G(G(y))) F(x,E(y)) -> F(G(x),E(y)) G(x) -> x Shift Processor (ldh) lab=left (force): strict: weak: Rule Labeling Processor: strict: weak: rule labeling (right): F(D(x),y) -> F(D(x),G(G(y))): 0 F(x,E(y)) -> F(G(x),E(y)): 1 G(x) -> x: 0 Decreasing Processor: The following diagrams are decreasing: peak: F(D(x27),G(G(E(y)))) <-0|[1,0]- F(D(x27),E(y)) -1|[1,1]-> F(G(D(x27)),E(y)) joins: F(G(D(x27)),E(y)) -2|0[1,0]-> F(D(x27),E(y)) -0|[1,0]-> F(D(x27),G(G(E(y)))) peak: F(G(D(x)),E(x30)) <-1|[1,1]- F(D(x),E(x30)) -0|[1,0]-> F(D(x),G(G(E(x30)))) joins: F(G(D(x)),E(x30)) -2|0[1,0]-> F(D(x),E(x30)) -0|[1,0]-> F(D(x),G(G(E(x30)))) Qed 1:H(I(x)) -> K(J(x)) J(x) -> K(J(x)) I(x) -> I(J(x)) J(x) -> J(K(J(x))) 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=2 interpretation: [1 0] [K](x0) = [0 0]x0, [1 0] [0] [J](x0) = [2 0]x0 + [2], [1 0] [2] [H](x0) = [0 0]x0 + [0], [2 0] [1] [I](x0) = [2 0]x0 + [3] orientation: [1 0] [0] [1 0] J(x) = [2 0]x + [2] >= [0 0]x = K(J(x)) [1 0] [0] [1 0] [0] J(x) = [2 0]x + [2] >= [2 0]x + [2] = J(K(J(x))) [1 0] [1 0] K(J(x)) = [0 0]x >= [0 0]x = K(J(K(J(x)))) [1 0] [0] [1 0] J(K(J(x))) = [2 0]x + [2] >= [0 0]x = K(J(K(J(x)))) [2 0] [3] [2 0] [3] H(I(x)) = [0 0]x + [0] >= [0 0]x + [0] = H(I(J(x))) [2 0] [3] [1 0] H(I(x)) = [0 0]x + [0] >= [0 0]x = K(J(x)) [2 0] [3] [1 0] H(I(J(x))) = [0 0]x + [0] >= [0 0]x = K(J(J(x))) [1 0] [1 0] K(J(J(x))) = [0 0]x >= [0 0]x = K(J(K(J(x)))) [1 0] [1 0] K(J(x)) = [0 0]x >= [0 0]x = K(J(K(J(x)))) [2 0] [3] [2 0] [3] H(I(J(x))) = [0 0]x + [0] >= [0 0]x + [0] = H(I(K(J(x)))) [2 0] [3] [1 0] H(I(K(J(x)))) = [0 0]x + [0] >= [0 0]x = K(J(K(J(x)))) [1 0] [1 0] K(J(x)) = [0 0]x >= [0 0]x = K(J(K(J(x)))) [1 0] [0] [1 0] [0] J(x) = [2 0]x + [2] >= [2 0]x + [2] = J(K(J(x))) [1 0] [0] [1 0] J(x) = [2 0]x + [2] >= [0 0]x = K(J(x)) [1 0] [0] [1 0] J(K(J(x))) = [2 0]x + [2] >= [0 0]x = K(J(K(J(x)))) [1 0] [1 0] K(J(x)) = [0 0]x >= [0 0]x = K(J(K(J(x)))) [2 0] [1] [2 0] [1] I(x) = [2 0]x + [3] >= [2 0]x + [3] = 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 2:S(x,T(x)) -> T(x) Church Rosser Transformation Processor (kb): S(x,T(x)) -> T(x) critical peaks: joinable DP Processor: DPs: TRS: S(x,T(x)) -> T(x) Qed