### CSI-0.1

``````Problem:
nats() -> :(0(),inc(nats()))
inc(:(x,y)) -> :(s(x),inc(y))
hd(:(x,y)) -> x
tl(:(x,y)) -> y
inc(tl(nats())) -> tl(inc(nats()))

Proof:
Church Rosser Transformation Processor (star):

strict:

weak:
tl(0)(:(1)(y)) -> y
hd(0)(:(0)(x)) -> x
inc(0)(:(0)(x)) -> :(0)(s(0)(x))
inc(0)(:(1)(y)) -> :(1)(inc(0)(y))
critical peaks: 1
inc(tl(:(0(),inc(nats())))) <-0|0,0[]- inc(tl(nats())) -4|[]-> tl(inc(nats()))
Matrix Interpretation Processor: dim=1, lab=right

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

[inc(0)](x0) = 2x0 + 2,

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

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

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

[tl(0)](x0) = 2x0
orientation:
tl(0)(:(1)(y)) = 2y >= y = y

hd(0)(:(0)(x)) = 2x + 1 >= x = x

inc(0)(:(0)(x)) = 2x + 2 >= 2x + 2 = :(0)(s(0)(x))

inc(0)(:(1)(y)) = 2y + 2 >= 2y + 2 = :(1)(inc(0)(y))
problem:

strict:

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

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

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

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

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

[tl(0)](x0) = x0 + 1
orientation:
tl(0)(:(1)(y)) = 2y + 1 >= y = y

inc(0)(:(0)(x)) = 2x >= 2x = :(0)(s(0)(x))

inc(0)(:(1)(y)) = 2y >= 2y = :(1)(inc(0)(y))
problem:

strict:

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

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

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

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

[:(1)](x0) = x0 + 1
orientation:
inc(0)(:(0)(x)) = 2x + 1 >= 2x + 1 = :(0)(s(0)(x))

inc(0)(:(1)(y)) = 2y + 3 >= 2y + 2 = :(1)(inc(0)(y))
problem:

strict:

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

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

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

[:(0)](x0) = x0
orientation:
inc(0)(:(0)(x)) = 2x + 1 >= 2x = :(0)(s(0)(x))
problem:

strict:

weak:

Shift Processor lab=left (dd):

strict:
inc(tl(nats())) -> inc(tl(:(0(),inc(nats()))))
inc(tl(nats())) -> tl(inc(nats()))
inc(tl(:(0(),inc(nats())))) -> inc(inc(nats()))
tl(inc(nats())) -> tl(inc(:(0(),inc(nats()))))
tl(inc(:(0(),inc(nats())))) -> tl(:(s(0()),inc(inc(nats()))))
tl(:(s(0()),inc(inc(nats())))) -> inc(inc(nats()))
weak:
nats() -> :(0(),inc(nats()))
inc(:(x,y)) -> :(s(x),inc(y))
hd(:(x,y)) -> x
tl(:(x,y)) -> y
inc(tl(nats())) -> tl(inc(nats()))
Matrix Interpretation Processor: dim=1

interpretation:
[tl](x0) = 4x0,

[hd](x0) = x0 + 5,

[s](x0) = 2x0,

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

[inc](x0) = 4x0,

[0] = 0,

[nats] = 0
orientation:
inc(tl(nats())) = 0 >= 0 = inc(tl(:(0(),inc(nats()))))

inc(tl(nats())) = 0 >= 0 = tl(inc(nats()))

inc(tl(:(0(),inc(nats())))) = 0 >= 0 = inc(inc(nats()))

tl(inc(nats())) = 0 >= 0 = tl(inc(:(0(),inc(nats()))))

tl(inc(:(0(),inc(nats())))) = 0 >= 0 = tl(:(s(0()),inc(inc(nats()))))

tl(:(s(0()),inc(inc(nats())))) = 0 >= 0 = inc(inc(nats()))

nats() = 0 >= 0 = :(0(),inc(nats()))

inc(:(x,y)) = 8x + 8y >= 4x + 8y = :(s(x),inc(y))

hd(:(x,y)) = 2x + 2y + 5 >= x = x

tl(:(x,y)) = 8x + 8y >= y = y
problem:

strict:
inc(tl(nats())) -> inc(tl(:(0(),inc(nats()))))
inc(tl(nats())) -> tl(inc(nats()))
inc(tl(:(0(),inc(nats())))) -> inc(inc(nats()))
tl(inc(nats())) -> tl(inc(:(0(),inc(nats()))))
tl(inc(:(0(),inc(nats())))) -> tl(:(s(0()),inc(inc(nats()))))
tl(:(s(0()),inc(inc(nats())))) -> inc(inc(nats()))
weak:
nats() -> :(0(),inc(nats()))
inc(:(x,y)) -> :(s(x),inc(y))
tl(:(x,y)) -> y
inc(tl(nats())) -> tl(inc(nats()))
Matrix Interpretation Processor: dim=1

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

[s](x0) = x0,

[:](x0, x1) = 4x0 + 2x1,

[inc](x0) = x0,

[0] = 0,

[nats] = 0
orientation:
inc(tl(nats())) = 2 >= 2 = inc(tl(:(0(),inc(nats()))))

inc(tl(nats())) = 2 >= 2 = tl(inc(nats()))

inc(tl(:(0(),inc(nats())))) = 2 >= 0 = inc(inc(nats()))

tl(inc(nats())) = 2 >= 2 = tl(inc(:(0(),inc(nats()))))

tl(inc(:(0(),inc(nats())))) = 2 >= 2 = tl(:(s(0()),inc(inc(nats()))))

tl(:(s(0()),inc(inc(nats())))) = 2 >= 0 = inc(inc(nats()))

nats() = 0 >= 0 = :(0(),inc(nats()))

inc(:(x,y)) = 4x + 2y >= 4x + 2y = :(s(x),inc(y))

tl(:(x,y)) = 4x + 2y + 2 >= y = y
problem:

strict:
inc(tl(nats())) -> inc(tl(:(0(),inc(nats()))))
inc(tl(nats())) -> tl(inc(nats()))
tl(inc(nats())) -> tl(inc(:(0(),inc(nats()))))
tl(inc(:(0(),inc(nats())))) -> tl(:(s(0()),inc(inc(nats()))))
weak:
nats() -> :(0(),inc(nats()))
inc(:(x,y)) -> :(s(x),inc(y))
inc(tl(nats())) -> tl(inc(nats()))
Matrix Interpretation Processor: dim=1

interpretation:
[tl](x0) = x0 + 3,

[s](x0) = 4x0,

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

[inc](x0) = 4x0,

[0] = 0,

[nats] = 0
orientation:
inc(tl(nats())) = 12 >= 12 = inc(tl(:(0(),inc(nats()))))

inc(tl(nats())) = 12 >= 3 = tl(inc(nats()))

tl(inc(nats())) = 3 >= 3 = tl(inc(:(0(),inc(nats()))))

tl(inc(:(0(),inc(nats())))) = 3 >= 3 = tl(:(s(0()),inc(inc(nats()))))

nats() = 0 >= 0 = :(0(),inc(nats()))

inc(:(x,y)) = 8x + 8y >= 8x + 8y = :(s(x),inc(y))
problem:

strict:
inc(tl(nats())) -> inc(tl(:(0(),inc(nats()))))
tl(inc(nats())) -> tl(inc(:(0(),inc(nats()))))
tl(inc(:(0(),inc(nats())))) -> tl(:(s(0()),inc(inc(nats()))))
weak:
nats() -> :(0(),inc(nats()))
inc(:(x,y)) -> :(s(x),inc(y))
Bounds Processor:
bound: 1
enrichment: match-rt
automaton:
final states: {7}
transitions:
s1(15) -> 51*
s1(7) -> 15*
s1(51) -> 15*
inc0(7) -> 7*
tl0(7) -> 7*
nats0() -> 7*
:0(7,7) -> 7*
00() -> 7*
s0(7) -> 7*
inc1(50) -> 14*
inc1(17) -> 14,7
inc1(7) -> 14*
inc1(14) -> 50*
inc1(16) -> 46*
inc1(13) -> 14*
tl1(46) -> 7*
tl1(16) -> 17*
:1(51,50) -> 50,7,14,46
:1(15,14) -> 50,14,13,7,16
01() -> 15*
nats1() -> 13*
problem:

strict:
tl(inc(nats())) -> tl(inc(:(0(),inc(nats()))))
tl(inc(:(0(),inc(nats())))) -> tl(:(s(0()),inc(inc(nats()))))
weak:
nats() -> :(0(),inc(nats()))
inc(:(x,y)) -> :(s(x),inc(y))
Bounds Processor:
bound: 1
enrichment: match-rt
automaton:
final states: {7}
transitions:
s1(15) -> 33*
s1(7) -> 15*
s1(33) -> 15*
inc0(7) -> 7*
tl0(7) -> 7*
nats0() -> 7*
:0(7,7) -> 7*
00() -> 7*
s0(7) -> 7*
inc1(32) -> 14*
inc1(7) -> 14*
inc1(14) -> 32*
inc1(16) -> 17*
inc1(13) -> 14*
tl1(17) -> 7*
:1(33,32) -> 32,7,14,17
:1(15,14) -> 32,14,13,7,16
01() -> 15*
nats1() -> 13*
problem:

strict:
tl(inc(:(0(),inc(nats())))) -> tl(:(s(0()),inc(inc(nats()))))
weak:
nats() -> :(0(),inc(nats()))
inc(:(x,y)) -> :(s(x),inc(y))
Bounds Processor:
bound: 1
enrichment: match-rt
automaton:
final states: {7}
transitions:
s1(17) -> 18*
s1(7) -> 17*
s1(18) -> 17*
inc0(7) -> 7*
tl0(7) -> 7*
nats0() -> 7*
:0(7,7) -> 7*
00() -> 7*
s0(7) -> 7*
inc1(15) -> 16*
inc1(7) -> 15*
inc1(14) -> 15*
inc1(16) -> 15*
tl1(19) -> 7*
:1(17,15) -> 16,15,14,7
:1(18,16) -> 16,15,7,19
01() -> 17*
nats1() -> 14*
problem:

strict:

weak:
nats() -> :(0(),inc(nats()))
inc(:(x,y)) -> :(s(x),inc(y))
Shift Processor (ldh) lab=left (force):

strict:

weak:

Rule Labeling Processor:

strict:

weak:

rule labeling (right):
nats() -> :(0(),inc(nats())): 1
inc(:(x,y)) -> :(s(x),inc(y)): 0
hd(:(x,y)) -> x: 0
tl(:(x,y)) -> y: 0
inc(tl(nats())) -> tl(inc(nats())): 0
Decreasing Processor:
The following diagrams are decreasing:
peak:
inc(tl(:(0(),inc(nats())))) <-0|0,0[1,2,0,1,0,1]- inc(tl(nats())) -4|
[1,0,0,0,0,0]->
tl(inc(nats()))
joins:
inc(tl(:(0(),inc(nats())))) -3|0[1,2,0,1,0,0]-> inc(inc(nats()))
tl(inc(nats())) -0|0,0[0,4,0,1,0,1]-> tl(inc(:(0(),inc(nats())))) -1|
0[0,0,0,0,0,0]->
tl(:(s(0()),inc(inc(nats())))) -3|[0,0,0,0,0,0]-> inc(inc(nats()))
Qed

``````
Nach oben scrollen