YES
Problem:
strict:
f(a(),g(y),z) -> f(a(),y,g(y))
f(b(),g(y),z) -> f(a(),y,z)
a() -> b()
weak:
f(x,y,z) -> f(x,y,g(z))
Proof:
Matrix Interpretation Processor: dim=5
interpretation:
[1 0 0 0 1] [0]
[0 1 1 0 0] [0]
[g](x0) = [1 1 1 0 0]x0 + [1]
[0 0 0 1 1] [1]
[0 0 0 0 0] [0],
[0]
[0]
[b] = [0]
[0]
[1],
[0]
[0]
[a] = [1]
[1]
[1],
[1 0 0 0 1] [1 1 1 1 0] [1 0 0 0 1]
[0 0 0 0 0] [0 1 0 0 0] [0 0 0 0 0]
[f](x0, x1, x2) = [0 0 0 0 1]x0 + [1 0 0 1 0]x1 + [0 0 0 0 0]x2
[0 0 0 0 1] [1 0 1 0 0] [0 0 0 0 0]
[0 0 1 0 1] [1 0 1 0 0] [1 0 0 0 1]
orientation:
[2 2 2 1 2] [1 0 0 0 1] [3] [2 1 1 1 1] [1]
[0 1 1 0 0] [0 0 0 0 0] [0] [0 1 0 0 0] [0]
f(a(),g(y),z) = [1 0 0 1 2]y + [0 0 0 0 0]z + [2] >= [1 0 0 1 0]y + [1] = f(a(),y,g(y))
[2 1 1 0 1] [0 0 0 0 0] [2] [1 0 1 0 0] [1]
[2 1 1 0 1] [1 0 0 0 1] [3] [2 0 1 0 1] [2]
[2 2 2 1 2] [1 0 0 0 1] [3] [1 1 1 1 0] [1 0 0 0 1] [1]
[0 1 1 0 0] [0 0 0 0 0] [0] [0 1 0 0 0] [0 0 0 0 0] [0]
f(b(),g(y),z) = [1 0 0 1 2]y + [0 0 0 0 0]z + [2] >= [1 0 0 1 0]y + [0 0 0 0 0]z + [1] = f(a(),y,z)
[2 1 1 0 1] [0 0 0 0 0] [2] [1 0 1 0 0] [0 0 0 0 0] [1]
[2 1 1 0 1] [1 0 0 0 1] [2] [1 0 1 0 0] [1 0 0 0 1] [2]
[0] [0]
[0] [0]
a() = [1] >= [0] = b()
[1] [0]
[1] [1]
[1 0 0 0 1] [1 1 1 1 0] [1 0 0 0 1] [1 0 0 0 1] [1 1 1 1 0] [1 0 0 0 1]
[0 0 0 0 0] [0 1 0 0 0] [0 0 0 0 0] [0 0 0 0 0] [0 1 0 0 0] [0 0 0 0 0]
f(x,y,z) = [0 0 0 0 1]x + [1 0 0 1 0]y + [0 0 0 0 0]z >= [0 0 0 0 1]x + [1 0 0 1 0]y + [0 0 0 0 0]z = f(x,y,g(z))
[0 0 0 0 1] [1 0 1 0 0] [0 0 0 0 0] [0 0 0 0 1] [1 0 1 0 0] [0 0 0 0 0]
[0 0 1 0 1] [1 0 1 0 0] [1 0 0 0 1] [0 0 1 0 1] [1 0 1 0 0] [1 0 0 0 1]
problem:
strict:
a() -> b()
weak:
f(x,y,z) -> f(x,y,g(z))
Matrix Interpretation Processor: dim=5
interpretation:
[1 0 0 0 1]
[0 0 1 0 0]
[g](x0) = [0 0 0 0 0]x0
[0 0 1 1 1]
[0 0 0 0 0] ,
[0]
[0]
[b] = [0]
[0]
[0],
[1]
[0]
[a] = [1]
[0]
[0],
[1 0 0 0 0] [1 0 0 0 0] [1 0 0 0 1] [0]
[0 0 0 0 0] [0 0 0 0 0] [1 1 1 0 1] [0]
[f](x0, x1, x2) = [0 0 0 0 0]x0 + [0 0 0 0 0]x1 + [0 1 1 0 0]x2 + [1]
[0 0 0 0 0] [0 0 0 0 0] [0 0 1 1 1] [0]
[0 0 0 0 0] [0 0 0 0 0] [0 0 1 1 1] [0]
orientation:
[1] [0]
[0] [0]
a() = [1] >= [0] = b()
[0] [0]
[0] [0]
[1 0 0 0 0] [1 0 0 0 0] [1 0 0 0 1] [0] [1 0 0 0 0] [1 0 0 0 0] [1 0 0 0 1] [0]
[0 0 0 0 0] [0 0 0 0 0] [1 1 1 0 1] [0] [0 0 0 0 0] [0 0 0 0 0] [1 0 1 0 1] [0]
f(x,y,z) = [0 0 0 0 0]x + [0 0 0 0 0]y + [0 1 1 0 0]z + [1] >= [0 0 0 0 0]x + [0 0 0 0 0]y + [0 0 1 0 0]z + [1] = f(x,y,g(z))
[0 0 0 0 0] [0 0 0 0 0] [0 0 1 1 1] [0] [0 0 0 0 0] [0 0 0 0 0] [0 0 1 1 1] [0]
[0 0 0 0 0] [0 0 0 0 0] [0 0 1 1 1] [0] [0 0 0 0 0] [0 0 0 0 0] [0 0 1 1 1] [0]
problem:
strict:
weak:
f(x,y,z) -> f(x,y,g(z))
Qed