Tool CaT
stdout:
YES(?,O(n^1))
Problem:
0(1(2(x1))) -> 0(1(3(2(x1))))
0(1(2(x1))) -> 0(2(1(0(x1))))
0(1(2(x1))) -> 0(2(1(3(x1))))
0(1(2(x1))) -> 0(2(2(1(x1))))
0(1(2(x1))) -> 0(2(2(1(4(x1)))))
0(1(2(x1))) -> 5(1(0(5(2(3(x1))))))
0(2(4(x1))) -> 0(2(1(4(3(x1)))))
0(4(2(x1))) -> 4(0(2(3(x1))))
0(4(2(x1))) -> 4(0(5(5(2(x1)))))
0(0(4(2(x1)))) -> 0(0(2(2(3(4(x1))))))
0(1(2(2(x1)))) -> 0(2(1(0(2(x1)))))
0(1(2(2(x1)))) -> 1(3(0(2(2(x1)))))
0(1(2(4(x1)))) -> 0(1(4(2(3(x1)))))
0(1(2(4(x1)))) -> 4(0(2(2(1(1(x1))))))
0(1(2(4(x1)))) -> 4(0(5(5(2(1(x1))))))
0(1(2(5(x1)))) -> 3(5(5(2(1(0(x1))))))
0(1(4(2(x1)))) -> 0(5(2(1(4(x1)))))
0(1(5(2(x1)))) -> 1(5(0(2(3(x1)))))
0(1(5(2(x1)))) -> 0(2(2(1(0(5(x1))))))
0(1(5(2(x1)))) -> 5(5(0(2(1(3(x1))))))
0(2(4(2(x1)))) -> 0(5(4(3(2(2(x1))))))
0(3(1(2(x1)))) -> 0(2(1(3(2(x1)))))
0(3(1(2(x1)))) -> 1(0(2(5(3(x1)))))
0(3(1(2(x1)))) -> 1(5(0(2(3(x1)))))
0(3(1(2(x1)))) -> 3(0(2(2(1(x1)))))
0(3(1(2(x1)))) -> 3(2(2(1(0(x1)))))
0(3(1(2(x1)))) -> 0(3(2(3(1(3(x1))))))
0(3(4(2(x1)))) -> 0(2(2(3(4(x1)))))
5(0(1(2(x1)))) -> 1(3(2(5(0(x1)))))
5(0(1(2(x1)))) -> 5(0(2(1(3(3(x1))))))
0(1(1(2(5(x1))))) -> 5(0(2(5(1(1(x1))))))
0(2(3(4(2(x1))))) -> 3(2(2(3(4(0(x1))))))
0(3(1(2(5(x1))))) -> 2(3(1(3(0(5(x1))))))
0(3(1(5(2(x1))))) -> 0(3(2(5(1(2(x1))))))
0(3(4(1(4(x1))))) -> 0(5(3(1(4(4(x1))))))
0(3(5(1(2(x1))))) -> 5(5(3(2(1(0(x1))))))
0(4(0(4(2(x1))))) -> 4(4(0(0(2(2(x1))))))
0(4(1(1(2(x1))))) -> 3(1(4(0(2(1(x1))))))
0(4(1(2(2(x1))))) -> 4(1(0(2(2(3(x1))))))
0(4(1(2(5(x1))))) -> 3(4(1(0(2(5(x1))))))
0(4(2(1(2(x1))))) -> 4(1(3(2(0(2(x1))))))
0(4(2(1(4(x1))))) -> 0(2(1(4(4(4(x1))))))
0(4(2(5(2(x1))))) -> 5(4(3(2(2(0(x1))))))
0(4(5(1(2(x1))))) -> 1(4(2(0(5(5(x1))))))
0(4(5(1(2(x1))))) -> 4(0(2(5(1(1(x1))))))
5(0(1(2(2(x1))))) -> 5(0(2(2(1(2(x1))))))
5(0(2(4(2(x1))))) -> 0(2(2(5(1(4(x1))))))
5(0(4(4(2(x1))))) -> 0(5(2(5(4(4(x1))))))
Proof:
Bounds Processor:
bound: 2
enrichment: match
automaton:
final states: {6,5}
transitions:
01(45) -> 46*
01(15) -> 16*
01(142) -> 143*
01(107) -> 108*
01(37) -> 38*
01(199) -> 200*
01(179) -> 180*
01(286) -> 287*
01(156) -> 157*
01(273) -> 274*
01(153) -> 154*
01(43) -> 44*
01(33) -> 34*
21(35) -> 36*
21(25) -> 26*
21(117) -> 118*
21(289) -> 290*
21(17) -> 18*
21(12) -> 13*
21(189) -> 190*
21(119) -> 120*
21(69) -> 70*
21(226) -> 227*
21(111) -> 112*
21(198) -> 199*
21(285) -> 286*
21(23) -> 24*
21(170) -> 171*
21(155) -> 156*
21(105) -> 106*
11(77) -> 78*
11(254) -> 255*
11(169) -> 170*
11(79) -> 80*
11(34) -> 35*
11(14) -> 15*
11(71) -> 72*
11(158) -> 159*
11(108) -> 109*
11(275) -> 276*
11(68) -> 69*
11(287) -> 288*
41(187) -> 188*
41(167) -> 168*
41(127) -> 128*
41(87) -> 88*
41(274) -> 275*
41(271) -> 272*
41(251) -> 252*
41(263) -> 264*
41(253) -> 254*
41(143) -> 144*
41(133) -> 134*
41(93) -> 94*
41(265) -> 266*
41(135) -> 136*
41(125) -> 126*
41(297) -> 298*
41(95) -> 96*
41(85) -> 86*
31(237) -> 238*
31(227) -> 228*
31(217) -> 218*
31(157) -> 158*
31(59) -> 60*
31(186) -> 187*
31(61) -> 62*
31(51) -> 52*
31(243) -> 244*
31(223) -> 224*
31(290) -> 291*
31(255) -> 256*
31(53) -> 54*
31(245) -> 246*
31(235) -> 236*
31(225) -> 226*
31(13) -> 14*
51(207) -> 208*
51(197) -> 198*
51(177) -> 178*
51(209) -> 210*
51(109) -> 110*
51(201) -> 202*
51(146) -> 147*
51(106) -> 107*
51(215) -> 216*
51(145) -> 146*
02(309) -> 310*
00(2) -> 5*
00(4) -> 5*
00(1) -> 5*
00(3) -> 5*
52(308) -> 309*
10(2) -> 1*
10(4) -> 1*
10(1) -> 1*
10(3) -> 1*
22(307) -> 308*
20(2) -> 2*
20(4) -> 2*
20(1) -> 2*
20(3) -> 2*
12(306) -> 307*
30(2) -> 3*
30(4) -> 3*
30(1) -> 3*
30(3) -> 3*
42(319) -> 320*
42(311) -> 312*
42(305) -> 306*
42(317) -> 318*
40(2) -> 4*
40(4) -> 4*
40(1) -> 4*
40(3) -> 4*
50(2) -> 6*
50(4) -> 6*
50(1) -> 6*
50(3) -> 6*
1 -> 93,77,59,43,23
2 -> 85,68,51,33,12
3 -> 95,79,61,45,25
4 -> 87,71,53,37,17
13 -> 155,153,145
15 -> 189*
16 -> 38,46,154,289,44,251,217,5
18 -> 13*
24 -> 13*
26 -> 13*
34 -> 251*
35 -> 225*
36 -> 15*
38 -> 34*
44 -> 34*
46 -> 34*
52 -> 197,125,105,34
54 -> 201,127,111,34
60 -> 207,133,117,34
62 -> 209,135,119,34
69 -> 169*
70 -> 273,177,35
72 -> 69*
78 -> 69*
80 -> 69*
86 -> 253,235,68
88 -> 263,237,68
94 -> 265,243,68
96 -> 271,245,68
105 -> 319*
106 -> 285,167,142
110 -> 44,251,5
111 -> 317*
112 -> 106*
117 -> 305*
118 -> 106*
119 -> 311*
120 -> 106*
126 -> 34*
128 -> 34*
134 -> 34*
136 -> 34*
143 -> 215*
144 -> 44,38,251,5
147 -> 142*
154 -> 289,34
156 -> 186*
159 -> 46,44,251,5
168 -> 14*
171 -> 105*
178 -> 179,146
180 -> 46,154,44,5
188 -> 177*
190 -> 223,15
200 -> 158*
202 -> 198*
208 -> 198*
210 -> 198*
216 -> 158*
218 -> 38,46,34,251,5
224 -> 16,154,143,217,46,34,251,5
228 -> 15*
236 -> 35*
238 -> 35*
244 -> 35*
246 -> 35*
252 -> 227*
254 -> 297*
256 -> 177*
264 -> 254*
266 -> 254*
272 -> 254*
276 -> 217*
288 -> 143*
291 -> 287*
298 -> 14*
310 -> 16,5,217
312 -> 306*
318 -> 306*
320 -> 306*
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(1(2(x1))) -> 0(1(3(2(x1))))
, 0(1(2(x1))) -> 0(2(1(0(x1))))
, 0(1(2(x1))) -> 0(2(1(3(x1))))
, 0(1(2(x1))) -> 0(2(2(1(x1))))
, 0(1(2(x1))) -> 0(2(2(1(4(x1)))))
, 0(1(2(x1))) -> 5(1(0(5(2(3(x1))))))
, 0(2(4(x1))) -> 0(2(1(4(3(x1)))))
, 0(4(2(x1))) -> 4(0(2(3(x1))))
, 0(4(2(x1))) -> 4(0(5(5(2(x1)))))
, 0(0(4(2(x1)))) -> 0(0(2(2(3(4(x1))))))
, 0(1(2(2(x1)))) -> 0(2(1(0(2(x1)))))
, 0(1(2(2(x1)))) -> 1(3(0(2(2(x1)))))
, 0(1(2(4(x1)))) -> 0(1(4(2(3(x1)))))
, 0(1(2(4(x1)))) -> 4(0(2(2(1(1(x1))))))
, 0(1(2(4(x1)))) -> 4(0(5(5(2(1(x1))))))
, 0(1(2(5(x1)))) -> 3(5(5(2(1(0(x1))))))
, 0(1(4(2(x1)))) -> 0(5(2(1(4(x1)))))
, 0(1(5(2(x1)))) -> 1(5(0(2(3(x1)))))
, 0(1(5(2(x1)))) -> 0(2(2(1(0(5(x1))))))
, 0(1(5(2(x1)))) -> 5(5(0(2(1(3(x1))))))
, 0(2(4(2(x1)))) -> 0(5(4(3(2(2(x1))))))
, 0(3(1(2(x1)))) -> 0(2(1(3(2(x1)))))
, 0(3(1(2(x1)))) -> 1(0(2(5(3(x1)))))
, 0(3(1(2(x1)))) -> 1(5(0(2(3(x1)))))
, 0(3(1(2(x1)))) -> 3(0(2(2(1(x1)))))
, 0(3(1(2(x1)))) -> 3(2(2(1(0(x1)))))
, 0(3(1(2(x1)))) -> 0(3(2(3(1(3(x1))))))
, 0(3(4(2(x1)))) -> 0(2(2(3(4(x1)))))
, 5(0(1(2(x1)))) -> 1(3(2(5(0(x1)))))
, 5(0(1(2(x1)))) -> 5(0(2(1(3(3(x1))))))
, 0(1(1(2(5(x1))))) -> 5(0(2(5(1(1(x1))))))
, 0(2(3(4(2(x1))))) -> 3(2(2(3(4(0(x1))))))
, 0(3(1(2(5(x1))))) -> 2(3(1(3(0(5(x1))))))
, 0(3(1(5(2(x1))))) -> 0(3(2(5(1(2(x1))))))
, 0(3(4(1(4(x1))))) -> 0(5(3(1(4(4(x1))))))
, 0(3(5(1(2(x1))))) -> 5(5(3(2(1(0(x1))))))
, 0(4(0(4(2(x1))))) -> 4(4(0(0(2(2(x1))))))
, 0(4(1(1(2(x1))))) -> 3(1(4(0(2(1(x1))))))
, 0(4(1(2(2(x1))))) -> 4(1(0(2(2(3(x1))))))
, 0(4(1(2(5(x1))))) -> 3(4(1(0(2(5(x1))))))
, 0(4(2(1(2(x1))))) -> 4(1(3(2(0(2(x1))))))
, 0(4(2(1(4(x1))))) -> 0(2(1(4(4(4(x1))))))
, 0(4(2(5(2(x1))))) -> 5(4(3(2(2(0(x1))))))
, 0(4(5(1(2(x1))))) -> 1(4(2(0(5(5(x1))))))
, 0(4(5(1(2(x1))))) -> 4(0(2(5(1(1(x1))))))
, 5(0(1(2(2(x1))))) -> 5(0(2(2(1(2(x1))))))
, 5(0(2(4(2(x1))))) -> 0(2(2(5(1(4(x1))))))
, 5(0(4(4(2(x1))))) -> 0(5(2(5(4(4(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(1(2(x1))) -> 0(1(3(2(x1))))
, 0(1(2(x1))) -> 0(2(1(0(x1))))
, 0(1(2(x1))) -> 0(2(1(3(x1))))
, 0(1(2(x1))) -> 0(2(2(1(x1))))
, 0(1(2(x1))) -> 0(2(2(1(4(x1)))))
, 0(1(2(x1))) -> 5(1(0(5(2(3(x1))))))
, 0(2(4(x1))) -> 0(2(1(4(3(x1)))))
, 0(4(2(x1))) -> 4(0(2(3(x1))))
, 0(4(2(x1))) -> 4(0(5(5(2(x1)))))
, 0(0(4(2(x1)))) -> 0(0(2(2(3(4(x1))))))
, 0(1(2(2(x1)))) -> 0(2(1(0(2(x1)))))
, 0(1(2(2(x1)))) -> 1(3(0(2(2(x1)))))
, 0(1(2(4(x1)))) -> 0(1(4(2(3(x1)))))
, 0(1(2(4(x1)))) -> 4(0(2(2(1(1(x1))))))
, 0(1(2(4(x1)))) -> 4(0(5(5(2(1(x1))))))
, 0(1(2(5(x1)))) -> 3(5(5(2(1(0(x1))))))
, 0(1(4(2(x1)))) -> 0(5(2(1(4(x1)))))
, 0(1(5(2(x1)))) -> 1(5(0(2(3(x1)))))
, 0(1(5(2(x1)))) -> 0(2(2(1(0(5(x1))))))
, 0(1(5(2(x1)))) -> 5(5(0(2(1(3(x1))))))
, 0(2(4(2(x1)))) -> 0(5(4(3(2(2(x1))))))
, 0(3(1(2(x1)))) -> 0(2(1(3(2(x1)))))
, 0(3(1(2(x1)))) -> 1(0(2(5(3(x1)))))
, 0(3(1(2(x1)))) -> 1(5(0(2(3(x1)))))
, 0(3(1(2(x1)))) -> 3(0(2(2(1(x1)))))
, 0(3(1(2(x1)))) -> 3(2(2(1(0(x1)))))
, 0(3(1(2(x1)))) -> 0(3(2(3(1(3(x1))))))
, 0(3(4(2(x1)))) -> 0(2(2(3(4(x1)))))
, 5(0(1(2(x1)))) -> 1(3(2(5(0(x1)))))
, 5(0(1(2(x1)))) -> 5(0(2(1(3(3(x1))))))
, 0(1(1(2(5(x1))))) -> 5(0(2(5(1(1(x1))))))
, 0(2(3(4(2(x1))))) -> 3(2(2(3(4(0(x1))))))
, 0(3(1(2(5(x1))))) -> 2(3(1(3(0(5(x1))))))
, 0(3(1(5(2(x1))))) -> 0(3(2(5(1(2(x1))))))
, 0(3(4(1(4(x1))))) -> 0(5(3(1(4(4(x1))))))
, 0(3(5(1(2(x1))))) -> 5(5(3(2(1(0(x1))))))
, 0(4(0(4(2(x1))))) -> 4(4(0(0(2(2(x1))))))
, 0(4(1(1(2(x1))))) -> 3(1(4(0(2(1(x1))))))
, 0(4(1(2(2(x1))))) -> 4(1(0(2(2(3(x1))))))
, 0(4(1(2(5(x1))))) -> 3(4(1(0(2(5(x1))))))
, 0(4(2(1(2(x1))))) -> 4(1(3(2(0(2(x1))))))
, 0(4(2(1(4(x1))))) -> 0(2(1(4(4(4(x1))))))
, 0(4(2(5(2(x1))))) -> 5(4(3(2(2(0(x1))))))
, 0(4(5(1(2(x1))))) -> 1(4(2(0(5(5(x1))))))
, 0(4(5(1(2(x1))))) -> 4(0(2(5(1(1(x1))))))
, 5(0(1(2(2(x1))))) -> 5(0(2(2(1(2(x1))))))
, 5(0(2(4(2(x1))))) -> 0(2(2(5(1(4(x1))))))
, 5(0(4(4(2(x1))))) -> 0(5(2(5(4(4(x1))))))}
Proof Output:
The problem is match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ 0_0(2) -> 1
, 0_1(2) -> 7
, 0_1(3) -> 1
, 0_1(3) -> 7
, 0_1(3) -> 43
, 0_1(3) -> 66
, 0_1(5) -> 7
, 0_1(6) -> 1
, 0_1(6) -> 7
, 0_1(6) -> 12
, 0_1(6) -> 66
, 0_1(11) -> 10
, 0_1(12) -> 13
, 0_1(14) -> 1
, 0_1(14) -> 7
, 0_1(14) -> 43
, 0_1(14) -> 66
, 0_1(17) -> 16
, 0_1(32) -> 15
, 0_1(53) -> 33
, 0_1(53) -> 90
, 0_1(53) -> 93
, 0_2(2) -> 66
, 0_2(8) -> 43
, 0_2(18) -> 43
, 0_2(19) -> 1
, 0_2(19) -> 7
, 0_2(19) -> 12
, 0_2(19) -> 43
, 0_2(19) -> 66
, 0_2(27) -> 13
, 0_2(56) -> 15
, 0_2(70) -> 69
, 0_2(75) -> 16
, 0_2(80) -> 79
, 0_2(83) -> 1
, 0_2(83) -> 7
, 0_2(83) -> 12
, 0_2(83) -> 66
, 0_2(95) -> 94
, 0_3(84) -> 1
, 0_3(84) -> 7
, 0_3(84) -> 12
, 0_3(84) -> 43
, 0_3(84) -> 66
, 1_0(2) -> 2
, 1_1(2) -> 8
, 1_1(4) -> 3
, 1_1(5) -> 3
, 1_1(7) -> 6
, 1_1(8) -> 18
, 1_1(10) -> 9
, 1_1(15) -> 1
, 1_1(15) -> 7
, 1_1(15) -> 43
, 1_1(15) -> 66
, 1_1(38) -> 33
, 1_1(38) -> 90
, 1_1(38) -> 93
, 1_2(2) -> 67
, 1_2(18) -> 67
, 1_2(22) -> 21
, 1_2(42) -> 65
, 1_2(43) -> 65
, 1_2(60) -> 59
, 1_2(63) -> 19
, 1_2(66) -> 65
, 1_2(67) -> 82
, 1_2(69) -> 68
, 1_2(73) -> 72
, 1_2(77) -> 76
, 1_2(88) -> 33
, 1_2(88) -> 90
, 1_2(88) -> 93
, 1_2(91) -> 11
, 1_2(91) -> 33
, 1_2(91) -> 90
, 1_2(91) -> 93
, 1_2(97) -> 96
, 1_3(87) -> 86
, 2_0(2) -> 2
, 2_1(2) -> 5
, 2_1(3) -> 3
, 2_1(5) -> 17
, 2_1(6) -> 3
, 2_1(7) -> 12
, 2_1(8) -> 6
, 2_1(12) -> 3
, 2_1(18) -> 7
, 2_1(33) -> 32
, 2_1(35) -> 34
, 2_1(54) -> 53
, 2_1(55) -> 54
, 2_1(62) -> 61
, 2_2(2) -> 64
, 2_2(8) -> 31
, 2_2(18) -> 31
, 2_2(21) -> 20
, 2_2(31) -> 30
, 2_2(40) -> 39
, 2_2(41) -> 40
, 2_2(43) -> 71
, 2_2(57) -> 56
, 2_2(58) -> 57
, 2_2(59) -> 65
, 2_2(65) -> 19
, 2_2(67) -> 65
, 2_2(72) -> 27
, 2_2(76) -> 75
, 2_2(81) -> 80
, 2_2(82) -> 81
, 2_2(90) -> 89
, 2_2(93) -> 92
, 2_2(96) -> 95
, 2_3(86) -> 85
, 3_0(2) -> 2
, 3_1(2) -> 7
, 3_1(3) -> 1
, 3_1(3) -> 7
, 3_1(3) -> 13
, 3_1(3) -> 66
, 3_1(5) -> 4
, 3_1(6) -> 35
, 3_1(7) -> 1
, 3_1(7) -> 7
, 3_1(8) -> 5
, 3_1(12) -> 7
, 3_1(16) -> 15
, 3_1(17) -> 25
, 3_1(32) -> 38
, 3_1(34) -> 3
, 3_1(66) -> 66
, 3_2(2) -> 43
, 3_2(6) -> 74
, 3_2(7) -> 74
, 3_2(13) -> 74
, 3_2(18) -> 43
, 3_2(25) -> 78
, 3_2(30) -> 29
, 3_2(31) -> 63
, 3_2(39) -> 13
, 3_2(42) -> 41
, 3_2(43) -> 97
, 3_2(64) -> 63
, 3_2(79) -> 74
, 3_2(89) -> 88
, 3_2(92) -> 91
, 4_0(2) -> 2
, 4_1(2) -> 2
, 4_1(6) -> 1
, 4_1(6) -> 7
, 4_1(6) -> 66
, 4_1(7) -> 7
, 4_1(12) -> 4
, 4_1(13) -> 1
, 4_1(13) -> 7
, 4_1(13) -> 43
, 4_1(13) -> 66
, 4_1(25) -> 5
, 4_2(2) -> 2
, 4_2(7) -> 22
, 4_2(8) -> 60
, 4_2(18) -> 60
, 4_2(29) -> 28
, 4_2(43) -> 42
, 4_2(71) -> 63
, 4_2(74) -> 73
, 4_2(78) -> 77
, 4_2(79) -> 1
, 4_2(79) -> 7
, 4_2(79) -> 43
, 4_2(79) -> 66
, 4_3(43) -> 87
, 5_0(2) -> 1
, 5_1(2) -> 62
, 5_1(5) -> 14
, 5_1(6) -> 14
, 5_1(7) -> 33
, 5_1(8) -> 55
, 5_1(9) -> 1
, 5_1(9) -> 7
, 5_1(9) -> 43
, 5_1(9) -> 66
, 5_1(12) -> 11
, 5_1(13) -> 15
, 5_1(14) -> 12
, 5_1(61) -> 53
, 5_1(66) -> 90
, 5_1(66) -> 93
, 5_2(20) -> 19
, 5_2(28) -> 27
, 5_2(43) -> 93
, 5_2(59) -> 58
, 5_2(65) -> 83
, 5_2(66) -> 90
, 5_2(68) -> 1
, 5_2(68) -> 7
, 5_2(68) -> 12
, 5_2(68) -> 43
, 5_2(68) -> 66
, 5_2(71) -> 70
, 5_2(83) -> 80
, 5_2(94) -> 11
, 5_2(94) -> 33
, 5_2(94) -> 90
, 5_2(94) -> 93
, 5_3(85) -> 84}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(1(2(x1))) -> 0(1(3(2(x1))))
, 0(1(2(x1))) -> 0(2(1(0(x1))))
, 0(1(2(x1))) -> 0(2(1(3(x1))))
, 0(1(2(x1))) -> 0(2(2(1(x1))))
, 0(1(2(x1))) -> 0(2(2(1(4(x1)))))
, 0(1(2(x1))) -> 5(1(0(5(2(3(x1))))))
, 0(2(4(x1))) -> 0(2(1(4(3(x1)))))
, 0(4(2(x1))) -> 4(0(2(3(x1))))
, 0(4(2(x1))) -> 4(0(5(5(2(x1)))))
, 0(0(4(2(x1)))) -> 0(0(2(2(3(4(x1))))))
, 0(1(2(2(x1)))) -> 0(2(1(0(2(x1)))))
, 0(1(2(2(x1)))) -> 1(3(0(2(2(x1)))))
, 0(1(2(4(x1)))) -> 0(1(4(2(3(x1)))))
, 0(1(2(4(x1)))) -> 4(0(2(2(1(1(x1))))))
, 0(1(2(4(x1)))) -> 4(0(5(5(2(1(x1))))))
, 0(1(2(5(x1)))) -> 3(5(5(2(1(0(x1))))))
, 0(1(4(2(x1)))) -> 0(5(2(1(4(x1)))))
, 0(1(5(2(x1)))) -> 1(5(0(2(3(x1)))))
, 0(1(5(2(x1)))) -> 0(2(2(1(0(5(x1))))))
, 0(1(5(2(x1)))) -> 5(5(0(2(1(3(x1))))))
, 0(2(4(2(x1)))) -> 0(5(4(3(2(2(x1))))))
, 0(3(1(2(x1)))) -> 0(2(1(3(2(x1)))))
, 0(3(1(2(x1)))) -> 1(0(2(5(3(x1)))))
, 0(3(1(2(x1)))) -> 1(5(0(2(3(x1)))))
, 0(3(1(2(x1)))) -> 3(0(2(2(1(x1)))))
, 0(3(1(2(x1)))) -> 3(2(2(1(0(x1)))))
, 0(3(1(2(x1)))) -> 0(3(2(3(1(3(x1))))))
, 0(3(4(2(x1)))) -> 0(2(2(3(4(x1)))))
, 5(0(1(2(x1)))) -> 1(3(2(5(0(x1)))))
, 5(0(1(2(x1)))) -> 5(0(2(1(3(3(x1))))))
, 0(1(1(2(5(x1))))) -> 5(0(2(5(1(1(x1))))))
, 0(2(3(4(2(x1))))) -> 3(2(2(3(4(0(x1))))))
, 0(3(1(2(5(x1))))) -> 2(3(1(3(0(5(x1))))))
, 0(3(1(5(2(x1))))) -> 0(3(2(5(1(2(x1))))))
, 0(3(4(1(4(x1))))) -> 0(5(3(1(4(4(x1))))))
, 0(3(5(1(2(x1))))) -> 5(5(3(2(1(0(x1))))))
, 0(4(0(4(2(x1))))) -> 4(4(0(0(2(2(x1))))))
, 0(4(1(1(2(x1))))) -> 3(1(4(0(2(1(x1))))))
, 0(4(1(2(2(x1))))) -> 4(1(0(2(2(3(x1))))))
, 0(4(1(2(5(x1))))) -> 3(4(1(0(2(5(x1))))))
, 0(4(2(1(2(x1))))) -> 4(1(3(2(0(2(x1))))))
, 0(4(2(1(4(x1))))) -> 0(2(1(4(4(4(x1))))))
, 0(4(2(5(2(x1))))) -> 5(4(3(2(2(0(x1))))))
, 0(4(5(1(2(x1))))) -> 1(4(2(0(5(5(x1))))))
, 0(4(5(1(2(x1))))) -> 4(0(2(5(1(1(x1))))))
, 5(0(1(2(2(x1))))) -> 5(0(2(2(1(2(x1))))))
, 5(0(2(4(2(x1))))) -> 0(2(2(5(1(4(x1))))))
, 5(0(4(4(2(x1))))) -> 0(5(2(5(4(4(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(1(2(x1))) -> 0(1(3(2(x1))))
, 0(1(2(x1))) -> 0(2(1(0(x1))))
, 0(1(2(x1))) -> 0(2(1(3(x1))))
, 0(1(2(x1))) -> 0(2(2(1(x1))))
, 0(1(2(x1))) -> 0(2(2(1(4(x1)))))
, 0(1(2(x1))) -> 5(1(0(5(2(3(x1))))))
, 0(2(4(x1))) -> 0(2(1(4(3(x1)))))
, 0(4(2(x1))) -> 4(0(2(3(x1))))
, 0(4(2(x1))) -> 4(0(5(5(2(x1)))))
, 0(0(4(2(x1)))) -> 0(0(2(2(3(4(x1))))))
, 0(1(2(2(x1)))) -> 0(2(1(0(2(x1)))))
, 0(1(2(2(x1)))) -> 1(3(0(2(2(x1)))))
, 0(1(2(4(x1)))) -> 0(1(4(2(3(x1)))))
, 0(1(2(4(x1)))) -> 4(0(2(2(1(1(x1))))))
, 0(1(2(4(x1)))) -> 4(0(5(5(2(1(x1))))))
, 0(1(2(5(x1)))) -> 3(5(5(2(1(0(x1))))))
, 0(1(4(2(x1)))) -> 0(5(2(1(4(x1)))))
, 0(1(5(2(x1)))) -> 1(5(0(2(3(x1)))))
, 0(1(5(2(x1)))) -> 0(2(2(1(0(5(x1))))))
, 0(1(5(2(x1)))) -> 5(5(0(2(1(3(x1))))))
, 0(2(4(2(x1)))) -> 0(5(4(3(2(2(x1))))))
, 0(3(1(2(x1)))) -> 0(2(1(3(2(x1)))))
, 0(3(1(2(x1)))) -> 1(0(2(5(3(x1)))))
, 0(3(1(2(x1)))) -> 1(5(0(2(3(x1)))))
, 0(3(1(2(x1)))) -> 3(0(2(2(1(x1)))))
, 0(3(1(2(x1)))) -> 3(2(2(1(0(x1)))))
, 0(3(1(2(x1)))) -> 0(3(2(3(1(3(x1))))))
, 0(3(4(2(x1)))) -> 0(2(2(3(4(x1)))))
, 5(0(1(2(x1)))) -> 1(3(2(5(0(x1)))))
, 5(0(1(2(x1)))) -> 5(0(2(1(3(3(x1))))))
, 0(1(1(2(5(x1))))) -> 5(0(2(5(1(1(x1))))))
, 0(2(3(4(2(x1))))) -> 3(2(2(3(4(0(x1))))))
, 0(3(1(2(5(x1))))) -> 2(3(1(3(0(5(x1))))))
, 0(3(1(5(2(x1))))) -> 0(3(2(5(1(2(x1))))))
, 0(3(4(1(4(x1))))) -> 0(5(3(1(4(4(x1))))))
, 0(3(5(1(2(x1))))) -> 5(5(3(2(1(0(x1))))))
, 0(4(0(4(2(x1))))) -> 4(4(0(0(2(2(x1))))))
, 0(4(1(1(2(x1))))) -> 3(1(4(0(2(1(x1))))))
, 0(4(1(2(2(x1))))) -> 4(1(0(2(2(3(x1))))))
, 0(4(1(2(5(x1))))) -> 3(4(1(0(2(5(x1))))))
, 0(4(2(1(2(x1))))) -> 4(1(3(2(0(2(x1))))))
, 0(4(2(1(4(x1))))) -> 0(2(1(4(4(4(x1))))))
, 0(4(2(5(2(x1))))) -> 5(4(3(2(2(0(x1))))))
, 0(4(5(1(2(x1))))) -> 1(4(2(0(5(5(x1))))))
, 0(4(5(1(2(x1))))) -> 4(0(2(5(1(1(x1))))))
, 5(0(1(2(2(x1))))) -> 5(0(2(2(1(2(x1))))))
, 5(0(2(4(2(x1))))) -> 0(2(2(5(1(4(x1))))))
, 5(0(4(4(2(x1))))) -> 0(5(2(5(4(4(x1))))))}
Proof Output:
The problem is match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ 0_0(2) -> 1
, 0_1(2) -> 7
, 0_1(3) -> 1
, 0_1(3) -> 7
, 0_1(3) -> 43
, 0_1(3) -> 66
, 0_1(5) -> 7
, 0_1(6) -> 1
, 0_1(6) -> 7
, 0_1(6) -> 12
, 0_1(6) -> 66
, 0_1(11) -> 10
, 0_1(12) -> 13
, 0_1(14) -> 1
, 0_1(14) -> 7
, 0_1(14) -> 43
, 0_1(14) -> 66
, 0_1(17) -> 16
, 0_1(32) -> 15
, 0_1(53) -> 33
, 0_1(53) -> 90
, 0_1(53) -> 93
, 0_2(2) -> 66
, 0_2(8) -> 43
, 0_2(18) -> 43
, 0_2(19) -> 1
, 0_2(19) -> 7
, 0_2(19) -> 12
, 0_2(19) -> 43
, 0_2(19) -> 66
, 0_2(27) -> 13
, 0_2(56) -> 15
, 0_2(70) -> 69
, 0_2(75) -> 16
, 0_2(80) -> 79
, 0_2(83) -> 1
, 0_2(83) -> 7
, 0_2(83) -> 12
, 0_2(83) -> 66
, 0_2(95) -> 94
, 0_3(84) -> 1
, 0_3(84) -> 7
, 0_3(84) -> 12
, 0_3(84) -> 43
, 0_3(84) -> 66
, 1_0(2) -> 2
, 1_1(2) -> 8
, 1_1(4) -> 3
, 1_1(5) -> 3
, 1_1(7) -> 6
, 1_1(8) -> 18
, 1_1(10) -> 9
, 1_1(15) -> 1
, 1_1(15) -> 7
, 1_1(15) -> 43
, 1_1(15) -> 66
, 1_1(38) -> 33
, 1_1(38) -> 90
, 1_1(38) -> 93
, 1_2(2) -> 67
, 1_2(18) -> 67
, 1_2(22) -> 21
, 1_2(42) -> 65
, 1_2(43) -> 65
, 1_2(60) -> 59
, 1_2(63) -> 19
, 1_2(66) -> 65
, 1_2(67) -> 82
, 1_2(69) -> 68
, 1_2(73) -> 72
, 1_2(77) -> 76
, 1_2(88) -> 33
, 1_2(88) -> 90
, 1_2(88) -> 93
, 1_2(91) -> 11
, 1_2(91) -> 33
, 1_2(91) -> 90
, 1_2(91) -> 93
, 1_2(97) -> 96
, 1_3(87) -> 86
, 2_0(2) -> 2
, 2_1(2) -> 5
, 2_1(3) -> 3
, 2_1(5) -> 17
, 2_1(6) -> 3
, 2_1(7) -> 12
, 2_1(8) -> 6
, 2_1(12) -> 3
, 2_1(18) -> 7
, 2_1(33) -> 32
, 2_1(35) -> 34
, 2_1(54) -> 53
, 2_1(55) -> 54
, 2_1(62) -> 61
, 2_2(2) -> 64
, 2_2(8) -> 31
, 2_2(18) -> 31
, 2_2(21) -> 20
, 2_2(31) -> 30
, 2_2(40) -> 39
, 2_2(41) -> 40
, 2_2(43) -> 71
, 2_2(57) -> 56
, 2_2(58) -> 57
, 2_2(59) -> 65
, 2_2(65) -> 19
, 2_2(67) -> 65
, 2_2(72) -> 27
, 2_2(76) -> 75
, 2_2(81) -> 80
, 2_2(82) -> 81
, 2_2(90) -> 89
, 2_2(93) -> 92
, 2_2(96) -> 95
, 2_3(86) -> 85
, 3_0(2) -> 2
, 3_1(2) -> 7
, 3_1(3) -> 1
, 3_1(3) -> 7
, 3_1(3) -> 13
, 3_1(3) -> 66
, 3_1(5) -> 4
, 3_1(6) -> 35
, 3_1(7) -> 1
, 3_1(7) -> 7
, 3_1(8) -> 5
, 3_1(12) -> 7
, 3_1(16) -> 15
, 3_1(17) -> 25
, 3_1(32) -> 38
, 3_1(34) -> 3
, 3_1(66) -> 66
, 3_2(2) -> 43
, 3_2(6) -> 74
, 3_2(7) -> 74
, 3_2(13) -> 74
, 3_2(18) -> 43
, 3_2(25) -> 78
, 3_2(30) -> 29
, 3_2(31) -> 63
, 3_2(39) -> 13
, 3_2(42) -> 41
, 3_2(43) -> 97
, 3_2(64) -> 63
, 3_2(79) -> 74
, 3_2(89) -> 88
, 3_2(92) -> 91
, 4_0(2) -> 2
, 4_1(2) -> 2
, 4_1(6) -> 1
, 4_1(6) -> 7
, 4_1(6) -> 66
, 4_1(7) -> 7
, 4_1(12) -> 4
, 4_1(13) -> 1
, 4_1(13) -> 7
, 4_1(13) -> 43
, 4_1(13) -> 66
, 4_1(25) -> 5
, 4_2(2) -> 2
, 4_2(7) -> 22
, 4_2(8) -> 60
, 4_2(18) -> 60
, 4_2(29) -> 28
, 4_2(43) -> 42
, 4_2(71) -> 63
, 4_2(74) -> 73
, 4_2(78) -> 77
, 4_2(79) -> 1
, 4_2(79) -> 7
, 4_2(79) -> 43
, 4_2(79) -> 66
, 4_3(43) -> 87
, 5_0(2) -> 1
, 5_1(2) -> 62
, 5_1(5) -> 14
, 5_1(6) -> 14
, 5_1(7) -> 33
, 5_1(8) -> 55
, 5_1(9) -> 1
, 5_1(9) -> 7
, 5_1(9) -> 43
, 5_1(9) -> 66
, 5_1(12) -> 11
, 5_1(13) -> 15
, 5_1(14) -> 12
, 5_1(61) -> 53
, 5_1(66) -> 90
, 5_1(66) -> 93
, 5_2(20) -> 19
, 5_2(28) -> 27
, 5_2(43) -> 93
, 5_2(59) -> 58
, 5_2(65) -> 83
, 5_2(66) -> 90
, 5_2(68) -> 1
, 5_2(68) -> 7
, 5_2(68) -> 12
, 5_2(68) -> 43
, 5_2(68) -> 66
, 5_2(71) -> 70
, 5_2(83) -> 80
, 5_2(94) -> 11
, 5_2(94) -> 33
, 5_2(94) -> 90
, 5_2(94) -> 93
, 5_3(85) -> 84}