Tool CaT
stdout:
YES(?,O(n^1))
Problem:
max(L(x)) -> x
max(N(L(0()),L(y))) -> y
max(N(L(s(x)),L(s(y)))) -> s(max(N(L(x),L(y))))
max(N(L(x),N(y,z))) -> max(N(L(x),L(max(N(y,z)))))
Proof:
Complexity Transformation Processor:
strict:
max(L(x)) -> x
max(N(L(0()),L(y))) -> y
max(N(L(s(x)),L(s(y)))) -> s(max(N(L(x),L(y))))
max(N(L(x),N(y,z))) -> max(N(L(x),L(max(N(y,z)))))
weak:
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[s](x0) = x0 + 11,
[N](x0, x1) = x0 + x1,
[0] = 7,
[max](x0) = x0 + 17,
[L](x0) = x0 + 9
orientation:
max(L(x)) = x + 26 >= x = x
max(N(L(0()),L(y))) = y + 42 >= y = y
max(N(L(s(x)),L(s(y)))) = x + y + 57 >= x + y + 46 = s(max(N(L(x),L(y))))
max(N(L(x),N(y,z))) = x + y + z + 26 >= x + y + z + 52 = max(N(L(x),L(max(N(y,z)))))
problem:
strict:
max(N(L(x),N(y,z))) -> max(N(L(x),L(max(N(y,z)))))
weak:
max(L(x)) -> x
max(N(L(0()),L(y))) -> y
max(N(L(s(x)),L(s(y)))) -> s(max(N(L(x),L(y))))
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {5}
transitions:
max1(10) -> 7,5
max1(6) -> 7*
N1(3,1) -> 6*
N1(3,3) -> 6*
N1(8,17) -> 6*
N1(4,2) -> 6*
N1(4,4) -> 6*
N1(9,8) -> 10*
N1(1,2) -> 6*
N1(1,4) -> 6*
N1(2,1) -> 6*
N1(2,3) -> 6*
N1(3,2) -> 6*
N1(3,4) -> 6*
N1(4,1) -> 6*
N1(4,3) -> 6*
N1(1,1) -> 6*
N1(1,3) -> 6*
N1(2,2) -> 6*
N1(2,4) -> 6*
L1(5) -> 17*
L1(7) -> 8*
L1(2) -> 9*
L1(4) -> 9*
L1(1) -> 9*
L1(3) -> 9*
s1(5) -> 7*
max0(2) -> 5*
max0(4) -> 5*
max0(1) -> 5*
max0(3) -> 5*
N0(3,1) -> 1*
N0(3,3) -> 1*
N0(4,2) -> 1*
N0(4,4) -> 1*
N0(1,2) -> 1*
N0(1,4) -> 1*
N0(2,1) -> 1*
N0(2,3) -> 1*
N0(3,2) -> 1*
N0(3,4) -> 1*
N0(4,1) -> 1*
N0(4,3) -> 1*
N0(1,1) -> 1*
N0(1,3) -> 1*
N0(2,2) -> 1*
N0(2,4) -> 1*
L0(2) -> 2*
L0(4) -> 2*
L0(1) -> 2*
L0(3) -> 2*
00() -> 3*
s0(5) -> 5*
s0(2) -> 4*
s0(4) -> 4*
s0(1) -> 4*
s0(3) -> 4*
1 -> 7,5
2 -> 7,5
3 -> 7,5
4 -> 7,5
5 -> 7*
7 -> 5*
problem:
strict:
weak:
max(N(L(x),N(y,z))) -> max(N(L(x),L(max(N(y,z)))))
max(L(x)) -> x
max(N(L(0()),L(y))) -> y
max(N(L(s(x)),L(s(y)))) -> s(max(N(L(x),L(y))))
Qed
Tool IRC1
stdout:
YES(?,O(n^1))
Tool IRC2
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: innermost runtime-complexity with respect to
Rules:
{ max(L(x)) -> x
, max(N(L(0()), L(y))) -> y
, max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y))))
, max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z)))))}
Proof Output:
Computation stopped due to timeout after 60.0 secondsTool RC1
stdout:
YES(?,O(n^1))
Tool RC2
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: runtime-complexity with respect to
Rules:
{ max(L(x)) -> x
, max(N(L(0()), L(y))) -> y
, max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y))))
, max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z)))))}
Proof Output:
Computation stopped due to timeout after 60.0 seconds