Problem:
f(0()) -> 0()
f(s(x)) -> f(id(x))
id(0()) -> 0()
id(s(x)) -> s(id(x))
Proof:
Complexity Transformation Processor:
strict:
f(0()) -> 0()
f(s(x)) -> f(id(x))
id(0()) -> 0()
id(s(x)) -> s(id(x))
weak:
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[id](x0) = x0 + 194,
[s](x0) = x0 + 82,
[f](x0) = x0 + 167,
[0] = 116
orientation:
f(0()) = 283 >= 116 = 0()
f(s(x)) = x + 249 >= x + 361 = f(id(x))
id(0()) = 310 >= 116 = 0()
id(s(x)) = x + 276 >= x + 276 = s(id(x))
problem:
strict:
f(s(x)) -> f(id(x))
id(s(x)) -> s(id(x))
weak:
f(0()) -> 0()
id(0()) -> 0()
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[id](x0) = x0,
[s](x0) = x0 + 1,
[f](x0) = x0,
[0] = 40
orientation:
f(s(x)) = x + 1 >= x = f(id(x))
id(s(x)) = x + 1 >= x + 1 = s(id(x))
f(0()) = 40 >= 40 = 0()
id(0()) = 40 >= 40 = 0()
problem:
strict:
id(s(x)) -> s(id(x))
weak:
f(s(x)) -> f(id(x))
f(0()) -> 0()
id(0()) -> 0()
Matrix Interpretation Processor:
dimension: 4
max_matrix:
[1 1 1 1]
[0 0 0 0]
[0 0 0 1]
[0 0 0 1]
interpretation:
[1 0 1 0] [1]
[0 0 0 0] [0]
[id](x0) = [0 0 0 1]x0 + [0]
[0 0 0 1] [0],
[1 1 1 1] [1]
[0 0 0 0] [0]
[s](x0) = [0 0 0 1]x0 + [1]
[0 0 0 1] [1],
[1 0 0 1] [1]
[0 0 0 0] [1]
[f](x0) = [0 0 0 0]x0 + [1]
[0 0 0 0] [1],
[0]
[0]
[0] = [0]
[0]
orientation:
[1 1 1 2] [3] [1 0 1 2] [2]
[0 0 0 0] [0] [0 0 0 0] [0]
id(s(x)) = [0 0 0 1]x + [1] >= [0 0 0 1]x + [1] = s(id(x))
[0 0 0 1] [1] [0 0 0 1] [1]
[1 1 1 2] [3] [1 0 1 1] [2]
[0 0 0 0] [1] [0 0 0 0] [1]
f(s(x)) = [0 0 0 0]x + [1] >= [0 0 0 0]x + [1] = f(id(x))
[0 0 0 0] [1] [0 0 0 0] [1]
[1] [0]
[1] [0]
f(0()) = [1] >= [0] = 0()
[1] [0]
[1] [0]
[0] [0]
id(0()) = [0] >= [0] = 0()
[0] [0]
problem:
strict:
weak:
id(s(x)) -> s(id(x))
f(s(x)) -> f(id(x))
f(0()) -> 0()
id(0()) -> 0()
Qed