 ### 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:

[a] = 
,

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

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

    
f(g(a())) =  >=  = f(h(a(),a()))
    

    
f(h(a(),a())) =  >=  = f(g(g(a())))
    

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

    
g(a()) =  >=  = g(g(a()))
    

    
h(a(),a()) =  >=  = g(g(a()))
    
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:

[a] = 
,

[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:
    
f(h(a(),a())) =  >=  = f(g(g(a())))
    

[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]

    
g(a()) =  >=  = g(g(a()))
    

    
h(a(),a()) =  >=  = g(g(a()))
    
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