Tool CaT
stdout:
YES(?,O(n^1))
Problem:
0(x1) -> 1(x1)
0(0(x1)) -> 0(x1)
3(4(5(x1))) -> 4(3(5(x1)))
2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2(2(2(2(2(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
0(0(1(0(0(0(1(1(1(0(1(1(1(1(1(0(0(1(0(0(1(0(1(1(0(1(0(0(1(1(0(0(0(1(
0
(
1
(
1
(
0
(
0
(
0
(
1
(
0
(
0
(
0
(
1
(
1
(
0
(
0
(
0
(
1
(
1
(
1
(
0
(
1
(
1
(
0
(
0
(
1
(
0
(
1
(
1
(
1
(
0
(
1
(
0
(
0
(
0
(
1
(
1
(
0
(
0
(
1
(
1
(
1
(
1
(
1
(
0
(
1
(
0
(
0
(
0
(
1
(
0
(
0
(
0
(
0
(
0
(
1
(
0
(
1
(
1
(
0
(
1
(
1
(
0
(
0
(
0
(
1
(
0
(
0
(
0
(
0
(
0
(
1
(
1
(
1
(
0
(
1
(
1
(
0
(
1
(
1
(
1
(
0
(
1
(
0
(
0
(
1
(
0
(
0
(
0
(
0
(
0
(
0
(
1
(
0
(
0
(
1
(
0
(
1
(
1
(
0
(
1
(
0
(
1
(
1
(
1
(
1
(
1
(
1
(
1
(
1
(
1
(
0
(
1
(
1
(
1
(
1
(
1
(
1
(
0
(
1
(
1
(
1
(
1
(
0
(
1
(
0
(
1
(
1
(
1
(
0
(
1
(
1
(
0
(
0
(
1
(
1
(
0
(
1
(
0
(
1
(
0
(
0
(
1
(
0
(
0
(
0
(
0
(
0
(
1
(
0
(
0
(
0
(
1
(
1
(
1
(
0
(
1
(
0
(
1
(
0
(
1
(
1
(
1
(
0
(
0
(
1
(
0
(
1
(
0
(
0
(
0
(
1
(
1
(
0
(
0
(
0
(
1
(
1
(
1
(
0
(
0
(
0
(
0
(
0
(
1
(
0
(
1
(
1
(
0
(
1
(
1
(
1
(
0
(
0
(
0
(
0
(
1
(
1
(
0
(
0
(
0
(
1
(
1
(
1
(
0
(
0
(
0
(
1
(
1
(
0
(
1
(
0
(
0
(
1
(
0
(
0
(
0
(
1
(
0
(
0
(
0
(
1
(
0
(
0
(
1
(
1
(
0
(
0
(
0
(
0
(
1
(
1
(
1
(
0
(
0
(
0
(
1
(
1
(
1
(
0
(
1
(
1
(
1
(
1
(
1
(
1
(
1
(
1
(
1
(
1
(
1
(
0
(
0
(
0
(
1
(
0
(
0
(
0
(
1
(
1
(
0
(
1
(
0
(
0
(
1
(
1
(
1
(
1
(
0
(
1
(
1
(
1
(
1
(
1
(
0
(
0
(
0
(
0
(
0
(
0
(
1
(
1
(
0
(
0
(
0
(
1
(
0
(
0
(
1
(
1
(
1
(
1
(
0
(
0
(
0
(
0
(
1
(
0
(
0
(
1
(
1
(
0
(
1
(
0(1(1(0(0(0(1(1(0(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
0(1(0(0(1(1(1(1(1(1(0(1(1(0(1(1(0(1(0(0(0(1(0(0(0(1(1(1(1(0(1(0(1(0(
1
(
1
(
0
(
1
(
1
(
1
(
1
(
1
(
0
(
0
(
1
(
0
(
1
(
1
(
0
(
1
(
0
(
0
(
1
(
0
(
1
(
1
(
0
(
1
(
0
(
1
(
1
(
1
(
0
(
1
(
1
(
1
(
0
(
0
(
0
(
0
(
1
(
0
(
0
(
1
(
1
(
0
(
0
(
1
(
1
(
0
(
0
(
1
(
0
(
0
(
1
(
1
(
1
(
1
(
1
(
1
(
1
(
0
(
1
(
0
(
0
(
0
(
1
(
0
(
1
(
0
(
0
(
0
(
1
(
1
(
0
(
1
(
0
(
1
(
1
(
1
(
1
(
0
(
0
(
0
(
0
(
1
(
0
(
1
(
1
(
1
(
1
(
1
(
0
(
1
(
1
(
1
(
0
(
0
(
1
(
0
(
1
(
1
(
1
(
1
(
0
(
1
(
1
(
0
(
0
(
0
(
1
(
0
(
0
(
1
(
0
(
1
(
0
(
1
(
1
(
0
(
0
(
1
(
1
(
0
(
1
(
0
(
0
(
1
(
1
(
1
(
0
(
1
(
0
(
1
(
0
(
1
(
1
(
0
(
1
(
0
(
1
(
0
(
0
(
1
(
0
(
0
(
0
(
0
(
1
(
1
(
1
(
1
(
0
(
1
(
0
(
0
(
0
(
0
(
0
(
0
(
0
(
1
(
1
(
0
(
1
(
1
(
0
(
1
(
0
(
0
(
1
(
1
(
1
(
1
(
0
(
1
(
0
(
1
(
0
(
0
(
0
(
1
(
0
(
1
(
0
(
0
(
1
(
0
(
1
(
0
(
0
(
1
(
1
(
0
(
1
(
1
(
1
(
0
(
1
(
0
(
1
(
0
(
0
(
0
(
1
(
0
(
0
(
1
(
0
(
1
(
0
(
0
(
1
(
1
(
1
(
0
(
1
(
0
(
1
(
1
(
0
(
1
(
0
(
0
(
0
(
1
(
1
(
1
(
1
(
1
(
0
(
0
(
0
(
0
(
1
(
0
(
1
(
0
(
1
(
0
(
0
(
0
(
1
(
0
(
0
(
0
(
0
(
0
(
1
(
0
(
1
(
1
(
0
(
0
(
0
(
0
(
0
(
1
(
0
(
1
(
0
(
0
(
0
(
0
(
1
(
1
(
1
(
0
(
0
(
0
(
0
(
0
(
1
(
1
(
1
(
0
(
1
(
0
(
1
(
0
(
0
(
0
(
0
(
1
(
1
(
1
(
0
(
0
(
1
(
1
(
1
(
1
(
0
(
1
(
0
(
0
(
1
(
0
(
1
(
0
(
1
(
0
(
1
(
0
(
0
(
1
(
1
(
1
(
1
(
1(0(0(0(1(0(0(0(0(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2(2(2(2(2(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
Proof:
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {6,5,4}
transitions:
41(21) -> 22*
31(20) -> 21*
51(29) -> 30*
51(19) -> 20*
51(31) -> 32*
11(17) -> 18*
11(9) -> 10*
11(11) -> 12*
00(2) -> 4*
00(1) -> 4*
00(3) -> 4*
10(2) -> 1*
10(1) -> 1*
10(3) -> 1*
30(2) -> 5*
30(1) -> 5*
30(3) -> 5*
40(2) -> 2*
40(1) -> 2*
40(3) -> 2*
50(2) -> 3*
50(1) -> 3*
50(3) -> 3*
20(2) -> 6*
20(1) -> 6*
20(3) -> 6*
1 -> 29,11
2 -> 19,17
3 -> 31,9
10 -> 4*
12 -> 4*
18 -> 4*
22 -> 5*
30 -> 20*
32 -> 20*
problem:
QedTool IRC1
stdout:
MAYBE
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:
{ 0(x1) -> 1(x1)
, 0(0(x1)) -> 0(x1)
, 3(4(5(x1))) -> 4(3(5(x1)))
, 2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
0(0(1(0(0(0(1(1(1(0(1(1(1(1(1(0(0(1(0(0(1(0(1(1(0(1(0(0(1(1(0(0(0(1(0(1(1(0(0(0(1(0(0(0(1(1(0(0(0(1(1(1(0(1(1(0(0(1(0(1(1(1(0(1(0(0(0(1(1(0(0(1(1(1(1(1(0(1(0(0(0(1(0(0(0(0(0(1(0(1(1(0(1(1(0(0(0(1(0(0(0(0(0(1(1(1(0(1(1(0(1(1(1(0(1(0(0(1(0(0(0(0(0(0(1(0(0(1(0(1(1(0(1(0(1(1(1(1(1(1(1(1(1(0(1(1(1(1(1(1(0(1(1(1(1(0(1(0(1(1(1(0(1(1(0(0(1(1(0(1(0(1(0(0(1(0(0(0(0(0(1(0(0(0(1(1(1(0(1(0(1(0(1(1(1(0(0(1(0(1(0(0(0(1(1(0(0(0(1(1(1(0(0(0(0(0(1(0(1(1(0(1(1(1(0(0(0(0(1(1(0(0(0(1(1(1(0(0(0(1(1(0(1(0(0(1(0(0(0(1(0(0(0(1(0(0(1(1(0(0(0(0(1(1(1(0(0(0(1(1(1(0(1(1(1(1(1(1(1(1(1(1(1(0(0(0(1(0(0(0(1(1(0(1(0(0(1(1(1(1(0(1(1(1(1(1(0(0(0(0(0(0(1(1(0(0(0(1(0(0(1(1(1(1(0(0(0(0(1(0(0(1(1(0(1(0(1(1(0(0(0(1(1(0(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
, 0(1(0(0(1(1(1(1(1(1(0(1(1(0(1(1(0(1(0(0(0(1(0(0(0(1(1(1(1(0(1(0(1(0(1(1(0(1(1(1(1(1(0(0(1(0(1(1(0(1(0(0(1(0(1(1(0(1(0(1(1(1(0(1(1(1(0(0(0(0(1(0(0(1(1(0(0(1(1(0(0(1(0(0(1(1(1(1(1(1(1(0(1(0(0(0(1(0(1(0(0(0(1(1(0(1(0(1(1(1(1(0(0(0(0(1(0(1(1(1(1(1(0(1(1(1(0(0(1(0(1(1(1(1(0(1(1(0(0(0(1(0(0(1(0(1(0(1(1(0(0(1(1(0(1(0(0(1(1(1(0(1(0(1(0(1(1(0(1(0(1(0(0(1(0(0(0(0(1(1(1(1(0(1(0(0(0(0(0(0(0(1(1(0(1(1(0(1(0(0(1(1(1(1(0(1(0(1(0(0(0(1(0(1(0(0(1(0(1(0(0(1(1(0(1(1(1(0(1(0(1(0(0(0(1(0(0(1(0(1(0(0(1(1(1(0(1(0(1(1(0(1(0(0(0(1(1(1(1(1(0(0(0(0(1(0(1(0(1(0(0(0(1(0(0(0(0(0(1(0(1(1(0(0(0(0(0(1(0(1(0(0(0(0(1(1(1(0(0(0(0(0(1(1(1(0(1(0(1(0(0(0(0(1(1(1(0(0(1(1(1(1(0(1(0(0(1(0(1(0(1(0(1(0(0(1(1(1(1(1(0(0(0(1(0(0(0(0(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(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:
{ 0(x1) -> 1(x1)
, 0(0(x1)) -> 0(x1)
, 3(4(5(x1))) -> 4(3(5(x1)))
, 2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
0(0(1(0(0(0(1(1(1(0(1(1(1(1(1(0(0(1(0(0(1(0(1(1(0(1(0(0(1(1(0(0(0(1(0(1(1(0(0(0(1(0(0(0(1(1(0(0(0(1(1(1(0(1(1(0(0(1(0(1(1(1(0(1(0(0(0(1(1(0(0(1(1(1(1(1(0(1(0(0(0(1(0(0(0(0(0(1(0(1(1(0(1(1(0(0(0(1(0(0(0(0(0(1(1(1(0(1(1(0(1(1(1(0(1(0(0(1(0(0(0(0(0(0(1(0(0(1(0(1(1(0(1(0(1(1(1(1(1(1(1(1(1(0(1(1(1(1(1(1(0(1(1(1(1(0(1(0(1(1(1(0(1(1(0(0(1(1(0(1(0(1(0(0(1(0(0(0(0(0(1(0(0(0(1(1(1(0(1(0(1(0(1(1(1(0(0(1(0(1(0(0(0(1(1(0(0(0(1(1(1(0(0(0(0(0(1(0(1(1(0(1(1(1(0(0(0(0(1(1(0(0(0(1(1(1(0(0(0(1(1(0(1(0(0(1(0(0(0(1(0(0(0(1(0(0(1(1(0(0(0(0(1(1(1(0(0(0(1(1(1(0(1(1(1(1(1(1(1(1(1(1(1(0(0(0(1(0(0(0(1(1(0(1(0(0(1(1(1(1(0(1(1(1(1(1(0(0(0(0(0(0(1(1(0(0(0(1(0(0(1(1(1(1(0(0(0(0(1(0(0(1(1(0(1(0(1(1(0(0(0(1(1(0(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
, 0(1(0(0(1(1(1(1(1(1(0(1(1(0(1(1(0(1(0(0(0(1(0(0(0(1(1(1(1(0(1(0(1(0(1(1(0(1(1(1(1(1(0(0(1(0(1(1(0(1(0(0(1(0(1(1(0(1(0(1(1(1(0(1(1(1(0(0(0(0(1(0(0(1(1(0(0(1(1(0(0(1(0(0(1(1(1(1(1(1(1(0(1(0(0(0(1(0(1(0(0(0(1(1(0(1(0(1(1(1(1(0(0(0(0(1(0(1(1(1(1(1(0(1(1(1(0(0(1(0(1(1(1(1(0(1(1(0(0(0(1(0(0(1(0(1(0(1(1(0(0(1(1(0(1(0(0(1(1(1(0(1(0(1(0(1(1(0(1(0(1(0(0(1(0(0(0(0(1(1(1(1(0(1(0(0(0(0(0(0(0(1(1(0(1(1(0(1(0(0(1(1(1(1(0(1(0(1(0(0(0(1(0(1(0(0(1(0(1(0(0(1(1(0(1(1(1(0(1(0(1(0(0(0(1(0(0(1(0(1(0(0(1(1(1(0(1(0(1(1(0(1(0(0(0(1(1(1(1(1(0(0(0(0(1(0(1(0(1(0(0(0(1(0(0(0(0(0(1(0(1(1(0(0(0(0(0(1(0(1(0(0(0(0(1(1(1(0(0(0(0(0(1(1(1(0(1(0(1(0(0(0(0(1(1(1(0(0(1(1(1(1(0(1(0(0(1(0(1(0(1(0(1(0(0(1(1(1(1(1(0(0(0(1(0(0(0(0(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))}
Proof Output:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ 0_0(2) -> 1
, 1_0(2) -> 2
, 1_1(2) -> 1
, 3_0(2) -> 1
, 3_1(4) -> 3
, 4_0(2) -> 2
, 4_1(3) -> 1
, 5_0(2) -> 2
, 5_1(2) -> 4
, 2_0(2) -> 1}Tool RC1
stdout:
MAYBE
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:
{ 0(x1) -> 1(x1)
, 0(0(x1)) -> 0(x1)
, 3(4(5(x1))) -> 4(3(5(x1)))
, 2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
0(0(1(0(0(0(1(1(1(0(1(1(1(1(1(0(0(1(0(0(1(0(1(1(0(1(0(0(1(1(0(0(0(1(0(1(1(0(0(0(1(0(0(0(1(1(0(0(0(1(1(1(0(1(1(0(0(1(0(1(1(1(0(1(0(0(0(1(1(0(0(1(1(1(1(1(0(1(0(0(0(1(0(0(0(0(0(1(0(1(1(0(1(1(0(0(0(1(0(0(0(0(0(1(1(1(0(1(1(0(1(1(1(0(1(0(0(1(0(0(0(0(0(0(1(0(0(1(0(1(1(0(1(0(1(1(1(1(1(1(1(1(1(0(1(1(1(1(1(1(0(1(1(1(1(0(1(0(1(1(1(0(1(1(0(0(1(1(0(1(0(1(0(0(1(0(0(0(0(0(1(0(0(0(1(1(1(0(1(0(1(0(1(1(1(0(0(1(0(1(0(0(0(1(1(0(0(0(1(1(1(0(0(0(0(0(1(0(1(1(0(1(1(1(0(0(0(0(1(1(0(0(0(1(1(1(0(0(0(1(1(0(1(0(0(1(0(0(0(1(0(0(0(1(0(0(1(1(0(0(0(0(1(1(1(0(0(0(1(1(1(0(1(1(1(1(1(1(1(1(1(1(1(0(0(0(1(0(0(0(1(1(0(1(0(0(1(1(1(1(0(1(1(1(1(1(0(0(0(0(0(0(1(1(0(0(0(1(0(0(1(1(1(1(0(0(0(0(1(0(0(1(1(0(1(0(1(1(0(0(0(1(1(0(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
, 0(1(0(0(1(1(1(1(1(1(0(1(1(0(1(1(0(1(0(0(0(1(0(0(0(1(1(1(1(0(1(0(1(0(1(1(0(1(1(1(1(1(0(0(1(0(1(1(0(1(0(0(1(0(1(1(0(1(0(1(1(1(0(1(1(1(0(0(0(0(1(0(0(1(1(0(0(1(1(0(0(1(0(0(1(1(1(1(1(1(1(0(1(0(0(0(1(0(1(0(0(0(1(1(0(1(0(1(1(1(1(0(0(0(0(1(0(1(1(1(1(1(0(1(1(1(0(0(1(0(1(1(1(1(0(1(1(0(0(0(1(0(0(1(0(1(0(1(1(0(0(1(1(0(1(0(0(1(1(1(0(1(0(1(0(1(1(0(1(0(1(0(0(1(0(0(0(0(1(1(1(1(0(1(0(0(0(0(0(0(0(1(1(0(1(1(0(1(0(0(1(1(1(1(0(1(0(1(0(0(0(1(0(1(0(0(1(0(1(0(0(1(1(0(1(1(1(0(1(0(1(0(0(0(1(0(0(1(0(1(0(0(1(1(1(0(1(0(1(1(0(1(0(0(0(1(1(1(1(1(0(0(0(0(1(0(1(0(1(0(0(0(1(0(0(0(0(0(1(0(1(1(0(0(0(0(0(1(0(1(0(0(0(0(1(1(1(0(0(0(0(0(1(1(1(0(1(0(1(0(0(0(0(1(1(1(0(0(1(1(1(1(0(1(0(0(1(0(1(0(1(0(1(0(0(1(1(1(1(1(0(0(0(1(0(0(0(0(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(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:
{ 0(x1) -> 1(x1)
, 0(0(x1)) -> 0(x1)
, 3(4(5(x1))) -> 4(3(5(x1)))
, 2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
0(0(1(0(0(0(1(1(1(0(1(1(1(1(1(0(0(1(0(0(1(0(1(1(0(1(0(0(1(1(0(0(0(1(0(1(1(0(0(0(1(0(0(0(1(1(0(0(0(1(1(1(0(1(1(0(0(1(0(1(1(1(0(1(0(0(0(1(1(0(0(1(1(1(1(1(0(1(0(0(0(1(0(0(0(0(0(1(0(1(1(0(1(1(0(0(0(1(0(0(0(0(0(1(1(1(0(1(1(0(1(1(1(0(1(0(0(1(0(0(0(0(0(0(1(0(0(1(0(1(1(0(1(0(1(1(1(1(1(1(1(1(1(0(1(1(1(1(1(1(0(1(1(1(1(0(1(0(1(1(1(0(1(1(0(0(1(1(0(1(0(1(0(0(1(0(0(0(0(0(1(0(0(0(1(1(1(0(1(0(1(0(1(1(1(0(0(1(0(1(0(0(0(1(1(0(0(0(1(1(1(0(0(0(0(0(1(0(1(1(0(1(1(1(0(0(0(0(1(1(0(0(0(1(1(1(0(0(0(1(1(0(1(0(0(1(0(0(0(1(0(0(0(1(0(0(1(1(0(0(0(0(1(1(1(0(0(0(1(1(1(0(1(1(1(1(1(1(1(1(1(1(1(0(0(0(1(0(0(0(1(1(0(1(0(0(1(1(1(1(0(1(1(1(1(1(0(0(0(0(0(0(1(1(0(0(0(1(0(0(1(1(1(1(0(0(0(0(1(0(0(1(1(0(1(0(1(1(0(0(0(1(1(0(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
, 0(1(0(0(1(1(1(1(1(1(0(1(1(0(1(1(0(1(0(0(0(1(0(0(0(1(1(1(1(0(1(0(1(0(1(1(0(1(1(1(1(1(0(0(1(0(1(1(0(1(0(0(1(0(1(1(0(1(0(1(1(1(0(1(1(1(0(0(0(0(1(0(0(1(1(0(0(1(1(0(0(1(0(0(1(1(1(1(1(1(1(0(1(0(0(0(1(0(1(0(0(0(1(1(0(1(0(1(1(1(1(0(0(0(0(1(0(1(1(1(1(1(0(1(1(1(0(0(1(0(1(1(1(1(0(1(1(0(0(0(1(0(0(1(0(1(0(1(1(0(0(1(1(0(1(0(0(1(1(1(0(1(0(1(0(1(1(0(1(0(1(0(0(1(0(0(0(0(1(1(1(1(0(1(0(0(0(0(0(0(0(1(1(0(1(1(0(1(0(0(1(1(1(1(0(1(0(1(0(0(0(1(0(1(0(0(1(0(1(0(0(1(1(0(1(1(1(0(1(0(1(0(0(0(1(0(0(1(0(1(0(0(1(1(1(0(1(0(1(1(0(1(0(0(0(1(1(1(1(1(0(0(0(0(1(0(1(0(1(0(0(0(1(0(0(0(0(0(1(0(1(1(0(0(0(0(0(1(0(1(0(0(0(0(1(1(1(0(0(0(0(0(1(1(1(0(1(0(1(0(0(0(0(1(1(1(0(0(1(1(1(1(0(1(0(0(1(0(1(0(1(0(1(0(0(1(1(1(1(1(0(0(0(1(0(0(0(0(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))}
Proof Output:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ 0_0(2) -> 1
, 1_0(2) -> 2
, 1_1(2) -> 1
, 3_0(2) -> 1
, 3_1(4) -> 3
, 4_0(2) -> 2
, 4_1(3) -> 1
, 5_0(2) -> 2
, 5_1(2) -> 4
, 2_0(2) -> 1}