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|[1]- f(a()) -2|[1]-> f(b())
joins:
f(f(a())) -2|[1]-> f(b())
peak:
f(b()) <-1|0[1]- f(a()) -0|[1]-> f(f(a()))
joins:
f(f(a())) -2|[1]-> f(b())
peak:
f(b()) <-2|[1]- f(a()) -0|[1]-> f(f(a()))
joins:
f(f(a())) -2|[1]-> f(b())
Qed