Tool CaT
stdout:
YES(?,O(n^1))
Problem:
q0(a(x1)) -> x(q1(x1))
q1(a(x1)) -> a(q1(x1))
q1(y(x1)) -> y(q1(x1))
a(q1(b(x1))) -> q2(a(y(x1)))
a(q2(a(x1))) -> q2(a(a(x1)))
a(q2(y(x1))) -> q2(a(y(x1)))
y(q1(b(x1))) -> q2(y(y(x1)))
y(q2(a(x1))) -> q2(y(a(x1)))
y(q2(y(x1))) -> q2(y(y(x1)))
q2(x(x1)) -> x(q0(x1))
q0(y(x1)) -> y(q3(x1))
q3(y(x1)) -> y(q3(x1))
q3(bl(x1)) -> bl(q4(x1))
Proof:
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {10,9,8,7,6,5}
transitions:
bl1(33) -> 34*
q41(35) -> 36*
q41(32) -> 33*
q41(41) -> 42*
q41(43) -> 44*
x1(15) -> 16*
q01(25) -> 26*
q01(17) -> 18*
q01(14) -> 15*
q01(23) -> 24*
q00(2) -> 5*
q00(4) -> 5*
q00(1) -> 5*
q00(3) -> 5*
a0(2) -> 7*
a0(4) -> 7*
a0(1) -> 7*
a0(3) -> 7*
x0(2) -> 1*
x0(4) -> 1*
x0(1) -> 1*
x0(3) -> 1*
q10(2) -> 6*
q10(4) -> 6*
q10(1) -> 6*
q10(3) -> 6*
y0(2) -> 8*
y0(4) -> 8*
y0(1) -> 8*
y0(3) -> 8*
b0(2) -> 2*
b0(4) -> 2*
b0(1) -> 2*
b0(3) -> 2*
q20(2) -> 9*
q20(4) -> 9*
q20(1) -> 9*
q20(3) -> 9*
q30(2) -> 10*
q30(4) -> 10*
q30(1) -> 10*
q30(3) -> 10*
bl0(2) -> 3*
bl0(4) -> 3*
bl0(1) -> 3*
bl0(3) -> 3*
q40(2) -> 4*
q40(4) -> 4*
q40(1) -> 4*
q40(3) -> 4*
1 -> 41,23
2 -> 32,14
3 -> 43,25
4 -> 35,17
16 -> 9*
18 -> 15*
24 -> 15*
26 -> 15*
34 -> 10*
36 -> 33*
42 -> 33*
44 -> 33*
problem:
QedTool 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:
{ q0(a(x1)) -> x(q1(x1))
, q1(a(x1)) -> a(q1(x1))
, q1(y(x1)) -> y(q1(x1))
, a(q1(b(x1))) -> q2(a(y(x1)))
, a(q2(a(x1))) -> q2(a(a(x1)))
, a(q2(y(x1))) -> q2(a(y(x1)))
, y(q1(b(x1))) -> q2(y(y(x1)))
, y(q2(a(x1))) -> q2(y(a(x1)))
, y(q2(y(x1))) -> q2(y(y(x1)))
, q2(x(x1)) -> x(q0(x1))
, q0(y(x1)) -> y(q3(x1))
, q3(y(x1)) -> y(q3(x1))
, q3(bl(x1)) -> bl(q4(x1))}
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:
{ q0(a(x1)) -> x(q1(x1))
, q1(a(x1)) -> a(q1(x1))
, q1(y(x1)) -> y(q1(x1))
, a(q1(b(x1))) -> q2(a(y(x1)))
, a(q2(a(x1))) -> q2(a(a(x1)))
, a(q2(y(x1))) -> q2(a(y(x1)))
, y(q1(b(x1))) -> q2(y(y(x1)))
, y(q2(a(x1))) -> q2(y(a(x1)))
, y(q2(y(x1))) -> q2(y(y(x1)))
, q2(x(x1)) -> x(q0(x1))
, q0(y(x1)) -> y(q3(x1))
, q3(y(x1)) -> y(q3(x1))
, q3(bl(x1)) -> bl(q4(x1))}
Proof Output:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ q0_0(2) -> 1
, q0_1(2) -> 3
, a_0(2) -> 1
, x_0(2) -> 2
, x_1(3) -> 1
, q1_0(2) -> 1
, y_0(2) -> 1
, b_0(2) -> 2
, q2_0(2) -> 1
, q3_0(2) -> 1
, bl_0(2) -> 2
, bl_1(4) -> 1
, q4_0(2) -> 2
, q4_1(2) -> 4}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:
{ q0(a(x1)) -> x(q1(x1))
, q1(a(x1)) -> a(q1(x1))
, q1(y(x1)) -> y(q1(x1))
, a(q1(b(x1))) -> q2(a(y(x1)))
, a(q2(a(x1))) -> q2(a(a(x1)))
, a(q2(y(x1))) -> q2(a(y(x1)))
, y(q1(b(x1))) -> q2(y(y(x1)))
, y(q2(a(x1))) -> q2(y(a(x1)))
, y(q2(y(x1))) -> q2(y(y(x1)))
, q2(x(x1)) -> x(q0(x1))
, q0(y(x1)) -> y(q3(x1))
, q3(y(x1)) -> y(q3(x1))
, q3(bl(x1)) -> bl(q4(x1))}
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:
{ q0(a(x1)) -> x(q1(x1))
, q1(a(x1)) -> a(q1(x1))
, q1(y(x1)) -> y(q1(x1))
, a(q1(b(x1))) -> q2(a(y(x1)))
, a(q2(a(x1))) -> q2(a(a(x1)))
, a(q2(y(x1))) -> q2(a(y(x1)))
, y(q1(b(x1))) -> q2(y(y(x1)))
, y(q2(a(x1))) -> q2(y(a(x1)))
, y(q2(y(x1))) -> q2(y(y(x1)))
, q2(x(x1)) -> x(q0(x1))
, q0(y(x1)) -> y(q3(x1))
, q3(y(x1)) -> y(q3(x1))
, q3(bl(x1)) -> bl(q4(x1))}
Proof Output:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ q0_0(2) -> 1
, q0_1(2) -> 3
, a_0(2) -> 1
, x_0(2) -> 2
, x_1(3) -> 1
, q1_0(2) -> 1
, y_0(2) -> 1
, b_0(2) -> 2
, q2_0(2) -> 1
, q3_0(2) -> 1
, bl_0(2) -> 2
, bl_1(4) -> 1
, q4_0(2) -> 2
, q4_1(2) -> 4}