### CSI-0.1

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

Proof:
Church Rosser Transformation Processor (star):

strict:

weak:
f(0)(x) -> h(0)(x)
critical peaks: 1
g(b()) <-2|0[]- g(a()) -0|[]-> f(g(a()))
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(a())
c(a()) -> c(b())
f(g(a())) -> h(g(a()))
h(g(a())) -> c(b())
weak:
g(a()) -> f(g(a()))
g(b()) -> c(a())
a() -> b()
f(x) -> h(x)
h(x) -> c(b())
Matrix Interpretation Processor: dim=1

interpretation:
[h](x0) = x0,

[c](x0) = 2x0,

[b] = 0,

[f](x0) = x0,

[g](x0) = 2x0 + 1,

[a] = 0
orientation:
g(a()) = 1 >= 1 = g(b())

g(a()) = 1 >= 1 = f(g(a()))

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

c(a()) = 0 >= 0 = c(b())

f(g(a())) = 1 >= 1 = h(g(a()))

h(g(a())) = 1 >= 0 = c(b())

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

f(x) = x >= x = h(x)

h(x) = x >= 0 = c(b())
problem:

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

interpretation:
[h](x0) = x0,

[c](x0) = 2x0,

[b] = 0,

[f](x0) = x0,

[g](x0) = x0,

[a] = 1
orientation:
g(a()) = 1 >= 0 = g(b())

g(a()) = 1 >= 1 = f(g(a()))

c(a()) = 2 >= 0 = c(b())

f(g(a())) = 1 >= 1 = h(g(a()))

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

f(x) = x >= x = h(x)

h(x) = x >= 0 = c(b())
problem:

strict:
g(a()) -> f(g(a()))
f(g(a())) -> h(g(a()))
weak:
g(a()) -> f(g(a()))
f(x) -> h(x)
h(x) -> c(b())
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(a()): 0
a() -> b(): 0
f(x) -> h(x): 0
h(x) -> c(b()): 0
Decreasing Processor:
The following diagrams are decreasing:
peak:
g(b()) <-2|0[1,0,0]- g(a()) -0|[1,0,1]-> f(g(a()))
joins:
g(b()) -1|[0,0,0]-> c(a()) -2|0[0,0,0]-> c(b())
f(g(a())) -3|[1,0,0]-> h(g(a())) -4|[1,0,0]-> c(b())
Qed

Nach oben scrollen