Problem: H(F(x,y)) -> F(H(R(x)),y) F(x,K(y,z)) -> G(P(y),Q(z,x)) H(Q(x,y)) -> Q(x,H(R(y))) Q(x,H(R(y))) -> H(Q(x,y)) H(G(x,y)) -> G(x,H(y)) Proof: Church Rosser Transformation Processor (star): strict: weak: H(0)(G(0)(x)) -> G(0)(x) H(0)(G(1)(y)) -> G(1)(H(0)(y)) Q(0)(x) -> H(0)(Q(0)(x)) Q(1)(H(0)(R(0)(y))) -> H(0)(Q(1)(y)) H(0)(Q(0)(x)) -> Q(0)(x) H(0)(Q(1)(y)) -> Q(1)(H(0)(R(0)(y))) F(0)(x) -> G(1)(Q(1)(x)) F(1)(K(0)(y)) -> G(0)(P(0)(y)) F(1)(K(1)(z)) -> G(1)(Q(0)(z)) H(0)(F(0)(x)) -> F(0)(H(0)(R(0)(x))) H(0)(F(1)(y)) -> F(1)(y) critical peaks: 2 H(G(P(x125),Q(x126,x))) <-1|0[]- H(F(x,K(x125,x126))) -0|[]-> F(H(R(x)),K(x125,x126)) H(H(Q(x,x128))) <-3|0[]- H(Q(x,H(R(x128)))) -2|[]-> Q(x,H(R(H(R(x128))))) Matrix Interpretation Processor: dim=1, lab=right interpretation: [K(1)](x0) = 2x0 + 1, [P(0)](x0) = x0, [K(0)](x0) = 2x0 + 1, [F(1)](x0) = x0 + 2, [F(0)](x0) = 2x0 + 3, [R(0)](x0) = x0, [Q(1)](x0) = 2x0, [Q(0)](x0) = 2x0, [G(1)](x0) = x0 + 3, [G(0)](x0) = 2x0 + 2, [H(0)](x0) = x0 orientation: H(0)(G(0)(x)) = 2x + 2 >= 2x + 2 = G(0)(x) H(0)(G(1)(y)) = y + 3 >= y + 3 = G(1)(H(0)(y)) Q(0)(x) = 2x >= 2x = H(0)(Q(0)(x)) Q(1)(H(0)(R(0)(y))) = 2y >= 2y = H(0)(Q(1)(y)) H(0)(Q(0)(x)) = 2x >= 2x = Q(0)(x) H(0)(Q(1)(y)) = 2y >= 2y = Q(1)(H(0)(R(0)(y))) F(0)(x) = 2x + 3 >= 2x + 3 = G(1)(Q(1)(x)) F(1)(K(0)(y)) = 2y + 3 >= 2y + 2 = G(0)(P(0)(y)) F(1)(K(1)(z)) = 2z + 3 >= 2z + 3 = G(1)(Q(0)(z)) H(0)(F(0)(x)) = 2x + 3 >= 2x + 3 = F(0)(H(0)(R(0)(x))) H(0)(F(1)(y)) = y + 2 >= y + 2 = F(1)(y) problem: strict: weak: H(0)(G(0)(x)) -> G(0)(x) H(0)(G(1)(y)) -> G(1)(H(0)(y)) Q(0)(x) -> H(0)(Q(0)(x)) Q(1)(H(0)(R(0)(y))) -> H(0)(Q(1)(y)) H(0)(Q(0)(x)) -> Q(0)(x) H(0)(Q(1)(y)) -> Q(1)(H(0)(R(0)(y))) F(0)(x) -> G(1)(Q(1)(x)) F(1)(K(1)(z)) -> G(1)(Q(0)(z)) H(0)(F(0)(x)) -> F(0)(H(0)(R(0)(x))) H(0)(F(1)(y)) -> F(1)(y) Matrix Interpretation Processor: dim=1, lab=right interpretation: [K(1)](x0) = 2x0 + 1, [F(1)](x0) = x0, [F(0)](x0) = 3x0, [R(0)](x0) = x0, [Q(1)](x0) = x0, [Q(0)](x0) = x0, [G(1)](x0) = 2x0, [G(0)](x0) = 2x0, [H(0)](x0) = x0 orientation: H(0)(G(0)(x)) = 2x >= 2x = G(0)(x) H(0)(G(1)(y)) = 2y >= 2y = G(1)(H(0)(y)) Q(0)(x) = x >= x = H(0)(Q(0)(x)) Q(1)(H(0)(R(0)(y))) = y >= y = H(0)(Q(1)(y)) H(0)(Q(0)(x)) = x >= x = Q(0)(x) H(0)(Q(1)(y)) = y >= y = Q(1)(H(0)(R(0)(y))) F(0)(x) = 3x >= 2x = G(1)(Q(1)(x)) F(1)(K(1)(z)) = 2z + 1 >= 2z = G(1)(Q(0)(z)) H(0)(F(0)(x)) = 3x >= 3x = F(0)(H(0)(R(0)(x))) H(0)(F(1)(y)) = y >= y = F(1)(y) problem: strict: weak: H(0)(G(0)(x)) -> G(0)(x) H(0)(G(1)(y)) -> G(1)(H(0)(y)) Q(0)(x) -> H(0)(Q(0)(x)) Q(1)(H(0)(R(0)(y))) -> H(0)(Q(1)(y)) H(0)(Q(0)(x)) -> Q(0)(x) H(0)(Q(1)(y)) -> Q(1)(H(0)(R(0)(y))) F(0)(x) -> G(1)(Q(1)(x)) H(0)(F(0)(x)) -> F(0)(H(0)(R(0)(x))) H(0)(F(1)(y)) -> F(1)(y) Matrix Interpretation Processor: dim=1, lab=right interpretation: [F(1)](x0) = 3x0 + 2, [F(0)](x0) = 2x0 + 1, [R(0)](x0) = x0, [Q(1)](x0) = x0, [Q(0)](x0) = x0, [G(1)](x0) = 2x0, [G(0)](x0) = x0, [H(0)](x0) = x0 orientation: H(0)(G(0)(x)) = x >= x = G(0)(x) H(0)(G(1)(y)) = 2y >= 2y = G(1)(H(0)(y)) Q(0)(x) = x >= x = H(0)(Q(0)(x)) Q(1)(H(0)(R(0)(y))) = y >= y = H(0)(Q(1)(y)) H(0)(Q(0)(x)) = x >= x = Q(0)(x) H(0)(Q(1)(y)) = y >= y = Q(1)(H(0)(R(0)(y))) F(0)(x) = 2x + 1 >= 2x = G(1)(Q(1)(x)) H(0)(F(0)(x)) = 2x + 1 >= 2x + 1 = F(0)(H(0)(R(0)(x))) H(0)(F(1)(y)) = 3y + 2 >= 3y + 2 = F(1)(y) problem: strict: weak: H(0)(G(0)(x)) -> G(0)(x) H(0)(G(1)(y)) -> G(1)(H(0)(y)) Q(0)(x) -> H(0)(Q(0)(x)) Q(1)(H(0)(R(0)(y))) -> H(0)(Q(1)(y)) H(0)(Q(0)(x)) -> Q(0)(x) H(0)(Q(1)(y)) -> Q(1)(H(0)(R(0)(y))) H(0)(F(0)(x)) -> F(0)(H(0)(R(0)(x))) H(0)(F(1)(y)) -> F(1)(y) Matrix Interpretation Processor: dim=2, lab=right interpretation: [2 0] [F(1)](x0) = [0 0]x0, [2 1] [F(0)](x0) = [0 0]x0, [1 0] [R(0)](x0) = [0 0]x0, [2 0] [Q(1)](x0) = [0 0]x0, [1 0] [Q(0)](x0) = [0 0]x0, [2] [G(1)](x0) = x0 + [0], [2 0] [1] [G(0)](x0) = [0 0]x0 + [1], [1 2] [H(0)](x0) = [0 1]x0 orientation: [2 0] [3] [2 0] [1] H(0)(G(0)(x)) = [0 0]x + [1] >= [0 0]x + [1] = G(0)(x) [1 2] [2] [1 2] [2] H(0)(G(1)(y)) = [0 1]y + [0] >= [0 1]y + [0] = G(1)(H(0)(y)) [1 0] [1 0] Q(0)(x) = [0 0]x >= [0 0]x = H(0)(Q(0)(x)) [2 0] [2 0] Q(1)(H(0)(R(0)(y))) = [0 0]y >= [0 0]y = H(0)(Q(1)(y)) [1 0] [1 0] H(0)(Q(0)(x)) = [0 0]x >= [0 0]x = Q(0)(x) [2 0] [2 0] H(0)(Q(1)(y)) = [0 0]y >= [0 0]y = Q(1)(H(0)(R(0)(y))) [2 1] [2 0] H(0)(F(0)(x)) = [0 0]x >= [0 0]x = F(0)(H(0)(R(0)(x))) [2 0] [2 0] H(0)(F(1)(y)) = [0 0]y >= [0 0]y = F(1)(y) problem: strict: weak: H(0)(G(1)(y)) -> G(1)(H(0)(y)) Q(0)(x) -> H(0)(Q(0)(x)) Q(1)(H(0)(R(0)(y))) -> H(0)(Q(1)(y)) H(0)(Q(0)(x)) -> Q(0)(x) H(0)(Q(1)(y)) -> Q(1)(H(0)(R(0)(y))) H(0)(F(0)(x)) -> F(0)(H(0)(R(0)(x))) H(0)(F(1)(y)) -> F(1)(y) Matrix Interpretation Processor: dim=2, lab=right interpretation: [1 0] [1] [F(1)](x0) = [1 0]x0 + [1], [2 0] [F(0)](x0) = [0 0]x0, [1 0] [R(0)](x0) = [0 0]x0, [1 0] [Q(1)](x0) = [0 0]x0, [1 0] [Q(0)](x0) = [0 0]x0, [2] [G(1)](x0) = x0 + [0], [1 2] [H(0)](x0) = [0 1]x0 orientation: [1 2] [2] [1 2] [2] H(0)(G(1)(y)) = [0 1]y + [0] >= [0 1]y + [0] = G(1)(H(0)(y)) [1 0] [1 0] Q(0)(x) = [0 0]x >= [0 0]x = H(0)(Q(0)(x)) [1 0] [1 0] Q(1)(H(0)(R(0)(y))) = [0 0]y >= [0 0]y = H(0)(Q(1)(y)) [1 0] [1 0] H(0)(Q(0)(x)) = [0 0]x >= [0 0]x = Q(0)(x) [1 0] [1 0] H(0)(Q(1)(y)) = [0 0]y >= [0 0]y = Q(1)(H(0)(R(0)(y))) [2 0] [2 0] H(0)(F(0)(x)) = [0 0]x >= [0 0]x = F(0)(H(0)(R(0)(x))) [3 0] [3] [1 0] [1] H(0)(F(1)(y)) = [1 0]y + [1] >= [1 0]y + [1] = F(1)(y) problem: strict: weak: H(0)(G(1)(y)) -> G(1)(H(0)(y)) Q(0)(x) -> H(0)(Q(0)(x)) Q(1)(H(0)(R(0)(y))) -> H(0)(Q(1)(y)) H(0)(Q(0)(x)) -> Q(0)(x) H(0)(Q(1)(y)) -> Q(1)(H(0)(R(0)(y))) H(0)(F(0)(x)) -> F(0)(H(0)(R(0)(x))) Matrix Interpretation Processor: dim=2, lab=right interpretation: [1 0] [0] [F(0)](x0) = [1 0]x0 + [1], [2 0] [R(0)](x0) = [0 0]x0, [1 0] [2] [Q(1)](x0) = [1 0]x0 + [0], [1 0] [Q(0)](x0) = [0 0]x0, [2] [G(1)](x0) = x0 + [0], [1 1] [H(0)](x0) = [0 2]x0 orientation: [1 1] [2] [1 1] [2] H(0)(G(1)(y)) = [0 2]y + [0] >= [0 2]y + [0] = G(1)(H(0)(y)) [1 0] [1 0] Q(0)(x) = [0 0]x >= [0 0]x = H(0)(Q(0)(x)) [2 0] [2] [2 0] [2] Q(1)(H(0)(R(0)(y))) = [2 0]y + [0] >= [2 0]y + [0] = H(0)(Q(1)(y)) [1 0] [1 0] H(0)(Q(0)(x)) = [0 0]x >= [0 0]x = Q(0)(x) [2 0] [2] [2 0] [2] H(0)(Q(1)(y)) = [2 0]y + [0] >= [2 0]y + [0] = Q(1)(H(0)(R(0)(y))) [2 0] [1] [2 0] [0] H(0)(F(0)(x)) = [2 0]x + [2] >= [2 0]x + [1] = F(0)(H(0)(R(0)(x))) problem: strict: weak: H(0)(G(1)(y)) -> G(1)(H(0)(y)) Q(0)(x) -> H(0)(Q(0)(x)) Q(1)(H(0)(R(0)(y))) -> H(0)(Q(1)(y)) H(0)(Q(0)(x)) -> Q(0)(x) H(0)(Q(1)(y)) -> Q(1)(H(0)(R(0)(y))) Matrix Interpretation Processor: dim=2, lab=right interpretation: [1 0] [R(0)](x0) = [0 0]x0, [2 0] [Q(1)](x0) = [0 0]x0, [1 0] [Q(0)](x0) = [0 0]x0, [0] [G(1)](x0) = x0 + [1], [1 2] [H(0)](x0) = [0 1]x0 orientation: [1 2] [2] [1 2] [0] H(0)(G(1)(y)) = [0 1]y + [1] >= [0 1]y + [1] = G(1)(H(0)(y)) [1 0] [1 0] Q(0)(x) = [0 0]x >= [0 0]x = H(0)(Q(0)(x)) [2 0] [2 0] Q(1)(H(0)(R(0)(y))) = [0 0]y >= [0 0]y = H(0)(Q(1)(y)) [1 0] [1 0] H(0)(Q(0)(x)) = [0 0]x >= [0 0]x = Q(0)(x) [2 0] [2 0] H(0)(Q(1)(y)) = [0 0]y >= [0 0]y = Q(1)(H(0)(R(0)(y))) problem: strict: weak: Q(0)(x) -> H(0)(Q(0)(x)) Q(1)(H(0)(R(0)(y))) -> H(0)(Q(1)(y)) H(0)(Q(0)(x)) -> Q(0)(x) H(0)(Q(1)(y)) -> Q(1)(H(0)(R(0)(y))) Shift Processor lab=left (dd): strict: H(F(x,K(x125,x126))) -> H(G(P(x125),Q(x126,x))) H(F(x,K(x125,x126))) -> F(H(R(x)),K(x125,x126)) H(G(P(x125),Q(x126,x))) -> G(P(x125),H(Q(x126,x))) F(H(R(x)),K(x125,x126)) -> G(P(x125),Q(x126,H(R(x)))) G(P(x125),Q(x126,H(R(x)))) -> G(P(x125),H(Q(x126,x))) H(G(P(x125),Q(x126,x))) -> G(P(x125),H(Q(x126,x))) G(P(x125),H(Q(x126,x))) -> G(P(x125),Q(x126,H(R(x)))) F(H(R(x)),K(x125,x126)) -> G(P(x125),Q(x126,H(R(x)))) H(Q(x,H(R(x128)))) -> H(H(Q(x,x128))) H(Q(x,H(R(x128)))) -> Q(x,H(R(H(R(x128))))) H(H(Q(x,x128))) -> H(Q(x,H(R(x128)))) Q(x,H(R(H(R(x128))))) -> H(Q(x,H(R(x128)))) weak: H(F(x,y)) -> F(H(R(x)),y) F(x,K(y,z)) -> G(P(y),Q(z,x)) H(Q(x,y)) -> Q(x,H(R(y))) Q(x,H(R(y))) -> H(Q(x,y)) H(G(x,y)) -> G(x,H(y)) Matrix Interpretation Processor: dim=1 interpretation: [G](x0, x1) = 2x0 + 4x1 + 1, [Q](x0, x1) = x0 + x1, [P](x0) = 2x0 + 1, [K](x0, x1) = 4x0 + 4x1 + 4, [R](x0) = x0, [H](x0) = x0, [F](x0, x1) = 6x0 + 2x1 + 4 orientation: H(F(x,K(x125,x126))) = 6x + 8x125 + 8x126 + 12 >= 4x + 4x125 + 4x126 + 3 = H(G(P(x125),Q(x126,x))) H(F(x,K(x125,x126))) = 6x + 8x125 + 8x126 + 12 >= 6x + 8x125 + 8x126 + 12 = F(H(R(x)),K(x125,x126)) H(G(P(x125),Q(x126,x))) = 4x + 4x125 + 4x126 + 3 >= 4x + 4x125 + 4x126 + 3 = G(P(x125),H(Q(x126,x))) F(H(R(x)),K(x125,x126)) = 6x + 8x125 + 8x126 + 12 >= 4x + 4x125 + 4x126 + 3 = G(P(x125),Q(x126,H(R(x)))) G(P(x125),Q(x126,H(R(x)))) = 4x + 4x125 + 4x126 + 3 >= 4x + 4x125 + 4x126 + 3 = G(P(x125),H(Q(x126,x))) H(G(P(x125),Q(x126,x))) = 4x + 4x125 + 4x126 + 3 >= 4x + 4x125 + 4x126 + 3 = G(P(x125),H(Q(x126,x))) G(P(x125),H(Q(x126,x))) = 4x + 4x125 + 4x126 + 3 >= 4x + 4x125 + 4x126 + 3 = G(P(x125),Q(x126,H(R(x)))) F(H(R(x)),K(x125,x126)) = 6x + 8x125 + 8x126 + 12 >= 4x + 4x125 + 4x126 + 3 = G(P(x125),Q(x126,H(R(x)))) H(Q(x,H(R(x128)))) = x + x128 >= x + x128 = H(H(Q(x,x128))) H(Q(x,H(R(x128)))) = x + x128 >= x + x128 = Q(x,H(R(H(R(x128))))) H(H(Q(x,x128))) = x + x128 >= x + x128 = H(Q(x,H(R(x128)))) Q(x,H(R(H(R(x128))))) = x + x128 >= x + x128 = H(Q(x,H(R(x128)))) H(F(x,y)) = 6x + 2y + 4 >= 6x + 2y + 4 = F(H(R(x)),y) F(x,K(y,z)) = 6x + 8y + 8z + 12 >= 4x + 4y + 4z + 3 = G(P(y),Q(z,x)) H(Q(x,y)) = x + y >= x + y = Q(x,H(R(y))) Q(x,H(R(y))) = x + y >= x + y = H(Q(x,y)) H(G(x,y)) = 2x + 4y + 1 >= 2x + 4y + 1 = G(x,H(y)) problem: strict: H(F(x,K(x125,x126))) -> F(H(R(x)),K(x125,x126)) H(G(P(x125),Q(x126,x))) -> G(P(x125),H(Q(x126,x))) G(P(x125),Q(x126,H(R(x)))) -> G(P(x125),H(Q(x126,x))) H(G(P(x125),Q(x126,x))) -> G(P(x125),H(Q(x126,x))) G(P(x125),H(Q(x126,x))) -> G(P(x125),Q(x126,H(R(x)))) H(Q(x,H(R(x128)))) -> H(H(Q(x,x128))) H(Q(x,H(R(x128)))) -> Q(x,H(R(H(R(x128))))) H(H(Q(x,x128))) -> H(Q(x,H(R(x128)))) Q(x,H(R(H(R(x128))))) -> H(Q(x,H(R(x128)))) weak: H(F(x,y)) -> F(H(R(x)),y) H(Q(x,y)) -> Q(x,H(R(y))) Q(x,H(R(y))) -> H(Q(x,y)) H(G(x,y)) -> G(x,H(y)) Matrix Interpretation Processor: dim=2 interpretation: [1 2] [0] [G](x0, x1) = [0 0]x0 + x1 + [1], [2 0] [2 0] [Q](x0, x1) = [0 0]x0 + [0 0]x1, [1 0] [P](x0) = [0 0]x0, [2 0] [2 0] [1] [K](x0, x1) = [0 2]x0 + [1 0]x1 + [0], [1 0] [R](x0) = [0 0]x0, [1 2] [H](x0) = [0 2]x0, [2 0] [1 1] [F](x0, x1) = [0 0]x0 + [0 0]x1 orientation: [2 0] [2 2] [3 0] [1] [2 0] [2 2] [3 0] [1] H(F(x,K(x125,x126))) = [0 0]x + [0 0]x125 + [0 0]x126 + [0] >= [0 0]x + [0 0]x125 + [0 0]x126 + [0] = F(H(R(x)),K(x125,x126)) [2 0] [1 0] [2 0] [2] [2 0] [1 0] [2 0] [0] H(G(P(x125),Q(x126,x))) = [0 0]x + [0 0]x125 + [0 0]x126 + [2] >= [0 0]x + [0 0]x125 + [0 0]x126 + [1] = G(P(x125),H(Q(x126,x))) [2 0] [1 0] [2 0] [0] [2 0] [1 0] [2 0] [0] G(P(x125),Q(x126,H(R(x)))) = [0 0]x + [0 0]x125 + [0 0]x126 + [1] >= [0 0]x + [0 0]x125 + [0 0]x126 + [1] = G(P(x125),H(Q(x126,x))) [2 0] [1 0] [2 0] [2] [2 0] [1 0] [2 0] [0] H(G(P(x125),Q(x126,x))) = [0 0]x + [0 0]x125 + [0 0]x126 + [2] >= [0 0]x + [0 0]x125 + [0 0]x126 + [1] = G(P(x125),H(Q(x126,x))) [2 0] [1 0] [2 0] [0] [2 0] [1 0] [2 0] [0] G(P(x125),H(Q(x126,x))) = [0 0]x + [0 0]x125 + [0 0]x126 + [1] >= [0 0]x + [0 0]x125 + [0 0]x126 + [1] = G(P(x125),Q(x126,H(R(x)))) [2 0] [2 0] [2 0] [2 0] H(Q(x,H(R(x128)))) = [0 0]x + [0 0]x128 >= [0 0]x + [0 0]x128 = H(H(Q(x,x128))) [2 0] [2 0] [2 0] [2 0] H(Q(x,H(R(x128)))) = [0 0]x + [0 0]x128 >= [0 0]x + [0 0]x128 = Q(x,H(R(H(R(x128))))) [2 0] [2 0] [2 0] [2 0] H(H(Q(x,x128))) = [0 0]x + [0 0]x128 >= [0 0]x + [0 0]x128 = H(Q(x,H(R(x128)))) [2 0] [2 0] [2 0] [2 0] Q(x,H(R(H(R(x128))))) = [0 0]x + [0 0]x128 >= [0 0]x + [0 0]x128 = H(Q(x,H(R(x128)))) [2 0] [1 1] [2 0] [1 1] H(F(x,y)) = [0 0]x + [0 0]y >= [0 0]x + [0 0]y = F(H(R(x)),y) [2 0] [2 0] [2 0] [2 0] H(Q(x,y)) = [0 0]x + [0 0]y >= [0 0]x + [0 0]y = Q(x,H(R(y))) [2 0] [2 0] [2 0] [2 0] Q(x,H(R(y))) = [0 0]x + [0 0]y >= [0 0]x + [0 0]y = H(Q(x,y)) [1 2] [1 2] [2] [1 2] [1 2] [0] H(G(x,y)) = [0 0]x + [0 2]y + [2] >= [0 0]x + [0 2]y + [1] = G(x,H(y)) problem: strict: H(F(x,K(x125,x126))) -> F(H(R(x)),K(x125,x126)) G(P(x125),Q(x126,H(R(x)))) -> G(P(x125),H(Q(x126,x))) G(P(x125),H(Q(x126,x))) -> G(P(x125),Q(x126,H(R(x)))) H(Q(x,H(R(x128)))) -> H(H(Q(x,x128))) H(Q(x,H(R(x128)))) -> Q(x,H(R(H(R(x128))))) H(H(Q(x,x128))) -> H(Q(x,H(R(x128)))) Q(x,H(R(H(R(x128))))) -> H(Q(x,H(R(x128)))) weak: H(F(x,y)) -> F(H(R(x)),y) H(Q(x,y)) -> Q(x,H(R(y))) Q(x,H(R(y))) -> H(Q(x,y)) Matrix Interpretation Processor: dim=2 interpretation: [1 0] [1 0] [0] [G](x0, x1) = [0 0]x0 + [0 0]x1 + [3], [1 0] [2 0] [Q](x0, x1) = [0 0]x0 + [0 0]x1, [1 0] [P](x0) = [0 0]x0, [1 1] [1 3] [K](x0, x1) = [0 1]x0 + [2 0]x1, [1 0] [R](x0) = [0 0]x0, [1 2] [H](x0) = [0 2]x0, [2 0] [1 1] [0] [F](x0, x1) = [0 0]x0 + [0 0]x1 + [1] orientation: [2 0] [1 2] [3 3] [2] [2 0] [1 2] [3 3] [0] H(F(x,K(x125,x126))) = [0 0]x + [0 0]x125 + [0 0]x126 + [2] >= [0 0]x + [0 0]x125 + [0 0]x126 + [1] = F(H(R(x)),K(x125,x126)) [2 0] [1 0] [1 0] [0] [2 0] [1 0] [1 0] [0] G(P(x125),Q(x126,H(R(x)))) = [0 0]x + [0 0]x125 + [0 0]x126 + [3] >= [0 0]x + [0 0]x125 + [0 0]x126 + [3] = G(P(x125),H(Q(x126,x))) [2 0] [1 0] [1 0] [0] [2 0] [1 0] [1 0] [0] G(P(x125),H(Q(x126,x))) = [0 0]x + [0 0]x125 + [0 0]x126 + [3] >= [0 0]x + [0 0]x125 + [0 0]x126 + [3] = G(P(x125),Q(x126,H(R(x)))) [1 0] [2 0] [1 0] [2 0] H(Q(x,H(R(x128)))) = [0 0]x + [0 0]x128 >= [0 0]x + [0 0]x128 = H(H(Q(x,x128))) [1 0] [2 0] [1 0] [2 0] H(Q(x,H(R(x128)))) = [0 0]x + [0 0]x128 >= [0 0]x + [0 0]x128 = Q(x,H(R(H(R(x128))))) [1 0] [2 0] [1 0] [2 0] H(H(Q(x,x128))) = [0 0]x + [0 0]x128 >= [0 0]x + [0 0]x128 = H(Q(x,H(R(x128)))) [1 0] [2 0] [1 0] [2 0] Q(x,H(R(H(R(x128))))) = [0 0]x + [0 0]x128 >= [0 0]x + [0 0]x128 = H(Q(x,H(R(x128)))) [2 0] [1 1] [2] [2 0] [1 1] [0] H(F(x,y)) = [0 0]x + [0 0]y + [2] >= [0 0]x + [0 0]y + [1] = F(H(R(x)),y) [1 0] [2 0] [1 0] [2 0] H(Q(x,y)) = [0 0]x + [0 0]y >= [0 0]x + [0 0]y = Q(x,H(R(y))) [1 0] [2 0] [1 0] [2 0] Q(x,H(R(y))) = [0 0]x + [0 0]y >= [0 0]x + [0 0]y = H(Q(x,y)) problem: strict: G(P(x125),Q(x126,H(R(x)))) -> G(P(x125),H(Q(x126,x))) G(P(x125),H(Q(x126,x))) -> G(P(x125),Q(x126,H(R(x)))) H(Q(x,H(R(x128)))) -> H(H(Q(x,x128))) H(Q(x,H(R(x128)))) -> Q(x,H(R(H(R(x128))))) H(H(Q(x,x128))) -> H(Q(x,H(R(x128)))) Q(x,H(R(H(R(x128))))) -> H(Q(x,H(R(x128)))) weak: H(Q(x,y)) -> Q(x,H(R(y))) Q(x,H(R(y))) -> H(Q(x,y)) Shift Processor (ldh) lab=left (force): strict: weak: Decreasing Processor: The following diagrams are decreasing: peak: H(G(P(x125),Q(x126,x))) <-1|0[1,0,0,0,0,0,0,0]- H(F(x,K(x125,x126))) -0| [1,0,0,0,0,0,0,0]-> F(H(R(x)),K(x125,x126)) joins: H(G(P(x125),Q(x126,x))) -4|[0,0,0,0,0,0,0,0]-> G(P(x125),H(Q(x126,x))) F(H(R(x)),K(x125,x126)) -1|[0,0,0,0,0,0,0,0]-> G(P(x125),Q(x126,H(R(x)))) -3| 1[0,3,0,0,2,2,2,0]-> G(P(x125),H(Q(x126,x))) peak: H(H(Q(x,x128))) <-3|0[1,0,0,0,0,0,0,0]- H(Q(x,H(R(x128)))) -2| [1,0,0,0,0,0,0,0]-> Q(x,H(R(H(R(x128))))) joins: H(H(Q(x,x128))) -2|0[1,0,0,0,0,0,0,0]-> H(Q(x,H(R(x128)))) Q(x,H(R(H(R(x128))))) -3|[1,0,0,0,0,0,0,0]-> H(Q(x,H(R(x128)))) Qed