### CSI-0.1

``````Problem:
-(0(),0()) -> 0()
-(s(x),0()) -> s(x)
-(x,s(y)) -> -(d(x),y)
d(s(x)) -> x
-(s(x),s(y)) -> -(x,y)
-(d(x),y) -> -(x,s(y))

Proof:
Church Rosser Transformation Processor (star):

strict:

weak:
-(0)(d(0)(x)) -> -(0)(x)
-(1)(y) -> -(1)(s(0)(y))
-(0)(s(0)(x)) -> -(0)(x)
-(1)(s(0)(y)) -> -(1)(y)
d(0)(s(0)(x)) -> x
-(0)(x) -> -(0)(d(0)(x))
-(0)(s(0)(x)) -> s(0)(x)
critical peaks: 5
-(d(s(x)),y) <-2|[]- -(s(x),s(y)) -4|[]-> -(x,y)
-(d(d(x)),x125) <-2|[]- -(d(x),s(x125)) -5|[]-> -(x,s(s(x125)))
-(x126,y) <-3|0[]- -(d(s(x126)),y) -5|[]-> -(s(x126),s(y))
-(x127,y) <-4|[]- -(s(x127),s(y)) -2|[]-> -(d(s(x127)),y)
-(x129,s(s(y))) <-5|[]- -(d(x129),s(y)) -2|[]-> -(d(d(x129)),y)
Matrix Interpretation Processor: dim=1, lab=right

interpretation:
[s(0)](x0) = x0,

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

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

[-(0)](x0) = x0 + 1
orientation:
-(0)(d(0)(x)) = x + 1 >= x + 1 = -(0)(x)

-(1)(y) = 2y >= 2y = -(1)(s(0)(y))

-(0)(s(0)(x)) = x + 1 >= x + 1 = -(0)(x)

-(1)(s(0)(y)) = 2y >= 2y = -(1)(y)

d(0)(s(0)(x)) = x >= x = x

-(0)(x) = x + 1 >= x + 1 = -(0)(d(0)(x))

-(0)(s(0)(x)) = x + 1 >= x = s(0)(x)
problem:

strict:

weak:
-(0)(d(0)(x)) -> -(0)(x)
-(1)(y) -> -(1)(s(0)(y))
-(0)(s(0)(x)) -> -(0)(x)
-(1)(s(0)(y)) -> -(1)(y)
d(0)(s(0)(x)) -> x
-(0)(x) -> -(0)(d(0)(x))
Matrix Interpretation Processor: dim=2, lab=right

interpretation:
[1 0]     [0]
[s(0)](x0) = [2 2]x0 + [2],

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

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

[1 1]
[-(0)](x0) = [0 0]x0
orientation:
[1 1]     [1 1]
-(0)(d(0)(x)) = [0 0]x >= [0 0]x = -(0)(x)

[1 0]     [1 0]
-(1)(y) = [0 0]y >= [0 0]y = -(1)(s(0)(y))

[3 2]    [2]    [1 1]
-(0)(s(0)(x)) = [0 0]x + [0] >= [0 0]x = -(0)(x)

[1 0]     [1 0]
-(1)(s(0)(y)) = [0 0]y >= [0 0]y = -(1)(y)

[1 0]    [0]
d(0)(s(0)(x)) = [2 2]x + [2] >= x = x

[1 1]     [1 1]
-(0)(x) = [0 0]x >= [0 0]x = -(0)(d(0)(x))
problem:

strict:

weak:
-(0)(d(0)(x)) -> -(0)(x)
-(1)(y) -> -(1)(s(0)(y))
-(1)(s(0)(y)) -> -(1)(y)
d(0)(s(0)(x)) -> x
-(0)(x) -> -(0)(d(0)(x))
Shift Processor lab=left (dd):

strict:
-(s(x),s(y)) -> -(d(s(x)),y)
-(s(x),s(y)) -> -(x,y)
-(d(s(x)),y) -> -(x,y)
-(d(x),s(x125)) -> -(d(d(x)),x125)
-(d(x),s(x125)) -> -(x,s(s(x125)))
-(d(d(x)),x125) -> -(d(x),s(x125))
-(x,s(s(x125))) -> -(d(x),s(x125))
-(d(s(x126)),y) -> -(x126,y)
-(d(s(x126)),y) -> -(s(x126),s(y))
-(s(x126),s(y)) -> -(x126,y)
-(s(x127),s(y)) -> -(x127,y)
-(s(x127),s(y)) -> -(d(s(x127)),y)
-(d(s(x127)),y) -> -(x127,y)
-(d(x129),s(y)) -> -(x129,s(s(y)))
-(d(x129),s(y)) -> -(d(d(x129)),y)
-(x129,s(s(y))) -> -(d(x129),s(y))
-(d(d(x129)),y) -> -(d(x129),s(y))
weak:
-(0(),0()) -> 0()
-(s(x),0()) -> s(x)
-(x,s(y)) -> -(d(x),y)
d(s(x)) -> x
-(s(x),s(y)) -> -(x,y)
-(d(x),y) -> -(x,s(y))
Matrix Interpretation Processor: dim=1

interpretation:
[d](x0) = x0,

[s](x0) = x0,

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

[0] = 2
orientation:
-(s(x),s(y)) = 2x + 2y >= 2x + 2y = -(d(s(x)),y)

-(s(x),s(y)) = 2x + 2y >= 2x + 2y = -(x,y)

-(d(s(x)),y) = 2x + 2y >= 2x + 2y = -(x,y)

-(d(x),s(x125)) = 2x + 2x125 >= 2x + 2x125 = -(d(d(x)),x125)

-(d(x),s(x125)) = 2x + 2x125 >= 2x + 2x125 = -(x,s(s(x125)))

-(d(d(x)),x125) = 2x + 2x125 >= 2x + 2x125 = -(d(x),s(x125))

-(x,s(s(x125))) = 2x + 2x125 >= 2x + 2x125 = -(d(x),s(x125))

-(d(s(x126)),y) = 2x126 + 2y >= 2x126 + 2y = -(x126,y)

-(d(s(x126)),y) = 2x126 + 2y >= 2x126 + 2y = -(s(x126),s(y))

-(s(x126),s(y)) = 2x126 + 2y >= 2x126 + 2y = -(x126,y)

-(s(x127),s(y)) = 2x127 + 2y >= 2x127 + 2y = -(x127,y)

-(s(x127),s(y)) = 2x127 + 2y >= 2x127 + 2y = -(d(s(x127)),y)

-(d(s(x127)),y) = 2x127 + 2y >= 2x127 + 2y = -(x127,y)

-(d(x129),s(y)) = 2x129 + 2y >= 2x129 + 2y = -(x129,s(s(y)))

-(d(x129),s(y)) = 2x129 + 2y >= 2x129 + 2y = -(d(d(x129)),y)

-(x129,s(s(y))) = 2x129 + 2y >= 2x129 + 2y = -(d(x129),s(y))

-(d(d(x129)),y) = 2x129 + 2y >= 2x129 + 2y = -(d(x129),s(y))

-(0(),0()) = 8 >= 2 = 0()

-(s(x),0()) = 2x + 4 >= x = s(x)

-(x,s(y)) = 2x + 2y >= 2x + 2y = -(d(x),y)

d(s(x)) = x >= x = x

-(d(x),y) = 2x + 2y >= 2x + 2y = -(x,s(y))
problem:

strict:
-(s(x),s(y)) -> -(d(s(x)),y)
-(s(x),s(y)) -> -(x,y)
-(d(s(x)),y) -> -(x,y)
-(d(x),s(x125)) -> -(d(d(x)),x125)
-(d(x),s(x125)) -> -(x,s(s(x125)))
-(d(d(x)),x125) -> -(d(x),s(x125))
-(x,s(s(x125))) -> -(d(x),s(x125))
-(d(s(x126)),y) -> -(x126,y)
-(d(s(x126)),y) -> -(s(x126),s(y))
-(s(x126),s(y)) -> -(x126,y)
-(s(x127),s(y)) -> -(x127,y)
-(s(x127),s(y)) -> -(d(s(x127)),y)
-(d(s(x127)),y) -> -(x127,y)
-(d(x129),s(y)) -> -(x129,s(s(y)))
-(d(x129),s(y)) -> -(d(d(x129)),y)
-(x129,s(s(y))) -> -(d(x129),s(y))
-(d(d(x129)),y) -> -(d(x129),s(y))
weak:
-(x,s(y)) -> -(d(x),y)
d(s(x)) -> x
-(s(x),s(y)) -> -(x,y)
-(d(x),y) -> -(x,s(y))
Matrix Interpretation Processor: dim=1

interpretation:
[d](x0) = x0 + 2,

[s](x0) = x0 + 1,

[-](x0, x1) = x0 + 2x1
orientation:
-(s(x),s(y)) = x + 2y + 3 >= x + 2y + 3 = -(d(s(x)),y)

-(s(x),s(y)) = x + 2y + 3 >= x + 2y = -(x,y)

-(d(s(x)),y) = x + 2y + 3 >= x + 2y = -(x,y)

-(d(x),s(x125)) = x + 2x125 + 4 >= x + 2x125 + 4 = -(d(d(x)),x125)

-(d(x),s(x125)) = x + 2x125 + 4 >= x + 2x125 + 4 = -(x,s(s(x125)))

-(d(d(x)),x125) = x + 2x125 + 4 >= x + 2x125 + 4 = -(d(x),s(x125))

-(x,s(s(x125))) = x + 2x125 + 4 >= x + 2x125 + 4 = -(d(x),s(x125))

-(d(s(x126)),y) = x126 + 2y + 3 >= x126 + 2y = -(x126,y)

-(d(s(x126)),y) = x126 + 2y + 3 >= x126 + 2y + 3 = -(s(x126),s(y))

-(s(x126),s(y)) = x126 + 2y + 3 >= x126 + 2y = -(x126,y)

-(s(x127),s(y)) = x127 + 2y + 3 >= x127 + 2y = -(x127,y)

-(s(x127),s(y)) = x127 + 2y + 3 >= x127 + 2y + 3 = -(d(s(x127)),y)

-(d(s(x127)),y) = x127 + 2y + 3 >= x127 + 2y = -(x127,y)

-(d(x129),s(y)) = x129 + 2y + 4 >= x129 + 2y + 4 = -(x129,s(s(y)))

-(d(x129),s(y)) = x129 + 2y + 4 >= x129 + 2y + 4 = -(d(d(x129)),y)

-(x129,s(s(y))) = x129 + 2y + 4 >= x129 + 2y + 4 = -(d(x129),s(y))

-(d(d(x129)),y) = x129 + 2y + 4 >= x129 + 2y + 4 = -(d(x129),s(y))

-(x,s(y)) = x + 2y + 2 >= x + 2y + 2 = -(d(x),y)

d(s(x)) = x + 3 >= x = x

-(d(x),y) = x + 2y + 2 >= x + 2y + 2 = -(x,s(y))
problem:

strict:
-(s(x),s(y)) -> -(d(s(x)),y)
-(d(x),s(x125)) -> -(d(d(x)),x125)
-(d(x),s(x125)) -> -(x,s(s(x125)))
-(d(d(x)),x125) -> -(d(x),s(x125))
-(x,s(s(x125))) -> -(d(x),s(x125))
-(d(s(x126)),y) -> -(s(x126),s(y))
-(s(x127),s(y)) -> -(d(s(x127)),y)
-(d(x129),s(y)) -> -(x129,s(s(y)))
-(d(x129),s(y)) -> -(d(d(x129)),y)
-(x129,s(s(y))) -> -(d(x129),s(y))
-(d(d(x129)),y) -> -(d(x129),s(y))
weak:
-(x,s(y)) -> -(d(x),y)
-(d(x),y) -> -(x,s(y))
Shift Processor (ldh) lab=left (force):

strict:

weak:

Rule Labeling Processor:

strict:

weak:

rule labeling (left):
-(0(),0()) -> 0(): 0
-(s(x),0()) -> s(x): 0
-(x,s(y)) -> -(d(x),y): 0
d(s(x)) -> x: 0
-(s(x),s(y)) -> -(x,y): 1
-(d(x),y) -> -(x,s(y)): 2
Decreasing Processor:
The following diagrams are decreasing:
peak:
-(d(s(x)),y) <-2|[0,1,0,0]- -(s(x),s(y)) -4|[1,1,0,0]-> -(x,y)
joins:
-(d(s(x)),y) -3|0[0,1,1,0]-> -(x,y)

peak:
-(d(d(x)),x125) <-2|[0,1,0,0]- -(d(x),s(x125)) -5|[2,1,0,0]-> -(x,s(s(x125)))
joins:
-(d(d(x)),x125) -5|[2,1,0,0]-> -(d(x),s(x125))
-(x,s(s(x125))) -2|[0,1,0,0]-> -(d(x),s(x125))
peak:
-(x126,y) <-3|0[0,1,1,0]- -(d(s(x126)),y) -5|[2,1,0,0]-> -(s(x126),s(y))
joins:

-(s(x126),s(y)) -4|[1,1,0,0]-> -(x126,y)
peak:
-(x127,y) <-4|[1,1,0,0]- -(s(x127),s(y)) -2|[0,1,0,0]-> -(d(s(x127)),y)
joins:

-(d(s(x127)),y) -3|0[0,1,1,0]-> -(x127,y)
peak:
-(x129,s(s(y))) <-5|[2,1,0,0]- -(d(x129),s(y)) -2|[0,1,0,0]-> -(d(d(x129)),y)
joins:
-(x129,s(s(y))) -2|[0,1,0,0]-> -(d(x129),s(y))
-(d(d(x129)),y) -5|[2,1,0,0]-> -(d(x129),s(y))
Qed
``````
Nach oben scrollen