Tool CaT
stdout:
YES(?,O(n^1))
Problem:
0(1(1(x1))) -> 0(2(1(1(x1))))
0(1(1(x1))) -> 0(0(2(1(1(x1)))))
0(1(1(x1))) -> 0(2(1(2(1(x1)))))
0(1(1(x1))) -> 2(1(0(2(1(x1)))))
3(0(1(x1))) -> 1(3(0(0(2(4(x1))))))
3(5(1(x1))) -> 1(3(4(5(x1))))
3(5(1(x1))) -> 2(4(5(3(1(x1)))))
5(1(3(x1))) -> 5(3(1(2(x1))))
0(1(0(1(x1)))) -> 1(1(0(0(2(4(x1))))))
0(1(2(3(x1)))) -> 3(1(5(0(2(x1)))))
0(1(2(3(x1)))) -> 0(3(1(2(1(1(x1))))))
0(1(4(1(x1)))) -> 0(2(1(2(4(1(x1))))))
0(1(4(1(x1)))) -> 4(0(0(2(1(1(x1))))))
0(1(5(1(x1)))) -> 0(0(2(1(1(5(x1))))))
0(4(5(1(x1)))) -> 0(1(3(4(5(x1)))))
3(2(0(1(x1)))) -> 1(3(0(2(4(5(x1))))))
3(5(1(1(x1)))) -> 1(3(4(5(1(x1)))))
3(5(1(1(x1)))) -> 1(5(3(1(2(x1)))))
3(5(1(3(x1)))) -> 3(5(3(1(2(x1)))))
3(5(4(1(x1)))) -> 4(1(3(4(5(x1)))))
5(1(2(3(x1)))) -> 5(5(3(1(2(x1)))))
5(2(0(1(x1)))) -> 5(3(1(0(2(4(x1))))))
5(4(3(3(x1)))) -> 3(1(3(4(5(x1)))))
5(5(0(1(x1)))) -> 1(0(2(4(5(5(x1))))))
0(1(2(0(1(x1))))) -> 0(3(0(2(1(1(x1))))))
0(1(2(2(1(x1))))) -> 0(2(1(2(1(3(x1))))))
0(3(0(5(1(x1))))) -> 0(3(4(5(0(1(x1))))))
0(3(4(2(3(x1))))) -> 0(5(3(4(3(2(x1))))))
0(3(5(4(1(x1))))) -> 0(5(2(4(3(1(x1))))))
0(4(1(2(3(x1))))) -> 0(3(2(4(5(1(x1))))))
0(4(1(2(3(x1))))) -> 4(3(1(0(0(2(x1))))))
0(4(5(5(1(x1))))) -> 2(4(5(5(0(1(x1))))))
0(5(1(0(1(x1))))) -> 0(1(5(5(0(1(x1))))))
0(5(3(2(1(x1))))) -> 0(0(2(5(3(1(x1))))))
3(0(1(2(3(x1))))) -> 0(2(3(4(3(1(x1))))))
3(0(1(2(3(x1))))) -> 1(1(3(3(0(2(x1))))))
3(0(1(2(3(x1))))) -> 1(2(3(3(0(2(x1))))))
3(0(4(1(1(x1))))) -> 0(0(1(3(4(1(x1))))))
3(2(4(1(3(x1))))) -> 4(3(4(3(1(2(x1))))))
3(3(4(1(1(x1))))) -> 1(3(4(5(3(1(x1))))))
3(3(5(1(1(x1))))) -> 3(1(4(5(3(1(x1))))))
3(5(4(1(3(x1))))) -> 1(4(5(3(1(3(x1))))))
3(5(4(4(1(x1))))) -> 4(1(4(3(4(5(x1))))))
5(2(4(2(3(x1))))) -> 3(2(4(5(3(2(x1))))))
5(4(2(0(1(x1))))) -> 5(1(2(0(2(4(x1))))))
Proof:
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {6,5,4}
transitions:
01(10) -> 11*
01(37) -> 38*
01(27) -> 28*
21(39) -> 40*
21(29) -> 30*
21(9) -> 10*
11(7) -> 8*
11(19) -> 20*
11(21) -> 22*
11(38) -> 39*
11(8) -> 9*
31(55) -> 56*
31(57) -> 58*
31(49) -> 50*
41(47) -> 48*
41(41) -> 42*
00(2) -> 4*
00(1) -> 4*
00(3) -> 4*
10(2) -> 1*
10(1) -> 1*
10(3) -> 1*
20(2) -> 2*
20(1) -> 2*
20(3) -> 2*
30(2) -> 5*
30(1) -> 5*
30(3) -> 5*
40(2) -> 3*
40(1) -> 3*
40(3) -> 3*
50(2) -> 6*
50(1) -> 6*
50(3) -> 6*
1 -> 55,19
2 -> 49,7
3 -> 57,21
8 -> 41,29
11 -> 27,4
20 -> 8*
22 -> 8*
28 -> 47,4
30 -> 37,8
40 -> 4*
42 -> 29*
48 -> 4*
50 -> 7*
56 -> 7*
58 -> 7*
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(1(x1))) -> 0(2(1(1(x1))))
, 0(1(1(x1))) -> 0(0(2(1(1(x1)))))
, 0(1(1(x1))) -> 0(2(1(2(1(x1)))))
, 0(1(1(x1))) -> 2(1(0(2(1(x1)))))
, 3(0(1(x1))) -> 1(3(0(0(2(4(x1))))))
, 3(5(1(x1))) -> 1(3(4(5(x1))))
, 3(5(1(x1))) -> 2(4(5(3(1(x1)))))
, 5(1(3(x1))) -> 5(3(1(2(x1))))
, 0(1(0(1(x1)))) -> 1(1(0(0(2(4(x1))))))
, 0(1(2(3(x1)))) -> 3(1(5(0(2(x1)))))
, 0(1(2(3(x1)))) -> 0(3(1(2(1(1(x1))))))
, 0(1(4(1(x1)))) -> 0(2(1(2(4(1(x1))))))
, 0(1(4(1(x1)))) -> 4(0(0(2(1(1(x1))))))
, 0(1(5(1(x1)))) -> 0(0(2(1(1(5(x1))))))
, 0(4(5(1(x1)))) -> 0(1(3(4(5(x1)))))
, 3(2(0(1(x1)))) -> 1(3(0(2(4(5(x1))))))
, 3(5(1(1(x1)))) -> 1(3(4(5(1(x1)))))
, 3(5(1(1(x1)))) -> 1(5(3(1(2(x1)))))
, 3(5(1(3(x1)))) -> 3(5(3(1(2(x1)))))
, 3(5(4(1(x1)))) -> 4(1(3(4(5(x1)))))
, 5(1(2(3(x1)))) -> 5(5(3(1(2(x1)))))
, 5(2(0(1(x1)))) -> 5(3(1(0(2(4(x1))))))
, 5(4(3(3(x1)))) -> 3(1(3(4(5(x1)))))
, 5(5(0(1(x1)))) -> 1(0(2(4(5(5(x1))))))
, 0(1(2(0(1(x1))))) -> 0(3(0(2(1(1(x1))))))
, 0(1(2(2(1(x1))))) -> 0(2(1(2(1(3(x1))))))
, 0(3(0(5(1(x1))))) -> 0(3(4(5(0(1(x1))))))
, 0(3(4(2(3(x1))))) -> 0(5(3(4(3(2(x1))))))
, 0(3(5(4(1(x1))))) -> 0(5(2(4(3(1(x1))))))
, 0(4(1(2(3(x1))))) -> 0(3(2(4(5(1(x1))))))
, 0(4(1(2(3(x1))))) -> 4(3(1(0(0(2(x1))))))
, 0(4(5(5(1(x1))))) -> 2(4(5(5(0(1(x1))))))
, 0(5(1(0(1(x1))))) -> 0(1(5(5(0(1(x1))))))
, 0(5(3(2(1(x1))))) -> 0(0(2(5(3(1(x1))))))
, 3(0(1(2(3(x1))))) -> 0(2(3(4(3(1(x1))))))
, 3(0(1(2(3(x1))))) -> 1(1(3(3(0(2(x1))))))
, 3(0(1(2(3(x1))))) -> 1(2(3(3(0(2(x1))))))
, 3(0(4(1(1(x1))))) -> 0(0(1(3(4(1(x1))))))
, 3(2(4(1(3(x1))))) -> 4(3(4(3(1(2(x1))))))
, 3(3(4(1(1(x1))))) -> 1(3(4(5(3(1(x1))))))
, 3(3(5(1(1(x1))))) -> 3(1(4(5(3(1(x1))))))
, 3(5(4(1(3(x1))))) -> 1(4(5(3(1(3(x1))))))
, 3(5(4(4(1(x1))))) -> 4(1(4(3(4(5(x1))))))
, 5(2(4(2(3(x1))))) -> 3(2(4(5(3(2(x1))))))
, 5(4(2(0(1(x1))))) -> 5(1(2(0(2(4(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(1(x1))) -> 0(2(1(1(x1))))
, 0(1(1(x1))) -> 0(0(2(1(1(x1)))))
, 0(1(1(x1))) -> 0(2(1(2(1(x1)))))
, 0(1(1(x1))) -> 2(1(0(2(1(x1)))))
, 3(0(1(x1))) -> 1(3(0(0(2(4(x1))))))
, 3(5(1(x1))) -> 1(3(4(5(x1))))
, 3(5(1(x1))) -> 2(4(5(3(1(x1)))))
, 5(1(3(x1))) -> 5(3(1(2(x1))))
, 0(1(0(1(x1)))) -> 1(1(0(0(2(4(x1))))))
, 0(1(2(3(x1)))) -> 3(1(5(0(2(x1)))))
, 0(1(2(3(x1)))) -> 0(3(1(2(1(1(x1))))))
, 0(1(4(1(x1)))) -> 0(2(1(2(4(1(x1))))))
, 0(1(4(1(x1)))) -> 4(0(0(2(1(1(x1))))))
, 0(1(5(1(x1)))) -> 0(0(2(1(1(5(x1))))))
, 0(4(5(1(x1)))) -> 0(1(3(4(5(x1)))))
, 3(2(0(1(x1)))) -> 1(3(0(2(4(5(x1))))))
, 3(5(1(1(x1)))) -> 1(3(4(5(1(x1)))))
, 3(5(1(1(x1)))) -> 1(5(3(1(2(x1)))))
, 3(5(1(3(x1)))) -> 3(5(3(1(2(x1)))))
, 3(5(4(1(x1)))) -> 4(1(3(4(5(x1)))))
, 5(1(2(3(x1)))) -> 5(5(3(1(2(x1)))))
, 5(2(0(1(x1)))) -> 5(3(1(0(2(4(x1))))))
, 5(4(3(3(x1)))) -> 3(1(3(4(5(x1)))))
, 5(5(0(1(x1)))) -> 1(0(2(4(5(5(x1))))))
, 0(1(2(0(1(x1))))) -> 0(3(0(2(1(1(x1))))))
, 0(1(2(2(1(x1))))) -> 0(2(1(2(1(3(x1))))))
, 0(3(0(5(1(x1))))) -> 0(3(4(5(0(1(x1))))))
, 0(3(4(2(3(x1))))) -> 0(5(3(4(3(2(x1))))))
, 0(3(5(4(1(x1))))) -> 0(5(2(4(3(1(x1))))))
, 0(4(1(2(3(x1))))) -> 0(3(2(4(5(1(x1))))))
, 0(4(1(2(3(x1))))) -> 4(3(1(0(0(2(x1))))))
, 0(4(5(5(1(x1))))) -> 2(4(5(5(0(1(x1))))))
, 0(5(1(0(1(x1))))) -> 0(1(5(5(0(1(x1))))))
, 0(5(3(2(1(x1))))) -> 0(0(2(5(3(1(x1))))))
, 3(0(1(2(3(x1))))) -> 0(2(3(4(3(1(x1))))))
, 3(0(1(2(3(x1))))) -> 1(1(3(3(0(2(x1))))))
, 3(0(1(2(3(x1))))) -> 1(2(3(3(0(2(x1))))))
, 3(0(4(1(1(x1))))) -> 0(0(1(3(4(1(x1))))))
, 3(2(4(1(3(x1))))) -> 4(3(4(3(1(2(x1))))))
, 3(3(4(1(1(x1))))) -> 1(3(4(5(3(1(x1))))))
, 3(3(5(1(1(x1))))) -> 3(1(4(5(3(1(x1))))))
, 3(5(4(1(3(x1))))) -> 1(4(5(3(1(3(x1))))))
, 3(5(4(4(1(x1))))) -> 4(1(4(3(4(5(x1))))))
, 5(2(4(2(3(x1))))) -> 3(2(4(5(3(2(x1))))))
, 5(4(2(0(1(x1))))) -> 5(1(2(0(2(4(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(5) -> 1
, 0_1(1) -> 1
, 0_1(1) -> 13
, 0_1(7) -> 1
, 0_1(7) -> 13
, 0_1(9) -> 1
, 0_1(9) -> 13
, 0_1(24) -> 44
, 0_1(44) -> 43
, 0_2(13) -> 1
, 0_2(13) -> 13
, 0_2(56) -> 1
, 0_2(56) -> 13
, 0_2(60) -> 62
, 1_0(2) -> 2
, 1_0(3) -> 2
, 1_0(5) -> 2
, 1_1(2) -> 9
, 1_1(3) -> 9
, 1_1(5) -> 9
, 1_1(7) -> 37
, 1_1(9) -> 8
, 1_1(13) -> 12
, 1_1(24) -> 48
, 1_1(37) -> 48
, 1_1(43) -> 37
, 1_1(44) -> 12
, 1_1(49) -> 2
, 1_1(49) -> 4
, 1_1(72) -> 2
, 1_1(72) -> 4
, 1_1(72) -> 53
, 1_2(49) -> 58
, 1_2(58) -> 57
, 1_2(60) -> 59
, 1_2(62) -> 61
, 1_2(65) -> 64
, 1_2(72) -> 58
, 1_2(102) -> 101
, 2_0(2) -> 3
, 2_0(3) -> 3
, 2_0(5) -> 3
, 2_1(2) -> 24
, 2_1(3) -> 24
, 2_1(5) -> 24
, 2_1(8) -> 7
, 2_1(9) -> 9
, 2_1(12) -> 1
, 2_1(12) -> 13
, 2_1(38) -> 37
, 2_1(48) -> 1
, 2_1(49) -> 24
, 2_1(50) -> 24
, 2_1(54) -> 53
, 2_1(72) -> 24
, 2_1(73) -> 37
, 2_2(2) -> 65
, 2_2(3) -> 65
, 2_2(5) -> 65
, 2_2(49) -> 65
, 2_2(50) -> 102
, 2_2(57) -> 56
, 2_2(58) -> 60
, 2_2(59) -> 13
, 2_2(61) -> 1
, 2_2(61) -> 13
, 2_2(72) -> 65
, 2_2(73) -> 102
, 3_0(2) -> 4
, 3_0(3) -> 4
, 3_0(5) -> 4
, 3_1(2) -> 2
, 3_1(3) -> 2
, 3_1(5) -> 2
, 3_1(8) -> 1
, 3_1(9) -> 52
, 3_1(22) -> 21
, 3_1(24) -> 23
, 3_1(37) -> 1
, 3_1(37) -> 13
, 3_1(46) -> 45
, 3_1(48) -> 47
, 3_1(49) -> 2
, 3_1(50) -> 49
, 3_1(53) -> 6
, 3_1(53) -> 74
, 3_1(72) -> 2
, 3_1(73) -> 72
, 3_2(64) -> 63
, 3_2(97) -> 96
, 3_2(99) -> 98
, 3_2(101) -> 100
, 4_0(2) -> 5
, 4_0(3) -> 5
, 4_0(5) -> 5
, 4_1(1) -> 1
, 4_1(1) -> 13
, 4_1(4) -> 2
, 4_1(9) -> 9
, 4_1(23) -> 22
, 4_1(41) -> 38
, 4_1(45) -> 2
, 4_1(45) -> 4
, 4_1(45) -> 23
, 4_1(47) -> 46
, 4_1(51) -> 50
, 4_1(55) -> 54
, 4_1(74) -> 73
, 4_2(13) -> 1
, 4_2(13) -> 13
, 4_2(58) -> 58
, 4_2(63) -> 97
, 4_2(96) -> 52
, 4_2(98) -> 23
, 4_2(100) -> 99
, 5_0(2) -> 6
, 5_0(3) -> 6
, 5_0(5) -> 6
, 5_1(2) -> 74
, 5_1(3) -> 74
, 5_1(5) -> 74
, 5_1(6) -> 6
, 5_1(6) -> 41
, 5_1(9) -> 41
, 5_1(21) -> 1
, 5_1(23) -> 55
, 5_1(44) -> 43
, 5_1(47) -> 6
, 5_1(47) -> 74
, 5_1(49) -> 74
, 5_1(50) -> 74
, 5_1(52) -> 51
, 5_1(72) -> 74
, 5_1(73) -> 74
, 5_1(74) -> 74
, 5_2(63) -> 41
, 5_2(100) -> 74}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(1(x1))) -> 0(2(1(1(x1))))
, 0(1(1(x1))) -> 0(0(2(1(1(x1)))))
, 0(1(1(x1))) -> 0(2(1(2(1(x1)))))
, 0(1(1(x1))) -> 2(1(0(2(1(x1)))))
, 3(0(1(x1))) -> 1(3(0(0(2(4(x1))))))
, 3(5(1(x1))) -> 1(3(4(5(x1))))
, 3(5(1(x1))) -> 2(4(5(3(1(x1)))))
, 5(1(3(x1))) -> 5(3(1(2(x1))))
, 0(1(0(1(x1)))) -> 1(1(0(0(2(4(x1))))))
, 0(1(2(3(x1)))) -> 3(1(5(0(2(x1)))))
, 0(1(2(3(x1)))) -> 0(3(1(2(1(1(x1))))))
, 0(1(4(1(x1)))) -> 0(2(1(2(4(1(x1))))))
, 0(1(4(1(x1)))) -> 4(0(0(2(1(1(x1))))))
, 0(1(5(1(x1)))) -> 0(0(2(1(1(5(x1))))))
, 0(4(5(1(x1)))) -> 0(1(3(4(5(x1)))))
, 3(2(0(1(x1)))) -> 1(3(0(2(4(5(x1))))))
, 3(5(1(1(x1)))) -> 1(3(4(5(1(x1)))))
, 3(5(1(1(x1)))) -> 1(5(3(1(2(x1)))))
, 3(5(1(3(x1)))) -> 3(5(3(1(2(x1)))))
, 3(5(4(1(x1)))) -> 4(1(3(4(5(x1)))))
, 5(1(2(3(x1)))) -> 5(5(3(1(2(x1)))))
, 5(2(0(1(x1)))) -> 5(3(1(0(2(4(x1))))))
, 5(4(3(3(x1)))) -> 3(1(3(4(5(x1)))))
, 5(5(0(1(x1)))) -> 1(0(2(4(5(5(x1))))))
, 0(1(2(0(1(x1))))) -> 0(3(0(2(1(1(x1))))))
, 0(1(2(2(1(x1))))) -> 0(2(1(2(1(3(x1))))))
, 0(3(0(5(1(x1))))) -> 0(3(4(5(0(1(x1))))))
, 0(3(4(2(3(x1))))) -> 0(5(3(4(3(2(x1))))))
, 0(3(5(4(1(x1))))) -> 0(5(2(4(3(1(x1))))))
, 0(4(1(2(3(x1))))) -> 0(3(2(4(5(1(x1))))))
, 0(4(1(2(3(x1))))) -> 4(3(1(0(0(2(x1))))))
, 0(4(5(5(1(x1))))) -> 2(4(5(5(0(1(x1))))))
, 0(5(1(0(1(x1))))) -> 0(1(5(5(0(1(x1))))))
, 0(5(3(2(1(x1))))) -> 0(0(2(5(3(1(x1))))))
, 3(0(1(2(3(x1))))) -> 0(2(3(4(3(1(x1))))))
, 3(0(1(2(3(x1))))) -> 1(1(3(3(0(2(x1))))))
, 3(0(1(2(3(x1))))) -> 1(2(3(3(0(2(x1))))))
, 3(0(4(1(1(x1))))) -> 0(0(1(3(4(1(x1))))))
, 3(2(4(1(3(x1))))) -> 4(3(4(3(1(2(x1))))))
, 3(3(4(1(1(x1))))) -> 1(3(4(5(3(1(x1))))))
, 3(3(5(1(1(x1))))) -> 3(1(4(5(3(1(x1))))))
, 3(5(4(1(3(x1))))) -> 1(4(5(3(1(3(x1))))))
, 3(5(4(4(1(x1))))) -> 4(1(4(3(4(5(x1))))))
, 5(2(4(2(3(x1))))) -> 3(2(4(5(3(2(x1))))))
, 5(4(2(0(1(x1))))) -> 5(1(2(0(2(4(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(1(x1))) -> 0(2(1(1(x1))))
, 0(1(1(x1))) -> 0(0(2(1(1(x1)))))
, 0(1(1(x1))) -> 0(2(1(2(1(x1)))))
, 0(1(1(x1))) -> 2(1(0(2(1(x1)))))
, 3(0(1(x1))) -> 1(3(0(0(2(4(x1))))))
, 3(5(1(x1))) -> 1(3(4(5(x1))))
, 3(5(1(x1))) -> 2(4(5(3(1(x1)))))
, 5(1(3(x1))) -> 5(3(1(2(x1))))
, 0(1(0(1(x1)))) -> 1(1(0(0(2(4(x1))))))
, 0(1(2(3(x1)))) -> 3(1(5(0(2(x1)))))
, 0(1(2(3(x1)))) -> 0(3(1(2(1(1(x1))))))
, 0(1(4(1(x1)))) -> 0(2(1(2(4(1(x1))))))
, 0(1(4(1(x1)))) -> 4(0(0(2(1(1(x1))))))
, 0(1(5(1(x1)))) -> 0(0(2(1(1(5(x1))))))
, 0(4(5(1(x1)))) -> 0(1(3(4(5(x1)))))
, 3(2(0(1(x1)))) -> 1(3(0(2(4(5(x1))))))
, 3(5(1(1(x1)))) -> 1(3(4(5(1(x1)))))
, 3(5(1(1(x1)))) -> 1(5(3(1(2(x1)))))
, 3(5(1(3(x1)))) -> 3(5(3(1(2(x1)))))
, 3(5(4(1(x1)))) -> 4(1(3(4(5(x1)))))
, 5(1(2(3(x1)))) -> 5(5(3(1(2(x1)))))
, 5(2(0(1(x1)))) -> 5(3(1(0(2(4(x1))))))
, 5(4(3(3(x1)))) -> 3(1(3(4(5(x1)))))
, 5(5(0(1(x1)))) -> 1(0(2(4(5(5(x1))))))
, 0(1(2(0(1(x1))))) -> 0(3(0(2(1(1(x1))))))
, 0(1(2(2(1(x1))))) -> 0(2(1(2(1(3(x1))))))
, 0(3(0(5(1(x1))))) -> 0(3(4(5(0(1(x1))))))
, 0(3(4(2(3(x1))))) -> 0(5(3(4(3(2(x1))))))
, 0(3(5(4(1(x1))))) -> 0(5(2(4(3(1(x1))))))
, 0(4(1(2(3(x1))))) -> 0(3(2(4(5(1(x1))))))
, 0(4(1(2(3(x1))))) -> 4(3(1(0(0(2(x1))))))
, 0(4(5(5(1(x1))))) -> 2(4(5(5(0(1(x1))))))
, 0(5(1(0(1(x1))))) -> 0(1(5(5(0(1(x1))))))
, 0(5(3(2(1(x1))))) -> 0(0(2(5(3(1(x1))))))
, 3(0(1(2(3(x1))))) -> 0(2(3(4(3(1(x1))))))
, 3(0(1(2(3(x1))))) -> 1(1(3(3(0(2(x1))))))
, 3(0(1(2(3(x1))))) -> 1(2(3(3(0(2(x1))))))
, 3(0(4(1(1(x1))))) -> 0(0(1(3(4(1(x1))))))
, 3(2(4(1(3(x1))))) -> 4(3(4(3(1(2(x1))))))
, 3(3(4(1(1(x1))))) -> 1(3(4(5(3(1(x1))))))
, 3(3(5(1(1(x1))))) -> 3(1(4(5(3(1(x1))))))
, 3(5(4(1(3(x1))))) -> 1(4(5(3(1(3(x1))))))
, 3(5(4(4(1(x1))))) -> 4(1(4(3(4(5(x1))))))
, 5(2(4(2(3(x1))))) -> 3(2(4(5(3(2(x1))))))
, 5(4(2(0(1(x1))))) -> 5(1(2(0(2(4(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(5) -> 1
, 0_1(1) -> 1
, 0_1(1) -> 13
, 0_1(7) -> 1
, 0_1(7) -> 13
, 0_1(9) -> 1
, 0_1(9) -> 13
, 0_1(24) -> 44
, 0_1(44) -> 43
, 0_2(13) -> 1
, 0_2(13) -> 13
, 0_2(56) -> 1
, 0_2(56) -> 13
, 0_2(60) -> 62
, 1_0(2) -> 2
, 1_0(3) -> 2
, 1_0(5) -> 2
, 1_1(2) -> 9
, 1_1(3) -> 9
, 1_1(5) -> 9
, 1_1(7) -> 37
, 1_1(9) -> 8
, 1_1(13) -> 12
, 1_1(24) -> 48
, 1_1(37) -> 48
, 1_1(43) -> 37
, 1_1(44) -> 12
, 1_1(49) -> 2
, 1_1(49) -> 4
, 1_1(72) -> 2
, 1_1(72) -> 4
, 1_1(72) -> 53
, 1_2(49) -> 58
, 1_2(58) -> 57
, 1_2(60) -> 59
, 1_2(62) -> 61
, 1_2(65) -> 64
, 1_2(72) -> 58
, 1_2(102) -> 101
, 2_0(2) -> 3
, 2_0(3) -> 3
, 2_0(5) -> 3
, 2_1(2) -> 24
, 2_1(3) -> 24
, 2_1(5) -> 24
, 2_1(8) -> 7
, 2_1(9) -> 9
, 2_1(12) -> 1
, 2_1(12) -> 13
, 2_1(38) -> 37
, 2_1(48) -> 1
, 2_1(49) -> 24
, 2_1(50) -> 24
, 2_1(54) -> 53
, 2_1(72) -> 24
, 2_1(73) -> 37
, 2_2(2) -> 65
, 2_2(3) -> 65
, 2_2(5) -> 65
, 2_2(49) -> 65
, 2_2(50) -> 102
, 2_2(57) -> 56
, 2_2(58) -> 60
, 2_2(59) -> 13
, 2_2(61) -> 1
, 2_2(61) -> 13
, 2_2(72) -> 65
, 2_2(73) -> 102
, 3_0(2) -> 4
, 3_0(3) -> 4
, 3_0(5) -> 4
, 3_1(2) -> 2
, 3_1(3) -> 2
, 3_1(5) -> 2
, 3_1(8) -> 1
, 3_1(9) -> 52
, 3_1(22) -> 21
, 3_1(24) -> 23
, 3_1(37) -> 1
, 3_1(37) -> 13
, 3_1(46) -> 45
, 3_1(48) -> 47
, 3_1(49) -> 2
, 3_1(50) -> 49
, 3_1(53) -> 6
, 3_1(53) -> 74
, 3_1(72) -> 2
, 3_1(73) -> 72
, 3_2(64) -> 63
, 3_2(97) -> 96
, 3_2(99) -> 98
, 3_2(101) -> 100
, 4_0(2) -> 5
, 4_0(3) -> 5
, 4_0(5) -> 5
, 4_1(1) -> 1
, 4_1(1) -> 13
, 4_1(4) -> 2
, 4_1(9) -> 9
, 4_1(23) -> 22
, 4_1(41) -> 38
, 4_1(45) -> 2
, 4_1(45) -> 4
, 4_1(45) -> 23
, 4_1(47) -> 46
, 4_1(51) -> 50
, 4_1(55) -> 54
, 4_1(74) -> 73
, 4_2(13) -> 1
, 4_2(13) -> 13
, 4_2(58) -> 58
, 4_2(63) -> 97
, 4_2(96) -> 52
, 4_2(98) -> 23
, 4_2(100) -> 99
, 5_0(2) -> 6
, 5_0(3) -> 6
, 5_0(5) -> 6
, 5_1(2) -> 74
, 5_1(3) -> 74
, 5_1(5) -> 74
, 5_1(6) -> 6
, 5_1(6) -> 41
, 5_1(9) -> 41
, 5_1(21) -> 1
, 5_1(23) -> 55
, 5_1(44) -> 43
, 5_1(47) -> 6
, 5_1(47) -> 74
, 5_1(49) -> 74
, 5_1(50) -> 74
, 5_1(52) -> 51
, 5_1(72) -> 74
, 5_1(73) -> 74
, 5_1(74) -> 74
, 5_2(63) -> 41
, 5_2(100) -> 74}