### CSI-0.1

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

Proof:
Church Rosser Transformation Processor (star):

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

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

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

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

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

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

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

Matrix Interpretation Processor: dim=1, lab=right

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

[f(0)](x0) = x0 + 1
orientation:
f(0)(x) = x + 1 >= x = h(0)(x)
problem:

strict:

weak:

Shift Processor lab=left (dd):

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

strict:

weak:

Rule Labeling Processor:

strict:

weak:

rule labeling (right):
g(a()) -> f(g(a())): 1
g(b()) -> c(): 0
a() -> b(): 0
f(x) -> h(x,x): 0
h(x,y) -> c(): 0
Decreasing Processor:
The following diagrams are decreasing:
peak:
g(b()) <-2|0[1,0,0,0]- g(a()) -0|[1,0,0,1]-> f(g(a()))
joins:
g(b()) -1|[1,0,0,0]-> c()
f(g(a())) -3|[1,0,0,0]-> h(g(a()),g(a())) -4|[1,0,0,0]-> c()
Qed
``````
Nach oben scrollen