### CSI-0.1

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

Proof:
sorted: (order)
0:f(a(x),x) -> f(x,a(x))
f(b(x),x) -> f(x,b(x))
a(x) -> b(x)
1:g(b(x),y) -> g(a(a(x)),y)
g(c(x),y) -> y
a(x) -> b(x)
-----
sorts
[1>3, 2>4, 2>8, 3>7, 4>5, 4>7, 5>6]
sort attachment (non-strict)
f : 3 x 7 -> 1
a : 7 -> 7
b : 7 -> 7
g : 4 x 8 -> 2
c : 6 -> 5
-----
0:f(a(x),x) -> f(x,a(x))
f(b(x),x) -> f(x,b(x))
a(x) -> b(x)
Church Rosser Transformation Processor (kb):
f(a(x),x) -> f(x,a(x))
f(b(x),x) -> f(x,b(x))
a(x) -> b(x)
critical peaks: joinable
Matrix Interpretation Processor: dim=1

interpretation:
[b](x0) = x0,

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

[a](x0) = x0 + 3
orientation:
f(a(x),x) = 2x + 7 >= 2x + 7 = f(x,a(x))

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

a(x) = x + 3 >= x = b(x)
problem:
f(a(x),x) -> f(x,a(x))
f(b(x),x) -> f(x,b(x))
Matrix Interpretation Processor: dim=1

interpretation:
[b](x0) = x0 + 1,

[f](x0, x1) = 2x0 + x1 + 1,

[a](x0) = x0
orientation:
f(a(x),x) = 3x + 1 >= 3x + 1 = f(x,a(x))

f(b(x),x) = 3x + 3 >= 3x + 2 = f(x,b(x))
problem:
f(a(x),x) -> f(x,a(x))
Matrix Interpretation Processor: dim=3

interpretation:
[1 0 1]     [1 0 0]
[f](x0, x1) = [1 1 0]x0 + [1 1 0]x1
[0 0 1]     [0 0 1]  ,

[1 1 0]     [0]
[a](x0) = [1 1 0]x0 + [0]
[0 0 1]     [1]
orientation:
[2 1 1]    [1]    [2 1 1]    [0]
f(a(x),x) = [3 3 0]x + [0] >= [3 3 0]x + [0] = f(x,a(x))
[0 0 2]    [1]    [0 0 2]    [1]
problem:

Qed

1:g(b(x),y) -> g(a(a(x)),y)
g(c(x),y) -> y
a(x) -> b(x)
Church Rosser Transformation Processor:

strict:

weak:

critical peaks: 0
Qed
``````
Nach oben scrollen