### CSI-0.1

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

Proof:
sorted: (order)
0:f(x,y) -> x
f(x,y) -> f(x,g(y))
g(x) -> h(x)
1:g(x) -> h(x)
F(g(x),x) -> F(x,g(x))
F(h(x),x) -> F(x,h(x))
-----
sorts
[1>4, 1>5, 2>3, 3>5]
sort attachment (non-strict)
f : 4 x 5 -> 1
g : 5 -> 5
h : 5 -> 5
F : 3 x 5 -> 2
-----
0:f(x,y) -> x
f(x,y) -> f(x,g(y))
g(x) -> h(x)
Church Rosser Transformation Processor:

strict:

weak:

critical peaks: 2
x <-0|[]- f(x,y) -1|[]-> f(x,g(y))
f(x,g(y)) <-1|[]- f(x,y) -0|[]-> x
Closedness Processor (*parallel*):

strict:

weak:

Qed

1:g(x) -> h(x)
F(g(x),x) -> F(x,g(x))
F(h(x),x) -> F(x,h(x))
Church Rosser Transformation Processor (kb):
g(x) -> h(x)
F(g(x),x) -> F(x,g(x))
F(h(x),x) -> F(x,h(x))
critical peaks: joinable
Matrix Interpretation Processor: dim=1

interpretation:
[F](x0, x1) = 5x0 + 4x1,

[h](x0) = 3x0,

[g](x0) = 4x0 + 4
orientation:
g(x) = 4x + 4 >= 3x = h(x)

F(g(x),x) = 24x + 20 >= 21x + 16 = F(x,g(x))

F(h(x),x) = 19x >= 17x = F(x,h(x))
problem:
F(h(x),x) -> F(x,h(x))
Matrix Interpretation Processor: dim=1

interpretation:
[F](x0, x1) = 4x0 + 3x1 + 3,

[h](x0) = 4x0 + 7
orientation:
F(h(x),x) = 19x + 31 >= 16x + 24 = F(x,h(x))
problem:

Qed``````
Nach oben scrollen