 ### CSI-0.1

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

Proof:
Church Rosser Transformation Processor (star):

strict:

weak:

critical peaks: 3
f(f(a())) <-0|[]- f(a()) -2|[]-> f(b())
f(b()) <-1|0[]- f(a()) -0|[]-> f(f(a()))
f(b()) <-2|[]- f(a()) -0|[]-> f(f(a()))
Shift Processor lab=left (dd):

strict:
f(a()) -> f(f(a()))
f(a()) -> f(b())
f(f(a())) -> f(b())
f(a()) -> f(b())
f(a()) -> f(f(a()))
f(f(a())) -> f(b())
f(a()) -> f(b())
f(a()) -> f(f(a()))
f(f(a())) -> f(b())
weak:
f(a()) -> f(f(a()))
a() -> b()
f(x) -> f(b())
Polynomial Interpretation Processor:
dimension: 1
interpretation:
[b] = 0,

[f](x0) = x0,

[a] = 1
orientation:
f(a()) = 1 >= 1 = f(f(a()))

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

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

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

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

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

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

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

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

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

f(x) = x >= 0 = f(b())
problem:

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

strict:

weak:

Decreasing Processor:
The following diagrams are decreasing:
peak:
f(f(a())) <-0|- f(a()) -2|-> f(b())
joins:
f(f(a())) -2|-> f(b())

peak:
f(b()) <-1|0- f(a()) -0|-> f(f(a()))
joins:

f(f(a())) -2|-> f(b())
peak:
f(b()) <-2|- f(a()) -0|-> f(f(a()))
joins:

f(f(a())) -2|-> f(b())
Qed
``````
Nach oben scrollen