Tool CaT
stdout:
YES(?,O(n^1))
Problem:
0(1(0(2(x1)))) -> 2(0(3(1(0(x1)))))
0(1(0(2(x1)))) -> 2(0(0(3(1(2(x1))))))
0(1(0(2(x1)))) -> 2(0(3(1(0(4(x1))))))
0(1(0(2(x1)))) -> 2(2(0(3(1(0(x1))))))
0(1(0(2(x1)))) -> 2(3(1(0(0(2(x1))))))
0(1(0(2(x1)))) -> 2(3(1(0(3(0(x1))))))
0(1(0(2(x1)))) -> 4(1(0(3(0(2(x1))))))
0(1(0(2(x1)))) -> 4(1(0(4(0(2(x1))))))
0(1(4(2(x1)))) -> 2(3(1(0(4(x1)))))
0(1(4(2(x1)))) -> 2(4(0(3(1(x1)))))
0(1(4(2(x1)))) -> 3(2(1(0(4(x1)))))
0(1(4(2(x1)))) -> 3(2(1(4(0(x1)))))
0(1(4(2(x1)))) -> 4(0(3(1(2(x1)))))
0(1(4(2(x1)))) -> 4(1(0(3(2(x1)))))
0(1(4(2(x1)))) -> 4(1(0(4(2(x1)))))
0(1(4(2(x1)))) -> 4(1(0(5(2(x1)))))
0(1(4(2(x1)))) -> 2(0(3(1(0(4(x1))))))
0(1(4(2(x1)))) -> 2(0(3(1(4(4(x1))))))
0(1(4(2(x1)))) -> 2(3(1(4(0(4(x1))))))
0(1(4(2(x1)))) -> 2(4(3(0(4(1(x1))))))
0(1(4(2(x1)))) -> 2(4(3(1(0(3(x1))))))
0(1(4(2(x1)))) -> 3(2(1(0(4(1(x1))))))
0(1(4(2(x1)))) -> 3(2(2(1(4(0(x1))))))
0(1(4(2(x1)))) -> 3(2(3(1(0(4(x1))))))
0(1(4(2(x1)))) -> 3(2(3(1(4(0(x1))))))
0(1(4(2(x1)))) -> 4(0(3(1(3(2(x1))))))
0(1(4(2(x1)))) -> 4(0(3(1(4(2(x1))))))
0(1(4(2(x1)))) -> 4(1(0(4(3(2(x1))))))
0(1(4(2(x1)))) -> 4(1(0(4(5(2(x1))))))
0(1(4(2(x1)))) -> 4(1(0(5(3(2(x1))))))
0(1(4(2(x1)))) -> 4(1(1(0(5(2(x1))))))
0(1(4(2(x1)))) -> 4(1(3(0(5(2(x1))))))
0(1(4(2(x1)))) -> 4(3(0(3(1(2(x1))))))
0(1(4(2(x1)))) -> 4(4(0(3(1(2(x1))))))
0(0(1(0(2(x1))))) -> 1(0(0(2(0(4(x1))))))
0(0(1(0(2(x1))))) -> 1(0(4(0(0(2(x1))))))
0(0(1(0(2(x1))))) -> 2(1(0(3(0(0(x1))))))
0(0(1(4(2(x1))))) -> 0(0(3(1(2(4(x1))))))
0(0(1(4(2(x1))))) -> 0(2(3(1(0(4(x1))))))
0(0(1(4(2(x1))))) -> 0(2(4(0(3(1(x1))))))
0(0(1(4(2(x1))))) -> 0(3(1(0(2(4(x1))))))
0(0(1(4(2(x1))))) -> 1(0(3(4(0(2(x1))))))
0(0(1(4(2(x1))))) -> 2(0(0(3(1(4(x1))))))
0(0(1(4(2(x1))))) -> 2(1(0(4(0(0(x1))))))
0(1(2(0(2(x1))))) -> 2(0(1(0(4(2(x1))))))
0(1(2(4(2(x1))))) -> 2(3(1(0(2(4(x1))))))
0(1(2(4(2(x1))))) -> 4(1(0(2(2(4(x1))))))
0(1(3(4(2(x1))))) -> 2(3(1(4(4(0(x1))))))
0(1(3(4(2(x1))))) -> 2(4(3(0(4(1(x1))))))
0(1(3(4(2(x1))))) -> 3(2(1(0(4(0(x1))))))
0(1(3(4(2(x1))))) -> 4(0(3(3(1(2(x1))))))
0(1(3(4(2(x1))))) -> 4(1(4(0(3(2(x1))))))
0(1(4(0(2(x1))))) -> 2(0(3(1(0(4(x1))))))
0(1(5(0(2(x1))))) -> 0(2(3(1(0(5(x1))))))
0(1(5(0(2(x1))))) -> 3(0(5(1(0(2(x1))))))
0(1(5(0(2(x1))))) -> 5(1(3(0(0(2(x1))))))
0(1(5(4(2(x1))))) -> 0(4(4(1(2(5(x1))))))
0(1(5(4(2(x1))))) -> 1(0(4(5(1(2(x1))))))
0(1(5(4(2(x1))))) -> 2(0(4(4(5(1(x1))))))
0(1(5(4(2(x1))))) -> 4(0(2(3(1(5(x1))))))
0(1(5(4(2(x1))))) -> 4(1(0(2(5(2(x1))))))
0(1(5(4(2(x1))))) -> 4(1(0(5(2(5(x1))))))
0(1(5(4(2(x1))))) -> 4(2(1(3(0(5(x1))))))
0(1(5(4(2(x1))))) -> 4(3(1(0(2(5(x1))))))
0(1(5(4(2(x1))))) -> 4(4(0(5(1(2(x1))))))
0(1(5(4(2(x1))))) -> 4(4(2(1(0(5(x1))))))
0(1(5(4(2(x1))))) -> 5(0(4(5(2(1(x1))))))
0(1(5(4(2(x1))))) -> 5(1(2(0(4(3(x1))))))
0(1(5(4(2(x1))))) -> 5(3(1(0(4(2(x1))))))
0(2(1(4(2(x1))))) -> 0(4(4(1(2(2(x1))))))
0(2(1(4(2(x1))))) -> 3(2(2(1(4(0(x1))))))
0(2(1(4(2(x1))))) -> 4(1(0(3(2(2(x1))))))
5(0(1(4(2(x1))))) -> 2(0(4(3(5(1(x1))))))
5(0(1(4(2(x1))))) -> 2(4(0(3(1(5(x1))))))
5(0(1(4(2(x1))))) -> 4(1(0(5(3(2(x1))))))
5(0(1(4(2(x1))))) -> 5(2(1(1(0(4(x1))))))
5(0(2(0(2(x1))))) -> 5(0(3(0(2(2(x1))))))
5(0(2(0(2(x1))))) -> 5(0(4(0(2(2(x1))))))
5(0(2(4(2(x1))))) -> 5(4(0(3(2(2(x1))))))
5(1(5(0(2(x1))))) -> 5(2(1(4(5(0(x1))))))
5(1(5(4(2(x1))))) -> 5(2(1(0(4(5(x1))))))
5(4(1(4(2(x1))))) -> 3(2(1(4(4(5(x1))))))
5(4(1(4(2(x1))))) -> 4(4(3(5(1(2(x1))))))
5(4(2(0(2(x1))))) -> 3(0(5(2(2(4(x1))))))
5(4(2(0(2(x1))))) -> 4(0(5(3(2(2(x1))))))
5(4(2(0(2(x1))))) -> 5(2(2(2(4(0(x1))))))
5(4(2(0(2(x1))))) -> 5(3(2(2(4(0(x1))))))
5(4(2(0(2(x1))))) -> 5(4(2(2(4(0(x1))))))
5(4(2(4(2(x1))))) -> 0(4(4(5(2(2(x1))))))
5(4(2(4(2(x1))))) -> 5(4(4(3(2(2(x1))))))
5(4(5(4(2(x1))))) -> 4(5(0(4(5(2(x1))))))
Proof:
Bounds Processor:
bound: 2
enrichment: match
automaton:
final states: {6,5}
transitions:
51(257) -> 258*
51(177) -> 178*
51(279) -> 280*
51(274) -> 275*
51(259) -> 260*
51(249) -> 250*
51(251) -> 252*
51(233) -> 234*
51(113) -> 114*
41(262) -> 263*
41(60) -> 61*
41(25) -> 26*
41(127) -> 128*
41(234) -> 235*
41(27) -> 28*
41(219) -> 220*
41(129) -> 130*
41(276) -> 277*
41(261) -> 262*
41(39) -> 40*
41(19) -> 20*
41(201) -> 202*
41(121) -> 122*
41(111) -> 112*
41(81) -> 82*
41(193) -> 194*
41(275) -> 276*
41(235) -> 236*
41(220) -> 221*
41(215) -> 216*
41(13) -> 14*
41(175) -> 176*
31(167) -> 168*
31(57) -> 58*
31(37) -> 38*
31(209) -> 210*
31(79) -> 80*
31(231) -> 232*
31(191) -> 192*
31(151) -> 152*
31(141) -> 142*
31(131) -> 132*
31(101) -> 102*
31(238) -> 239*
31(16) -> 17*
31(153) -> 154*
31(260) -> 261*
31(185) -> 186*
31(145) -> 146*
21(237) -> 238*
21(217) -> 218*
21(77) -> 78*
21(17) -> 18*
21(199) -> 200*
21(99) -> 100*
21(161) -> 162*
21(91) -> 92*
21(56) -> 57*
21(93) -> 94*
01(80) -> 81*
01(277) -> 278*
01(75) -> 76*
01(207) -> 208*
01(142) -> 143*
01(102) -> 103*
01(67) -> 68*
01(119) -> 120*
01(69) -> 70*
01(59) -> 60*
01(221) -> 222*
01(14) -> 15*
01(38) -> 39*
01(130) -> 131*
11(15) -> 16*
11(47) -> 48*
11(169) -> 170*
11(159) -> 160*
11(49) -> 50*
11(236) -> 237*
11(41) -> 42*
11(36) -> 37*
11(218) -> 219*
11(183) -> 184*
11(143) -> 144*
11(103) -> 104*
11(78) -> 79*
42(314) -> 315*
42(311) -> 312*
42(291) -> 292*
00(2) -> 5*
00(4) -> 5*
00(1) -> 5*
00(3) -> 5*
52(313) -> 314*
52(303) -> 304*
52(310) -> 311*
52(305) -> 306*
52(295) -> 296*
52(290) -> 291*
52(297) -> 298*
10(2) -> 1*
10(4) -> 1*
10(1) -> 1*
10(3) -> 1*
02(312) -> 313*
02(292) -> 293*
20(2) -> 2*
20(4) -> 2*
20(1) -> 2*
20(3) -> 2*
22(309) -> 310*
22(294) -> 295*
22(316) -> 317*
22(325) -> 326*
22(327) -> 328*
30(2) -> 3*
30(4) -> 3*
30(1) -> 3*
30(3) -> 3*
12(293) -> 294*
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 -> 251,151,93,69,47,25
2 -> 233,141,77,59,36,13
3 -> 257,153,99,75,49,27
4 -> 249,145,91,67,41,19
14 -> 199,121
15 -> 127*
16 -> 201,56
17 -> 119*
18 -> 70,167,5
20 -> 14*
26 -> 14*
28 -> 14*
37 -> 129*
40 -> 17*
42 -> 37*
48 -> 37*
50 -> 37*
57 -> 161*
58 -> 70,5
61 -> 70,207,15
68 -> 60*
70 -> 60*
76 -> 60*
77 -> 309,290
78 -> 217,113,111,101
79 -> 259*
80 -> 209*
81 -> 191*
82 -> 70,193,5
91 -> 325,303
92 -> 78*
93 -> 327,305
94 -> 78*
99 -> 316,297
100 -> 78*
102 -> 177,175,169
103 -> 215,185
104 -> 183,81
112 -> 102*
114 -> 102*
120 -> 17*
122 -> 15*
128 -> 279,15
131 -> 159*
132 -> 39*
144 -> 131*
146 -> 142*
152 -> 142*
154 -> 142*
160 -> 56*
162 -> 57*
168 -> 70,5
170 -> 79*
176 -> 102*
178 -> 102*
184 -> 81*
186 -> 103*
192 -> 81*
194 -> 5*
200 -> 14*
202 -> 70,60,5
208 -> 15*
210 -> 80*
216 -> 15*
218 -> 274,231
222 -> 60,5
232 -> 14*
239 -> 304,291,250,234,6
250 -> 234*
252 -> 234*
258 -> 234*
263 -> 304,291,250,234,6
278 -> 304,291,178,102,250,169,177,6
280 -> 304,291,178,102,250,169,177,6
296 -> 260*
298 -> 291*
304 -> 291*
306 -> 291*
315 -> 178,102,169,177
317 -> 310*
326 -> 310*
328 -> 310*
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(0(2(x1)))) -> 2(0(3(1(0(x1)))))
, 0(1(0(2(x1)))) -> 2(0(0(3(1(2(x1))))))
, 0(1(0(2(x1)))) -> 2(0(3(1(0(4(x1))))))
, 0(1(0(2(x1)))) -> 2(2(0(3(1(0(x1))))))
, 0(1(0(2(x1)))) -> 2(3(1(0(0(2(x1))))))
, 0(1(0(2(x1)))) -> 2(3(1(0(3(0(x1))))))
, 0(1(0(2(x1)))) -> 4(1(0(3(0(2(x1))))))
, 0(1(0(2(x1)))) -> 4(1(0(4(0(2(x1))))))
, 0(1(4(2(x1)))) -> 2(3(1(0(4(x1)))))
, 0(1(4(2(x1)))) -> 2(4(0(3(1(x1)))))
, 0(1(4(2(x1)))) -> 3(2(1(0(4(x1)))))
, 0(1(4(2(x1)))) -> 3(2(1(4(0(x1)))))
, 0(1(4(2(x1)))) -> 4(0(3(1(2(x1)))))
, 0(1(4(2(x1)))) -> 4(1(0(3(2(x1)))))
, 0(1(4(2(x1)))) -> 4(1(0(4(2(x1)))))
, 0(1(4(2(x1)))) -> 4(1(0(5(2(x1)))))
, 0(1(4(2(x1)))) -> 2(0(3(1(0(4(x1))))))
, 0(1(4(2(x1)))) -> 2(0(3(1(4(4(x1))))))
, 0(1(4(2(x1)))) -> 2(3(1(4(0(4(x1))))))
, 0(1(4(2(x1)))) -> 2(4(3(0(4(1(x1))))))
, 0(1(4(2(x1)))) -> 2(4(3(1(0(3(x1))))))
, 0(1(4(2(x1)))) -> 3(2(1(0(4(1(x1))))))
, 0(1(4(2(x1)))) -> 3(2(2(1(4(0(x1))))))
, 0(1(4(2(x1)))) -> 3(2(3(1(0(4(x1))))))
, 0(1(4(2(x1)))) -> 3(2(3(1(4(0(x1))))))
, 0(1(4(2(x1)))) -> 4(0(3(1(3(2(x1))))))
, 0(1(4(2(x1)))) -> 4(0(3(1(4(2(x1))))))
, 0(1(4(2(x1)))) -> 4(1(0(4(3(2(x1))))))
, 0(1(4(2(x1)))) -> 4(1(0(4(5(2(x1))))))
, 0(1(4(2(x1)))) -> 4(1(0(5(3(2(x1))))))
, 0(1(4(2(x1)))) -> 4(1(1(0(5(2(x1))))))
, 0(1(4(2(x1)))) -> 4(1(3(0(5(2(x1))))))
, 0(1(4(2(x1)))) -> 4(3(0(3(1(2(x1))))))
, 0(1(4(2(x1)))) -> 4(4(0(3(1(2(x1))))))
, 0(0(1(0(2(x1))))) -> 1(0(0(2(0(4(x1))))))
, 0(0(1(0(2(x1))))) -> 1(0(4(0(0(2(x1))))))
, 0(0(1(0(2(x1))))) -> 2(1(0(3(0(0(x1))))))
, 0(0(1(4(2(x1))))) -> 0(0(3(1(2(4(x1))))))
, 0(0(1(4(2(x1))))) -> 0(2(3(1(0(4(x1))))))
, 0(0(1(4(2(x1))))) -> 0(2(4(0(3(1(x1))))))
, 0(0(1(4(2(x1))))) -> 0(3(1(0(2(4(x1))))))
, 0(0(1(4(2(x1))))) -> 1(0(3(4(0(2(x1))))))
, 0(0(1(4(2(x1))))) -> 2(0(0(3(1(4(x1))))))
, 0(0(1(4(2(x1))))) -> 2(1(0(4(0(0(x1))))))
, 0(1(2(0(2(x1))))) -> 2(0(1(0(4(2(x1))))))
, 0(1(2(4(2(x1))))) -> 2(3(1(0(2(4(x1))))))
, 0(1(2(4(2(x1))))) -> 4(1(0(2(2(4(x1))))))
, 0(1(3(4(2(x1))))) -> 2(3(1(4(4(0(x1))))))
, 0(1(3(4(2(x1))))) -> 2(4(3(0(4(1(x1))))))
, 0(1(3(4(2(x1))))) -> 3(2(1(0(4(0(x1))))))
, 0(1(3(4(2(x1))))) -> 4(0(3(3(1(2(x1))))))
, 0(1(3(4(2(x1))))) -> 4(1(4(0(3(2(x1))))))
, 0(1(4(0(2(x1))))) -> 2(0(3(1(0(4(x1))))))
, 0(1(5(0(2(x1))))) -> 0(2(3(1(0(5(x1))))))
, 0(1(5(0(2(x1))))) -> 3(0(5(1(0(2(x1))))))
, 0(1(5(0(2(x1))))) -> 5(1(3(0(0(2(x1))))))
, 0(1(5(4(2(x1))))) -> 0(4(4(1(2(5(x1))))))
, 0(1(5(4(2(x1))))) -> 1(0(4(5(1(2(x1))))))
, 0(1(5(4(2(x1))))) -> 2(0(4(4(5(1(x1))))))
, 0(1(5(4(2(x1))))) -> 4(0(2(3(1(5(x1))))))
, 0(1(5(4(2(x1))))) -> 4(1(0(2(5(2(x1))))))
, 0(1(5(4(2(x1))))) -> 4(1(0(5(2(5(x1))))))
, 0(1(5(4(2(x1))))) -> 4(2(1(3(0(5(x1))))))
, 0(1(5(4(2(x1))))) -> 4(3(1(0(2(5(x1))))))
, 0(1(5(4(2(x1))))) -> 4(4(0(5(1(2(x1))))))
, 0(1(5(4(2(x1))))) -> 4(4(2(1(0(5(x1))))))
, 0(1(5(4(2(x1))))) -> 5(0(4(5(2(1(x1))))))
, 0(1(5(4(2(x1))))) -> 5(1(2(0(4(3(x1))))))
, 0(1(5(4(2(x1))))) -> 5(3(1(0(4(2(x1))))))
, 0(2(1(4(2(x1))))) -> 0(4(4(1(2(2(x1))))))
, 0(2(1(4(2(x1))))) -> 3(2(2(1(4(0(x1))))))
, 0(2(1(4(2(x1))))) -> 4(1(0(3(2(2(x1))))))
, 5(0(1(4(2(x1))))) -> 2(0(4(3(5(1(x1))))))
, 5(0(1(4(2(x1))))) -> 2(4(0(3(1(5(x1))))))
, 5(0(1(4(2(x1))))) -> 4(1(0(5(3(2(x1))))))
, 5(0(1(4(2(x1))))) -> 5(2(1(1(0(4(x1))))))
, 5(0(2(0(2(x1))))) -> 5(0(3(0(2(2(x1))))))
, 5(0(2(0(2(x1))))) -> 5(0(4(0(2(2(x1))))))
, 5(0(2(4(2(x1))))) -> 5(4(0(3(2(2(x1))))))
, 5(1(5(0(2(x1))))) -> 5(2(1(4(5(0(x1))))))
, 5(1(5(4(2(x1))))) -> 5(2(1(0(4(5(x1))))))
, 5(4(1(4(2(x1))))) -> 3(2(1(4(4(5(x1))))))
, 5(4(1(4(2(x1))))) -> 4(4(3(5(1(2(x1))))))
, 5(4(2(0(2(x1))))) -> 3(0(5(2(2(4(x1))))))
, 5(4(2(0(2(x1))))) -> 4(0(5(3(2(2(x1))))))
, 5(4(2(0(2(x1))))) -> 5(2(2(2(4(0(x1))))))
, 5(4(2(0(2(x1))))) -> 5(3(2(2(4(0(x1))))))
, 5(4(2(0(2(x1))))) -> 5(4(2(2(4(0(x1))))))
, 5(4(2(4(2(x1))))) -> 0(4(4(5(2(2(x1))))))
, 5(4(2(4(2(x1))))) -> 5(4(4(3(2(2(x1))))))
, 5(4(5(4(2(x1))))) -> 4(5(0(4(5(2(x1))))))}
Proof Output:
'Bounds with perSymbol-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with perSymbol-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with perSymbol-enrichment and initial automaton 'match''
----------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ 0(1(0(2(x1)))) -> 2(0(3(1(0(x1)))))
, 0(1(0(2(x1)))) -> 2(0(0(3(1(2(x1))))))
, 0(1(0(2(x1)))) -> 2(0(3(1(0(4(x1))))))
, 0(1(0(2(x1)))) -> 2(2(0(3(1(0(x1))))))
, 0(1(0(2(x1)))) -> 2(3(1(0(0(2(x1))))))
, 0(1(0(2(x1)))) -> 2(3(1(0(3(0(x1))))))
, 0(1(0(2(x1)))) -> 4(1(0(3(0(2(x1))))))
, 0(1(0(2(x1)))) -> 4(1(0(4(0(2(x1))))))
, 0(1(4(2(x1)))) -> 2(3(1(0(4(x1)))))
, 0(1(4(2(x1)))) -> 2(4(0(3(1(x1)))))
, 0(1(4(2(x1)))) -> 3(2(1(0(4(x1)))))
, 0(1(4(2(x1)))) -> 3(2(1(4(0(x1)))))
, 0(1(4(2(x1)))) -> 4(0(3(1(2(x1)))))
, 0(1(4(2(x1)))) -> 4(1(0(3(2(x1)))))
, 0(1(4(2(x1)))) -> 4(1(0(4(2(x1)))))
, 0(1(4(2(x1)))) -> 4(1(0(5(2(x1)))))
, 0(1(4(2(x1)))) -> 2(0(3(1(0(4(x1))))))
, 0(1(4(2(x1)))) -> 2(0(3(1(4(4(x1))))))
, 0(1(4(2(x1)))) -> 2(3(1(4(0(4(x1))))))
, 0(1(4(2(x1)))) -> 2(4(3(0(4(1(x1))))))
, 0(1(4(2(x1)))) -> 2(4(3(1(0(3(x1))))))
, 0(1(4(2(x1)))) -> 3(2(1(0(4(1(x1))))))
, 0(1(4(2(x1)))) -> 3(2(2(1(4(0(x1))))))
, 0(1(4(2(x1)))) -> 3(2(3(1(0(4(x1))))))
, 0(1(4(2(x1)))) -> 3(2(3(1(4(0(x1))))))
, 0(1(4(2(x1)))) -> 4(0(3(1(3(2(x1))))))
, 0(1(4(2(x1)))) -> 4(0(3(1(4(2(x1))))))
, 0(1(4(2(x1)))) -> 4(1(0(4(3(2(x1))))))
, 0(1(4(2(x1)))) -> 4(1(0(4(5(2(x1))))))
, 0(1(4(2(x1)))) -> 4(1(0(5(3(2(x1))))))
, 0(1(4(2(x1)))) -> 4(1(1(0(5(2(x1))))))
, 0(1(4(2(x1)))) -> 4(1(3(0(5(2(x1))))))
, 0(1(4(2(x1)))) -> 4(3(0(3(1(2(x1))))))
, 0(1(4(2(x1)))) -> 4(4(0(3(1(2(x1))))))
, 0(0(1(0(2(x1))))) -> 1(0(0(2(0(4(x1))))))
, 0(0(1(0(2(x1))))) -> 1(0(4(0(0(2(x1))))))
, 0(0(1(0(2(x1))))) -> 2(1(0(3(0(0(x1))))))
, 0(0(1(4(2(x1))))) -> 0(0(3(1(2(4(x1))))))
, 0(0(1(4(2(x1))))) -> 0(2(3(1(0(4(x1))))))
, 0(0(1(4(2(x1))))) -> 0(2(4(0(3(1(x1))))))
, 0(0(1(4(2(x1))))) -> 0(3(1(0(2(4(x1))))))
, 0(0(1(4(2(x1))))) -> 1(0(3(4(0(2(x1))))))
, 0(0(1(4(2(x1))))) -> 2(0(0(3(1(4(x1))))))
, 0(0(1(4(2(x1))))) -> 2(1(0(4(0(0(x1))))))
, 0(1(2(0(2(x1))))) -> 2(0(1(0(4(2(x1))))))
, 0(1(2(4(2(x1))))) -> 2(3(1(0(2(4(x1))))))
, 0(1(2(4(2(x1))))) -> 4(1(0(2(2(4(x1))))))
, 0(1(3(4(2(x1))))) -> 2(3(1(4(4(0(x1))))))
, 0(1(3(4(2(x1))))) -> 2(4(3(0(4(1(x1))))))
, 0(1(3(4(2(x1))))) -> 3(2(1(0(4(0(x1))))))
, 0(1(3(4(2(x1))))) -> 4(0(3(3(1(2(x1))))))
, 0(1(3(4(2(x1))))) -> 4(1(4(0(3(2(x1))))))
, 0(1(4(0(2(x1))))) -> 2(0(3(1(0(4(x1))))))
, 0(1(5(0(2(x1))))) -> 0(2(3(1(0(5(x1))))))
, 0(1(5(0(2(x1))))) -> 3(0(5(1(0(2(x1))))))
, 0(1(5(0(2(x1))))) -> 5(1(3(0(0(2(x1))))))
, 0(1(5(4(2(x1))))) -> 0(4(4(1(2(5(x1))))))
, 0(1(5(4(2(x1))))) -> 1(0(4(5(1(2(x1))))))
, 0(1(5(4(2(x1))))) -> 2(0(4(4(5(1(x1))))))
, 0(1(5(4(2(x1))))) -> 4(0(2(3(1(5(x1))))))
, 0(1(5(4(2(x1))))) -> 4(1(0(2(5(2(x1))))))
, 0(1(5(4(2(x1))))) -> 4(1(0(5(2(5(x1))))))
, 0(1(5(4(2(x1))))) -> 4(2(1(3(0(5(x1))))))
, 0(1(5(4(2(x1))))) -> 4(3(1(0(2(5(x1))))))
, 0(1(5(4(2(x1))))) -> 4(4(0(5(1(2(x1))))))
, 0(1(5(4(2(x1))))) -> 4(4(2(1(0(5(x1))))))
, 0(1(5(4(2(x1))))) -> 5(0(4(5(2(1(x1))))))
, 0(1(5(4(2(x1))))) -> 5(1(2(0(4(3(x1))))))
, 0(1(5(4(2(x1))))) -> 5(3(1(0(4(2(x1))))))
, 0(2(1(4(2(x1))))) -> 0(4(4(1(2(2(x1))))))
, 0(2(1(4(2(x1))))) -> 3(2(2(1(4(0(x1))))))
, 0(2(1(4(2(x1))))) -> 4(1(0(3(2(2(x1))))))
, 5(0(1(4(2(x1))))) -> 2(0(4(3(5(1(x1))))))
, 5(0(1(4(2(x1))))) -> 2(4(0(3(1(5(x1))))))
, 5(0(1(4(2(x1))))) -> 4(1(0(5(3(2(x1))))))
, 5(0(1(4(2(x1))))) -> 5(2(1(1(0(4(x1))))))
, 5(0(2(0(2(x1))))) -> 5(0(3(0(2(2(x1))))))
, 5(0(2(0(2(x1))))) -> 5(0(4(0(2(2(x1))))))
, 5(0(2(4(2(x1))))) -> 5(4(0(3(2(2(x1))))))
, 5(1(5(0(2(x1))))) -> 5(2(1(4(5(0(x1))))))
, 5(1(5(4(2(x1))))) -> 5(2(1(0(4(5(x1))))))
, 5(4(1(4(2(x1))))) -> 3(2(1(4(4(5(x1))))))
, 5(4(1(4(2(x1))))) -> 4(4(3(5(1(2(x1))))))
, 5(4(2(0(2(x1))))) -> 3(0(5(2(2(4(x1))))))
, 5(4(2(0(2(x1))))) -> 4(0(5(3(2(2(x1))))))
, 5(4(2(0(2(x1))))) -> 5(2(2(2(4(0(x1))))))
, 5(4(2(0(2(x1))))) -> 5(3(2(2(4(0(x1))))))
, 5(4(2(0(2(x1))))) -> 5(4(2(2(4(0(x1))))))
, 5(4(2(4(2(x1))))) -> 0(4(4(5(2(2(x1))))))
, 5(4(2(4(2(x1))))) -> 5(4(4(3(2(2(x1))))))
, 5(4(5(4(2(x1))))) -> 4(5(0(4(5(2(x1))))))}
Proof Output:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ 0_0(2) -> 1
, 0_0(3) -> 1
, 0_0(4) -> 1
, 0_0(5) -> 1
, 0_1(2) -> 15
, 0_1(3) -> 15
, 0_1(4) -> 15
, 0_1(5) -> 15
, 0_1(7) -> 7
, 0_1(7) -> 9
, 0_1(9) -> 58
, 0_1(10) -> 9
, 0_1(12) -> 11
, 0_1(15) -> 9
, 0_1(17) -> 16
, 0_1(19) -> 61
, 0_1(21) -> 20
, 0_1(23) -> 22
, 0_1(25) -> 24
, 0_1(30) -> 1
, 0_1(30) -> 15
, 0_1(30) -> 61
, 0_1(30) -> 96
, 0_1(44) -> 6
, 0_1(44) -> 21
, 0_1(44) -> 40
, 0_1(44) -> 65
, 0_1(44) -> 68
, 0_1(59) -> 58
, 0_2(7) -> 66
, 0_2(9) -> 91
, 0_2(10) -> 66
, 0_2(49) -> 48
, 0_2(51) -> 96
, 0_2(67) -> 64
, 0_2(70) -> 69
, 0_2(75) -> 74
, 0_2(82) -> 6
, 0_2(82) -> 21
, 0_2(82) -> 40
, 0_2(82) -> 65
, 0_2(82) -> 68
, 0_2(89) -> 88
, 0_2(92) -> 89
, 0_2(96) -> 95
, 0_2(105) -> 104
, 0_2(107) -> 106
, 1_0(2) -> 2
, 1_0(3) -> 2
, 1_0(4) -> 2
, 1_0(5) -> 2
, 1_1(2) -> 13
, 1_1(3) -> 13
, 1_1(4) -> 13
, 1_1(5) -> 13
, 1_1(9) -> 8
, 1_1(10) -> 17
, 1_1(16) -> 16
, 1_1(19) -> 18
, 1_1(20) -> 16
, 1_1(21) -> 18
, 1_1(22) -> 8
, 1_1(24) -> 22
, 1_1(33) -> 32
, 1_1(38) -> 37
, 1_1(58) -> 9
, 1_2(51) -> 93
, 1_2(64) -> 63
, 1_2(91) -> 90
, 1_2(95) -> 94
, 1_2(104) -> 103
, 1_2(106) -> 9
, 2_0(2) -> 3
, 2_0(3) -> 3
, 2_0(4) -> 3
, 2_0(5) -> 3
, 2_1(2) -> 19
, 2_1(3) -> 19
, 2_1(4) -> 19
, 2_1(5) -> 19
, 2_1(7) -> 1
, 2_1(7) -> 15
, 2_1(7) -> 16
, 2_1(8) -> 14
, 2_1(9) -> 9
, 2_1(10) -> 10
, 2_1(14) -> 14
, 2_1(19) -> 33
, 2_1(37) -> 36
, 2_2(2) -> 51
, 2_2(3) -> 51
, 2_2(4) -> 51
, 2_2(5) -> 51
, 2_2(7) -> 51
, 2_2(9) -> 51
, 2_2(10) -> 51
, 2_2(51) -> 77
, 2_2(63) -> 62
, 2_2(72) -> 71
, 2_2(73) -> 72
, 2_2(79) -> 78
, 2_2(80) -> 79
, 2_2(81) -> 80
, 2_2(88) -> 58
, 2_2(88) -> 91
, 2_2(91) -> 58
, 2_2(91) -> 91
, 3_0(2) -> 4
, 3_0(3) -> 4
, 3_0(4) -> 4
, 3_0(5) -> 4
, 3_1(2) -> 25
, 3_1(3) -> 25
, 3_1(4) -> 25
, 3_1(5) -> 25
, 3_1(8) -> 7
, 3_1(13) -> 12
, 3_1(14) -> 1
, 3_1(14) -> 15
, 3_1(14) -> 16
, 3_1(14) -> 61
, 3_1(14) -> 96
, 3_1(15) -> 1
, 3_1(15) -> 15
, 3_1(16) -> 16
, 3_1(17) -> 2
, 3_1(18) -> 17
, 3_1(19) -> 21
, 3_1(20) -> 16
, 3_1(22) -> 11
, 3_1(33) -> 10
, 3_1(36) -> 6
, 3_1(36) -> 40
, 3_1(36) -> 68
, 3_1(43) -> 42
, 3_1(60) -> 59
, 3_2(69) -> 6
, 3_2(69) -> 21
, 3_2(69) -> 40
, 3_2(69) -> 65
, 3_2(69) -> 68
, 3_2(77) -> 76
, 3_2(79) -> 78
, 3_2(90) -> 89
, 3_2(91) -> 96
, 3_2(93) -> 92
, 3_2(94) -> 88
, 3_2(96) -> 105
, 4_0(2) -> 5
, 4_0(3) -> 5
, 4_0(4) -> 5
, 4_0(5) -> 5
, 4_1(2) -> 10
, 4_1(3) -> 10
, 4_1(4) -> 10
, 4_1(5) -> 10
, 4_1(8) -> 1
, 4_1(8) -> 15
, 4_1(8) -> 16
, 4_1(8) -> 61
, 4_1(8) -> 96
, 4_1(9) -> 9
, 4_1(10) -> 9
, 4_1(11) -> 7
, 4_1(13) -> 23
, 4_1(15) -> 1
, 4_1(15) -> 9
, 4_1(15) -> 15
, 4_1(16) -> 1
, 4_1(16) -> 15
, 4_1(16) -> 16
, 4_1(19) -> 21
, 4_1(20) -> 9
, 4_1(21) -> 21
, 4_1(31) -> 30
, 4_1(32) -> 31
, 4_1(39) -> 38
, 4_1(40) -> 39
, 4_1(41) -> 6
, 4_1(41) -> 40
, 4_1(41) -> 68
, 4_1(42) -> 41
, 4_1(45) -> 44
, 4_1(46) -> 45
, 4_1(61) -> 60
, 4_2(7) -> 73
, 4_2(9) -> 9
, 4_2(10) -> 73
, 4_2(47) -> 21
, 4_2(50) -> 49
, 4_2(51) -> 107
, 4_2(65) -> 64
, 4_2(66) -> 81
, 4_2(68) -> 67
, 4_2(74) -> 6
, 4_2(74) -> 21
, 4_2(74) -> 40
, 4_2(74) -> 65
, 4_2(74) -> 68
, 4_2(76) -> 79
, 4_2(79) -> 78
, 4_2(83) -> 82
, 4_2(84) -> 83
, 4_2(96) -> 105
, 4_2(103) -> 58
, 4_2(103) -> 91
, 5_0(2) -> 6
, 5_0(3) -> 6
, 5_0(4) -> 6
, 5_0(5) -> 6
, 5_1(2) -> 40
, 5_1(3) -> 40
, 5_1(4) -> 40
, 5_1(5) -> 40
, 5_1(9) -> 6
, 5_1(9) -> 21
, 5_1(9) -> 40
, 5_1(9) -> 65
, 5_1(9) -> 68
, 5_1(18) -> 43
, 5_1(19) -> 21
, 5_1(21) -> 21
, 5_1(33) -> 46
, 5_2(2) -> 68
, 5_2(3) -> 68
, 5_2(4) -> 68
, 5_2(5) -> 68
, 5_2(7) -> 68
, 5_2(9) -> 68
, 5_2(10) -> 68
, 5_2(48) -> 47
, 5_2(51) -> 50
, 5_2(62) -> 43
, 5_2(66) -> 65
, 5_2(71) -> 70
, 5_2(76) -> 75
, 5_2(77) -> 84
, 5_2(78) -> 6
, 5_2(78) -> 21
, 5_2(78) -> 40
, 5_2(78) -> 65
, 5_2(78) -> 68
, 5_2(79) -> 50
, 5_2(80) -> 68}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(0(2(x1)))) -> 2(0(3(1(0(x1)))))
, 0(1(0(2(x1)))) -> 2(0(0(3(1(2(x1))))))
, 0(1(0(2(x1)))) -> 2(0(3(1(0(4(x1))))))
, 0(1(0(2(x1)))) -> 2(2(0(3(1(0(x1))))))
, 0(1(0(2(x1)))) -> 2(3(1(0(0(2(x1))))))
, 0(1(0(2(x1)))) -> 2(3(1(0(3(0(x1))))))
, 0(1(0(2(x1)))) -> 4(1(0(3(0(2(x1))))))
, 0(1(0(2(x1)))) -> 4(1(0(4(0(2(x1))))))
, 0(1(4(2(x1)))) -> 2(3(1(0(4(x1)))))
, 0(1(4(2(x1)))) -> 2(4(0(3(1(x1)))))
, 0(1(4(2(x1)))) -> 3(2(1(0(4(x1)))))
, 0(1(4(2(x1)))) -> 3(2(1(4(0(x1)))))
, 0(1(4(2(x1)))) -> 4(0(3(1(2(x1)))))
, 0(1(4(2(x1)))) -> 4(1(0(3(2(x1)))))
, 0(1(4(2(x1)))) -> 4(1(0(4(2(x1)))))
, 0(1(4(2(x1)))) -> 4(1(0(5(2(x1)))))
, 0(1(4(2(x1)))) -> 2(0(3(1(0(4(x1))))))
, 0(1(4(2(x1)))) -> 2(0(3(1(4(4(x1))))))
, 0(1(4(2(x1)))) -> 2(3(1(4(0(4(x1))))))
, 0(1(4(2(x1)))) -> 2(4(3(0(4(1(x1))))))
, 0(1(4(2(x1)))) -> 2(4(3(1(0(3(x1))))))
, 0(1(4(2(x1)))) -> 3(2(1(0(4(1(x1))))))
, 0(1(4(2(x1)))) -> 3(2(2(1(4(0(x1))))))
, 0(1(4(2(x1)))) -> 3(2(3(1(0(4(x1))))))
, 0(1(4(2(x1)))) -> 3(2(3(1(4(0(x1))))))
, 0(1(4(2(x1)))) -> 4(0(3(1(3(2(x1))))))
, 0(1(4(2(x1)))) -> 4(0(3(1(4(2(x1))))))
, 0(1(4(2(x1)))) -> 4(1(0(4(3(2(x1))))))
, 0(1(4(2(x1)))) -> 4(1(0(4(5(2(x1))))))
, 0(1(4(2(x1)))) -> 4(1(0(5(3(2(x1))))))
, 0(1(4(2(x1)))) -> 4(1(1(0(5(2(x1))))))
, 0(1(4(2(x1)))) -> 4(1(3(0(5(2(x1))))))
, 0(1(4(2(x1)))) -> 4(3(0(3(1(2(x1))))))
, 0(1(4(2(x1)))) -> 4(4(0(3(1(2(x1))))))
, 0(0(1(0(2(x1))))) -> 1(0(0(2(0(4(x1))))))
, 0(0(1(0(2(x1))))) -> 1(0(4(0(0(2(x1))))))
, 0(0(1(0(2(x1))))) -> 2(1(0(3(0(0(x1))))))
, 0(0(1(4(2(x1))))) -> 0(0(3(1(2(4(x1))))))
, 0(0(1(4(2(x1))))) -> 0(2(3(1(0(4(x1))))))
, 0(0(1(4(2(x1))))) -> 0(2(4(0(3(1(x1))))))
, 0(0(1(4(2(x1))))) -> 0(3(1(0(2(4(x1))))))
, 0(0(1(4(2(x1))))) -> 1(0(3(4(0(2(x1))))))
, 0(0(1(4(2(x1))))) -> 2(0(0(3(1(4(x1))))))
, 0(0(1(4(2(x1))))) -> 2(1(0(4(0(0(x1))))))
, 0(1(2(0(2(x1))))) -> 2(0(1(0(4(2(x1))))))
, 0(1(2(4(2(x1))))) -> 2(3(1(0(2(4(x1))))))
, 0(1(2(4(2(x1))))) -> 4(1(0(2(2(4(x1))))))
, 0(1(3(4(2(x1))))) -> 2(3(1(4(4(0(x1))))))
, 0(1(3(4(2(x1))))) -> 2(4(3(0(4(1(x1))))))
, 0(1(3(4(2(x1))))) -> 3(2(1(0(4(0(x1))))))
, 0(1(3(4(2(x1))))) -> 4(0(3(3(1(2(x1))))))
, 0(1(3(4(2(x1))))) -> 4(1(4(0(3(2(x1))))))
, 0(1(4(0(2(x1))))) -> 2(0(3(1(0(4(x1))))))
, 0(1(5(0(2(x1))))) -> 0(2(3(1(0(5(x1))))))
, 0(1(5(0(2(x1))))) -> 3(0(5(1(0(2(x1))))))
, 0(1(5(0(2(x1))))) -> 5(1(3(0(0(2(x1))))))
, 0(1(5(4(2(x1))))) -> 0(4(4(1(2(5(x1))))))
, 0(1(5(4(2(x1))))) -> 1(0(4(5(1(2(x1))))))
, 0(1(5(4(2(x1))))) -> 2(0(4(4(5(1(x1))))))
, 0(1(5(4(2(x1))))) -> 4(0(2(3(1(5(x1))))))
, 0(1(5(4(2(x1))))) -> 4(1(0(2(5(2(x1))))))
, 0(1(5(4(2(x1))))) -> 4(1(0(5(2(5(x1))))))
, 0(1(5(4(2(x1))))) -> 4(2(1(3(0(5(x1))))))
, 0(1(5(4(2(x1))))) -> 4(3(1(0(2(5(x1))))))
, 0(1(5(4(2(x1))))) -> 4(4(0(5(1(2(x1))))))
, 0(1(5(4(2(x1))))) -> 4(4(2(1(0(5(x1))))))
, 0(1(5(4(2(x1))))) -> 5(0(4(5(2(1(x1))))))
, 0(1(5(4(2(x1))))) -> 5(1(2(0(4(3(x1))))))
, 0(1(5(4(2(x1))))) -> 5(3(1(0(4(2(x1))))))
, 0(2(1(4(2(x1))))) -> 0(4(4(1(2(2(x1))))))
, 0(2(1(4(2(x1))))) -> 3(2(2(1(4(0(x1))))))
, 0(2(1(4(2(x1))))) -> 4(1(0(3(2(2(x1))))))
, 5(0(1(4(2(x1))))) -> 2(0(4(3(5(1(x1))))))
, 5(0(1(4(2(x1))))) -> 2(4(0(3(1(5(x1))))))
, 5(0(1(4(2(x1))))) -> 4(1(0(5(3(2(x1))))))
, 5(0(1(4(2(x1))))) -> 5(2(1(1(0(4(x1))))))
, 5(0(2(0(2(x1))))) -> 5(0(3(0(2(2(x1))))))
, 5(0(2(0(2(x1))))) -> 5(0(4(0(2(2(x1))))))
, 5(0(2(4(2(x1))))) -> 5(4(0(3(2(2(x1))))))
, 5(1(5(0(2(x1))))) -> 5(2(1(4(5(0(x1))))))
, 5(1(5(4(2(x1))))) -> 5(2(1(0(4(5(x1))))))
, 5(4(1(4(2(x1))))) -> 3(2(1(4(4(5(x1))))))
, 5(4(1(4(2(x1))))) -> 4(4(3(5(1(2(x1))))))
, 5(4(2(0(2(x1))))) -> 3(0(5(2(2(4(x1))))))
, 5(4(2(0(2(x1))))) -> 4(0(5(3(2(2(x1))))))
, 5(4(2(0(2(x1))))) -> 5(2(2(2(4(0(x1))))))
, 5(4(2(0(2(x1))))) -> 5(3(2(2(4(0(x1))))))
, 5(4(2(0(2(x1))))) -> 5(4(2(2(4(0(x1))))))
, 5(4(2(4(2(x1))))) -> 0(4(4(5(2(2(x1))))))
, 5(4(2(4(2(x1))))) -> 5(4(4(3(2(2(x1))))))
, 5(4(5(4(2(x1))))) -> 4(5(0(4(5(2(x1))))))}
Proof Output:
'Bounds with perSymbol-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with perSymbol-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with perSymbol-enrichment and initial automaton 'match''
----------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ 0(1(0(2(x1)))) -> 2(0(3(1(0(x1)))))
, 0(1(0(2(x1)))) -> 2(0(0(3(1(2(x1))))))
, 0(1(0(2(x1)))) -> 2(0(3(1(0(4(x1))))))
, 0(1(0(2(x1)))) -> 2(2(0(3(1(0(x1))))))
, 0(1(0(2(x1)))) -> 2(3(1(0(0(2(x1))))))
, 0(1(0(2(x1)))) -> 2(3(1(0(3(0(x1))))))
, 0(1(0(2(x1)))) -> 4(1(0(3(0(2(x1))))))
, 0(1(0(2(x1)))) -> 4(1(0(4(0(2(x1))))))
, 0(1(4(2(x1)))) -> 2(3(1(0(4(x1)))))
, 0(1(4(2(x1)))) -> 2(4(0(3(1(x1)))))
, 0(1(4(2(x1)))) -> 3(2(1(0(4(x1)))))
, 0(1(4(2(x1)))) -> 3(2(1(4(0(x1)))))
, 0(1(4(2(x1)))) -> 4(0(3(1(2(x1)))))
, 0(1(4(2(x1)))) -> 4(1(0(3(2(x1)))))
, 0(1(4(2(x1)))) -> 4(1(0(4(2(x1)))))
, 0(1(4(2(x1)))) -> 4(1(0(5(2(x1)))))
, 0(1(4(2(x1)))) -> 2(0(3(1(0(4(x1))))))
, 0(1(4(2(x1)))) -> 2(0(3(1(4(4(x1))))))
, 0(1(4(2(x1)))) -> 2(3(1(4(0(4(x1))))))
, 0(1(4(2(x1)))) -> 2(4(3(0(4(1(x1))))))
, 0(1(4(2(x1)))) -> 2(4(3(1(0(3(x1))))))
, 0(1(4(2(x1)))) -> 3(2(1(0(4(1(x1))))))
, 0(1(4(2(x1)))) -> 3(2(2(1(4(0(x1))))))
, 0(1(4(2(x1)))) -> 3(2(3(1(0(4(x1))))))
, 0(1(4(2(x1)))) -> 3(2(3(1(4(0(x1))))))
, 0(1(4(2(x1)))) -> 4(0(3(1(3(2(x1))))))
, 0(1(4(2(x1)))) -> 4(0(3(1(4(2(x1))))))
, 0(1(4(2(x1)))) -> 4(1(0(4(3(2(x1))))))
, 0(1(4(2(x1)))) -> 4(1(0(4(5(2(x1))))))
, 0(1(4(2(x1)))) -> 4(1(0(5(3(2(x1))))))
, 0(1(4(2(x1)))) -> 4(1(1(0(5(2(x1))))))
, 0(1(4(2(x1)))) -> 4(1(3(0(5(2(x1))))))
, 0(1(4(2(x1)))) -> 4(3(0(3(1(2(x1))))))
, 0(1(4(2(x1)))) -> 4(4(0(3(1(2(x1))))))
, 0(0(1(0(2(x1))))) -> 1(0(0(2(0(4(x1))))))
, 0(0(1(0(2(x1))))) -> 1(0(4(0(0(2(x1))))))
, 0(0(1(0(2(x1))))) -> 2(1(0(3(0(0(x1))))))
, 0(0(1(4(2(x1))))) -> 0(0(3(1(2(4(x1))))))
, 0(0(1(4(2(x1))))) -> 0(2(3(1(0(4(x1))))))
, 0(0(1(4(2(x1))))) -> 0(2(4(0(3(1(x1))))))
, 0(0(1(4(2(x1))))) -> 0(3(1(0(2(4(x1))))))
, 0(0(1(4(2(x1))))) -> 1(0(3(4(0(2(x1))))))
, 0(0(1(4(2(x1))))) -> 2(0(0(3(1(4(x1))))))
, 0(0(1(4(2(x1))))) -> 2(1(0(4(0(0(x1))))))
, 0(1(2(0(2(x1))))) -> 2(0(1(0(4(2(x1))))))
, 0(1(2(4(2(x1))))) -> 2(3(1(0(2(4(x1))))))
, 0(1(2(4(2(x1))))) -> 4(1(0(2(2(4(x1))))))
, 0(1(3(4(2(x1))))) -> 2(3(1(4(4(0(x1))))))
, 0(1(3(4(2(x1))))) -> 2(4(3(0(4(1(x1))))))
, 0(1(3(4(2(x1))))) -> 3(2(1(0(4(0(x1))))))
, 0(1(3(4(2(x1))))) -> 4(0(3(3(1(2(x1))))))
, 0(1(3(4(2(x1))))) -> 4(1(4(0(3(2(x1))))))
, 0(1(4(0(2(x1))))) -> 2(0(3(1(0(4(x1))))))
, 0(1(5(0(2(x1))))) -> 0(2(3(1(0(5(x1))))))
, 0(1(5(0(2(x1))))) -> 3(0(5(1(0(2(x1))))))
, 0(1(5(0(2(x1))))) -> 5(1(3(0(0(2(x1))))))
, 0(1(5(4(2(x1))))) -> 0(4(4(1(2(5(x1))))))
, 0(1(5(4(2(x1))))) -> 1(0(4(5(1(2(x1))))))
, 0(1(5(4(2(x1))))) -> 2(0(4(4(5(1(x1))))))
, 0(1(5(4(2(x1))))) -> 4(0(2(3(1(5(x1))))))
, 0(1(5(4(2(x1))))) -> 4(1(0(2(5(2(x1))))))
, 0(1(5(4(2(x1))))) -> 4(1(0(5(2(5(x1))))))
, 0(1(5(4(2(x1))))) -> 4(2(1(3(0(5(x1))))))
, 0(1(5(4(2(x1))))) -> 4(3(1(0(2(5(x1))))))
, 0(1(5(4(2(x1))))) -> 4(4(0(5(1(2(x1))))))
, 0(1(5(4(2(x1))))) -> 4(4(2(1(0(5(x1))))))
, 0(1(5(4(2(x1))))) -> 5(0(4(5(2(1(x1))))))
, 0(1(5(4(2(x1))))) -> 5(1(2(0(4(3(x1))))))
, 0(1(5(4(2(x1))))) -> 5(3(1(0(4(2(x1))))))
, 0(2(1(4(2(x1))))) -> 0(4(4(1(2(2(x1))))))
, 0(2(1(4(2(x1))))) -> 3(2(2(1(4(0(x1))))))
, 0(2(1(4(2(x1))))) -> 4(1(0(3(2(2(x1))))))
, 5(0(1(4(2(x1))))) -> 2(0(4(3(5(1(x1))))))
, 5(0(1(4(2(x1))))) -> 2(4(0(3(1(5(x1))))))
, 5(0(1(4(2(x1))))) -> 4(1(0(5(3(2(x1))))))
, 5(0(1(4(2(x1))))) -> 5(2(1(1(0(4(x1))))))
, 5(0(2(0(2(x1))))) -> 5(0(3(0(2(2(x1))))))
, 5(0(2(0(2(x1))))) -> 5(0(4(0(2(2(x1))))))
, 5(0(2(4(2(x1))))) -> 5(4(0(3(2(2(x1))))))
, 5(1(5(0(2(x1))))) -> 5(2(1(4(5(0(x1))))))
, 5(1(5(4(2(x1))))) -> 5(2(1(0(4(5(x1))))))
, 5(4(1(4(2(x1))))) -> 3(2(1(4(4(5(x1))))))
, 5(4(1(4(2(x1))))) -> 4(4(3(5(1(2(x1))))))
, 5(4(2(0(2(x1))))) -> 3(0(5(2(2(4(x1))))))
, 5(4(2(0(2(x1))))) -> 4(0(5(3(2(2(x1))))))
, 5(4(2(0(2(x1))))) -> 5(2(2(2(4(0(x1))))))
, 5(4(2(0(2(x1))))) -> 5(3(2(2(4(0(x1))))))
, 5(4(2(0(2(x1))))) -> 5(4(2(2(4(0(x1))))))
, 5(4(2(4(2(x1))))) -> 0(4(4(5(2(2(x1))))))
, 5(4(2(4(2(x1))))) -> 5(4(4(3(2(2(x1))))))
, 5(4(5(4(2(x1))))) -> 4(5(0(4(5(2(x1))))))}
Proof Output:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ 0_0(2) -> 1
, 0_0(3) -> 1
, 0_0(4) -> 1
, 0_0(5) -> 1
, 0_1(2) -> 15
, 0_1(3) -> 15
, 0_1(4) -> 15
, 0_1(5) -> 15
, 0_1(7) -> 7
, 0_1(7) -> 9
, 0_1(9) -> 58
, 0_1(10) -> 9
, 0_1(12) -> 11
, 0_1(15) -> 9
, 0_1(17) -> 16
, 0_1(19) -> 61
, 0_1(21) -> 20
, 0_1(23) -> 22
, 0_1(25) -> 24
, 0_1(30) -> 1
, 0_1(30) -> 15
, 0_1(30) -> 61
, 0_1(30) -> 96
, 0_1(44) -> 6
, 0_1(44) -> 21
, 0_1(44) -> 40
, 0_1(44) -> 65
, 0_1(44) -> 68
, 0_1(59) -> 58
, 0_2(7) -> 66
, 0_2(9) -> 91
, 0_2(10) -> 66
, 0_2(49) -> 48
, 0_2(51) -> 96
, 0_2(67) -> 64
, 0_2(70) -> 69
, 0_2(75) -> 74
, 0_2(82) -> 6
, 0_2(82) -> 21
, 0_2(82) -> 40
, 0_2(82) -> 65
, 0_2(82) -> 68
, 0_2(89) -> 88
, 0_2(92) -> 89
, 0_2(96) -> 95
, 0_2(105) -> 104
, 0_2(107) -> 106
, 1_0(2) -> 2
, 1_0(3) -> 2
, 1_0(4) -> 2
, 1_0(5) -> 2
, 1_1(2) -> 13
, 1_1(3) -> 13
, 1_1(4) -> 13
, 1_1(5) -> 13
, 1_1(9) -> 8
, 1_1(10) -> 17
, 1_1(16) -> 16
, 1_1(19) -> 18
, 1_1(20) -> 16
, 1_1(21) -> 18
, 1_1(22) -> 8
, 1_1(24) -> 22
, 1_1(33) -> 32
, 1_1(38) -> 37
, 1_1(58) -> 9
, 1_2(51) -> 93
, 1_2(64) -> 63
, 1_2(91) -> 90
, 1_2(95) -> 94
, 1_2(104) -> 103
, 1_2(106) -> 9
, 2_0(2) -> 3
, 2_0(3) -> 3
, 2_0(4) -> 3
, 2_0(5) -> 3
, 2_1(2) -> 19
, 2_1(3) -> 19
, 2_1(4) -> 19
, 2_1(5) -> 19
, 2_1(7) -> 1
, 2_1(7) -> 15
, 2_1(7) -> 16
, 2_1(8) -> 14
, 2_1(9) -> 9
, 2_1(10) -> 10
, 2_1(14) -> 14
, 2_1(19) -> 33
, 2_1(37) -> 36
, 2_2(2) -> 51
, 2_2(3) -> 51
, 2_2(4) -> 51
, 2_2(5) -> 51
, 2_2(7) -> 51
, 2_2(9) -> 51
, 2_2(10) -> 51
, 2_2(51) -> 77
, 2_2(63) -> 62
, 2_2(72) -> 71
, 2_2(73) -> 72
, 2_2(79) -> 78
, 2_2(80) -> 79
, 2_2(81) -> 80
, 2_2(88) -> 58
, 2_2(88) -> 91
, 2_2(91) -> 58
, 2_2(91) -> 91
, 3_0(2) -> 4
, 3_0(3) -> 4
, 3_0(4) -> 4
, 3_0(5) -> 4
, 3_1(2) -> 25
, 3_1(3) -> 25
, 3_1(4) -> 25
, 3_1(5) -> 25
, 3_1(8) -> 7
, 3_1(13) -> 12
, 3_1(14) -> 1
, 3_1(14) -> 15
, 3_1(14) -> 16
, 3_1(14) -> 61
, 3_1(14) -> 96
, 3_1(15) -> 1
, 3_1(15) -> 15
, 3_1(16) -> 16
, 3_1(17) -> 2
, 3_1(18) -> 17
, 3_1(19) -> 21
, 3_1(20) -> 16
, 3_1(22) -> 11
, 3_1(33) -> 10
, 3_1(36) -> 6
, 3_1(36) -> 40
, 3_1(36) -> 68
, 3_1(43) -> 42
, 3_1(60) -> 59
, 3_2(69) -> 6
, 3_2(69) -> 21
, 3_2(69) -> 40
, 3_2(69) -> 65
, 3_2(69) -> 68
, 3_2(77) -> 76
, 3_2(79) -> 78
, 3_2(90) -> 89
, 3_2(91) -> 96
, 3_2(93) -> 92
, 3_2(94) -> 88
, 3_2(96) -> 105
, 4_0(2) -> 5
, 4_0(3) -> 5
, 4_0(4) -> 5
, 4_0(5) -> 5
, 4_1(2) -> 10
, 4_1(3) -> 10
, 4_1(4) -> 10
, 4_1(5) -> 10
, 4_1(8) -> 1
, 4_1(8) -> 15
, 4_1(8) -> 16
, 4_1(8) -> 61
, 4_1(8) -> 96
, 4_1(9) -> 9
, 4_1(10) -> 9
, 4_1(11) -> 7
, 4_1(13) -> 23
, 4_1(15) -> 1
, 4_1(15) -> 9
, 4_1(15) -> 15
, 4_1(16) -> 1
, 4_1(16) -> 15
, 4_1(16) -> 16
, 4_1(19) -> 21
, 4_1(20) -> 9
, 4_1(21) -> 21
, 4_1(31) -> 30
, 4_1(32) -> 31
, 4_1(39) -> 38
, 4_1(40) -> 39
, 4_1(41) -> 6
, 4_1(41) -> 40
, 4_1(41) -> 68
, 4_1(42) -> 41
, 4_1(45) -> 44
, 4_1(46) -> 45
, 4_1(61) -> 60
, 4_2(7) -> 73
, 4_2(9) -> 9
, 4_2(10) -> 73
, 4_2(47) -> 21
, 4_2(50) -> 49
, 4_2(51) -> 107
, 4_2(65) -> 64
, 4_2(66) -> 81
, 4_2(68) -> 67
, 4_2(74) -> 6
, 4_2(74) -> 21
, 4_2(74) -> 40
, 4_2(74) -> 65
, 4_2(74) -> 68
, 4_2(76) -> 79
, 4_2(79) -> 78
, 4_2(83) -> 82
, 4_2(84) -> 83
, 4_2(96) -> 105
, 4_2(103) -> 58
, 4_2(103) -> 91
, 5_0(2) -> 6
, 5_0(3) -> 6
, 5_0(4) -> 6
, 5_0(5) -> 6
, 5_1(2) -> 40
, 5_1(3) -> 40
, 5_1(4) -> 40
, 5_1(5) -> 40
, 5_1(9) -> 6
, 5_1(9) -> 21
, 5_1(9) -> 40
, 5_1(9) -> 65
, 5_1(9) -> 68
, 5_1(18) -> 43
, 5_1(19) -> 21
, 5_1(21) -> 21
, 5_1(33) -> 46
, 5_2(2) -> 68
, 5_2(3) -> 68
, 5_2(4) -> 68
, 5_2(5) -> 68
, 5_2(7) -> 68
, 5_2(9) -> 68
, 5_2(10) -> 68
, 5_2(48) -> 47
, 5_2(51) -> 50
, 5_2(62) -> 43
, 5_2(66) -> 65
, 5_2(71) -> 70
, 5_2(76) -> 75
, 5_2(77) -> 84
, 5_2(78) -> 6
, 5_2(78) -> 21
, 5_2(78) -> 40
, 5_2(78) -> 65
, 5_2(78) -> 68
, 5_2(79) -> 50
, 5_2(80) -> 68}