Tool CaT
stdout:
YES(?,O(n^1))
Problem:
0(1(0(2(x1)))) -> 0(0(3(1(2(x1)))))
0(1(3(4(x1)))) -> 0(4(1(0(3(x1)))))
0(1(3(4(x1)))) -> 0(4(1(1(3(x1)))))
0(1(3(4(x1)))) -> 0(4(1(3(1(x1)))))
0(2(1(4(x1)))) -> 0(4(1(2(3(x1)))))
0(2(1(4(x1)))) -> 0(4(1(3(2(x1)))))
0(2(1(4(x1)))) -> 2(0(4(1(4(x1)))))
0(2(1(4(x1)))) -> 5(5(0(4(1(2(x1))))))
0(2(1(5(x1)))) -> 5(0(4(1(2(x1)))))
0(2(2(4(x1)))) -> 0(4(2(2(5(x1)))))
0(2(2(4(x1)))) -> 0(4(2(5(2(x1)))))
3(4(0(2(x1)))) -> 3(0(4(5(2(x1)))))
3(4(0(2(x1)))) -> 3(5(0(4(2(x1)))))
0(0(1(4(5(x1))))) -> 0(4(1(0(3(5(x1))))))
0(1(0(2(4(x1))))) -> 2(0(0(4(1(1(x1))))))
0(1(2(3(4(x1))))) -> 2(0(4(1(0(3(x1))))))
0(1(3(3(4(x1))))) -> 0(0(3(1(3(4(x1))))))
0(1(4(0(2(x1))))) -> 0(4(1(5(0(2(x1))))))
0(1(4(1(5(x1))))) -> 2(5(0(4(1(1(x1))))))
0(1(4(3(4(x1))))) -> 0(4(0(3(1(4(x1))))))
0(1(4(3(4(x1))))) -> 3(0(4(1(5(4(x1))))))
0(1(4(3(5(x1))))) -> 5(4(5(0(3(1(x1))))))
0(1(5(0(2(x1))))) -> 0(0(4(1(2(5(x1))))))
0(1(5(1(4(x1))))) -> 4(5(0(3(1(1(x1))))))
0(2(1(4(4(x1))))) -> 0(4(1(2(4(3(x1))))))
0(2(1(4(5(x1))))) -> 0(4(1(2(5(2(x1))))))
0(2(1(5(4(x1))))) -> 5(0(2(0(4(1(x1))))))
0(2(4(1(5(x1))))) -> 5(0(4(1(5(2(x1))))))
0(2(4(3(5(x1))))) -> 0(4(5(2(5(3(x1))))))
0(2(5(1(4(x1))))) -> 0(0(5(4(1(2(x1))))))
3(0(1(3(2(x1))))) -> 0(3(1(0(3(2(x1))))))
3(0(2(1(4(x1))))) -> 4(0(4(1(3(2(x1))))))
3(0(2(1(5(x1))))) -> 5(3(2(0(4(1(x1))))))
3(0(4(0(2(x1))))) -> 0(3(4(0(4(2(x1))))))
3(0(4(0(2(x1))))) -> 0(4(1(2(0(3(x1))))))
3(0(5(1(4(x1))))) -> 3(0(4(1(1(5(x1))))))
3(0(5(1(5(x1))))) -> 0(4(1(3(5(5(x1))))))
3(2(4(1(2(x1))))) -> 3(1(2(2(5(4(x1))))))
3(2(4(1(5(x1))))) -> 3(1(4(5(2(5(x1))))))
3(4(0(1(2(x1))))) -> 0(4(2(0(3(1(x1))))))
3(4(0(1(4(x1))))) -> 0(4(1(5(3(4(x1))))))
3(4(0(1(5(x1))))) -> 0(4(1(5(5(3(x1))))))
3(4(0(2(4(x1))))) -> 0(3(4(0(4(2(x1))))))
3(4(1(2(4(x1))))) -> 0(4(1(2(4(3(x1))))))
3(4(1(3(5(x1))))) -> 4(3(0(3(1(5(x1))))))
3(4(3(0(2(x1))))) -> 3(3(0(4(1(2(x1))))))
3(4(5(0(2(x1))))) -> 0(3(0(4(2(5(x1))))))
3(5(0(2(2(x1))))) -> 0(3(2(5(2(5(x1))))))
3(5(2(1(4(x1))))) -> 3(5(1(0(4(2(x1))))))
Proof:
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {6,5}
transitions:
31(32) -> 33*
31(7) -> 8*
31(179) -> 180*
31(29) -> 30*
31(21) -> 22*
31(138) -> 139*
31(23) -> 24*
51(97) -> 98*
51(77) -> 78*
51(119) -> 120*
51(181) -> 182*
51(76) -> 77*
51(163) -> 164*
51(103) -> 104*
51(190) -> 191*
51(175) -> 176*
51(140) -> 141*
51(105) -> 106*
51(95) -> 96*
51(85) -> 86*
11(50) -> 51*
11(127) -> 128*
11(189) -> 190*
11(149) -> 150*
11(129) -> 130*
11(9) -> 10*
11(161) -> 162*
11(121) -> 122*
11(116) -> 117*
11(178) -> 179*
11(73) -> 74*
11(115) -> 116*
01(75) -> 76*
01(152) -> 153*
01(52) -> 53*
01(164) -> 165*
01(139) -> 140*
01(11) -> 12*
01(188) -> 189*
01(118) -> 119*
41(65) -> 66*
41(10) -> 11*
41(187) -> 188*
41(182) -> 183*
41(117) -> 118*
41(74) -> 75*
41(49) -> 50*
41(151) -> 152*
41(141) -> 142*
41(71) -> 72*
41(51) -> 52*
41(143) -> 144*
41(63) -> 64*
21(177) -> 178*
21(87) -> 88*
21(47) -> 48*
21(39) -> 40*
21(176) -> 177*
21(86) -> 87*
21(41) -> 42*
21(31) -> 32*
21(153) -> 154*
21(53) -> 54*
21(8) -> 9*
00(2) -> 5*
00(4) -> 5*
00(1) -> 5*
00(3) -> 5*
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) -> 6*
30(4) -> 6*
30(1) -> 6*
30(3) -> 6*
40(2) -> 3*
40(4) -> 3*
40(1) -> 3*
40(3) -> 3*
50(2) -> 4*
50(4) -> 4*
50(1) -> 4*
50(3) -> 4*
1 -> 127,97,65,41,23
2 -> 115,85,49,31,7
3 -> 129,103,71,47,29
4 -> 121,95,63,39,21
8 -> 143*
12 -> 30,8,143,6,5
22 -> 8*
24 -> 8*
30 -> 8*
32 -> 187,105,73
33 -> 9*
40 -> 32*
42 -> 32*
48 -> 32*
50 -> 175*
54 -> 5*
64 -> 50*
66 -> 50*
72 -> 50*
75 -> 163*
77 -> 5*
78 -> 5*
87 -> 181*
88 -> 149,10
96 -> 86*
98 -> 86*
104 -> 86*
106 -> 161,87
116 -> 151*
117 -> 138*
120 -> 53*
122 -> 116*
128 -> 116*
130 -> 116*
142 -> 5*
144 -> 8*
150 -> 10*
154 -> 75*
162 -> 74*
165 -> 11*
180 -> 22,33,8,143,9,6
183 -> 178*
191 -> 179*
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)))) -> 0(0(3(1(2(x1)))))
, 0(1(3(4(x1)))) -> 0(4(1(0(3(x1)))))
, 0(1(3(4(x1)))) -> 0(4(1(1(3(x1)))))
, 0(1(3(4(x1)))) -> 0(4(1(3(1(x1)))))
, 0(2(1(4(x1)))) -> 0(4(1(2(3(x1)))))
, 0(2(1(4(x1)))) -> 0(4(1(3(2(x1)))))
, 0(2(1(4(x1)))) -> 2(0(4(1(4(x1)))))
, 0(2(1(4(x1)))) -> 5(5(0(4(1(2(x1))))))
, 0(2(1(5(x1)))) -> 5(0(4(1(2(x1)))))
, 0(2(2(4(x1)))) -> 0(4(2(2(5(x1)))))
, 0(2(2(4(x1)))) -> 0(4(2(5(2(x1)))))
, 3(4(0(2(x1)))) -> 3(0(4(5(2(x1)))))
, 3(4(0(2(x1)))) -> 3(5(0(4(2(x1)))))
, 0(0(1(4(5(x1))))) -> 0(4(1(0(3(5(x1))))))
, 0(1(0(2(4(x1))))) -> 2(0(0(4(1(1(x1))))))
, 0(1(2(3(4(x1))))) -> 2(0(4(1(0(3(x1))))))
, 0(1(3(3(4(x1))))) -> 0(0(3(1(3(4(x1))))))
, 0(1(4(0(2(x1))))) -> 0(4(1(5(0(2(x1))))))
, 0(1(4(1(5(x1))))) -> 2(5(0(4(1(1(x1))))))
, 0(1(4(3(4(x1))))) -> 0(4(0(3(1(4(x1))))))
, 0(1(4(3(4(x1))))) -> 3(0(4(1(5(4(x1))))))
, 0(1(4(3(5(x1))))) -> 5(4(5(0(3(1(x1))))))
, 0(1(5(0(2(x1))))) -> 0(0(4(1(2(5(x1))))))
, 0(1(5(1(4(x1))))) -> 4(5(0(3(1(1(x1))))))
, 0(2(1(4(4(x1))))) -> 0(4(1(2(4(3(x1))))))
, 0(2(1(4(5(x1))))) -> 0(4(1(2(5(2(x1))))))
, 0(2(1(5(4(x1))))) -> 5(0(2(0(4(1(x1))))))
, 0(2(4(1(5(x1))))) -> 5(0(4(1(5(2(x1))))))
, 0(2(4(3(5(x1))))) -> 0(4(5(2(5(3(x1))))))
, 0(2(5(1(4(x1))))) -> 0(0(5(4(1(2(x1))))))
, 3(0(1(3(2(x1))))) -> 0(3(1(0(3(2(x1))))))
, 3(0(2(1(4(x1))))) -> 4(0(4(1(3(2(x1))))))
, 3(0(2(1(5(x1))))) -> 5(3(2(0(4(1(x1))))))
, 3(0(4(0(2(x1))))) -> 0(3(4(0(4(2(x1))))))
, 3(0(4(0(2(x1))))) -> 0(4(1(2(0(3(x1))))))
, 3(0(5(1(4(x1))))) -> 3(0(4(1(1(5(x1))))))
, 3(0(5(1(5(x1))))) -> 0(4(1(3(5(5(x1))))))
, 3(2(4(1(2(x1))))) -> 3(1(2(2(5(4(x1))))))
, 3(2(4(1(5(x1))))) -> 3(1(4(5(2(5(x1))))))
, 3(4(0(1(2(x1))))) -> 0(4(2(0(3(1(x1))))))
, 3(4(0(1(4(x1))))) -> 0(4(1(5(3(4(x1))))))
, 3(4(0(1(5(x1))))) -> 0(4(1(5(5(3(x1))))))
, 3(4(0(2(4(x1))))) -> 0(3(4(0(4(2(x1))))))
, 3(4(1(2(4(x1))))) -> 0(4(1(2(4(3(x1))))))
, 3(4(1(3(5(x1))))) -> 4(3(0(3(1(5(x1))))))
, 3(4(3(0(2(x1))))) -> 3(3(0(4(1(2(x1))))))
, 3(4(5(0(2(x1))))) -> 0(3(0(4(2(5(x1))))))
, 3(5(0(2(2(x1))))) -> 0(3(2(5(2(5(x1))))))
, 3(5(2(1(4(x1))))) -> 3(5(1(0(4(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(1(0(2(x1)))) -> 0(0(3(1(2(x1)))))
, 0(1(3(4(x1)))) -> 0(4(1(0(3(x1)))))
, 0(1(3(4(x1)))) -> 0(4(1(1(3(x1)))))
, 0(1(3(4(x1)))) -> 0(4(1(3(1(x1)))))
, 0(2(1(4(x1)))) -> 0(4(1(2(3(x1)))))
, 0(2(1(4(x1)))) -> 0(4(1(3(2(x1)))))
, 0(2(1(4(x1)))) -> 2(0(4(1(4(x1)))))
, 0(2(1(4(x1)))) -> 5(5(0(4(1(2(x1))))))
, 0(2(1(5(x1)))) -> 5(0(4(1(2(x1)))))
, 0(2(2(4(x1)))) -> 0(4(2(2(5(x1)))))
, 0(2(2(4(x1)))) -> 0(4(2(5(2(x1)))))
, 3(4(0(2(x1)))) -> 3(0(4(5(2(x1)))))
, 3(4(0(2(x1)))) -> 3(5(0(4(2(x1)))))
, 0(0(1(4(5(x1))))) -> 0(4(1(0(3(5(x1))))))
, 0(1(0(2(4(x1))))) -> 2(0(0(4(1(1(x1))))))
, 0(1(2(3(4(x1))))) -> 2(0(4(1(0(3(x1))))))
, 0(1(3(3(4(x1))))) -> 0(0(3(1(3(4(x1))))))
, 0(1(4(0(2(x1))))) -> 0(4(1(5(0(2(x1))))))
, 0(1(4(1(5(x1))))) -> 2(5(0(4(1(1(x1))))))
, 0(1(4(3(4(x1))))) -> 0(4(0(3(1(4(x1))))))
, 0(1(4(3(4(x1))))) -> 3(0(4(1(5(4(x1))))))
, 0(1(4(3(5(x1))))) -> 5(4(5(0(3(1(x1))))))
, 0(1(5(0(2(x1))))) -> 0(0(4(1(2(5(x1))))))
, 0(1(5(1(4(x1))))) -> 4(5(0(3(1(1(x1))))))
, 0(2(1(4(4(x1))))) -> 0(4(1(2(4(3(x1))))))
, 0(2(1(4(5(x1))))) -> 0(4(1(2(5(2(x1))))))
, 0(2(1(5(4(x1))))) -> 5(0(2(0(4(1(x1))))))
, 0(2(4(1(5(x1))))) -> 5(0(4(1(5(2(x1))))))
, 0(2(4(3(5(x1))))) -> 0(4(5(2(5(3(x1))))))
, 0(2(5(1(4(x1))))) -> 0(0(5(4(1(2(x1))))))
, 3(0(1(3(2(x1))))) -> 0(3(1(0(3(2(x1))))))
, 3(0(2(1(4(x1))))) -> 4(0(4(1(3(2(x1))))))
, 3(0(2(1(5(x1))))) -> 5(3(2(0(4(1(x1))))))
, 3(0(4(0(2(x1))))) -> 0(3(4(0(4(2(x1))))))
, 3(0(4(0(2(x1))))) -> 0(4(1(2(0(3(x1))))))
, 3(0(5(1(4(x1))))) -> 3(0(4(1(1(5(x1))))))
, 3(0(5(1(5(x1))))) -> 0(4(1(3(5(5(x1))))))
, 3(2(4(1(2(x1))))) -> 3(1(2(2(5(4(x1))))))
, 3(2(4(1(5(x1))))) -> 3(1(4(5(2(5(x1))))))
, 3(4(0(1(2(x1))))) -> 0(4(2(0(3(1(x1))))))
, 3(4(0(1(4(x1))))) -> 0(4(1(5(3(4(x1))))))
, 3(4(0(1(5(x1))))) -> 0(4(1(5(5(3(x1))))))
, 3(4(0(2(4(x1))))) -> 0(3(4(0(4(2(x1))))))
, 3(4(1(2(4(x1))))) -> 0(4(1(2(4(3(x1))))))
, 3(4(1(3(5(x1))))) -> 4(3(0(3(1(5(x1))))))
, 3(4(3(0(2(x1))))) -> 3(3(0(4(1(2(x1))))))
, 3(4(5(0(2(x1))))) -> 0(3(0(4(2(5(x1))))))
, 3(5(0(2(2(x1))))) -> 0(3(2(5(2(5(x1))))))
, 3(5(2(1(4(x1))))) -> 3(5(1(0(4(2(x1))))))}
Proof Output:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ 0_0(2) -> 1
, 0_1(3) -> 1
, 0_1(3) -> 6
, 0_1(9) -> 8
, 0_1(14) -> 13
, 0_1(19) -> 18
, 0_1(24) -> 23
, 0_1(27) -> 26
, 0_1(32) -> 3
, 0_1(40) -> 39
, 1_0(2) -> 2
, 1_1(2) -> 21
, 1_1(4) -> 4
, 1_1(5) -> 4
, 1_1(7) -> 15
, 1_1(11) -> 10
, 1_1(16) -> 15
, 1_1(21) -> 20
, 1_1(34) -> 33
, 1_1(39) -> 38
, 2_0(2) -> 2
, 2_1(2) -> 7
, 2_1(6) -> 5
, 2_1(8) -> 1
, 2_1(16) -> 4
, 2_1(17) -> 16
, 2_1(26) -> 14
, 2_1(35) -> 34
, 2_1(36) -> 35
, 3_0(2) -> 1
, 3_1(2) -> 6
, 3_1(7) -> 5
, 3_1(20) -> 24
, 3_1(33) -> 1
, 3_1(33) -> 5
, 3_1(33) -> 6
, 4_0(2) -> 2
, 4_1(2) -> 11
, 4_1(4) -> 3
, 4_1(6) -> 6
, 4_1(7) -> 40
, 4_1(10) -> 9
, 4_1(15) -> 14
, 4_1(20) -> 19
, 4_1(21) -> 27
, 4_1(22) -> 1
, 4_1(37) -> 34
, 5_0(2) -> 2
, 5_1(2) -> 17
, 5_1(7) -> 16
, 5_1(11) -> 36
, 5_1(12) -> 1
, 5_1(13) -> 1
, 5_1(13) -> 12
, 5_1(14) -> 32
, 5_1(16) -> 37
, 5_1(18) -> 8
, 5_1(23) -> 22
, 5_1(38) -> 33}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)))) -> 0(0(3(1(2(x1)))))
, 0(1(3(4(x1)))) -> 0(4(1(0(3(x1)))))
, 0(1(3(4(x1)))) -> 0(4(1(1(3(x1)))))
, 0(1(3(4(x1)))) -> 0(4(1(3(1(x1)))))
, 0(2(1(4(x1)))) -> 0(4(1(2(3(x1)))))
, 0(2(1(4(x1)))) -> 0(4(1(3(2(x1)))))
, 0(2(1(4(x1)))) -> 2(0(4(1(4(x1)))))
, 0(2(1(4(x1)))) -> 5(5(0(4(1(2(x1))))))
, 0(2(1(5(x1)))) -> 5(0(4(1(2(x1)))))
, 0(2(2(4(x1)))) -> 0(4(2(2(5(x1)))))
, 0(2(2(4(x1)))) -> 0(4(2(5(2(x1)))))
, 3(4(0(2(x1)))) -> 3(0(4(5(2(x1)))))
, 3(4(0(2(x1)))) -> 3(5(0(4(2(x1)))))
, 0(0(1(4(5(x1))))) -> 0(4(1(0(3(5(x1))))))
, 0(1(0(2(4(x1))))) -> 2(0(0(4(1(1(x1))))))
, 0(1(2(3(4(x1))))) -> 2(0(4(1(0(3(x1))))))
, 0(1(3(3(4(x1))))) -> 0(0(3(1(3(4(x1))))))
, 0(1(4(0(2(x1))))) -> 0(4(1(5(0(2(x1))))))
, 0(1(4(1(5(x1))))) -> 2(5(0(4(1(1(x1))))))
, 0(1(4(3(4(x1))))) -> 0(4(0(3(1(4(x1))))))
, 0(1(4(3(4(x1))))) -> 3(0(4(1(5(4(x1))))))
, 0(1(4(3(5(x1))))) -> 5(4(5(0(3(1(x1))))))
, 0(1(5(0(2(x1))))) -> 0(0(4(1(2(5(x1))))))
, 0(1(5(1(4(x1))))) -> 4(5(0(3(1(1(x1))))))
, 0(2(1(4(4(x1))))) -> 0(4(1(2(4(3(x1))))))
, 0(2(1(4(5(x1))))) -> 0(4(1(2(5(2(x1))))))
, 0(2(1(5(4(x1))))) -> 5(0(2(0(4(1(x1))))))
, 0(2(4(1(5(x1))))) -> 5(0(4(1(5(2(x1))))))
, 0(2(4(3(5(x1))))) -> 0(4(5(2(5(3(x1))))))
, 0(2(5(1(4(x1))))) -> 0(0(5(4(1(2(x1))))))
, 3(0(1(3(2(x1))))) -> 0(3(1(0(3(2(x1))))))
, 3(0(2(1(4(x1))))) -> 4(0(4(1(3(2(x1))))))
, 3(0(2(1(5(x1))))) -> 5(3(2(0(4(1(x1))))))
, 3(0(4(0(2(x1))))) -> 0(3(4(0(4(2(x1))))))
, 3(0(4(0(2(x1))))) -> 0(4(1(2(0(3(x1))))))
, 3(0(5(1(4(x1))))) -> 3(0(4(1(1(5(x1))))))
, 3(0(5(1(5(x1))))) -> 0(4(1(3(5(5(x1))))))
, 3(2(4(1(2(x1))))) -> 3(1(2(2(5(4(x1))))))
, 3(2(4(1(5(x1))))) -> 3(1(4(5(2(5(x1))))))
, 3(4(0(1(2(x1))))) -> 0(4(2(0(3(1(x1))))))
, 3(4(0(1(4(x1))))) -> 0(4(1(5(3(4(x1))))))
, 3(4(0(1(5(x1))))) -> 0(4(1(5(5(3(x1))))))
, 3(4(0(2(4(x1))))) -> 0(3(4(0(4(2(x1))))))
, 3(4(1(2(4(x1))))) -> 0(4(1(2(4(3(x1))))))
, 3(4(1(3(5(x1))))) -> 4(3(0(3(1(5(x1))))))
, 3(4(3(0(2(x1))))) -> 3(3(0(4(1(2(x1))))))
, 3(4(5(0(2(x1))))) -> 0(3(0(4(2(5(x1))))))
, 3(5(0(2(2(x1))))) -> 0(3(2(5(2(5(x1))))))
, 3(5(2(1(4(x1))))) -> 3(5(1(0(4(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(1(0(2(x1)))) -> 0(0(3(1(2(x1)))))
, 0(1(3(4(x1)))) -> 0(4(1(0(3(x1)))))
, 0(1(3(4(x1)))) -> 0(4(1(1(3(x1)))))
, 0(1(3(4(x1)))) -> 0(4(1(3(1(x1)))))
, 0(2(1(4(x1)))) -> 0(4(1(2(3(x1)))))
, 0(2(1(4(x1)))) -> 0(4(1(3(2(x1)))))
, 0(2(1(4(x1)))) -> 2(0(4(1(4(x1)))))
, 0(2(1(4(x1)))) -> 5(5(0(4(1(2(x1))))))
, 0(2(1(5(x1)))) -> 5(0(4(1(2(x1)))))
, 0(2(2(4(x1)))) -> 0(4(2(2(5(x1)))))
, 0(2(2(4(x1)))) -> 0(4(2(5(2(x1)))))
, 3(4(0(2(x1)))) -> 3(0(4(5(2(x1)))))
, 3(4(0(2(x1)))) -> 3(5(0(4(2(x1)))))
, 0(0(1(4(5(x1))))) -> 0(4(1(0(3(5(x1))))))
, 0(1(0(2(4(x1))))) -> 2(0(0(4(1(1(x1))))))
, 0(1(2(3(4(x1))))) -> 2(0(4(1(0(3(x1))))))
, 0(1(3(3(4(x1))))) -> 0(0(3(1(3(4(x1))))))
, 0(1(4(0(2(x1))))) -> 0(4(1(5(0(2(x1))))))
, 0(1(4(1(5(x1))))) -> 2(5(0(4(1(1(x1))))))
, 0(1(4(3(4(x1))))) -> 0(4(0(3(1(4(x1))))))
, 0(1(4(3(4(x1))))) -> 3(0(4(1(5(4(x1))))))
, 0(1(4(3(5(x1))))) -> 5(4(5(0(3(1(x1))))))
, 0(1(5(0(2(x1))))) -> 0(0(4(1(2(5(x1))))))
, 0(1(5(1(4(x1))))) -> 4(5(0(3(1(1(x1))))))
, 0(2(1(4(4(x1))))) -> 0(4(1(2(4(3(x1))))))
, 0(2(1(4(5(x1))))) -> 0(4(1(2(5(2(x1))))))
, 0(2(1(5(4(x1))))) -> 5(0(2(0(4(1(x1))))))
, 0(2(4(1(5(x1))))) -> 5(0(4(1(5(2(x1))))))
, 0(2(4(3(5(x1))))) -> 0(4(5(2(5(3(x1))))))
, 0(2(5(1(4(x1))))) -> 0(0(5(4(1(2(x1))))))
, 3(0(1(3(2(x1))))) -> 0(3(1(0(3(2(x1))))))
, 3(0(2(1(4(x1))))) -> 4(0(4(1(3(2(x1))))))
, 3(0(2(1(5(x1))))) -> 5(3(2(0(4(1(x1))))))
, 3(0(4(0(2(x1))))) -> 0(3(4(0(4(2(x1))))))
, 3(0(4(0(2(x1))))) -> 0(4(1(2(0(3(x1))))))
, 3(0(5(1(4(x1))))) -> 3(0(4(1(1(5(x1))))))
, 3(0(5(1(5(x1))))) -> 0(4(1(3(5(5(x1))))))
, 3(2(4(1(2(x1))))) -> 3(1(2(2(5(4(x1))))))
, 3(2(4(1(5(x1))))) -> 3(1(4(5(2(5(x1))))))
, 3(4(0(1(2(x1))))) -> 0(4(2(0(3(1(x1))))))
, 3(4(0(1(4(x1))))) -> 0(4(1(5(3(4(x1))))))
, 3(4(0(1(5(x1))))) -> 0(4(1(5(5(3(x1))))))
, 3(4(0(2(4(x1))))) -> 0(3(4(0(4(2(x1))))))
, 3(4(1(2(4(x1))))) -> 0(4(1(2(4(3(x1))))))
, 3(4(1(3(5(x1))))) -> 4(3(0(3(1(5(x1))))))
, 3(4(3(0(2(x1))))) -> 3(3(0(4(1(2(x1))))))
, 3(4(5(0(2(x1))))) -> 0(3(0(4(2(5(x1))))))
, 3(5(0(2(2(x1))))) -> 0(3(2(5(2(5(x1))))))
, 3(5(2(1(4(x1))))) -> 3(5(1(0(4(2(x1))))))}
Proof Output:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ 0_0(2) -> 1
, 0_1(3) -> 1
, 0_1(3) -> 6
, 0_1(9) -> 8
, 0_1(14) -> 13
, 0_1(19) -> 18
, 0_1(24) -> 23
, 0_1(27) -> 26
, 0_1(32) -> 3
, 0_1(40) -> 39
, 1_0(2) -> 2
, 1_1(2) -> 21
, 1_1(4) -> 4
, 1_1(5) -> 4
, 1_1(7) -> 15
, 1_1(11) -> 10
, 1_1(16) -> 15
, 1_1(21) -> 20
, 1_1(34) -> 33
, 1_1(39) -> 38
, 2_0(2) -> 2
, 2_1(2) -> 7
, 2_1(6) -> 5
, 2_1(8) -> 1
, 2_1(16) -> 4
, 2_1(17) -> 16
, 2_1(26) -> 14
, 2_1(35) -> 34
, 2_1(36) -> 35
, 3_0(2) -> 1
, 3_1(2) -> 6
, 3_1(7) -> 5
, 3_1(20) -> 24
, 3_1(33) -> 1
, 3_1(33) -> 5
, 3_1(33) -> 6
, 4_0(2) -> 2
, 4_1(2) -> 11
, 4_1(4) -> 3
, 4_1(6) -> 6
, 4_1(7) -> 40
, 4_1(10) -> 9
, 4_1(15) -> 14
, 4_1(20) -> 19
, 4_1(21) -> 27
, 4_1(22) -> 1
, 4_1(37) -> 34
, 5_0(2) -> 2
, 5_1(2) -> 17
, 5_1(7) -> 16
, 5_1(11) -> 36
, 5_1(12) -> 1
, 5_1(13) -> 1
, 5_1(13) -> 12
, 5_1(14) -> 32
, 5_1(16) -> 37
, 5_1(18) -> 8
, 5_1(23) -> 22
, 5_1(38) -> 33}