Problem:
f(g(x)) -> f(h(x,x))
g(a()) -> g(g(a()))
h(a(),a()) -> g(g(a()))
Proof:
Church Rosser Transformation Processor (star):
strict:
f(0)(g(0)(x)) -> f(0)(h(0)(x))
f(0)(g(0)(x)) -> f(0)(h(1)(x))
weak:
critical peaks: 1
f(g(g(a()))) <-1|0[]- f(g(a())) -0|[]-> f(h(a(),a()))
Matrix Interpretation Processor: dim=1, lab=right
interpretation:
[h(1)](x0) = 3x0,
[h(0)](x0) = 2x0 + 1,
[g(0)](x0) = 3x0 + 3,
[f(0)](x0) = x0
orientation:
f(0)(g(0)(x)) = 3x + 3 >= 2x + 1 = f(0)(h(0)(x))
f(0)(g(0)(x)) = 3x + 3 >= 3x = f(0)(h(1)(x))
problem:
strict:
weak:
Shift Processor lab=left (dd):
strict:
f(g(a())) -> f(g(g(a())))
f(g(a())) -> f(h(a(),a()))
f(h(a(),a())) -> f(g(g(a())))
weak:
f(g(x)) -> f(h(x,x))
g(a()) -> g(g(a()))
h(a(),a()) -> g(g(a()))
Matrix Interpretation Processor: dim=3
interpretation:
[1]
[a] = [1]
[1],
[1 0 0] [1 0 0]
[h](x0, x1) = [0 0 1]x0 + [0 0 0]x1
[1 1 0] [0 0 0] ,
[1 1 0]
[f](x0) = [0 1 0]x0
[1 1 0] ,
[1 0 0]
[g](x0) = [1 0 1]x0
[0 0 0]
orientation:
[3] [2]
f(g(a())) = [2] >= [1] = f(g(g(a())))
[3] [2]
[3] [3]
f(g(a())) = [2] >= [1] = f(h(a(),a()))
[3] [3]
[3] [2]
f(h(a(),a())) = [1] >= [1] = f(g(g(a())))
[3] [2]
[2 0 1] [2 0 1]
f(g(x)) = [1 0 1]x >= [0 0 1]x = f(h(x,x))
[2 0 1] [2 0 1]
[1] [1]
g(a()) = [2] >= [1] = g(g(a()))
[0] [0]
[2] [1]
h(a(),a()) = [1] >= [1] = g(g(a()))
[2] [0]
problem:
strict:
f(g(a())) -> f(h(a(),a()))
weak:
f(g(x)) -> f(h(x,x))
g(a()) -> g(g(a()))
Matrix Interpretation Processor: dim=2
interpretation:
[1]
[a] = [0],
[1 0] [1 0]
[h](x0, x1) = [0 0]x0 + [0 0]x1,
[1 2]
[f](x0) = [0 2]x0,
[1 0]
[g](x0) = [1 0]x0
orientation:
[3] [2]
f(g(a())) = [2] >= [0] = f(h(a(),a()))
[3 0] [2 0]
f(g(x)) = [2 0]x >= [0 0]x = f(h(x,x))
[1] [1]
g(a()) = [1] >= [1] = g(g(a()))
problem:
strict:
weak:
f(g(x)) -> f(h(x,x))
g(a()) -> g(g(a()))
Shift Processor (ldh) lab=left (force):
strict:
weak:
Decreasing Processor:
The following diagrams are decreasing:
peak:
f(g(g(a()))) <-1|0[1,0]- f(g(a())) -0|[1,0]-> f(h(a(),a()))
joins:
f(h(a(),a())) -2|0[1,0]-> f(g(g(a())))
Qed