### CSI-0.1

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

Proof:
Church Rosser Transformation Processor (star):

strict:

weak:
g(0)(x) -> x
f(1)(x) -> f(1)(g(0)(x))
critical peaks: 1
f(b(),x) <-1|0[]- f(a(),x) -0|[]-> f(a(),g(x))
Shift Processor lab=left (dd):

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

interpretation:
[b] = 0,

[g](x0) = x0,

[f](x0, x1) = 4x0 + 4x1,

[a] = 1
orientation:
f(a(),x) = 4x + 4 >= 4x = f(b(),x)

f(a(),x) = 4x + 4 >= 4x + 4 = f(a(),g(x))

f(a(),g(x)) = 4x + 4 >= 4x = f(b(),g(x))

f(b(),g(x)) = 4x >= 4x = f(b(),x)

f(a(),g(x)) = 4x + 4 >= 4x + 4 = f(a(),x)

f(a(),x) = 4x + 4 >= 4x = f(b(),x)

a() = 1 >= 0 = b()

g(x) = x >= x = x
problem:

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

strict:

weak:

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

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