Tool CaT
stdout:
YES(?,O(n^1))
Problem:
0(1(0(1(x1)))) -> 0(0(2(1(3(1(x1))))))
0(1(0(1(x1)))) -> 2(1(0(2(0(1(x1))))))
0(1(0(1(x1)))) -> 2(1(3(1(0(0(x1))))))
4(1(0(1(x1)))) -> 1(0(4(2(1(x1)))))
4(1(0(1(x1)))) -> 4(1(0(2(1(x1)))))
4(1(0(1(x1)))) -> 0(2(1(3(4(1(x1))))))
4(1(0(1(x1)))) -> 0(4(2(1(3(1(x1))))))
4(1(0(1(x1)))) -> 1(0(2(4(1(3(x1))))))
4(1(0(1(x1)))) -> 1(0(4(2(2(1(x1))))))
4(1(0(1(x1)))) -> 1(0(4(5(2(1(x1))))))
4(1(0(1(x1)))) -> 4(0(2(1(3(1(x1))))))
4(1(0(1(x1)))) -> 4(1(0(2(1(3(x1))))))
4(1(0(1(x1)))) -> 4(1(3(0(2(1(x1))))))
4(1(1(1(x1)))) -> 4(1(3(1(3(1(x1))))))
4(3(0(1(x1)))) -> 0(2(1(3(4(x1)))))
4(3(0(1(x1)))) -> 0(2(4(1(3(x1)))))
4(3(0(1(x1)))) -> 0(4(2(1(3(x1)))))
4(3(0(1(x1)))) -> 3(0(4(2(1(x1)))))
4(3(0(1(x1)))) -> 3(4(0(2(1(x1)))))
4(3(0(1(x1)))) -> 4(0(2(1(3(x1)))))
4(3(0(1(x1)))) -> 4(3(0(2(1(x1)))))
4(3(0(1(x1)))) -> 0(2(1(3(3(4(x1))))))
4(3(0(1(x1)))) -> 0(2(1(3(4(3(x1))))))
4(3(0(1(x1)))) -> 0(2(4(1(3(3(x1))))))
4(3(0(1(x1)))) -> 0(4(2(2(1(3(x1))))))
4(3(0(1(x1)))) -> 0(4(5(2(1(3(x1))))))
4(3(0(1(x1)))) -> 1(0(2(1(3(4(x1))))))
4(3(0(1(x1)))) -> 1(0(2(4(1(3(x1))))))
4(3(0(1(x1)))) -> 1(0(4(2(1(3(x1))))))
4(3(0(1(x1)))) -> 1(3(0(4(2(1(x1))))))
4(3(0(1(x1)))) -> 3(0(4(5(2(1(x1))))))
4(3(0(1(x1)))) -> 3(1(0(4(2(1(x1))))))
4(3(0(1(x1)))) -> 3(3(4(0(2(1(x1))))))
4(3(0(1(x1)))) -> 3(4(0(2(1(3(x1))))))
4(3(0(1(x1)))) -> 3(4(0(2(2(1(x1))))))
4(3(0(1(x1)))) -> 3(4(0(5(2(1(x1))))))
4(3(0(1(x1)))) -> 3(4(1(0(2(1(x1))))))
4(3(0(1(x1)))) -> 3(4(3(0(2(1(x1))))))
4(3(0(1(x1)))) -> 4(3(0(2(1(3(x1))))))
4(3(0(1(x1)))) -> 4(3(0(5(2(1(x1))))))
4(3(0(1(x1)))) -> 4(3(1(0(2(1(x1))))))
4(3(0(1(x1)))) -> 4(3(3(0(2(1(x1))))))
4(5(1(1(x1)))) -> 4(5(2(1(1(x1)))))
4(5(1(1(x1)))) -> 4(2(5(2(1(1(x1))))))
4(5(1(1(x1)))) -> 4(5(2(1(3(1(x1))))))
4(5(1(1(x1)))) -> 4(5(2(2(1(1(x1))))))
4(5(1(1(x1)))) -> 4(5(5(2(1(1(x1))))))
0(0(1(0(1(x1))))) -> 0(0(1(0(2(1(x1))))))
0(0(3(1(1(x1))))) -> 2(1(3(1(0(0(x1))))))
0(0(5(1(1(x1))))) -> 5(0(0(2(1(1(x1))))))
0(4(1(0(1(x1))))) -> 2(1(0(4(0(1(x1))))))
0(4(3(0(1(x1))))) -> 0(0(2(1(3(4(x1))))))
0(4(3(0(1(x1))))) -> 0(4(3(0(2(1(x1))))))
0(4(3(0(1(x1))))) -> 2(3(1(0(4(0(x1))))))
0(4(3(1(1(x1))))) -> 2(1(4(1(3(0(x1))))))
0(4(3(1(1(x1))))) -> 4(2(0(3(1(1(x1))))))
0(4(5(1(1(x1))))) -> 4(0(1(5(2(1(x1))))))
0(4(5(1(1(x1))))) -> 5(2(1(4(0(1(x1))))))
4(0(3(0(1(x1))))) -> 0(0(4(2(1(3(x1))))))
4(0(3(0(1(x1))))) -> 2(0(4(0(1(3(x1))))))
4(0(3(0(1(x1))))) -> 2(0(4(0(3(1(x1))))))
4(1(0(1(1(x1))))) -> 1(0(4(2(1(1(x1))))))
4(1(1(0(1(x1))))) -> 4(1(0(2(1(1(x1))))))
4(1(2(0(1(x1))))) -> 0(4(2(1(3(1(x1))))))
4(1(2(0(1(x1))))) -> 1(0(2(4(1(3(x1))))))
4(1(2(0(1(x1))))) -> 4(0(2(2(1(1(x1))))))
4(1(2(0(1(x1))))) -> 4(1(0(2(2(1(x1))))))
4(1(3(0(1(x1))))) -> 4(1(3(0(2(1(x1))))))
4(1(5(0(1(x1))))) -> 1(1(5(0(4(2(x1))))))
4(1(5(1(1(x1))))) -> 1(4(5(2(1(1(x1))))))
4(3(0(1(1(x1))))) -> 1(3(0(2(1(4(x1))))))
4(3(0(1(1(x1))))) -> 1(3(1(4(0(2(x1))))))
4(3(0(1(1(x1))))) -> 1(3(1(4(2(0(x1))))))
4(3(0(1(1(x1))))) -> 3(1(0(2(4(1(x1))))))
4(3(0(1(1(x1))))) -> 4(3(1(1(0(2(x1))))))
4(3(1(0(1(x1))))) -> 0(4(2(1(3(1(x1))))))
4(3(1(0(1(x1))))) -> 1(3(4(0(2(1(x1))))))
4(3(2(0(1(x1))))) -> 3(4(0(2(2(1(x1))))))
4(3(2(0(1(x1))))) -> 3(4(0(5(2(1(x1))))))
4(3(2(0(1(x1))))) -> 4(0(2(1(3(1(x1))))))
4(3(2(0(1(x1))))) -> 4(3(0(2(1(3(x1))))))
4(3(2(1(1(x1))))) -> 1(3(1(2(4(2(x1))))))
4(3(2(1(1(x1))))) -> 1(3(1(4(5(2(x1))))))
4(3(2(1(1(x1))))) -> 3(1(3(4(1(2(x1))))))
4(3(2(1(1(x1))))) -> 4(1(3(1(2(2(x1))))))
4(3(2(1(1(x1))))) -> 4(1(3(3(1(2(x1))))))
4(3(3(0(1(x1))))) -> 4(3(3(0(2(1(x1))))))
4(3(4(0(1(x1))))) -> 3(4(0(4(2(1(x1))))))
4(3(4(0(1(x1))))) -> 4(4(0(2(1(3(x1))))))
4(3(5(0(1(x1))))) -> 0(5(2(3(1(4(x1))))))
4(3(5(0(1(x1))))) -> 1(3(0(2(5(4(x1))))))
4(3(5(0(1(x1))))) -> 1(3(0(4(2(5(x1))))))
4(3(5(0(1(x1))))) -> 1(3(4(0(5(2(x1))))))
4(3(5(0(1(x1))))) -> 3(1(0(4(2(5(x1))))))
4(3(5(0(1(x1))))) -> 3(1(5(0(4(2(x1))))))
4(3(5(0(1(x1))))) -> 3(4(0(2(1(5(x1))))))
4(3(5(0(1(x1))))) -> 3(4(1(5(0(2(x1))))))
4(3(5(0(1(x1))))) -> 3(5(1(0(4(2(x1))))))
4(3(5(0(1(x1))))) -> 4(3(0(2(1(5(x1))))))
4(3(5(0(1(x1))))) -> 5(1(3(4(0(2(x1))))))
4(3(5(1(1(x1))))) -> 1(4(5(2(1(3(x1))))))
4(3(5(1(1(x1))))) -> 3(1(1(5(4(2(x1))))))
4(3(5(1(1(x1))))) -> 3(1(4(5(2(1(x1))))))
4(3(5(1(1(x1))))) -> 4(1(3(1(3(5(x1))))))
4(3(5(1(1(x1))))) -> 4(1(5(2(1(3(x1))))))
4(3(5(1(1(x1))))) -> 4(3(1(5(2(1(x1))))))
4(4(1(0(1(x1))))) -> 4(4(1(0(2(1(x1))))))
4(4(3(0(1(x1))))) -> 0(4(4(2(1(3(x1))))))
4(4(3(0(1(x1))))) -> 4(0(2(1(3(4(x1))))))
4(4(3(0(1(x1))))) -> 4(3(4(0(2(1(x1))))))
4(4(3(0(1(x1))))) -> 4(4(3(0(2(1(x1))))))
4(5(1(0(1(x1))))) -> 0(5(1(3(4(1(x1))))))
4(5(1(0(1(x1))))) -> 0(5(4(1(3(1(x1))))))
4(5(1(0(1(x1))))) -> 1(0(4(5(2(1(x1))))))
4(5(1(0(1(x1))))) -> 4(0(5(2(1(1(x1))))))
4(5(1(0(1(x1))))) -> 4(5(1(0(2(1(x1))))))
4(5(1(0(1(x1))))) -> 5(1(0(2(4(1(x1))))))
4(5(1(0(1(x1))))) -> 5(4(1(0(2(1(x1))))))
4(5(1(1(1(x1))))) -> 4(5(2(1(1(1(x1))))))
4(5(3(0(1(x1))))) -> 0(2(1(3(4(5(x1))))))
4(5(3(0(1(x1))))) -> 0(5(2(1(3(4(x1))))))
4(5(3(0(1(x1))))) -> 0(5(2(4(3(1(x1))))))
4(5(3(0(1(x1))))) -> 0(5(4(2(1(3(x1))))))
4(5(3(0(1(x1))))) -> 1(0(5(1(3(4(x1))))))
4(5(3(0(1(x1))))) -> 1(5(0(3(3(4(x1))))))
4(5(3(0(1(x1))))) -> 2(1(4(5(0(3(x1))))))
4(5(3(0(1(x1))))) -> 2(4(1(3(5(0(x1))))))
4(5(3(0(1(x1))))) -> 3(0(4(5(2(1(x1))))))
4(5(3(0(1(x1))))) -> 4(0(3(1(5(2(x1))))))
4(5(3(0(1(x1))))) -> 4(0(3(3(5(1(x1))))))
4(5(3(0(1(x1))))) -> 4(0(5(4(1(3(x1))))))
4(5(3(0(1(x1))))) -> 4(1(3(5(0(3(x1))))))
4(5(3(0(1(x1))))) -> 4(1(3(5(5(0(x1))))))
4(5(3(0(1(x1))))) -> 4(2(5(0(3(1(x1))))))
4(5(3(0(1(x1))))) -> 4(5(2(0(3(1(x1))))))
4(5(3(0(1(x1))))) -> 5(0(3(1(4(1(x1))))))
4(5(3(0(1(x1))))) -> 5(0(3(4(4(1(x1))))))
4(5(3(0(1(x1))))) -> 5(1(3(0(3(4(x1))))))
4(5(3(0(1(x1))))) -> 5(2(1(3(4(0(x1))))))
4(5(3(0(1(x1))))) -> 5(2(4(1(3(0(x1))))))
4(5(3(0(1(x1))))) -> 5(3(0(4(2(1(x1))))))
4(5(3(0(1(x1))))) -> 5(4(1(3(0(1(x1))))))
4(5(3(0(1(x1))))) -> 5(4(1(3(2(0(x1))))))
4(5(3(0(1(x1))))) -> 5(4(3(0(2(1(x1))))))
4(5(3(1(1(x1))))) -> 2(4(1(3(1(5(x1))))))
4(5(3(1(1(x1))))) -> 4(5(2(1(3(1(x1))))))
4(5(3(1(1(x1))))) -> 5(1(3(4(1(2(x1))))))
4(5(3(1(1(x1))))) -> 5(2(1(4(1(3(x1))))))
4(5(3(1(1(x1))))) -> 5(4(2(1(3(1(x1))))))
4(5(5(1(1(x1))))) -> 5(5(2(1(1(4(x1))))))
4(5(5(1(1(x1))))) -> 5(5(2(4(1(1(x1))))))
Proof:
Bounds Processor:
bound: 2
enrichment: match
automaton:
final states: {6,5}
transitions:
51(55) -> 56*
51(134) -> 135*
51(39) -> 40*
51(201) -> 202*
51(151) -> 152*
51(183) -> 184*
51(153) -> 154*
51(143) -> 144*
51(88) -> 89*
51(145) -> 146*
51(130) -> 131*
21(187) -> 188*
21(67) -> 68*
21(47) -> 48*
21(174) -> 175*
21(79) -> 80*
21(69) -> 70*
21(49) -> 50*
21(81) -> 82*
21(41) -> 42*
21(133) -> 134*
21(73) -> 74*
21(38) -> 39*
21(200) -> 201*
21(105) -> 106*
41(197) -> 198*
41(92) -> 93*
41(219) -> 220*
41(89) -> 90*
41(221) -> 222*
41(19) -> 20*
41(211) -> 212*
41(213) -> 214*
41(173) -> 174*
41(68) -> 69*
41(195) -> 196*
41(185) -> 186*
41(135) -> 136*
11(70) -> 71*
11(172) -> 173*
11(57) -> 58*
11(37) -> 38*
11(27) -> 28*
11(199) -> 200*
11(169) -> 170*
11(159) -> 160*
11(94) -> 95*
11(29) -> 30*
11(14) -> 15*
11(186) -> 187*
11(161) -> 162*
11(131) -> 132*
11(91) -> 92*
11(21) -> 22*
11(16) -> 17*
11(198) -> 199*
11(18) -> 19*
31(15) -> 16*
31(162) -> 163*
31(107) -> 108*
31(17) -> 18*
31(171) -> 172*
31(121) -> 122*
31(71) -> 72*
31(123) -> 124*
31(113) -> 114*
31(93) -> 94*
31(115) -> 116*
31(95) -> 96*
42(237) -> 238*
12(257) -> 258*
12(232) -> 233*
12(234) -> 235*
12(251) -> 252*
12(236) -> 237*
12(253) -> 254*
12(243) -> 244*
12(245) -> 246*
00(2) -> 5*
00(4) -> 5*
00(1) -> 5*
00(3) -> 5*
32(233) -> 234*
32(235) -> 236*
10(2) -> 1*
10(4) -> 1*
10(1) -> 1*
10(3) -> 1*
20(2) -> 2*
20(4) -> 2*
20(1) -> 2*
20(3) -> 2*
30(2) -> 3*
30(4) -> 3*
30(1) -> 3*
30(3) -> 3*
40(2) -> 6*
40(4) -> 6*
40(1) -> 6*
40(3) -> 6*
50(2) -> 4*
50(4) -> 4*
50(1) -> 4*
50(3) -> 4*
1 -> 213,151,121,79,27
2 -> 197,143,113,67,14
3 -> 219,153,123,81,29
4 -> 211,145,115,73,21
14 -> 245*
15 -> 133,37
17 -> 185,47
20 -> 220,212,222,214,198,200,57,6
21 -> 251*
22 -> 15*
27 -> 232*
28 -> 15*
29 -> 243*
30 -> 15*
37 -> 253*
38 -> 221,171,169
39 -> 49*
40 -> 159,55,41,19
42 -> 19*
48 -> 195,39
50 -> 39*
56 -> 19*
58 -> 220,222,214,198,200,6
68 -> 105,91,88
69 -> 130*
72 -> 57*
74 -> 68*
80 -> 68*
82 -> 68*
90 -> 70*
92 -> 107*
95 -> 183*
96 -> 220,198,6
106 -> 16*
108 -> 17*
114 -> 16*
116 -> 16*
122 -> 16*
124 -> 16*
132 -> 94*
135 -> 161*
136 -> 94*
144 -> 15*
146 -> 15*
152 -> 15*
154 -> 15*
160 -> 19*
163 -> 19*
169 -> 257*
170 -> 38*
175 -> 212,198,6
184 -> 212,198,6
188 -> 183*
196 -> 183*
202 -> 183*
212 -> 198*
214 -> 198*
220 -> 198*
222 -> 200*
238 -> 222,200
244 -> 233*
246 -> 233*
252 -> 233*
254 -> 233*
258 -> 233*
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(1(x1)))) -> 0(0(2(1(3(1(x1))))))
, 0(1(0(1(x1)))) -> 2(1(0(2(0(1(x1))))))
, 0(1(0(1(x1)))) -> 2(1(3(1(0(0(x1))))))
, 4(1(0(1(x1)))) -> 1(0(4(2(1(x1)))))
, 4(1(0(1(x1)))) -> 4(1(0(2(1(x1)))))
, 4(1(0(1(x1)))) -> 0(2(1(3(4(1(x1))))))
, 4(1(0(1(x1)))) -> 0(4(2(1(3(1(x1))))))
, 4(1(0(1(x1)))) -> 1(0(2(4(1(3(x1))))))
, 4(1(0(1(x1)))) -> 1(0(4(2(2(1(x1))))))
, 4(1(0(1(x1)))) -> 1(0(4(5(2(1(x1))))))
, 4(1(0(1(x1)))) -> 4(0(2(1(3(1(x1))))))
, 4(1(0(1(x1)))) -> 4(1(0(2(1(3(x1))))))
, 4(1(0(1(x1)))) -> 4(1(3(0(2(1(x1))))))
, 4(1(1(1(x1)))) -> 4(1(3(1(3(1(x1))))))
, 4(3(0(1(x1)))) -> 0(2(1(3(4(x1)))))
, 4(3(0(1(x1)))) -> 0(2(4(1(3(x1)))))
, 4(3(0(1(x1)))) -> 0(4(2(1(3(x1)))))
, 4(3(0(1(x1)))) -> 3(0(4(2(1(x1)))))
, 4(3(0(1(x1)))) -> 3(4(0(2(1(x1)))))
, 4(3(0(1(x1)))) -> 4(0(2(1(3(x1)))))
, 4(3(0(1(x1)))) -> 4(3(0(2(1(x1)))))
, 4(3(0(1(x1)))) -> 0(2(1(3(3(4(x1))))))
, 4(3(0(1(x1)))) -> 0(2(1(3(4(3(x1))))))
, 4(3(0(1(x1)))) -> 0(2(4(1(3(3(x1))))))
, 4(3(0(1(x1)))) -> 0(4(2(2(1(3(x1))))))
, 4(3(0(1(x1)))) -> 0(4(5(2(1(3(x1))))))
, 4(3(0(1(x1)))) -> 1(0(2(1(3(4(x1))))))
, 4(3(0(1(x1)))) -> 1(0(2(4(1(3(x1))))))
, 4(3(0(1(x1)))) -> 1(0(4(2(1(3(x1))))))
, 4(3(0(1(x1)))) -> 1(3(0(4(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(0(4(5(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(1(0(4(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(3(4(0(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(4(0(2(1(3(x1))))))
, 4(3(0(1(x1)))) -> 3(4(0(2(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(4(0(5(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(4(1(0(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(4(3(0(2(1(x1))))))
, 4(3(0(1(x1)))) -> 4(3(0(2(1(3(x1))))))
, 4(3(0(1(x1)))) -> 4(3(0(5(2(1(x1))))))
, 4(3(0(1(x1)))) -> 4(3(1(0(2(1(x1))))))
, 4(3(0(1(x1)))) -> 4(3(3(0(2(1(x1))))))
, 4(5(1(1(x1)))) -> 4(5(2(1(1(x1)))))
, 4(5(1(1(x1)))) -> 4(2(5(2(1(1(x1))))))
, 4(5(1(1(x1)))) -> 4(5(2(1(3(1(x1))))))
, 4(5(1(1(x1)))) -> 4(5(2(2(1(1(x1))))))
, 4(5(1(1(x1)))) -> 4(5(5(2(1(1(x1))))))
, 0(0(1(0(1(x1))))) -> 0(0(1(0(2(1(x1))))))
, 0(0(3(1(1(x1))))) -> 2(1(3(1(0(0(x1))))))
, 0(0(5(1(1(x1))))) -> 5(0(0(2(1(1(x1))))))
, 0(4(1(0(1(x1))))) -> 2(1(0(4(0(1(x1))))))
, 0(4(3(0(1(x1))))) -> 0(0(2(1(3(4(x1))))))
, 0(4(3(0(1(x1))))) -> 0(4(3(0(2(1(x1))))))
, 0(4(3(0(1(x1))))) -> 2(3(1(0(4(0(x1))))))
, 0(4(3(1(1(x1))))) -> 2(1(4(1(3(0(x1))))))
, 0(4(3(1(1(x1))))) -> 4(2(0(3(1(1(x1))))))
, 0(4(5(1(1(x1))))) -> 4(0(1(5(2(1(x1))))))
, 0(4(5(1(1(x1))))) -> 5(2(1(4(0(1(x1))))))
, 4(0(3(0(1(x1))))) -> 0(0(4(2(1(3(x1))))))
, 4(0(3(0(1(x1))))) -> 2(0(4(0(1(3(x1))))))
, 4(0(3(0(1(x1))))) -> 2(0(4(0(3(1(x1))))))
, 4(1(0(1(1(x1))))) -> 1(0(4(2(1(1(x1))))))
, 4(1(1(0(1(x1))))) -> 4(1(0(2(1(1(x1))))))
, 4(1(2(0(1(x1))))) -> 0(4(2(1(3(1(x1))))))
, 4(1(2(0(1(x1))))) -> 1(0(2(4(1(3(x1))))))
, 4(1(2(0(1(x1))))) -> 4(0(2(2(1(1(x1))))))
, 4(1(2(0(1(x1))))) -> 4(1(0(2(2(1(x1))))))
, 4(1(3(0(1(x1))))) -> 4(1(3(0(2(1(x1))))))
, 4(1(5(0(1(x1))))) -> 1(1(5(0(4(2(x1))))))
, 4(1(5(1(1(x1))))) -> 1(4(5(2(1(1(x1))))))
, 4(3(0(1(1(x1))))) -> 1(3(0(2(1(4(x1))))))
, 4(3(0(1(1(x1))))) -> 1(3(1(4(0(2(x1))))))
, 4(3(0(1(1(x1))))) -> 1(3(1(4(2(0(x1))))))
, 4(3(0(1(1(x1))))) -> 3(1(0(2(4(1(x1))))))
, 4(3(0(1(1(x1))))) -> 4(3(1(1(0(2(x1))))))
, 4(3(1(0(1(x1))))) -> 0(4(2(1(3(1(x1))))))
, 4(3(1(0(1(x1))))) -> 1(3(4(0(2(1(x1))))))
, 4(3(2(0(1(x1))))) -> 3(4(0(2(2(1(x1))))))
, 4(3(2(0(1(x1))))) -> 3(4(0(5(2(1(x1))))))
, 4(3(2(0(1(x1))))) -> 4(0(2(1(3(1(x1))))))
, 4(3(2(0(1(x1))))) -> 4(3(0(2(1(3(x1))))))
, 4(3(2(1(1(x1))))) -> 1(3(1(2(4(2(x1))))))
, 4(3(2(1(1(x1))))) -> 1(3(1(4(5(2(x1))))))
, 4(3(2(1(1(x1))))) -> 3(1(3(4(1(2(x1))))))
, 4(3(2(1(1(x1))))) -> 4(1(3(1(2(2(x1))))))
, 4(3(2(1(1(x1))))) -> 4(1(3(3(1(2(x1))))))
, 4(3(3(0(1(x1))))) -> 4(3(3(0(2(1(x1))))))
, 4(3(4(0(1(x1))))) -> 3(4(0(4(2(1(x1))))))
, 4(3(4(0(1(x1))))) -> 4(4(0(2(1(3(x1))))))
, 4(3(5(0(1(x1))))) -> 0(5(2(3(1(4(x1))))))
, 4(3(5(0(1(x1))))) -> 1(3(0(2(5(4(x1))))))
, 4(3(5(0(1(x1))))) -> 1(3(0(4(2(5(x1))))))
, 4(3(5(0(1(x1))))) -> 1(3(4(0(5(2(x1))))))
, 4(3(5(0(1(x1))))) -> 3(1(0(4(2(5(x1))))))
, 4(3(5(0(1(x1))))) -> 3(1(5(0(4(2(x1))))))
, 4(3(5(0(1(x1))))) -> 3(4(0(2(1(5(x1))))))
, 4(3(5(0(1(x1))))) -> 3(4(1(5(0(2(x1))))))
, 4(3(5(0(1(x1))))) -> 3(5(1(0(4(2(x1))))))
, 4(3(5(0(1(x1))))) -> 4(3(0(2(1(5(x1))))))
, 4(3(5(0(1(x1))))) -> 5(1(3(4(0(2(x1))))))
, 4(3(5(1(1(x1))))) -> 1(4(5(2(1(3(x1))))))
, 4(3(5(1(1(x1))))) -> 3(1(1(5(4(2(x1))))))
, 4(3(5(1(1(x1))))) -> 3(1(4(5(2(1(x1))))))
, 4(3(5(1(1(x1))))) -> 4(1(3(1(3(5(x1))))))
, 4(3(5(1(1(x1))))) -> 4(1(5(2(1(3(x1))))))
, 4(3(5(1(1(x1))))) -> 4(3(1(5(2(1(x1))))))
, 4(4(1(0(1(x1))))) -> 4(4(1(0(2(1(x1))))))
, 4(4(3(0(1(x1))))) -> 0(4(4(2(1(3(x1))))))
, 4(4(3(0(1(x1))))) -> 4(0(2(1(3(4(x1))))))
, 4(4(3(0(1(x1))))) -> 4(3(4(0(2(1(x1))))))
, 4(4(3(0(1(x1))))) -> 4(4(3(0(2(1(x1))))))
, 4(5(1(0(1(x1))))) -> 0(5(1(3(4(1(x1))))))
, 4(5(1(0(1(x1))))) -> 0(5(4(1(3(1(x1))))))
, 4(5(1(0(1(x1))))) -> 1(0(4(5(2(1(x1))))))
, 4(5(1(0(1(x1))))) -> 4(0(5(2(1(1(x1))))))
, 4(5(1(0(1(x1))))) -> 4(5(1(0(2(1(x1))))))
, 4(5(1(0(1(x1))))) -> 5(1(0(2(4(1(x1))))))
, 4(5(1(0(1(x1))))) -> 5(4(1(0(2(1(x1))))))
, 4(5(1(1(1(x1))))) -> 4(5(2(1(1(1(x1))))))
, 4(5(3(0(1(x1))))) -> 0(2(1(3(4(5(x1))))))
, 4(5(3(0(1(x1))))) -> 0(5(2(1(3(4(x1))))))
, 4(5(3(0(1(x1))))) -> 0(5(2(4(3(1(x1))))))
, 4(5(3(0(1(x1))))) -> 0(5(4(2(1(3(x1))))))
, 4(5(3(0(1(x1))))) -> 1(0(5(1(3(4(x1))))))
, 4(5(3(0(1(x1))))) -> 1(5(0(3(3(4(x1))))))
, 4(5(3(0(1(x1))))) -> 2(1(4(5(0(3(x1))))))
, 4(5(3(0(1(x1))))) -> 2(4(1(3(5(0(x1))))))
, 4(5(3(0(1(x1))))) -> 3(0(4(5(2(1(x1))))))
, 4(5(3(0(1(x1))))) -> 4(0(3(1(5(2(x1))))))
, 4(5(3(0(1(x1))))) -> 4(0(3(3(5(1(x1))))))
, 4(5(3(0(1(x1))))) -> 4(0(5(4(1(3(x1))))))
, 4(5(3(0(1(x1))))) -> 4(1(3(5(0(3(x1))))))
, 4(5(3(0(1(x1))))) -> 4(1(3(5(5(0(x1))))))
, 4(5(3(0(1(x1))))) -> 4(2(5(0(3(1(x1))))))
, 4(5(3(0(1(x1))))) -> 4(5(2(0(3(1(x1))))))
, 4(5(3(0(1(x1))))) -> 5(0(3(1(4(1(x1))))))
, 4(5(3(0(1(x1))))) -> 5(0(3(4(4(1(x1))))))
, 4(5(3(0(1(x1))))) -> 5(1(3(0(3(4(x1))))))
, 4(5(3(0(1(x1))))) -> 5(2(1(3(4(0(x1))))))
, 4(5(3(0(1(x1))))) -> 5(2(4(1(3(0(x1))))))
, 4(5(3(0(1(x1))))) -> 5(3(0(4(2(1(x1))))))
, 4(5(3(0(1(x1))))) -> 5(4(1(3(0(1(x1))))))
, 4(5(3(0(1(x1))))) -> 5(4(1(3(2(0(x1))))))
, 4(5(3(0(1(x1))))) -> 5(4(3(0(2(1(x1))))))
, 4(5(3(1(1(x1))))) -> 2(4(1(3(1(5(x1))))))
, 4(5(3(1(1(x1))))) -> 4(5(2(1(3(1(x1))))))
, 4(5(3(1(1(x1))))) -> 5(1(3(4(1(2(x1))))))
, 4(5(3(1(1(x1))))) -> 5(2(1(4(1(3(x1))))))
, 4(5(3(1(1(x1))))) -> 5(4(2(1(3(1(x1))))))
, 4(5(5(1(1(x1))))) -> 5(5(2(1(1(4(x1))))))
, 4(5(5(1(1(x1))))) -> 5(5(2(4(1(1(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(0(1(x1)))) -> 0(0(2(1(3(1(x1))))))
, 0(1(0(1(x1)))) -> 2(1(0(2(0(1(x1))))))
, 0(1(0(1(x1)))) -> 2(1(3(1(0(0(x1))))))
, 4(1(0(1(x1)))) -> 1(0(4(2(1(x1)))))
, 4(1(0(1(x1)))) -> 4(1(0(2(1(x1)))))
, 4(1(0(1(x1)))) -> 0(2(1(3(4(1(x1))))))
, 4(1(0(1(x1)))) -> 0(4(2(1(3(1(x1))))))
, 4(1(0(1(x1)))) -> 1(0(2(4(1(3(x1))))))
, 4(1(0(1(x1)))) -> 1(0(4(2(2(1(x1))))))
, 4(1(0(1(x1)))) -> 1(0(4(5(2(1(x1))))))
, 4(1(0(1(x1)))) -> 4(0(2(1(3(1(x1))))))
, 4(1(0(1(x1)))) -> 4(1(0(2(1(3(x1))))))
, 4(1(0(1(x1)))) -> 4(1(3(0(2(1(x1))))))
, 4(1(1(1(x1)))) -> 4(1(3(1(3(1(x1))))))
, 4(3(0(1(x1)))) -> 0(2(1(3(4(x1)))))
, 4(3(0(1(x1)))) -> 0(2(4(1(3(x1)))))
, 4(3(0(1(x1)))) -> 0(4(2(1(3(x1)))))
, 4(3(0(1(x1)))) -> 3(0(4(2(1(x1)))))
, 4(3(0(1(x1)))) -> 3(4(0(2(1(x1)))))
, 4(3(0(1(x1)))) -> 4(0(2(1(3(x1)))))
, 4(3(0(1(x1)))) -> 4(3(0(2(1(x1)))))
, 4(3(0(1(x1)))) -> 0(2(1(3(3(4(x1))))))
, 4(3(0(1(x1)))) -> 0(2(1(3(4(3(x1))))))
, 4(3(0(1(x1)))) -> 0(2(4(1(3(3(x1))))))
, 4(3(0(1(x1)))) -> 0(4(2(2(1(3(x1))))))
, 4(3(0(1(x1)))) -> 0(4(5(2(1(3(x1))))))
, 4(3(0(1(x1)))) -> 1(0(2(1(3(4(x1))))))
, 4(3(0(1(x1)))) -> 1(0(2(4(1(3(x1))))))
, 4(3(0(1(x1)))) -> 1(0(4(2(1(3(x1))))))
, 4(3(0(1(x1)))) -> 1(3(0(4(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(0(4(5(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(1(0(4(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(3(4(0(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(4(0(2(1(3(x1))))))
, 4(3(0(1(x1)))) -> 3(4(0(2(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(4(0(5(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(4(1(0(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(4(3(0(2(1(x1))))))
, 4(3(0(1(x1)))) -> 4(3(0(2(1(3(x1))))))
, 4(3(0(1(x1)))) -> 4(3(0(5(2(1(x1))))))
, 4(3(0(1(x1)))) -> 4(3(1(0(2(1(x1))))))
, 4(3(0(1(x1)))) -> 4(3(3(0(2(1(x1))))))
, 4(5(1(1(x1)))) -> 4(5(2(1(1(x1)))))
, 4(5(1(1(x1)))) -> 4(2(5(2(1(1(x1))))))
, 4(5(1(1(x1)))) -> 4(5(2(1(3(1(x1))))))
, 4(5(1(1(x1)))) -> 4(5(2(2(1(1(x1))))))
, 4(5(1(1(x1)))) -> 4(5(5(2(1(1(x1))))))
, 0(0(1(0(1(x1))))) -> 0(0(1(0(2(1(x1))))))
, 0(0(3(1(1(x1))))) -> 2(1(3(1(0(0(x1))))))
, 0(0(5(1(1(x1))))) -> 5(0(0(2(1(1(x1))))))
, 0(4(1(0(1(x1))))) -> 2(1(0(4(0(1(x1))))))
, 0(4(3(0(1(x1))))) -> 0(0(2(1(3(4(x1))))))
, 0(4(3(0(1(x1))))) -> 0(4(3(0(2(1(x1))))))
, 0(4(3(0(1(x1))))) -> 2(3(1(0(4(0(x1))))))
, 0(4(3(1(1(x1))))) -> 2(1(4(1(3(0(x1))))))
, 0(4(3(1(1(x1))))) -> 4(2(0(3(1(1(x1))))))
, 0(4(5(1(1(x1))))) -> 4(0(1(5(2(1(x1))))))
, 0(4(5(1(1(x1))))) -> 5(2(1(4(0(1(x1))))))
, 4(0(3(0(1(x1))))) -> 0(0(4(2(1(3(x1))))))
, 4(0(3(0(1(x1))))) -> 2(0(4(0(1(3(x1))))))
, 4(0(3(0(1(x1))))) -> 2(0(4(0(3(1(x1))))))
, 4(1(0(1(1(x1))))) -> 1(0(4(2(1(1(x1))))))
, 4(1(1(0(1(x1))))) -> 4(1(0(2(1(1(x1))))))
, 4(1(2(0(1(x1))))) -> 0(4(2(1(3(1(x1))))))
, 4(1(2(0(1(x1))))) -> 1(0(2(4(1(3(x1))))))
, 4(1(2(0(1(x1))))) -> 4(0(2(2(1(1(x1))))))
, 4(1(2(0(1(x1))))) -> 4(1(0(2(2(1(x1))))))
, 4(1(3(0(1(x1))))) -> 4(1(3(0(2(1(x1))))))
, 4(1(5(0(1(x1))))) -> 1(1(5(0(4(2(x1))))))
, 4(1(5(1(1(x1))))) -> 1(4(5(2(1(1(x1))))))
, 4(3(0(1(1(x1))))) -> 1(3(0(2(1(4(x1))))))
, 4(3(0(1(1(x1))))) -> 1(3(1(4(0(2(x1))))))
, 4(3(0(1(1(x1))))) -> 1(3(1(4(2(0(x1))))))
, 4(3(0(1(1(x1))))) -> 3(1(0(2(4(1(x1))))))
, 4(3(0(1(1(x1))))) -> 4(3(1(1(0(2(x1))))))
, 4(3(1(0(1(x1))))) -> 0(4(2(1(3(1(x1))))))
, 4(3(1(0(1(x1))))) -> 1(3(4(0(2(1(x1))))))
, 4(3(2(0(1(x1))))) -> 3(4(0(2(2(1(x1))))))
, 4(3(2(0(1(x1))))) -> 3(4(0(5(2(1(x1))))))
, 4(3(2(0(1(x1))))) -> 4(0(2(1(3(1(x1))))))
, 4(3(2(0(1(x1))))) -> 4(3(0(2(1(3(x1))))))
, 4(3(2(1(1(x1))))) -> 1(3(1(2(4(2(x1))))))
, 4(3(2(1(1(x1))))) -> 1(3(1(4(5(2(x1))))))
, 4(3(2(1(1(x1))))) -> 3(1(3(4(1(2(x1))))))
, 4(3(2(1(1(x1))))) -> 4(1(3(1(2(2(x1))))))
, 4(3(2(1(1(x1))))) -> 4(1(3(3(1(2(x1))))))
, 4(3(3(0(1(x1))))) -> 4(3(3(0(2(1(x1))))))
, 4(3(4(0(1(x1))))) -> 3(4(0(4(2(1(x1))))))
, 4(3(4(0(1(x1))))) -> 4(4(0(2(1(3(x1))))))
, 4(3(5(0(1(x1))))) -> 0(5(2(3(1(4(x1))))))
, 4(3(5(0(1(x1))))) -> 1(3(0(2(5(4(x1))))))
, 4(3(5(0(1(x1))))) -> 1(3(0(4(2(5(x1))))))
, 4(3(5(0(1(x1))))) -> 1(3(4(0(5(2(x1))))))
, 4(3(5(0(1(x1))))) -> 3(1(0(4(2(5(x1))))))
, 4(3(5(0(1(x1))))) -> 3(1(5(0(4(2(x1))))))
, 4(3(5(0(1(x1))))) -> 3(4(0(2(1(5(x1))))))
, 4(3(5(0(1(x1))))) -> 3(4(1(5(0(2(x1))))))
, 4(3(5(0(1(x1))))) -> 3(5(1(0(4(2(x1))))))
, 4(3(5(0(1(x1))))) -> 4(3(0(2(1(5(x1))))))
, 4(3(5(0(1(x1))))) -> 5(1(3(4(0(2(x1))))))
, 4(3(5(1(1(x1))))) -> 1(4(5(2(1(3(x1))))))
, 4(3(5(1(1(x1))))) -> 3(1(1(5(4(2(x1))))))
, 4(3(5(1(1(x1))))) -> 3(1(4(5(2(1(x1))))))
, 4(3(5(1(1(x1))))) -> 4(1(3(1(3(5(x1))))))
, 4(3(5(1(1(x1))))) -> 4(1(5(2(1(3(x1))))))
, 4(3(5(1(1(x1))))) -> 4(3(1(5(2(1(x1))))))
, 4(4(1(0(1(x1))))) -> 4(4(1(0(2(1(x1))))))
, 4(4(3(0(1(x1))))) -> 0(4(4(2(1(3(x1))))))
, 4(4(3(0(1(x1))))) -> 4(0(2(1(3(4(x1))))))
, 4(4(3(0(1(x1))))) -> 4(3(4(0(2(1(x1))))))
, 4(4(3(0(1(x1))))) -> 4(4(3(0(2(1(x1))))))
, 4(5(1(0(1(x1))))) -> 0(5(1(3(4(1(x1))))))
, 4(5(1(0(1(x1))))) -> 0(5(4(1(3(1(x1))))))
, 4(5(1(0(1(x1))))) -> 1(0(4(5(2(1(x1))))))
, 4(5(1(0(1(x1))))) -> 4(0(5(2(1(1(x1))))))
, 4(5(1(0(1(x1))))) -> 4(5(1(0(2(1(x1))))))
, 4(5(1(0(1(x1))))) -> 5(1(0(2(4(1(x1))))))
, 4(5(1(0(1(x1))))) -> 5(4(1(0(2(1(x1))))))
, 4(5(1(1(1(x1))))) -> 4(5(2(1(1(1(x1))))))
, 4(5(3(0(1(x1))))) -> 0(2(1(3(4(5(x1))))))
, 4(5(3(0(1(x1))))) -> 0(5(2(1(3(4(x1))))))
, 4(5(3(0(1(x1))))) -> 0(5(2(4(3(1(x1))))))
, 4(5(3(0(1(x1))))) -> 0(5(4(2(1(3(x1))))))
, 4(5(3(0(1(x1))))) -> 1(0(5(1(3(4(x1))))))
, 4(5(3(0(1(x1))))) -> 1(5(0(3(3(4(x1))))))
, 4(5(3(0(1(x1))))) -> 2(1(4(5(0(3(x1))))))
, 4(5(3(0(1(x1))))) -> 2(4(1(3(5(0(x1))))))
, 4(5(3(0(1(x1))))) -> 3(0(4(5(2(1(x1))))))
, 4(5(3(0(1(x1))))) -> 4(0(3(1(5(2(x1))))))
, 4(5(3(0(1(x1))))) -> 4(0(3(3(5(1(x1))))))
, 4(5(3(0(1(x1))))) -> 4(0(5(4(1(3(x1))))))
, 4(5(3(0(1(x1))))) -> 4(1(3(5(0(3(x1))))))
, 4(5(3(0(1(x1))))) -> 4(1(3(5(5(0(x1))))))
, 4(5(3(0(1(x1))))) -> 4(2(5(0(3(1(x1))))))
, 4(5(3(0(1(x1))))) -> 4(5(2(0(3(1(x1))))))
, 4(5(3(0(1(x1))))) -> 5(0(3(1(4(1(x1))))))
, 4(5(3(0(1(x1))))) -> 5(0(3(4(4(1(x1))))))
, 4(5(3(0(1(x1))))) -> 5(1(3(0(3(4(x1))))))
, 4(5(3(0(1(x1))))) -> 5(2(1(3(4(0(x1))))))
, 4(5(3(0(1(x1))))) -> 5(2(4(1(3(0(x1))))))
, 4(5(3(0(1(x1))))) -> 5(3(0(4(2(1(x1))))))
, 4(5(3(0(1(x1))))) -> 5(4(1(3(0(1(x1))))))
, 4(5(3(0(1(x1))))) -> 5(4(1(3(2(0(x1))))))
, 4(5(3(0(1(x1))))) -> 5(4(3(0(2(1(x1))))))
, 4(5(3(1(1(x1))))) -> 2(4(1(3(1(5(x1))))))
, 4(5(3(1(1(x1))))) -> 4(5(2(1(3(1(x1))))))
, 4(5(3(1(1(x1))))) -> 5(1(3(4(1(2(x1))))))
, 4(5(3(1(1(x1))))) -> 5(2(1(4(1(3(x1))))))
, 4(5(3(1(1(x1))))) -> 5(4(2(1(3(1(x1))))))
, 4(5(5(1(1(x1))))) -> 5(5(2(1(1(4(x1))))))
, 4(5(5(1(1(x1))))) -> 5(5(2(4(1(1(x1))))))}
Proof Output:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ 0_0(2) -> 1
, 1_0(2) -> 2
, 1_1(1) -> 1
, 1_1(1) -> 33
, 1_1(1) -> 38
, 1_1(2) -> 7
, 1_1(3) -> 3
, 1_1(4) -> 3
, 1_1(6) -> 5
, 1_1(7) -> 9
, 1_1(9) -> 3
, 1_1(11) -> 10
, 1_1(13) -> 16
, 1_1(14) -> 21
, 1_1(18) -> 11
, 1_1(29) -> 28
, 1_1(32) -> 31
, 1_1(33) -> 32
, 1_1(38) -> 31
, 1_1(38) -> 33
, 1_1(38) -> 38
, 1_2(2) -> 42
, 1_2(3) -> 26
, 1_2(4) -> 26
, 1_2(7) -> 26
, 1_2(9) -> 26
, 1_2(25) -> 24
, 1_2(26) -> 25
, 1_2(37) -> 36
, 1_2(38) -> 1
, 1_2(38) -> 31
, 1_2(38) -> 33
, 1_2(38) -> 36
, 1_2(38) -> 37
, 1_2(38) -> 38
, 1_2(39) -> 22
, 1_2(41) -> 40
, 1_2(42) -> 25
, 2_0(2) -> 2
, 2_1(1) -> 10
, 2_1(2) -> 13
, 2_1(3) -> 3
, 2_1(5) -> 8
, 2_1(7) -> 13
, 2_1(8) -> 8
, 2_1(9) -> 8
, 2_1(12) -> 11
, 2_1(13) -> 6
, 2_1(27) -> 1
, 2_1(27) -> 33
, 2_1(27) -> 38
, 2_1(31) -> 30
, 2_2(22) -> 22
, 2_2(23) -> 23
, 2_2(24) -> 23
, 2_2(25) -> 23
, 2_2(36) -> 35
, 2_2(40) -> 23
, 3_0(2) -> 2
, 3_1(2) -> 4
, 3_1(5) -> 4
, 3_1(7) -> 6
, 3_1(9) -> 29
, 3_1(10) -> 1
, 3_1(10) -> 33
, 3_1(10) -> 38
, 3_1(15) -> 11
, 3_1(16) -> 5
, 3_1(21) -> 3
, 3_2(26) -> 41
, 3_2(40) -> 39
, 3_2(42) -> 41
, 4_0(2) -> 1
, 4_1(2) -> 33
, 4_1(3) -> 1
, 4_1(3) -> 31
, 4_1(3) -> 33
, 4_1(3) -> 36
, 4_1(3) -> 38
, 4_1(8) -> 10
, 4_1(9) -> 31
, 4_1(13) -> 12
, 4_1(14) -> 11
, 4_1(16) -> 15
, 4_1(28) -> 27
, 4_2(3) -> 38
, 4_2(4) -> 38
, 4_2(7) -> 38
, 4_2(9) -> 38
, 4_2(22) -> 1
, 4_2(22) -> 31
, 4_2(22) -> 33
, 4_2(22) -> 36
, 4_2(22) -> 38
, 4_2(25) -> 36
, 5_0(2) -> 2
, 5_1(2) -> 7
, 5_1(3) -> 3
, 5_1(8) -> 3
, 5_1(10) -> 1
, 5_1(10) -> 33
, 5_1(10) -> 38
, 5_1(12) -> 18
, 5_1(13) -> 14
, 5_1(30) -> 10
, 5_2(22) -> 22
, 5_2(23) -> 22
, 5_2(34) -> 1
, 5_2(34) -> 31
, 5_2(34) -> 33
, 5_2(34) -> 36
, 5_2(34) -> 38
, 5_2(35) -> 34}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(1(x1)))) -> 0(0(2(1(3(1(x1))))))
, 0(1(0(1(x1)))) -> 2(1(0(2(0(1(x1))))))
, 0(1(0(1(x1)))) -> 2(1(3(1(0(0(x1))))))
, 4(1(0(1(x1)))) -> 1(0(4(2(1(x1)))))
, 4(1(0(1(x1)))) -> 4(1(0(2(1(x1)))))
, 4(1(0(1(x1)))) -> 0(2(1(3(4(1(x1))))))
, 4(1(0(1(x1)))) -> 0(4(2(1(3(1(x1))))))
, 4(1(0(1(x1)))) -> 1(0(2(4(1(3(x1))))))
, 4(1(0(1(x1)))) -> 1(0(4(2(2(1(x1))))))
, 4(1(0(1(x1)))) -> 1(0(4(5(2(1(x1))))))
, 4(1(0(1(x1)))) -> 4(0(2(1(3(1(x1))))))
, 4(1(0(1(x1)))) -> 4(1(0(2(1(3(x1))))))
, 4(1(0(1(x1)))) -> 4(1(3(0(2(1(x1))))))
, 4(1(1(1(x1)))) -> 4(1(3(1(3(1(x1))))))
, 4(3(0(1(x1)))) -> 0(2(1(3(4(x1)))))
, 4(3(0(1(x1)))) -> 0(2(4(1(3(x1)))))
, 4(3(0(1(x1)))) -> 0(4(2(1(3(x1)))))
, 4(3(0(1(x1)))) -> 3(0(4(2(1(x1)))))
, 4(3(0(1(x1)))) -> 3(4(0(2(1(x1)))))
, 4(3(0(1(x1)))) -> 4(0(2(1(3(x1)))))
, 4(3(0(1(x1)))) -> 4(3(0(2(1(x1)))))
, 4(3(0(1(x1)))) -> 0(2(1(3(3(4(x1))))))
, 4(3(0(1(x1)))) -> 0(2(1(3(4(3(x1))))))
, 4(3(0(1(x1)))) -> 0(2(4(1(3(3(x1))))))
, 4(3(0(1(x1)))) -> 0(4(2(2(1(3(x1))))))
, 4(3(0(1(x1)))) -> 0(4(5(2(1(3(x1))))))
, 4(3(0(1(x1)))) -> 1(0(2(1(3(4(x1))))))
, 4(3(0(1(x1)))) -> 1(0(2(4(1(3(x1))))))
, 4(3(0(1(x1)))) -> 1(0(4(2(1(3(x1))))))
, 4(3(0(1(x1)))) -> 1(3(0(4(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(0(4(5(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(1(0(4(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(3(4(0(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(4(0(2(1(3(x1))))))
, 4(3(0(1(x1)))) -> 3(4(0(2(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(4(0(5(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(4(1(0(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(4(3(0(2(1(x1))))))
, 4(3(0(1(x1)))) -> 4(3(0(2(1(3(x1))))))
, 4(3(0(1(x1)))) -> 4(3(0(5(2(1(x1))))))
, 4(3(0(1(x1)))) -> 4(3(1(0(2(1(x1))))))
, 4(3(0(1(x1)))) -> 4(3(3(0(2(1(x1))))))
, 4(5(1(1(x1)))) -> 4(5(2(1(1(x1)))))
, 4(5(1(1(x1)))) -> 4(2(5(2(1(1(x1))))))
, 4(5(1(1(x1)))) -> 4(5(2(1(3(1(x1))))))
, 4(5(1(1(x1)))) -> 4(5(2(2(1(1(x1))))))
, 4(5(1(1(x1)))) -> 4(5(5(2(1(1(x1))))))
, 0(0(1(0(1(x1))))) -> 0(0(1(0(2(1(x1))))))
, 0(0(3(1(1(x1))))) -> 2(1(3(1(0(0(x1))))))
, 0(0(5(1(1(x1))))) -> 5(0(0(2(1(1(x1))))))
, 0(4(1(0(1(x1))))) -> 2(1(0(4(0(1(x1))))))
, 0(4(3(0(1(x1))))) -> 0(0(2(1(3(4(x1))))))
, 0(4(3(0(1(x1))))) -> 0(4(3(0(2(1(x1))))))
, 0(4(3(0(1(x1))))) -> 2(3(1(0(4(0(x1))))))
, 0(4(3(1(1(x1))))) -> 2(1(4(1(3(0(x1))))))
, 0(4(3(1(1(x1))))) -> 4(2(0(3(1(1(x1))))))
, 0(4(5(1(1(x1))))) -> 4(0(1(5(2(1(x1))))))
, 0(4(5(1(1(x1))))) -> 5(2(1(4(0(1(x1))))))
, 4(0(3(0(1(x1))))) -> 0(0(4(2(1(3(x1))))))
, 4(0(3(0(1(x1))))) -> 2(0(4(0(1(3(x1))))))
, 4(0(3(0(1(x1))))) -> 2(0(4(0(3(1(x1))))))
, 4(1(0(1(1(x1))))) -> 1(0(4(2(1(1(x1))))))
, 4(1(1(0(1(x1))))) -> 4(1(0(2(1(1(x1))))))
, 4(1(2(0(1(x1))))) -> 0(4(2(1(3(1(x1))))))
, 4(1(2(0(1(x1))))) -> 1(0(2(4(1(3(x1))))))
, 4(1(2(0(1(x1))))) -> 4(0(2(2(1(1(x1))))))
, 4(1(2(0(1(x1))))) -> 4(1(0(2(2(1(x1))))))
, 4(1(3(0(1(x1))))) -> 4(1(3(0(2(1(x1))))))
, 4(1(5(0(1(x1))))) -> 1(1(5(0(4(2(x1))))))
, 4(1(5(1(1(x1))))) -> 1(4(5(2(1(1(x1))))))
, 4(3(0(1(1(x1))))) -> 1(3(0(2(1(4(x1))))))
, 4(3(0(1(1(x1))))) -> 1(3(1(4(0(2(x1))))))
, 4(3(0(1(1(x1))))) -> 1(3(1(4(2(0(x1))))))
, 4(3(0(1(1(x1))))) -> 3(1(0(2(4(1(x1))))))
, 4(3(0(1(1(x1))))) -> 4(3(1(1(0(2(x1))))))
, 4(3(1(0(1(x1))))) -> 0(4(2(1(3(1(x1))))))
, 4(3(1(0(1(x1))))) -> 1(3(4(0(2(1(x1))))))
, 4(3(2(0(1(x1))))) -> 3(4(0(2(2(1(x1))))))
, 4(3(2(0(1(x1))))) -> 3(4(0(5(2(1(x1))))))
, 4(3(2(0(1(x1))))) -> 4(0(2(1(3(1(x1))))))
, 4(3(2(0(1(x1))))) -> 4(3(0(2(1(3(x1))))))
, 4(3(2(1(1(x1))))) -> 1(3(1(2(4(2(x1))))))
, 4(3(2(1(1(x1))))) -> 1(3(1(4(5(2(x1))))))
, 4(3(2(1(1(x1))))) -> 3(1(3(4(1(2(x1))))))
, 4(3(2(1(1(x1))))) -> 4(1(3(1(2(2(x1))))))
, 4(3(2(1(1(x1))))) -> 4(1(3(3(1(2(x1))))))
, 4(3(3(0(1(x1))))) -> 4(3(3(0(2(1(x1))))))
, 4(3(4(0(1(x1))))) -> 3(4(0(4(2(1(x1))))))
, 4(3(4(0(1(x1))))) -> 4(4(0(2(1(3(x1))))))
, 4(3(5(0(1(x1))))) -> 0(5(2(3(1(4(x1))))))
, 4(3(5(0(1(x1))))) -> 1(3(0(2(5(4(x1))))))
, 4(3(5(0(1(x1))))) -> 1(3(0(4(2(5(x1))))))
, 4(3(5(0(1(x1))))) -> 1(3(4(0(5(2(x1))))))
, 4(3(5(0(1(x1))))) -> 3(1(0(4(2(5(x1))))))
, 4(3(5(0(1(x1))))) -> 3(1(5(0(4(2(x1))))))
, 4(3(5(0(1(x1))))) -> 3(4(0(2(1(5(x1))))))
, 4(3(5(0(1(x1))))) -> 3(4(1(5(0(2(x1))))))
, 4(3(5(0(1(x1))))) -> 3(5(1(0(4(2(x1))))))
, 4(3(5(0(1(x1))))) -> 4(3(0(2(1(5(x1))))))
, 4(3(5(0(1(x1))))) -> 5(1(3(4(0(2(x1))))))
, 4(3(5(1(1(x1))))) -> 1(4(5(2(1(3(x1))))))
, 4(3(5(1(1(x1))))) -> 3(1(1(5(4(2(x1))))))
, 4(3(5(1(1(x1))))) -> 3(1(4(5(2(1(x1))))))
, 4(3(5(1(1(x1))))) -> 4(1(3(1(3(5(x1))))))
, 4(3(5(1(1(x1))))) -> 4(1(5(2(1(3(x1))))))
, 4(3(5(1(1(x1))))) -> 4(3(1(5(2(1(x1))))))
, 4(4(1(0(1(x1))))) -> 4(4(1(0(2(1(x1))))))
, 4(4(3(0(1(x1))))) -> 0(4(4(2(1(3(x1))))))
, 4(4(3(0(1(x1))))) -> 4(0(2(1(3(4(x1))))))
, 4(4(3(0(1(x1))))) -> 4(3(4(0(2(1(x1))))))
, 4(4(3(0(1(x1))))) -> 4(4(3(0(2(1(x1))))))
, 4(5(1(0(1(x1))))) -> 0(5(1(3(4(1(x1))))))
, 4(5(1(0(1(x1))))) -> 0(5(4(1(3(1(x1))))))
, 4(5(1(0(1(x1))))) -> 1(0(4(5(2(1(x1))))))
, 4(5(1(0(1(x1))))) -> 4(0(5(2(1(1(x1))))))
, 4(5(1(0(1(x1))))) -> 4(5(1(0(2(1(x1))))))
, 4(5(1(0(1(x1))))) -> 5(1(0(2(4(1(x1))))))
, 4(5(1(0(1(x1))))) -> 5(4(1(0(2(1(x1))))))
, 4(5(1(1(1(x1))))) -> 4(5(2(1(1(1(x1))))))
, 4(5(3(0(1(x1))))) -> 0(2(1(3(4(5(x1))))))
, 4(5(3(0(1(x1))))) -> 0(5(2(1(3(4(x1))))))
, 4(5(3(0(1(x1))))) -> 0(5(2(4(3(1(x1))))))
, 4(5(3(0(1(x1))))) -> 0(5(4(2(1(3(x1))))))
, 4(5(3(0(1(x1))))) -> 1(0(5(1(3(4(x1))))))
, 4(5(3(0(1(x1))))) -> 1(5(0(3(3(4(x1))))))
, 4(5(3(0(1(x1))))) -> 2(1(4(5(0(3(x1))))))
, 4(5(3(0(1(x1))))) -> 2(4(1(3(5(0(x1))))))
, 4(5(3(0(1(x1))))) -> 3(0(4(5(2(1(x1))))))
, 4(5(3(0(1(x1))))) -> 4(0(3(1(5(2(x1))))))
, 4(5(3(0(1(x1))))) -> 4(0(3(3(5(1(x1))))))
, 4(5(3(0(1(x1))))) -> 4(0(5(4(1(3(x1))))))
, 4(5(3(0(1(x1))))) -> 4(1(3(5(0(3(x1))))))
, 4(5(3(0(1(x1))))) -> 4(1(3(5(5(0(x1))))))
, 4(5(3(0(1(x1))))) -> 4(2(5(0(3(1(x1))))))
, 4(5(3(0(1(x1))))) -> 4(5(2(0(3(1(x1))))))
, 4(5(3(0(1(x1))))) -> 5(0(3(1(4(1(x1))))))
, 4(5(3(0(1(x1))))) -> 5(0(3(4(4(1(x1))))))
, 4(5(3(0(1(x1))))) -> 5(1(3(0(3(4(x1))))))
, 4(5(3(0(1(x1))))) -> 5(2(1(3(4(0(x1))))))
, 4(5(3(0(1(x1))))) -> 5(2(4(1(3(0(x1))))))
, 4(5(3(0(1(x1))))) -> 5(3(0(4(2(1(x1))))))
, 4(5(3(0(1(x1))))) -> 5(4(1(3(0(1(x1))))))
, 4(5(3(0(1(x1))))) -> 5(4(1(3(2(0(x1))))))
, 4(5(3(0(1(x1))))) -> 5(4(3(0(2(1(x1))))))
, 4(5(3(1(1(x1))))) -> 2(4(1(3(1(5(x1))))))
, 4(5(3(1(1(x1))))) -> 4(5(2(1(3(1(x1))))))
, 4(5(3(1(1(x1))))) -> 5(1(3(4(1(2(x1))))))
, 4(5(3(1(1(x1))))) -> 5(2(1(4(1(3(x1))))))
, 4(5(3(1(1(x1))))) -> 5(4(2(1(3(1(x1))))))
, 4(5(5(1(1(x1))))) -> 5(5(2(1(1(4(x1))))))
, 4(5(5(1(1(x1))))) -> 5(5(2(4(1(1(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(0(1(x1)))) -> 0(0(2(1(3(1(x1))))))
, 0(1(0(1(x1)))) -> 2(1(0(2(0(1(x1))))))
, 0(1(0(1(x1)))) -> 2(1(3(1(0(0(x1))))))
, 4(1(0(1(x1)))) -> 1(0(4(2(1(x1)))))
, 4(1(0(1(x1)))) -> 4(1(0(2(1(x1)))))
, 4(1(0(1(x1)))) -> 0(2(1(3(4(1(x1))))))
, 4(1(0(1(x1)))) -> 0(4(2(1(3(1(x1))))))
, 4(1(0(1(x1)))) -> 1(0(2(4(1(3(x1))))))
, 4(1(0(1(x1)))) -> 1(0(4(2(2(1(x1))))))
, 4(1(0(1(x1)))) -> 1(0(4(5(2(1(x1))))))
, 4(1(0(1(x1)))) -> 4(0(2(1(3(1(x1))))))
, 4(1(0(1(x1)))) -> 4(1(0(2(1(3(x1))))))
, 4(1(0(1(x1)))) -> 4(1(3(0(2(1(x1))))))
, 4(1(1(1(x1)))) -> 4(1(3(1(3(1(x1))))))
, 4(3(0(1(x1)))) -> 0(2(1(3(4(x1)))))
, 4(3(0(1(x1)))) -> 0(2(4(1(3(x1)))))
, 4(3(0(1(x1)))) -> 0(4(2(1(3(x1)))))
, 4(3(0(1(x1)))) -> 3(0(4(2(1(x1)))))
, 4(3(0(1(x1)))) -> 3(4(0(2(1(x1)))))
, 4(3(0(1(x1)))) -> 4(0(2(1(3(x1)))))
, 4(3(0(1(x1)))) -> 4(3(0(2(1(x1)))))
, 4(3(0(1(x1)))) -> 0(2(1(3(3(4(x1))))))
, 4(3(0(1(x1)))) -> 0(2(1(3(4(3(x1))))))
, 4(3(0(1(x1)))) -> 0(2(4(1(3(3(x1))))))
, 4(3(0(1(x1)))) -> 0(4(2(2(1(3(x1))))))
, 4(3(0(1(x1)))) -> 0(4(5(2(1(3(x1))))))
, 4(3(0(1(x1)))) -> 1(0(2(1(3(4(x1))))))
, 4(3(0(1(x1)))) -> 1(0(2(4(1(3(x1))))))
, 4(3(0(1(x1)))) -> 1(0(4(2(1(3(x1))))))
, 4(3(0(1(x1)))) -> 1(3(0(4(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(0(4(5(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(1(0(4(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(3(4(0(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(4(0(2(1(3(x1))))))
, 4(3(0(1(x1)))) -> 3(4(0(2(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(4(0(5(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(4(1(0(2(1(x1))))))
, 4(3(0(1(x1)))) -> 3(4(3(0(2(1(x1))))))
, 4(3(0(1(x1)))) -> 4(3(0(2(1(3(x1))))))
, 4(3(0(1(x1)))) -> 4(3(0(5(2(1(x1))))))
, 4(3(0(1(x1)))) -> 4(3(1(0(2(1(x1))))))
, 4(3(0(1(x1)))) -> 4(3(3(0(2(1(x1))))))
, 4(5(1(1(x1)))) -> 4(5(2(1(1(x1)))))
, 4(5(1(1(x1)))) -> 4(2(5(2(1(1(x1))))))
, 4(5(1(1(x1)))) -> 4(5(2(1(3(1(x1))))))
, 4(5(1(1(x1)))) -> 4(5(2(2(1(1(x1))))))
, 4(5(1(1(x1)))) -> 4(5(5(2(1(1(x1))))))
, 0(0(1(0(1(x1))))) -> 0(0(1(0(2(1(x1))))))
, 0(0(3(1(1(x1))))) -> 2(1(3(1(0(0(x1))))))
, 0(0(5(1(1(x1))))) -> 5(0(0(2(1(1(x1))))))
, 0(4(1(0(1(x1))))) -> 2(1(0(4(0(1(x1))))))
, 0(4(3(0(1(x1))))) -> 0(0(2(1(3(4(x1))))))
, 0(4(3(0(1(x1))))) -> 0(4(3(0(2(1(x1))))))
, 0(4(3(0(1(x1))))) -> 2(3(1(0(4(0(x1))))))
, 0(4(3(1(1(x1))))) -> 2(1(4(1(3(0(x1))))))
, 0(4(3(1(1(x1))))) -> 4(2(0(3(1(1(x1))))))
, 0(4(5(1(1(x1))))) -> 4(0(1(5(2(1(x1))))))
, 0(4(5(1(1(x1))))) -> 5(2(1(4(0(1(x1))))))
, 4(0(3(0(1(x1))))) -> 0(0(4(2(1(3(x1))))))
, 4(0(3(0(1(x1))))) -> 2(0(4(0(1(3(x1))))))
, 4(0(3(0(1(x1))))) -> 2(0(4(0(3(1(x1))))))
, 4(1(0(1(1(x1))))) -> 1(0(4(2(1(1(x1))))))
, 4(1(1(0(1(x1))))) -> 4(1(0(2(1(1(x1))))))
, 4(1(2(0(1(x1))))) -> 0(4(2(1(3(1(x1))))))
, 4(1(2(0(1(x1))))) -> 1(0(2(4(1(3(x1))))))
, 4(1(2(0(1(x1))))) -> 4(0(2(2(1(1(x1))))))
, 4(1(2(0(1(x1))))) -> 4(1(0(2(2(1(x1))))))
, 4(1(3(0(1(x1))))) -> 4(1(3(0(2(1(x1))))))
, 4(1(5(0(1(x1))))) -> 1(1(5(0(4(2(x1))))))
, 4(1(5(1(1(x1))))) -> 1(4(5(2(1(1(x1))))))
, 4(3(0(1(1(x1))))) -> 1(3(0(2(1(4(x1))))))
, 4(3(0(1(1(x1))))) -> 1(3(1(4(0(2(x1))))))
, 4(3(0(1(1(x1))))) -> 1(3(1(4(2(0(x1))))))
, 4(3(0(1(1(x1))))) -> 3(1(0(2(4(1(x1))))))
, 4(3(0(1(1(x1))))) -> 4(3(1(1(0(2(x1))))))
, 4(3(1(0(1(x1))))) -> 0(4(2(1(3(1(x1))))))
, 4(3(1(0(1(x1))))) -> 1(3(4(0(2(1(x1))))))
, 4(3(2(0(1(x1))))) -> 3(4(0(2(2(1(x1))))))
, 4(3(2(0(1(x1))))) -> 3(4(0(5(2(1(x1))))))
, 4(3(2(0(1(x1))))) -> 4(0(2(1(3(1(x1))))))
, 4(3(2(0(1(x1))))) -> 4(3(0(2(1(3(x1))))))
, 4(3(2(1(1(x1))))) -> 1(3(1(2(4(2(x1))))))
, 4(3(2(1(1(x1))))) -> 1(3(1(4(5(2(x1))))))
, 4(3(2(1(1(x1))))) -> 3(1(3(4(1(2(x1))))))
, 4(3(2(1(1(x1))))) -> 4(1(3(1(2(2(x1))))))
, 4(3(2(1(1(x1))))) -> 4(1(3(3(1(2(x1))))))
, 4(3(3(0(1(x1))))) -> 4(3(3(0(2(1(x1))))))
, 4(3(4(0(1(x1))))) -> 3(4(0(4(2(1(x1))))))
, 4(3(4(0(1(x1))))) -> 4(4(0(2(1(3(x1))))))
, 4(3(5(0(1(x1))))) -> 0(5(2(3(1(4(x1))))))
, 4(3(5(0(1(x1))))) -> 1(3(0(2(5(4(x1))))))
, 4(3(5(0(1(x1))))) -> 1(3(0(4(2(5(x1))))))
, 4(3(5(0(1(x1))))) -> 1(3(4(0(5(2(x1))))))
, 4(3(5(0(1(x1))))) -> 3(1(0(4(2(5(x1))))))
, 4(3(5(0(1(x1))))) -> 3(1(5(0(4(2(x1))))))
, 4(3(5(0(1(x1))))) -> 3(4(0(2(1(5(x1))))))
, 4(3(5(0(1(x1))))) -> 3(4(1(5(0(2(x1))))))
, 4(3(5(0(1(x1))))) -> 3(5(1(0(4(2(x1))))))
, 4(3(5(0(1(x1))))) -> 4(3(0(2(1(5(x1))))))
, 4(3(5(0(1(x1))))) -> 5(1(3(4(0(2(x1))))))
, 4(3(5(1(1(x1))))) -> 1(4(5(2(1(3(x1))))))
, 4(3(5(1(1(x1))))) -> 3(1(1(5(4(2(x1))))))
, 4(3(5(1(1(x1))))) -> 3(1(4(5(2(1(x1))))))
, 4(3(5(1(1(x1))))) -> 4(1(3(1(3(5(x1))))))
, 4(3(5(1(1(x1))))) -> 4(1(5(2(1(3(x1))))))
, 4(3(5(1(1(x1))))) -> 4(3(1(5(2(1(x1))))))
, 4(4(1(0(1(x1))))) -> 4(4(1(0(2(1(x1))))))
, 4(4(3(0(1(x1))))) -> 0(4(4(2(1(3(x1))))))
, 4(4(3(0(1(x1))))) -> 4(0(2(1(3(4(x1))))))
, 4(4(3(0(1(x1))))) -> 4(3(4(0(2(1(x1))))))
, 4(4(3(0(1(x1))))) -> 4(4(3(0(2(1(x1))))))
, 4(5(1(0(1(x1))))) -> 0(5(1(3(4(1(x1))))))
, 4(5(1(0(1(x1))))) -> 0(5(4(1(3(1(x1))))))
, 4(5(1(0(1(x1))))) -> 1(0(4(5(2(1(x1))))))
, 4(5(1(0(1(x1))))) -> 4(0(5(2(1(1(x1))))))
, 4(5(1(0(1(x1))))) -> 4(5(1(0(2(1(x1))))))
, 4(5(1(0(1(x1))))) -> 5(1(0(2(4(1(x1))))))
, 4(5(1(0(1(x1))))) -> 5(4(1(0(2(1(x1))))))
, 4(5(1(1(1(x1))))) -> 4(5(2(1(1(1(x1))))))
, 4(5(3(0(1(x1))))) -> 0(2(1(3(4(5(x1))))))
, 4(5(3(0(1(x1))))) -> 0(5(2(1(3(4(x1))))))
, 4(5(3(0(1(x1))))) -> 0(5(2(4(3(1(x1))))))
, 4(5(3(0(1(x1))))) -> 0(5(4(2(1(3(x1))))))
, 4(5(3(0(1(x1))))) -> 1(0(5(1(3(4(x1))))))
, 4(5(3(0(1(x1))))) -> 1(5(0(3(3(4(x1))))))
, 4(5(3(0(1(x1))))) -> 2(1(4(5(0(3(x1))))))
, 4(5(3(0(1(x1))))) -> 2(4(1(3(5(0(x1))))))
, 4(5(3(0(1(x1))))) -> 3(0(4(5(2(1(x1))))))
, 4(5(3(0(1(x1))))) -> 4(0(3(1(5(2(x1))))))
, 4(5(3(0(1(x1))))) -> 4(0(3(3(5(1(x1))))))
, 4(5(3(0(1(x1))))) -> 4(0(5(4(1(3(x1))))))
, 4(5(3(0(1(x1))))) -> 4(1(3(5(0(3(x1))))))
, 4(5(3(0(1(x1))))) -> 4(1(3(5(5(0(x1))))))
, 4(5(3(0(1(x1))))) -> 4(2(5(0(3(1(x1))))))
, 4(5(3(0(1(x1))))) -> 4(5(2(0(3(1(x1))))))
, 4(5(3(0(1(x1))))) -> 5(0(3(1(4(1(x1))))))
, 4(5(3(0(1(x1))))) -> 5(0(3(4(4(1(x1))))))
, 4(5(3(0(1(x1))))) -> 5(1(3(0(3(4(x1))))))
, 4(5(3(0(1(x1))))) -> 5(2(1(3(4(0(x1))))))
, 4(5(3(0(1(x1))))) -> 5(2(4(1(3(0(x1))))))
, 4(5(3(0(1(x1))))) -> 5(3(0(4(2(1(x1))))))
, 4(5(3(0(1(x1))))) -> 5(4(1(3(0(1(x1))))))
, 4(5(3(0(1(x1))))) -> 5(4(1(3(2(0(x1))))))
, 4(5(3(0(1(x1))))) -> 5(4(3(0(2(1(x1))))))
, 4(5(3(1(1(x1))))) -> 2(4(1(3(1(5(x1))))))
, 4(5(3(1(1(x1))))) -> 4(5(2(1(3(1(x1))))))
, 4(5(3(1(1(x1))))) -> 5(1(3(4(1(2(x1))))))
, 4(5(3(1(1(x1))))) -> 5(2(1(4(1(3(x1))))))
, 4(5(3(1(1(x1))))) -> 5(4(2(1(3(1(x1))))))
, 4(5(5(1(1(x1))))) -> 5(5(2(1(1(4(x1))))))
, 4(5(5(1(1(x1))))) -> 5(5(2(4(1(1(x1))))))}
Proof Output:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ 0_0(2) -> 1
, 1_0(2) -> 2
, 1_1(1) -> 1
, 1_1(1) -> 33
, 1_1(1) -> 38
, 1_1(2) -> 7
, 1_1(3) -> 3
, 1_1(4) -> 3
, 1_1(6) -> 5
, 1_1(7) -> 9
, 1_1(9) -> 3
, 1_1(11) -> 10
, 1_1(13) -> 16
, 1_1(14) -> 21
, 1_1(18) -> 11
, 1_1(29) -> 28
, 1_1(32) -> 31
, 1_1(33) -> 32
, 1_1(38) -> 31
, 1_1(38) -> 33
, 1_1(38) -> 38
, 1_2(2) -> 42
, 1_2(3) -> 26
, 1_2(4) -> 26
, 1_2(7) -> 26
, 1_2(9) -> 26
, 1_2(25) -> 24
, 1_2(26) -> 25
, 1_2(37) -> 36
, 1_2(38) -> 1
, 1_2(38) -> 31
, 1_2(38) -> 33
, 1_2(38) -> 36
, 1_2(38) -> 37
, 1_2(38) -> 38
, 1_2(39) -> 22
, 1_2(41) -> 40
, 1_2(42) -> 25
, 2_0(2) -> 2
, 2_1(1) -> 10
, 2_1(2) -> 13
, 2_1(3) -> 3
, 2_1(5) -> 8
, 2_1(7) -> 13
, 2_1(8) -> 8
, 2_1(9) -> 8
, 2_1(12) -> 11
, 2_1(13) -> 6
, 2_1(27) -> 1
, 2_1(27) -> 33
, 2_1(27) -> 38
, 2_1(31) -> 30
, 2_2(22) -> 22
, 2_2(23) -> 23
, 2_2(24) -> 23
, 2_2(25) -> 23
, 2_2(36) -> 35
, 2_2(40) -> 23
, 3_0(2) -> 2
, 3_1(2) -> 4
, 3_1(5) -> 4
, 3_1(7) -> 6
, 3_1(9) -> 29
, 3_1(10) -> 1
, 3_1(10) -> 33
, 3_1(10) -> 38
, 3_1(15) -> 11
, 3_1(16) -> 5
, 3_1(21) -> 3
, 3_2(26) -> 41
, 3_2(40) -> 39
, 3_2(42) -> 41
, 4_0(2) -> 1
, 4_1(2) -> 33
, 4_1(3) -> 1
, 4_1(3) -> 31
, 4_1(3) -> 33
, 4_1(3) -> 36
, 4_1(3) -> 38
, 4_1(8) -> 10
, 4_1(9) -> 31
, 4_1(13) -> 12
, 4_1(14) -> 11
, 4_1(16) -> 15
, 4_1(28) -> 27
, 4_2(3) -> 38
, 4_2(4) -> 38
, 4_2(7) -> 38
, 4_2(9) -> 38
, 4_2(22) -> 1
, 4_2(22) -> 31
, 4_2(22) -> 33
, 4_2(22) -> 36
, 4_2(22) -> 38
, 4_2(25) -> 36
, 5_0(2) -> 2
, 5_1(2) -> 7
, 5_1(3) -> 3
, 5_1(8) -> 3
, 5_1(10) -> 1
, 5_1(10) -> 33
, 5_1(10) -> 38
, 5_1(12) -> 18
, 5_1(13) -> 14
, 5_1(30) -> 10
, 5_2(22) -> 22
, 5_2(23) -> 22
, 5_2(34) -> 1
, 5_2(34) -> 31
, 5_2(34) -> 33
, 5_2(34) -> 36
, 5_2(34) -> 38
, 5_2(35) -> 34}