Tool CaT
stdout:
YES(?,O(n^2))
Problem:
g(0(),f(x,x)) -> x
g(x,s(y)) -> g(f(x,y),0())
g(s(x),y) -> g(f(x,y),0())
g(f(x,y),0()) -> f(g(x,0()),g(y,0()))
Proof:
Complexity Transformation Processor:
strict:
g(0(),f(x,x)) -> x
g(x,s(y)) -> g(f(x,y),0())
g(s(x),y) -> g(f(x,y),0())
g(f(x,y),0()) -> f(g(x,0()),g(y,0()))
weak:
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[s](x0) = x0 + 24,
[g](x0, x1) = x0 + x1,
[f](x0, x1) = x0 + x1 + 5,
[0] = 0
orientation:
g(0(),f(x,x)) = 2x + 5 >= x = x
g(x,s(y)) = x + y + 24 >= x + y + 5 = g(f(x,y),0())
g(s(x),y) = x + y + 24 >= x + y + 5 = g(f(x,y),0())
g(f(x,y),0()) = x + y + 5 >= x + y + 5 = f(g(x,0()),g(y,0()))
problem:
strict:
g(f(x,y),0()) -> f(g(x,0()),g(y,0()))
weak:
g(0(),f(x,x)) -> x
g(x,s(y)) -> g(f(x,y),0())
g(s(x),y) -> g(f(x,y),0())
Matrix Interpretation Processor:
dimension: 2
max_matrix:
[1 2]
[0 1]
interpretation:
[1 2] [0]
[s](x0) = [0 1]x0 + [2],
[1 1] [1 1]
[g](x0, x1) = [0 1]x0 + [0 1]x1,
[0]
[f](x0, x1) = x0 + x1 + [1],
[0]
[0] = [0]
orientation:
[1 1] [1 1] [1] [1 1] [1 1] [0]
g(f(x,y),0()) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = f(g(x,0()),g(y,0()))
[2 2] [1]
g(0(),f(x,x)) = [0 2]x + [1] >= x = x
[1 1] [1 3] [2] [1 1] [1 1] [1]
g(x,s(y)) = [0 1]x + [0 1]y + [2] >= [0 1]x + [0 1]y + [1] = g(f(x,y),0())
[1 3] [1 1] [2] [1 1] [1 1] [1]
g(s(x),y) = [0 1]x + [0 1]y + [2] >= [0 1]x + [0 1]y + [1] = g(f(x,y),0())
problem:
strict:
weak:
g(f(x,y),0()) -> f(g(x,0()),g(y,0()))
g(0(),f(x,x)) -> x
g(x,s(y)) -> g(f(x,y),0())
g(s(x),y) -> g(f(x,y),0())
Qed
Tool IRC1
stdout:
YES(?,O(n^1))
Tool IRC2
stdout:
YES(?,O(n^1))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ g(0(), f(x, x)) -> x
, g(x, s(y)) -> g(f(x, y), 0())
, g(s(x), y) -> g(f(x, y), 0())
, g(f(x, y), 0()) -> f(g(x, 0()), g(y, 0()))}
Proof Output:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with minimal-enrichment and initial automaton 'match''
--------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ g(0(), f(x, x)) -> x
, g(x, s(y)) -> g(f(x, y), 0())
, g(s(x), y) -> g(f(x, y), 0())
, g(f(x, y), 0()) -> f(g(x, 0()), g(y, 0()))}
Proof Output:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ g_0(2, 2) -> 1
, g_1(2, 4) -> 5
, g_1(2, 4) -> 6
, g_1(3, 4) -> 1
, g_1(4, 4) -> 6
, g_1(11, 4) -> 7
, g_1(12, 4) -> 8
, g_2(2, 9) -> 7
, g_2(2, 10) -> 8
, g_2(4, 10) -> 13
, g_2(9, 10) -> 13
, g_2(10, 10) -> 13
, 0_0() -> 1
, 0_0() -> 2
, 0_1() -> 4
, 0_2() -> 9
, 0_2() -> 10
, f_0(2, 2) -> 1
, f_0(2, 2) -> 2
, f_1(2, 2) -> 3
, f_1(2, 4) -> 1
, f_1(2, 4) -> 2
, f_1(2, 9) -> 11
, f_1(2, 10) -> 12
, f_1(5, 6) -> 1
, f_1(6, 6) -> 5
, f_1(6, 6) -> 6
, f_1(6, 6) -> 7
, f_1(6, 6) -> 8
, f_2(7, 8) -> 1
, f_2(8, 13) -> 5
, f_2(8, 13) -> 6
, f_2(8, 13) -> 7
, f_2(8, 13) -> 8
, s_0(2) -> 1
, s_0(2) -> 2}Tool RC1
stdout:
YES(?,O(n^1))
Tool RC2
stdout:
YES(?,O(n^1))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ g(0(), f(x, x)) -> x
, g(x, s(y)) -> g(f(x, y), 0())
, g(s(x), y) -> g(f(x, y), 0())
, g(f(x, y), 0()) -> f(g(x, 0()), g(y, 0()))}
Proof Output:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with minimal-enrichment and initial automaton 'match''
--------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ g(0(), f(x, x)) -> x
, g(x, s(y)) -> g(f(x, y), 0())
, g(s(x), y) -> g(f(x, y), 0())
, g(f(x, y), 0()) -> f(g(x, 0()), g(y, 0()))}
Proof Output:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ g_0(2, 2) -> 1
, g_1(2, 4) -> 5
, g_1(2, 4) -> 6
, g_1(3, 4) -> 1
, g_1(4, 4) -> 6
, g_1(11, 4) -> 7
, g_1(12, 4) -> 8
, g_2(2, 9) -> 7
, g_2(2, 10) -> 8
, g_2(4, 10) -> 13
, g_2(9, 10) -> 13
, g_2(10, 10) -> 13
, 0_0() -> 1
, 0_0() -> 2
, 0_1() -> 4
, 0_2() -> 9
, 0_2() -> 10
, f_0(2, 2) -> 1
, f_0(2, 2) -> 2
, f_1(2, 2) -> 3
, f_1(2, 4) -> 1
, f_1(2, 4) -> 2
, f_1(2, 9) -> 11
, f_1(2, 10) -> 12
, f_1(5, 6) -> 1
, f_1(6, 6) -> 5
, f_1(6, 6) -> 6
, f_1(6, 6) -> 7
, f_1(6, 6) -> 8
, f_2(7, 8) -> 1
, f_2(8, 13) -> 5
, f_2(8, 13) -> 6
, f_2(8, 13) -> 7
, f_2(8, 13) -> 8
, s_0(2) -> 1
, s_0(2) -> 2}