Problem:
f(s(X),X) -> f(X,a(X))
f(X,c(X)) -> f(s(X),X)
f(X,X) -> c(X)
Proof:
Complexity Transformation Processor:
strict:
f(s(X),X) -> f(X,a(X))
f(X,c(X)) -> f(s(X),X)
f(X,X) -> c(X)
weak:
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[c](x0) = x0,
[a](x0) = x0,
[f](x0, x1) = x0 + x1 + 15,
[s](x0) = x0 + 4
orientation:
f(s(X),X) = 2X + 19 >= 2X + 15 = f(X,a(X))
f(X,c(X)) = 2X + 15 >= 2X + 19 = f(s(X),X)
f(X,X) = 2X + 15 >= X = c(X)
problem:
strict:
f(X,c(X)) -> f(s(X),X)
weak:
f(s(X),X) -> f(X,a(X))
f(X,X) -> c(X)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[c](x0) = x0 + 8,
[a](x0) = x0,
[f](x0, x1) = x0 + x1 + 8,
[s](x0) = x0
orientation:
f(X,c(X)) = 2X + 16 >= 2X + 8 = f(s(X),X)
f(s(X),X) = 2X + 8 >= 2X + 8 = f(X,a(X))
f(X,X) = 2X + 8 >= X + 8 = c(X)
problem:
strict:
weak:
f(X,c(X)) -> f(s(X),X)
f(s(X),X) -> f(X,a(X))
f(X,X) -> c(X)
Qed