### CSI-0.1

``````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) = x0,

[P(0)](x0) = x0 + 1,

[K(0)](x0) = 2x0 + 3,

[F(1)](x0) = x0,

[F(0)](x0) = 2x0,

[R(0)](x0) = x0,

[Q(1)](x0) = 2x0,

[Q(0)](x0) = x0,

[G(1)](x0) = x0,

[G(0)](x0) = 2x0,

[H(0)](x0) = x0
orientation:
H(0)(G(0)(x)) = 2x >= 2x = G(0)(x)

H(0)(G(1)(y)) = y >= y = G(1)(H(0)(y))

Q(0)(x) = x >= x = H(0)(Q(0)(x))

Q(1)(H(0)(R(0)(y))) = 2y >= 2y = H(0)(Q(1)(y))

H(0)(Q(0)(x)) = x >= x = Q(0)(x)

H(0)(Q(1)(y)) = 2y >= 2y = Q(1)(H(0)(R(0)(y)))

F(0)(x) = 2x >= 2x = G(1)(Q(1)(x))

F(1)(K(0)(y)) = 2y + 3 >= 2y + 2 = G(0)(P(0)(y))

F(1)(K(1)(z)) = z >= z = G(1)(Q(0)(z))

H(0)(F(0)(x)) = 2x >= 2x = 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))
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) = x0 + 1,

[F(1)](x0) = x0 + 1,

[F(0)](x0) = x0 + 3,

[R(0)](x0) = x0,

[Q(1)](x0) = x0,

[Q(0)](x0) = x0 + 1,

[G(1)](x0) = x0,

[G(0)](x0) = 2x0 + 1,

[H(0)](x0) = x0
orientation:
H(0)(G(0)(x)) = 2x + 1 >= 2x + 1 = G(0)(x)

H(0)(G(1)(y)) = y >= y = G(1)(H(0)(y))

Q(0)(x) = x + 1 >= x + 1 = 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 + 1 >= x + 1 = Q(0)(x)

H(0)(Q(1)(y)) = y >= y = Q(1)(H(0)(R(0)(y)))

F(0)(x) = x + 3 >= x = G(1)(Q(1)(x))

F(1)(K(1)(z)) = z + 2 >= z + 1 = G(1)(Q(0)(z))

H(0)(F(0)(x)) = x + 3 >= x + 3 = F(0)(H(0)(R(0)(x)))

H(0)(F(1)(y)) = y + 1 >= y + 1 = 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:
[1 0]     [2]
[F(1)](x0) = [0 0]x0 + [0],

[1 0]
[F(0)](x0) = [1 1]x0,

[1 1]
[R(0)](x0) = [0 0]x0,

[2 2]
[Q(1)](x0) = [0 0]x0,

[2 0]
[Q(0)](x0) = [0 0]x0,

[G(1)](x0) = x0,

[1 0]     [0]
[G(0)](x0) = [1 1]x0 + [1],

[1 2]
[H(0)](x0) = [0 2]x0
orientation:
[3 2]    [2]    [1 0]    [0]
H(0)(G(0)(x)) = [2 2]x + [2] >= [1 1]x + [1] = G(0)(x)

[1 2]     [1 2]
H(0)(G(1)(y)) = [0 2]y >= [0 2]y = G(1)(H(0)(y))

[2 0]     [2 0]
Q(0)(x) = [0 0]x >= [0 0]x = H(0)(Q(0)(x))

[2 2]     [2 2]
Q(1)(H(0)(R(0)(y))) = [0 0]y >= [0 0]y = H(0)(Q(1)(y))

[2 0]     [2 0]
H(0)(Q(0)(x)) = [0 0]x >= [0 0]x = Q(0)(x)

[2 2]     [2 2]
H(0)(Q(1)(y)) = [0 0]y >= [0 0]y = Q(1)(H(0)(R(0)(y)))

[3 2]     [1 1]
H(0)(F(0)(x)) = [2 2]x >= [1 1]x = F(0)(H(0)(R(0)(x)))

[1 0]    [2]    [1 0]    [2]
H(0)(F(1)(y)) = [0 0]y + [0] >= [0 0]y + [0] = 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]
[F(1)](x0) = [0 0]x0,

[F(0)](x0) = x0,

[1 1]
[R(0)](x0) = [0 0]x0,

[2 2]
[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 2]     [2 2]
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 2]     [2 2]
H(0)(Q(1)(y)) = [0 0]y >= [0 0]y = Q(1)(H(0)(R(0)(y)))

[1 2]     [1 1]
H(0)(F(0)(x)) = [0 1]x >= [0 0]x = F(0)(H(0)(R(0)(x)))

[1 0]     [1 0]
H(0)(F(1)(y)) = [0 0]y >= [0 0]y = F(1)(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)))
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]     [0]
[F(1)](x0) = [1 0]x0 + [1],

[1 2]
[F(0)](x0) = [1 1]x0,

[2 0]
[R(0)](x0) = [0 0]x0,

[1 0]
[Q(1)](x0) = [1 0]x0,

[1 0]     [2]
[Q(0)](x0) = [0 0]x0 + [0],

[1 1]
[H(0)](x0) = [0 2]x0
orientation:
[1 0]    [2]    [1 0]    [2]
Q(0)(x) = [0 0]x + [0] >= [0 0]x + [0] = H(0)(Q(0)(x))

[2 0]     [2 0]
Q(1)(H(0)(R(0)(y))) = [2 0]y >= [2 0]y = H(0)(Q(1)(y))

[1 0]    [2]    [1 0]    [2]
H(0)(Q(0)(x)) = [0 0]x + [0] >= [0 0]x + [0] = Q(0)(x)

[2 0]     [2 0]
H(0)(Q(1)(y)) = [2 0]y >= [2 0]y = Q(1)(H(0)(R(0)(y)))

[2 3]     [2 0]
H(0)(F(0)(x)) = [2 2]x >= [2 0]x = F(0)(H(0)(R(0)(x)))

[3 0]    [1]    [2 0]    [0]
H(0)(F(1)(y)) = [2 0]y + [2] >= [1 0]y + [1] = F(1)(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)))
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],

[1 0]
[R(0)](x0) = [0 0]x0,

[1 0]
[Q(1)](x0) = [0 0]x0,

[2 0]
[Q(0)](x0) = [0 0]x0,

[1 1]
[H(0)](x0) = [0 1]x0
orientation:
[2 0]     [2 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))

[2 0]     [2 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]    [1]    [1 0]    [0]
H(0)(F(0)(x)) = [1 0]x + [1] >= [1 0]x + [1] = F(0)(H(0)(R(0)(x)))
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) = 7x0 + 2x1,

[Q](x0, x1) = x0 + 2x1,

[P](x0) = x0,

[K](x0, x1) = 7x0 + 3x1 + 6,

[R](x0) = x0,

[H](x0) = x0,

[F](x0, x1) = 4x0 + x1 + 3
orientation:
H(F(x,K(x125,x126))) = 4x + 7x125 + 3x126 + 9 >= 4x + 7x125 + 2x126 = H(G(P(x125),Q(x126,x)))

H(F(x,K(x125,x126))) = 4x + 7x125 + 3x126 + 9 >= 4x + 7x125 + 3x126 + 9 = F(H(R(x)),K(x125,x126))

H(G(P(x125),Q(x126,x))) = 4x + 7x125 + 2x126 >= 4x + 7x125 + 2x126 = G(P(x125),H(Q(x126,x)))

F(H(R(x)),K(x125,x126)) = 4x + 7x125 + 3x126 + 9 >= 4x + 7x125 + 2x126 = G(P(x125),Q(x126,H(R(x))))

G(P(x125),Q(x126,H(R(x)))) = 4x + 7x125 + 2x126 >= 4x + 7x125 + 2x126 = G(P(x125),H(Q(x126,x)))

H(G(P(x125),Q(x126,x))) = 4x + 7x125 + 2x126 >= 4x + 7x125 + 2x126 = G(P(x125),H(Q(x126,x)))

G(P(x125),H(Q(x126,x))) = 4x + 7x125 + 2x126 >= 4x + 7x125 + 2x126 = G(P(x125),Q(x126,H(R(x))))

F(H(R(x)),K(x125,x126)) = 4x + 7x125 + 3x126 + 9 >= 4x + 7x125 + 2x126 = G(P(x125),Q(x126,H(R(x))))

H(Q(x,H(R(x128)))) = x + 2x128 >= x + 2x128 = H(H(Q(x,x128)))

H(Q(x,H(R(x128)))) = x + 2x128 >= x + 2x128 = Q(x,H(R(H(R(x128)))))

H(H(Q(x,x128))) = x + 2x128 >= x + 2x128 = H(Q(x,H(R(x128))))

Q(x,H(R(H(R(x128))))) = x + 2x128 >= x + 2x128 = H(Q(x,H(R(x128))))

H(F(x,y)) = 4x + y + 3 >= 4x + y + 3 = F(H(R(x)),y)

F(x,K(y,z)) = 4x + 7y + 3z + 9 >= 4x + 7y + 2z = G(P(y),Q(z,x))

H(Q(x,y)) = x + 2y >= x + 2y = Q(x,H(R(y)))

Q(x,H(R(y))) = x + 2y >= x + 2y = H(Q(x,y))

H(G(x,y)) = 7x + 2y >= 7x + 2y = 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:
[2 1]          [0]
[G](x0, x1) = [0 1]x0 + x1 + [1],

[1 0]     [2 0]
[Q](x0, x1) = [0 0]x0 + [0 0]x1,

[P](x0) = x0,

[1 0]     [1 0]
[K](x0, x1) = [0 0]x0 + [0 0]x1,

[1 0]
[R](x0) = [0 0]x0,

[1 2]
[H](x0) = [0 2]x0,

[2 0]     [2 2]     [2]
[F](x0, x1) = [0 1]x0 + [0 0]x1 + [0]
orientation:
[2 2]    [2 0]       [2 0]       [2]    [2 0]    [2 0]       [2 0]       [2]
H(F(x,K(x125,x126))) = [0 2]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]    [2 3]       [1 0]       [2]    [2 0]    [2 1]       [1 0]       [0]
H(G(P(x125),Q(x126,x))) = [0 0]x + [0 2]x125 + [0 0]x126 + [2] >= [0 0]x + [0 1]x125 + [0 0]x126 + [1] = G(P(x125),H(Q(x126,x)))

[2 0]    [2 1]       [1 0]       [0]    [2 0]    [2 1]       [1 0]       [0]
G(P(x125),Q(x126,H(R(x)))) = [0 0]x + [0 1]x125 + [0 0]x126 + [1] >= [0 0]x + [0 1]x125 + [0 0]x126 + [1] = G(P(x125),H(Q(x126,x)))

[2 0]    [2 3]       [1 0]       [2]    [2 0]    [2 1]       [1 0]       [0]
H(G(P(x125),Q(x126,x))) = [0 0]x + [0 2]x125 + [0 0]x126 + [2] >= [0 0]x + [0 1]x125 + [0 0]x126 + [1] = G(P(x125),H(Q(x126,x)))

[2 0]    [2 1]       [1 0]       [0]    [2 0]    [2 1]       [1 0]       [0]
G(P(x125),H(Q(x126,x))) = [0 0]x + [0 1]x125 + [0 0]x126 + [1] >= [0 0]x + [0 1]x125 + [0 0]x126 + [1] = 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 2]    [2 2]    [2]    [2 0]    [2 2]    [2]
H(F(x,y)) = [0 2]x + [0 0]y + [0] >= [0 0]x + [0 0]y + [0] = 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))

[2 3]    [1 2]    [2]    [2 1]    [1 2]    [0]
H(G(x,y)) = [0 2]x + [0 2]y + [2] >= [0 1]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]
[G](x0, x1) = [0 0]x0 + [1 0]x1,

[2 0]     [1 2]
[Q](x0, x1) = [0 0]x0 + [0 0]x1,

[2 0]
[P](x0) = [0 0]x0,

[1 1]     [1 0]     [0]
[K](x0, x1) = [0 0]x0 + [0 0]x1 + [1],

[1 2]
[R](x0) = [0 0]x0,

[1 2]
[H](x0) = [0 3]x0,

[1 2]     [2 0]
[F](x0, x1) = [0 0]x0 + [0 1]x1
orientation:
[1 2]    [2 2]       [2 0]       [2]    [1 2]    [2 2]       [2 0]       [0]
H(F(x,K(x125,x126))) = [0 0]x + [0 0]x125 + [0 0]x126 + [3] >= [0 0]x + [0 0]x125 + [0 0]x126 + [1] = F(H(R(x)),K(x125,x126))

[1 2]    [2 0]       [2 0]        [1 2]    [2 0]       [2 0]
G(P(x125),Q(x126,H(R(x)))) = [1 2]x + [0 0]x125 + [2 0]x126 >= [1 2]x + [0 0]x125 + [2 0]x126 = G(P(x125),H(Q(x126,x)))

[1 2]    [2 0]       [2 0]        [1 2]    [2 0]       [2 0]
G(P(x125),H(Q(x126,x))) = [1 2]x + [0 0]x125 + [2 0]x126 >= [1 2]x + [0 0]x125 + [2 0]x126 = G(P(x125),Q(x126,H(R(x))))

[2 0]    [1 2]        [2 0]    [1 2]
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]    [1 2]        [2 0]    [1 2]
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]    [1 2]        [2 0]    [1 2]
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]    [1 2]        [2 0]    [1 2]
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))))

[1 2]    [2 2]     [1 2]    [2 0]
H(F(x,y)) = [0 0]x + [0 3]y >= [0 0]x + [0 1]y = F(H(R(x)),y)

[2 0]    [1 2]     [2 0]    [1 2]
H(Q(x,y)) = [0 0]x + [0 0]y >= [0 0]x + [0 0]y = Q(x,H(R(y)))

[2 0]    [1 2]     [2 0]    [1 2]
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(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:
[2 0]     [1 0]
[G](x0, x1) = [0 0]x0 + [1 0]x1,

[1 0]     [2 2]
[Q](x0, x1) = [0 0]x0 + [0 0]x1,

[2 0]
[P](x0) = [0 0]x0,

[1 1]
[R](x0) = [0 0]x0,

[1 2]
[H](x0) = [0 2]x0,

[1 1]     [1 0]     [0]
[F](x0, x1) = [0 0]x0 + [0 0]x1 + [1]
orientation:
[2 2]    [4 0]       [1 0]        [2 2]    [4 0]       [1 0]
G(P(x125),Q(x126,H(R(x)))) = [2 2]x + [0 0]x125 + [1 0]x126 >= [2 2]x + [0 0]x125 + [1 0]x126 = G(P(x125),H(Q(x126,x)))

[2 2]    [4 0]       [1 0]        [2 2]    [4 0]       [1 0]
G(P(x125),H(Q(x126,x))) = [2 2]x + [0 0]x125 + [1 0]x126 >= [2 2]x + [0 0]x125 + [1 0]x126 = G(P(x125),Q(x126,H(R(x))))

[1 0]    [2 2]        [1 0]    [2 2]
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 2]        [1 0]    [2 2]
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 2]        [1 0]    [2 2]
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 2]        [1 0]    [2 2]
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))))

[1 1]    [1 0]    [2]    [1 1]    [1 0]    [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 2]     [1 0]    [2 2]
H(Q(x,y)) = [0 0]x + [0 0]y >= [0 0]x + [0 0]y = Q(x,H(R(y)))

[1 0]    [2 2]     [1 0]    [2 2]
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]- H(F(x,K(x125,x126))) -0|
[1,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]-> G(P(x125),H(Q(x126,x)))
F(H(R(x)),K(x125,x126)) -1|[0,0,0,0,0,0,0]-> G(P(x125),Q(x126,H(R(x)))) -3|
1[0,0,0,0,0,0,0]->
G(P(x125),H(Q(x126,x)))
peak:
H(H(Q(x,x128))) <-3|0[1,0,0,0,0,0,0]- H(Q(x,H(R(x128)))) -2|
[1,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]-> H(Q(x,H(R(x128))))
Q(x,H(R(H(R(x128))))) -3|[1,0,0,0,0,0,0]-> H(Q(x,H(R(x128))))
Qed
``````
Nach oben scrollen