Tool CaT
stdout:
YES(?,O(n^1))
Problem:
q0(0(x1)) -> 0'(q1(x1))
q1(0(x1)) -> 0(q1(x1))
q1(1'(x1)) -> 1'(q1(x1))
0(q1(1(x1))) -> q2(0(1'(x1)))
0'(q1(1(x1))) -> q2(0'(1'(x1)))
1'(q1(1(x1))) -> q2(1'(1'(x1)))
0(q2(0(x1))) -> q2(0(0(x1)))
0'(q2(0(x1))) -> q2(0'(0(x1)))
1'(q2(0(x1))) -> q2(1'(0(x1)))
0(q2(1'(x1))) -> q2(0(1'(x1)))
0'(q2(1'(x1))) -> q2(0'(1'(x1)))
1'(q2(1'(x1))) -> q2(1'(1'(x1)))
q2(0'(x1)) -> 0'(q0(x1))
q0(1'(x1)) -> 1'(q3(x1))
q3(1'(x1)) -> 1'(q3(x1))
q3(b(x1)) -> b(q4(x1))
Proof:
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {10,9,8,7,6,5,4}
transitions:
b1(12) -> 13*
q41(19) -> 20*
q41(21) -> 22*
q41(11) -> 12*
q00(2) -> 4*
q00(1) -> 4*
q00(3) -> 4*
00(2) -> 6*
00(1) -> 6*
00(3) -> 6*
0'0(2) -> 7*
0'0(1) -> 7*
0'0(3) -> 7*
q10(2) -> 5*
q10(1) -> 5*
q10(3) -> 5*
1'0(2) -> 8*
1'0(1) -> 8*
1'0(3) -> 8*
10(2) -> 1*
10(1) -> 1*
10(3) -> 1*
q20(2) -> 9*
q20(1) -> 9*
q20(3) -> 9*
q30(2) -> 10*
q30(1) -> 10*
q30(3) -> 10*
b0(2) -> 2*
b0(1) -> 2*
b0(3) -> 2*
q40(2) -> 3*
q40(1) -> 3*
q40(3) -> 3*
1 -> 19*
2 -> 11*
3 -> 21*
13 -> 10*
20 -> 12*
22 -> 12*
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(0(x1)) -> 0'(q1(x1))
, q1(0(x1)) -> 0(q1(x1))
, q1(1'(x1)) -> 1'(q1(x1))
, 0(q1(1(x1))) -> q2(0(1'(x1)))
, 0'(q1(1(x1))) -> q2(0'(1'(x1)))
, 1'(q1(1(x1))) -> q2(1'(1'(x1)))
, 0(q2(0(x1))) -> q2(0(0(x1)))
, 0'(q2(0(x1))) -> q2(0'(0(x1)))
, 1'(q2(0(x1))) -> q2(1'(0(x1)))
, 0(q2(1'(x1))) -> q2(0(1'(x1)))
, 0'(q2(1'(x1))) -> q2(0'(1'(x1)))
, 1'(q2(1'(x1))) -> q2(1'(1'(x1)))
, q2(0'(x1)) -> 0'(q0(x1))
, q0(1'(x1)) -> 1'(q3(x1))
, q3(1'(x1)) -> 1'(q3(x1))
, q3(b(x1)) -> b(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(0(x1)) -> 0'(q1(x1))
, q1(0(x1)) -> 0(q1(x1))
, q1(1'(x1)) -> 1'(q1(x1))
, 0(q1(1(x1))) -> q2(0(1'(x1)))
, 0'(q1(1(x1))) -> q2(0'(1'(x1)))
, 1'(q1(1(x1))) -> q2(1'(1'(x1)))
, 0(q2(0(x1))) -> q2(0(0(x1)))
, 0'(q2(0(x1))) -> q2(0'(0(x1)))
, 1'(q2(0(x1))) -> q2(1'(0(x1)))
, 0(q2(1'(x1))) -> q2(0(1'(x1)))
, 0'(q2(1'(x1))) -> q2(0'(1'(x1)))
, 1'(q2(1'(x1))) -> q2(1'(1'(x1)))
, q2(0'(x1)) -> 0'(q0(x1))
, q0(1'(x1)) -> 1'(q3(x1))
, q3(1'(x1)) -> 1'(q3(x1))
, q3(b(x1)) -> b(q4(x1))}
Proof Output:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ q0_0(2) -> 1
, 0_0(2) -> 1
, 0'_0(2) -> 1
, q1_0(2) -> 1
, 1'_0(2) -> 1
, 1_0(2) -> 2
, q2_0(2) -> 1
, q3_0(2) -> 1
, b_0(2) -> 2
, b_1(3) -> 1
, q4_0(2) -> 2
, q4_1(2) -> 3}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(0(x1)) -> 0'(q1(x1))
, q1(0(x1)) -> 0(q1(x1))
, q1(1'(x1)) -> 1'(q1(x1))
, 0(q1(1(x1))) -> q2(0(1'(x1)))
, 0'(q1(1(x1))) -> q2(0'(1'(x1)))
, 1'(q1(1(x1))) -> q2(1'(1'(x1)))
, 0(q2(0(x1))) -> q2(0(0(x1)))
, 0'(q2(0(x1))) -> q2(0'(0(x1)))
, 1'(q2(0(x1))) -> q2(1'(0(x1)))
, 0(q2(1'(x1))) -> q2(0(1'(x1)))
, 0'(q2(1'(x1))) -> q2(0'(1'(x1)))
, 1'(q2(1'(x1))) -> q2(1'(1'(x1)))
, q2(0'(x1)) -> 0'(q0(x1))
, q0(1'(x1)) -> 1'(q3(x1))
, q3(1'(x1)) -> 1'(q3(x1))
, q3(b(x1)) -> b(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(0(x1)) -> 0'(q1(x1))
, q1(0(x1)) -> 0(q1(x1))
, q1(1'(x1)) -> 1'(q1(x1))
, 0(q1(1(x1))) -> q2(0(1'(x1)))
, 0'(q1(1(x1))) -> q2(0'(1'(x1)))
, 1'(q1(1(x1))) -> q2(1'(1'(x1)))
, 0(q2(0(x1))) -> q2(0(0(x1)))
, 0'(q2(0(x1))) -> q2(0'(0(x1)))
, 1'(q2(0(x1))) -> q2(1'(0(x1)))
, 0(q2(1'(x1))) -> q2(0(1'(x1)))
, 0'(q2(1'(x1))) -> q2(0'(1'(x1)))
, 1'(q2(1'(x1))) -> q2(1'(1'(x1)))
, q2(0'(x1)) -> 0'(q0(x1))
, q0(1'(x1)) -> 1'(q3(x1))
, q3(1'(x1)) -> 1'(q3(x1))
, q3(b(x1)) -> b(q4(x1))}
Proof Output:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ q0_0(2) -> 1
, 0_0(2) -> 1
, 0'_0(2) -> 1
, q1_0(2) -> 1
, 1'_0(2) -> 1
, 1_0(2) -> 2
, q2_0(2) -> 1
, q3_0(2) -> 1
, b_0(2) -> 2
, b_1(3) -> 1
, q4_0(2) -> 2
, q4_1(2) -> 3}