### CSI-0.1

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

Proof:
Church Rosser Transformation Processor (kb):
f(g(g(x))) -> a()
f(g(h(x))) -> b()
f(h(g(x))) -> b()
f(h(h(x))) -> c()
g(x) -> h(x)
a() -> b()
b() -> c()
critical peaks: joinable
Matrix Interpretation Processor: dim=3

interpretation:
[0]
[c] = [0]
[0],

[0]
[b] = [0]
[0],

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

[0]
[a] = [0]
[0],

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

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

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

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

[1 0 0]    [1]    [0]
f(h(h(x))) = [0 0 0]x + [0] >= [0] = c()
[0 0 0]    [0]    [0]

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

[0]    [0]
a() = [0] >= [0] = b()
[0]    [0]

[0]    [0]
b() = [0] >= [0] = c()
[0]    [0]
problem:
g(x) -> h(x)
a() -> b()
b() -> c()
Matrix Interpretation Processor: dim=3

interpretation:
[0]
[c] = [0]
[0],

[0]
[b] = [0]
[0],

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

[1]
[a] = [0]
[0],

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

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

[0]    [0]
b() = [0] >= [0] = c()
[0]    [0]
problem:
b() -> c()
Matrix Interpretation Processor: dim=3

interpretation:
[0]
[c] = [0]
[0],

[1]
[b] = [0]
[0]
orientation:
[1]    [0]
b() = [0] >= [0] = c()
[0]    [0]
problem:

Qed
``````
Nach oben scrollen