Problem:
a__f(a(),X,X) -> a__f(X,a__b(),b())
a__b() -> a()
mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
mark(b()) -> a__b()
mark(a()) -> a()
a__f(X1,X2,X3) -> f(X1,X2,X3)
a__b() -> b()
Proof:
Complexity Transformation Processor:
strict:
a__f(a(),X,X) -> a__f(X,a__b(),b())
a__b() -> a()
mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
mark(b()) -> a__b()
mark(a()) -> a()
a__f(X1,X2,X3) -> f(X1,X2,X3)
a__b() -> b()
weak:
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[mark](x0) = x0,
[f](x0, x1, x2) = x0 + x1 + x2 + 8,
[b] = 0,
[a__b] = 1,
[a__f](x0, x1, x2) = x0 + x1 + x2 + 14,
[a] = 4
orientation:
a__f(a(),X,X) = 2X + 18 >= X + 15 = a__f(X,a__b(),b())
a__b() = 1 >= 4 = a()
mark(f(X1,X2,X3)) = X1 + X2 + X3 + 8 >= X1 + X2 + X3 + 14 = a__f(X1,mark(X2),X3)
mark(b()) = 0 >= 1 = a__b()
mark(a()) = 4 >= 4 = a()
a__f(X1,X2,X3) = X1 + X2 + X3 + 14 >= X1 + X2 + X3 + 8 = f(X1,X2,X3)
a__b() = 1 >= 0 = b()
problem:
strict:
a__b() -> a()
mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
mark(b()) -> a__b()
mark(a()) -> a()
weak:
a__f(a(),X,X) -> a__f(X,a__b(),b())
a__f(X1,X2,X3) -> f(X1,X2,X3)
a__b() -> b()
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[mark](x0) = x0 + 1,
[f](x0, x1, x2) = x0 + x1 + x2 + 12,
[b] = 4,
[a__b] = 4,
[a__f](x0, x1, x2) = x0 + x1 + x2 + 12,
[a] = 8
orientation:
a__b() = 4 >= 8 = a()
mark(f(X1,X2,X3)) = X1 + X2 + X3 + 13 >= X1 + X2 + X3 + 13 = a__f(X1,mark(X2),X3)
mark(b()) = 5 >= 4 = a__b()
mark(a()) = 9 >= 8 = a()
a__f(a(),X,X) = 2X + 20 >= X + 20 = a__f(X,a__b(),b())
a__f(X1,X2,X3) = X1 + X2 + X3 + 12 >= X1 + X2 + X3 + 12 = f(X1,X2,X3)
a__b() = 4 >= 4 = b()
problem:
strict:
a__b() -> a()
mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
weak:
mark(b()) -> a__b()
mark(a()) -> a()
a__f(a(),X,X) -> a__f(X,a__b(),b())
a__f(X1,X2,X3) -> f(X1,X2,X3)
a__b() -> b()
Splitting Processor:
strict:
a__b() -> a()
weak:
mark(b()) -> a__b()
mark(a()) -> a()
a__f(a(),X,X) -> a__f(X,a__b(),b())
a__f(X1,X2,X3) -> f(X1,X2,X3)
a__b() -> b()
mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
Matrix Interpretation Processor:
dimension: 4
max_matrix:
[1 0 1 1]
[0 0 1 1]
[0 0 0 0]
[0 0 0 0]
interpretation:
[1 0 0 1] [1]
[0 0 1 1] [1]
[mark](x0) = [0 0 0 0]x0 + [1]
[0 0 0 0] [1],
[1 0 1 1] [1 0 0 1] [1 0 1 0] [0]
[0 0 0 0] [0 0 0 0] [0 0 0 0] [0]
[f](x0, x1, x2) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0 0 0 0]x2 + [0]
[0 0 0 0] [0 0 0 0] [0 0 0 0] [1],
[0]
[0]
[b] = [0]
[0],
[1]
[0]
[a__b] = [1]
[1],
[1 0 1 1] [1 0 0 1] [1 0 1 0] [0]
[0 0 0 0] [0 0 0 0] [0 0 0 0] [1]
[a__f](x0, x1, x2) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0 0 0 0]x2 + [0]
[0 0 0 0] [0 0 0 0] [0 0 0 0] [1],
[0]
[0]
[a] = [1]
[1]
orientation:
[1] [0]
[0] [0]
a__b() = [1] >= [1] = a()
[1] [1]
[1] [1]
[1] [0]
mark(b()) = [1] >= [1] = a__b()
[1] [1]
[2] [0]
[3] [0]
mark(a()) = [1] >= [1] = a()
[1] [1]
[2 0 1 1] [2] [1 0 1 1] [2]
[0 0 0 0] [1] [0 0 0 0] [1]
a__f(a(),X,X) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = a__f(X,a__b(),b())
[0 0 0 0] [1] [0 0 0 0] [1]
[1 0 1 1] [1 0 0 1] [1 0 1 0] [0] [1 0 1 1] [1 0 0 1] [1 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] [0 0 0 0] [0]
a__f(X1,X2,X3) = [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 + [0] >= [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 + [0] = f(X1,X2,X3)
[0 0 0 0] [0 0 0 0] [0 0 0 0] [1] [0 0 0 0] [0 0 0 0] [0 0 0 0] [1]
[1] [0]
[0] [0]
a__b() = [1] >= [0] = b()
[1] [0]
[1 0 1 1] [1 0 0 1] [1 0 1 0] [2] [1 0 1 1] [1 0 0 1] [1 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 0 0] [2] [0 0 0 0] [0 0 0 0] [0 0 0 0] [1]
mark(f(X1,X2,X3)) = [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 + [1] >= [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 + [0] = a__f(X1,mark(X2),X3)
[0 0 0 0] [0 0 0 0] [0 0 0 0] [1] [0 0 0 0] [0 0 0 0] [0 0 0 0] [1]
problem:
strict:
weak:
a__b() -> a()
mark(b()) -> a__b()
mark(a()) -> a()
a__f(a(),X,X) -> a__f(X,a__b(),b())
a__f(X1,X2,X3) -> f(X1,X2,X3)
a__b() -> b()
mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
Qed
strict:
mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
weak:
a__b() -> a()
mark(b()) -> a__b()
mark(a()) -> a()
a__f(a(),X,X) -> a__f(X,a__b(),b())
a__f(X1,X2,X3) -> f(X1,X2,X3)
a__b() -> b()
Matrix Interpretation Processor:
dimension: 3
max_matrix:
[1 1 1]
[0 1 1]
[0 0 0]
interpretation:
[1 1 0]
[mark](x0) = [0 1 0]x0
[0 0 0] ,
[1 0 0] [1 0 0] [1 0 0] [0]
[f](x0, x1, x2) = [0 0 1]x0 + [0 1 1]x1 + [0 1 0]x2 + [1]
[0 0 0] [0 0 0] [0 0 0] [0],
[0]
[b] = [0]
[0],
[0]
[a__b] = [0]
[0],
[1 0 0] [1 0 1] [1 0 0] [0]
[a__f](x0, x1, x2) = [0 0 1]x0 + [0 1 1]x1 + [0 1 0]x2 + [1]
[0 0 0] [0 0 0] [0 0 0] [0],
[0]
[a] = [0]
[0]
orientation:
[1 0 1] [1 1 1] [1 1 0] [1] [1 0 0] [1 1 0] [1 0 0] [0]
mark(f(X1,X2,X3)) = [0 0 1]X1 + [0 1 1]X2 + [0 1 0]X3 + [1] >= [0 0 1]X1 + [0 1 0]X2 + [0 1 0]X3 + [1] = a__f(X1,mark(X2),X3)
[0 0 0] [0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0 0 0] [0]
[0] [0]
a__b() = [0] >= [0] = a()
[0] [0]
[0] [0]
mark(b()) = [0] >= [0] = a__b()
[0] [0]
[0] [0]
mark(a()) = [0] >= [0] = a()
[0] [0]
[2 0 1] [0] [1 0 0] [0]
a__f(a(),X,X) = [0 2 1]X + [1] >= [0 0 1]X + [1] = a__f(X,a__b(),b())
[0 0 0] [0] [0 0 0] [0]
[1 0 0] [1 0 1] [1 0 0] [0] [1 0 0] [1 0 0] [1 0 0] [0]
a__f(X1,X2,X3) = [0 0 1]X1 + [0 1 1]X2 + [0 1 0]X3 + [1] >= [0 0 1]X1 + [0 1 1]X2 + [0 1 0]X3 + [1] = f(X1,X2,X3)
[0 0 0] [0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0 0 0] [0]
[0] [0]
a__b() = [0] >= [0] = b()
[0] [0]
problem:
strict:
weak:
mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
a__b() -> a()
mark(b()) -> a__b()
mark(a()) -> a()
a__f(a(),X,X) -> a__f(X,a__b(),b())
a__f(X1,X2,X3) -> f(X1,X2,X3)
a__b() -> b()
Qed