### CSI-0.1

``````
Problem:
f(g(x)) -> f(h(x,x))
g(a()) -> g(g(a()))
h(a(),a()) -> g(g(a()))

Proof:
Church Rosser Transformation Processor (star):

strict:
f(0)(g(0)(x)) -> f(0)(h(0)(x))
f(0)(g(0)(x)) -> f(0)(h(1)(x))
weak:

critical peaks: 1
f(g(g(a()))) <-1|0[]- f(g(a())) -0|[]-> f(h(a(),a()))
Matrix Interpretation Processor: dim=1, lab=right

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

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

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

[f(0)](x0) = x0
orientation:
f(0)(g(0)(x)) = 2x + 2 >= x = f(0)(h(0)(x))

f(0)(g(0)(x)) = 2x + 2 >= 2x = f(0)(h(1)(x))
problem:

strict:

weak:

Shift Processor lab=left (dd):

strict:
f(g(a())) -> f(g(g(a())))
f(g(a())) -> f(h(a(),a()))
f(h(a(),a())) -> f(g(g(a())))
weak:
f(g(x)) -> f(h(x,x))
g(a()) -> g(g(a()))
h(a(),a()) -> g(g(a()))
Matrix Interpretation Processor: dim=3

interpretation:
[0]
[a] = [1]
[0],

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

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

[1 0 0]
[g](x0) = [0 0 0]x0
[1 1 0]
orientation:
[2]    [1]
f(g(a())) = [1] >= [0] = f(g(g(a())))
[1]    [0]

[2]    [1]
f(g(a())) = [1] >= [1] = f(h(a(),a()))
[1]    [1]

[1]    [1]
f(h(a(),a())) = [1] >= [0] = f(g(g(a())))
[1]    [0]

[2 1 0]    [1]    [2 0 0]    [1]
f(g(x)) = [2 1 0]x + [0] >= [2 1 0]x + [0] = f(h(x,x))
[1 1 0]    [0]    [0 1 0]    [0]

[0]    [0]
g(a()) = [0] >= [0] = g(g(a()))
[1]    [0]

[0]    [0]
h(a(),a()) = [1] >= [0] = g(g(a()))
[0]    [0]
problem:

strict:
f(h(a(),a())) -> f(g(g(a())))
weak:
f(g(x)) -> f(h(x,x))
g(a()) -> g(g(a()))
h(a(),a()) -> g(g(a()))
Matrix Interpretation Processor: dim=3

interpretation:
[1]
[a] = [1]
[0],

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

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

[1 0 0]
[g](x0) = [0 0 0]x0
[1 1 0]
orientation:
[3]    [2]
f(h(a(),a())) = [3] >= [2] = f(g(g(a())))
[1]    [1]

[2 1 0]     [2 1 0]
f(g(x)) = [2 1 0]x >= [2 1 0]x = f(h(x,x))
[1 1 0]     [0 1 0]

[1]    [1]
g(a()) = [0] >= [0] = g(g(a()))
[2]    [1]

[2]    [1]
h(a(),a()) = [1] >= [0] = g(g(a()))
[1]    [1]
problem:

strict:

weak:
f(g(x)) -> f(h(x,x))
g(a()) -> g(g(a()))
Shift Processor (ldh) lab=left (force):

strict:

weak:

Decreasing Processor:
The following diagrams are decreasing:
peak:
f(g(g(a()))) <-1|0[1,0]- f(g(a())) -0|[1,0]-> f(h(a(),a()))
joins:

f(h(a(),a())) -2|0[1,0]-> f(g(g(a())))
Qed
``````
Nach oben scrollen