Tool CaT
stdout:
YES(?,O(n^1))
Problem:
0(0(0(x1))) -> 0(0(1(0(2(x1)))))
0(3(2(x1))) -> 4(3(0(2(x1))))
0(0(4(2(x1)))) -> 0(4(1(0(2(x1)))))
0(0(5(2(x1)))) -> 5(0(2(3(0(x1)))))
0(1(3(2(x1)))) -> 0(3(1(0(2(x1)))))
0(1(3(2(x1)))) -> 3(1(1(0(2(x1)))))
0(1(3(2(x1)))) -> 0(1(4(3(1(2(x1))))))
0(4(1(3(x1)))) -> 1(4(3(0(2(2(x1))))))
0(4(2(3(x1)))) -> 5(4(3(0(2(x1)))))
0(4(5(2(x1)))) -> 5(0(2(2(4(2(x1))))))
0(5(1(3(x1)))) -> 3(0(1(5(1(2(x1))))))
0(5(3(0(x1)))) -> 5(0(1(4(3(0(x1))))))
0(5(3(2(x1)))) -> 5(1(5(0(2(3(x1))))))
4(0(2(3(x1)))) -> 3(4(3(0(2(x1)))))
4(0(2(3(x1)))) -> 4(3(5(0(2(x1)))))
4(4(1(3(x1)))) -> 4(3(4(1(2(2(x1))))))
4(5(2(0(x1)))) -> 4(2(1(5(0(2(x1))))))
4(5(2(0(x1)))) -> 5(1(0(2(2(4(x1))))))
5(1(0(0(x1)))) -> 5(1(0(2(0(x1)))))
5(1(0(0(x1)))) -> 5(2(1(0(2(0(x1))))))
5(1(3(0(x1)))) -> 5(0(2(1(3(x1)))))
5(1(3(2(x1)))) -> 3(0(1(5(1(2(x1))))))
5(1(3(2(x1)))) -> 3(1(1(5(2(2(x1))))))
5(3(0(0(x1)))) -> 5(0(4(3(0(2(x1))))))
0(0(4(1(3(x1))))) -> 4(0(1(0(2(3(x1))))))
0(0(4(5(2(x1))))) -> 5(0(1(0(2(4(x1))))))
0(0(5(3(2(x1))))) -> 0(1(5(0(2(3(x1))))))
0(1(0(5(2(x1))))) -> 1(0(2(5(1(0(x1))))))
0(1(4(5(2(x1))))) -> 2(1(5(0(2(4(x1))))))
0(3(1(4(0(x1))))) -> 4(1(0(1(0(3(x1))))))
0(3(2(0(0(x1))))) -> 0(0(1(0(2(3(x1))))))
0(3(4(0(2(x1))))) -> 4(3(0(2(1(0(x1))))))
0(3(4(0(2(x1))))) -> 4(3(0(2(3(0(x1))))))
0(3(4(4(2(x1))))) -> 4(0(3(4(2(2(x1))))))
0(4(2(5(3(x1))))) -> 0(4(3(5(1(2(x1))))))
0(5(1(2(0(x1))))) -> 3(0(1(5(0(2(x1))))))
4(4(2(2(0(x1))))) -> 4(1(0(2(2(4(x1))))))
4(5(1(2(0(x1))))) -> 5(0(4(1(2(2(x1))))))
4(5(2(3(2(x1))))) -> 5(4(3(5(2(2(x1))))))
5(1(0(3(2(x1))))) -> 5(0(3(1(0(2(x1))))))
5(1(0(5(3(x1))))) -> 5(5(0(1(3(1(x1))))))
5(1(3(0(0(x1))))) -> 3(5(0(1(2(0(x1))))))
5(1(3(0(2(x1))))) -> 3(0(2(1(5(2(x1))))))
5(1(3(0(2(x1))))) -> 5(0(1(0(3(2(x1))))))
5(1(3(0(2(x1))))) -> 5(0(1(1(2(3(x1))))))
5(1(3(2(0(x1))))) -> 5(3(1(5(2(0(x1))))))
5(1(3(2(3(x1))))) -> 3(4(3(5(1(2(x1))))))
5(1(4(5(2(x1))))) -> 5(1(4(1(5(2(x1))))))
5(5(1(3(2(x1))))) -> 3(5(5(4(1(2(x1))))))
Proof:
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {6,5,4}
transitions:
31(45) -> 46*
31(30) -> 31*
31(52) -> 53*
31(69) -> 70*
31(34) -> 35*
31(9) -> 10*
41(70) -> 71*
41(10) -> 11*
41(46) -> 47*
51(65) -> 66*
51(49) -> 50*
11(50) -> 51*
11(67) -> 68*
11(47) -> 48*
11(44) -> 45*
11(29) -> 30*
11(66) -> 67*
11(33) -> 34*
21(7) -> 8*
21(64) -> 65*
21(19) -> 20*
21(21) -> 22*
01(51) -> 52*
01(31) -> 32*
01(8) -> 9*
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) -> 3*
30(1) -> 3*
30(3) -> 3*
40(2) -> 5*
40(1) -> 5*
40(3) -> 5*
50(2) -> 6*
50(1) -> 6*
50(3) -> 6*
1 -> 19*
2 -> 7*
3 -> 21*
8 -> 64,44
9 -> 29*
11 -> 4*
20 -> 8*
22 -> 8*
30 -> 33*
32 -> 4*
35 -> 4*
45 -> 49*
48 -> 31*
50 -> 69*
53 -> 6*
68 -> 52*
71 -> 52*
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(0(0(x1))) -> 0(0(1(0(2(x1)))))
, 0(3(2(x1))) -> 4(3(0(2(x1))))
, 0(0(4(2(x1)))) -> 0(4(1(0(2(x1)))))
, 0(0(5(2(x1)))) -> 5(0(2(3(0(x1)))))
, 0(1(3(2(x1)))) -> 0(3(1(0(2(x1)))))
, 0(1(3(2(x1)))) -> 3(1(1(0(2(x1)))))
, 0(1(3(2(x1)))) -> 0(1(4(3(1(2(x1))))))
, 0(4(1(3(x1)))) -> 1(4(3(0(2(2(x1))))))
, 0(4(2(3(x1)))) -> 5(4(3(0(2(x1)))))
, 0(4(5(2(x1)))) -> 5(0(2(2(4(2(x1))))))
, 0(5(1(3(x1)))) -> 3(0(1(5(1(2(x1))))))
, 0(5(3(0(x1)))) -> 5(0(1(4(3(0(x1))))))
, 0(5(3(2(x1)))) -> 5(1(5(0(2(3(x1))))))
, 4(0(2(3(x1)))) -> 3(4(3(0(2(x1)))))
, 4(0(2(3(x1)))) -> 4(3(5(0(2(x1)))))
, 4(4(1(3(x1)))) -> 4(3(4(1(2(2(x1))))))
, 4(5(2(0(x1)))) -> 4(2(1(5(0(2(x1))))))
, 4(5(2(0(x1)))) -> 5(1(0(2(2(4(x1))))))
, 5(1(0(0(x1)))) -> 5(1(0(2(0(x1)))))
, 5(1(0(0(x1)))) -> 5(2(1(0(2(0(x1))))))
, 5(1(3(0(x1)))) -> 5(0(2(1(3(x1)))))
, 5(1(3(2(x1)))) -> 3(0(1(5(1(2(x1))))))
, 5(1(3(2(x1)))) -> 3(1(1(5(2(2(x1))))))
, 5(3(0(0(x1)))) -> 5(0(4(3(0(2(x1))))))
, 0(0(4(1(3(x1))))) -> 4(0(1(0(2(3(x1))))))
, 0(0(4(5(2(x1))))) -> 5(0(1(0(2(4(x1))))))
, 0(0(5(3(2(x1))))) -> 0(1(5(0(2(3(x1))))))
, 0(1(0(5(2(x1))))) -> 1(0(2(5(1(0(x1))))))
, 0(1(4(5(2(x1))))) -> 2(1(5(0(2(4(x1))))))
, 0(3(1(4(0(x1))))) -> 4(1(0(1(0(3(x1))))))
, 0(3(2(0(0(x1))))) -> 0(0(1(0(2(3(x1))))))
, 0(3(4(0(2(x1))))) -> 4(3(0(2(1(0(x1))))))
, 0(3(4(0(2(x1))))) -> 4(3(0(2(3(0(x1))))))
, 0(3(4(4(2(x1))))) -> 4(0(3(4(2(2(x1))))))
, 0(4(2(5(3(x1))))) -> 0(4(3(5(1(2(x1))))))
, 0(5(1(2(0(x1))))) -> 3(0(1(5(0(2(x1))))))
, 4(4(2(2(0(x1))))) -> 4(1(0(2(2(4(x1))))))
, 4(5(1(2(0(x1))))) -> 5(0(4(1(2(2(x1))))))
, 4(5(2(3(2(x1))))) -> 5(4(3(5(2(2(x1))))))
, 5(1(0(3(2(x1))))) -> 5(0(3(1(0(2(x1))))))
, 5(1(0(5(3(x1))))) -> 5(5(0(1(3(1(x1))))))
, 5(1(3(0(0(x1))))) -> 3(5(0(1(2(0(x1))))))
, 5(1(3(0(2(x1))))) -> 3(0(2(1(5(2(x1))))))
, 5(1(3(0(2(x1))))) -> 5(0(1(0(3(2(x1))))))
, 5(1(3(0(2(x1))))) -> 5(0(1(1(2(3(x1))))))
, 5(1(3(2(0(x1))))) -> 5(3(1(5(2(0(x1))))))
, 5(1(3(2(3(x1))))) -> 3(4(3(5(1(2(x1))))))
, 5(1(4(5(2(x1))))) -> 5(1(4(1(5(2(x1))))))
, 5(5(1(3(2(x1))))) -> 3(5(5(4(1(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(0(0(x1))) -> 0(0(1(0(2(x1)))))
, 0(3(2(x1))) -> 4(3(0(2(x1))))
, 0(0(4(2(x1)))) -> 0(4(1(0(2(x1)))))
, 0(0(5(2(x1)))) -> 5(0(2(3(0(x1)))))
, 0(1(3(2(x1)))) -> 0(3(1(0(2(x1)))))
, 0(1(3(2(x1)))) -> 3(1(1(0(2(x1)))))
, 0(1(3(2(x1)))) -> 0(1(4(3(1(2(x1))))))
, 0(4(1(3(x1)))) -> 1(4(3(0(2(2(x1))))))
, 0(4(2(3(x1)))) -> 5(4(3(0(2(x1)))))
, 0(4(5(2(x1)))) -> 5(0(2(2(4(2(x1))))))
, 0(5(1(3(x1)))) -> 3(0(1(5(1(2(x1))))))
, 0(5(3(0(x1)))) -> 5(0(1(4(3(0(x1))))))
, 0(5(3(2(x1)))) -> 5(1(5(0(2(3(x1))))))
, 4(0(2(3(x1)))) -> 3(4(3(0(2(x1)))))
, 4(0(2(3(x1)))) -> 4(3(5(0(2(x1)))))
, 4(4(1(3(x1)))) -> 4(3(4(1(2(2(x1))))))
, 4(5(2(0(x1)))) -> 4(2(1(5(0(2(x1))))))
, 4(5(2(0(x1)))) -> 5(1(0(2(2(4(x1))))))
, 5(1(0(0(x1)))) -> 5(1(0(2(0(x1)))))
, 5(1(0(0(x1)))) -> 5(2(1(0(2(0(x1))))))
, 5(1(3(0(x1)))) -> 5(0(2(1(3(x1)))))
, 5(1(3(2(x1)))) -> 3(0(1(5(1(2(x1))))))
, 5(1(3(2(x1)))) -> 3(1(1(5(2(2(x1))))))
, 5(3(0(0(x1)))) -> 5(0(4(3(0(2(x1))))))
, 0(0(4(1(3(x1))))) -> 4(0(1(0(2(3(x1))))))
, 0(0(4(5(2(x1))))) -> 5(0(1(0(2(4(x1))))))
, 0(0(5(3(2(x1))))) -> 0(1(5(0(2(3(x1))))))
, 0(1(0(5(2(x1))))) -> 1(0(2(5(1(0(x1))))))
, 0(1(4(5(2(x1))))) -> 2(1(5(0(2(4(x1))))))
, 0(3(1(4(0(x1))))) -> 4(1(0(1(0(3(x1))))))
, 0(3(2(0(0(x1))))) -> 0(0(1(0(2(3(x1))))))
, 0(3(4(0(2(x1))))) -> 4(3(0(2(1(0(x1))))))
, 0(3(4(0(2(x1))))) -> 4(3(0(2(3(0(x1))))))
, 0(3(4(4(2(x1))))) -> 4(0(3(4(2(2(x1))))))
, 0(4(2(5(3(x1))))) -> 0(4(3(5(1(2(x1))))))
, 0(5(1(2(0(x1))))) -> 3(0(1(5(0(2(x1))))))
, 4(4(2(2(0(x1))))) -> 4(1(0(2(2(4(x1))))))
, 4(5(1(2(0(x1))))) -> 5(0(4(1(2(2(x1))))))
, 4(5(2(3(2(x1))))) -> 5(4(3(5(2(2(x1))))))
, 5(1(0(3(2(x1))))) -> 5(0(3(1(0(2(x1))))))
, 5(1(0(5(3(x1))))) -> 5(5(0(1(3(1(x1))))))
, 5(1(3(0(0(x1))))) -> 3(5(0(1(2(0(x1))))))
, 5(1(3(0(2(x1))))) -> 3(0(2(1(5(2(x1))))))
, 5(1(3(0(2(x1))))) -> 5(0(1(0(3(2(x1))))))
, 5(1(3(0(2(x1))))) -> 5(0(1(1(2(3(x1))))))
, 5(1(3(2(0(x1))))) -> 5(3(1(5(2(0(x1))))))
, 5(1(3(2(3(x1))))) -> 3(4(3(5(1(2(x1))))))
, 5(1(4(5(2(x1))))) -> 5(1(4(1(5(2(x1))))))
, 5(5(1(3(2(x1))))) -> 3(5(5(4(1(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(5) -> 4
, 0_1(6) -> 1
, 0_1(12) -> 8
, 1_0(2) -> 2
, 1_1(4) -> 7
, 1_1(5) -> 11
, 1_1(7) -> 8
, 1_1(9) -> 6
, 1_1(13) -> 12
, 2_0(2) -> 2
, 2_1(2) -> 5
, 2_1(5) -> 14
, 3_0(2) -> 2
, 3_1(4) -> 3
, 3_1(7) -> 6
, 3_1(8) -> 1
, 3_1(11) -> 10
, 3_1(13) -> 15
, 4_0(2) -> 1
, 4_1(3) -> 1
, 4_1(10) -> 9
, 4_1(15) -> 8
, 5_0(2) -> 1
, 5_1(11) -> 13
, 5_1(14) -> 4}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(0(0(x1))) -> 0(0(1(0(2(x1)))))
, 0(3(2(x1))) -> 4(3(0(2(x1))))
, 0(0(4(2(x1)))) -> 0(4(1(0(2(x1)))))
, 0(0(5(2(x1)))) -> 5(0(2(3(0(x1)))))
, 0(1(3(2(x1)))) -> 0(3(1(0(2(x1)))))
, 0(1(3(2(x1)))) -> 3(1(1(0(2(x1)))))
, 0(1(3(2(x1)))) -> 0(1(4(3(1(2(x1))))))
, 0(4(1(3(x1)))) -> 1(4(3(0(2(2(x1))))))
, 0(4(2(3(x1)))) -> 5(4(3(0(2(x1)))))
, 0(4(5(2(x1)))) -> 5(0(2(2(4(2(x1))))))
, 0(5(1(3(x1)))) -> 3(0(1(5(1(2(x1))))))
, 0(5(3(0(x1)))) -> 5(0(1(4(3(0(x1))))))
, 0(5(3(2(x1)))) -> 5(1(5(0(2(3(x1))))))
, 4(0(2(3(x1)))) -> 3(4(3(0(2(x1)))))
, 4(0(2(3(x1)))) -> 4(3(5(0(2(x1)))))
, 4(4(1(3(x1)))) -> 4(3(4(1(2(2(x1))))))
, 4(5(2(0(x1)))) -> 4(2(1(5(0(2(x1))))))
, 4(5(2(0(x1)))) -> 5(1(0(2(2(4(x1))))))
, 5(1(0(0(x1)))) -> 5(1(0(2(0(x1)))))
, 5(1(0(0(x1)))) -> 5(2(1(0(2(0(x1))))))
, 5(1(3(0(x1)))) -> 5(0(2(1(3(x1)))))
, 5(1(3(2(x1)))) -> 3(0(1(5(1(2(x1))))))
, 5(1(3(2(x1)))) -> 3(1(1(5(2(2(x1))))))
, 5(3(0(0(x1)))) -> 5(0(4(3(0(2(x1))))))
, 0(0(4(1(3(x1))))) -> 4(0(1(0(2(3(x1))))))
, 0(0(4(5(2(x1))))) -> 5(0(1(0(2(4(x1))))))
, 0(0(5(3(2(x1))))) -> 0(1(5(0(2(3(x1))))))
, 0(1(0(5(2(x1))))) -> 1(0(2(5(1(0(x1))))))
, 0(1(4(5(2(x1))))) -> 2(1(5(0(2(4(x1))))))
, 0(3(1(4(0(x1))))) -> 4(1(0(1(0(3(x1))))))
, 0(3(2(0(0(x1))))) -> 0(0(1(0(2(3(x1))))))
, 0(3(4(0(2(x1))))) -> 4(3(0(2(1(0(x1))))))
, 0(3(4(0(2(x1))))) -> 4(3(0(2(3(0(x1))))))
, 0(3(4(4(2(x1))))) -> 4(0(3(4(2(2(x1))))))
, 0(4(2(5(3(x1))))) -> 0(4(3(5(1(2(x1))))))
, 0(5(1(2(0(x1))))) -> 3(0(1(5(0(2(x1))))))
, 4(4(2(2(0(x1))))) -> 4(1(0(2(2(4(x1))))))
, 4(5(1(2(0(x1))))) -> 5(0(4(1(2(2(x1))))))
, 4(5(2(3(2(x1))))) -> 5(4(3(5(2(2(x1))))))
, 5(1(0(3(2(x1))))) -> 5(0(3(1(0(2(x1))))))
, 5(1(0(5(3(x1))))) -> 5(5(0(1(3(1(x1))))))
, 5(1(3(0(0(x1))))) -> 3(5(0(1(2(0(x1))))))
, 5(1(3(0(2(x1))))) -> 3(0(2(1(5(2(x1))))))
, 5(1(3(0(2(x1))))) -> 5(0(1(0(3(2(x1))))))
, 5(1(3(0(2(x1))))) -> 5(0(1(1(2(3(x1))))))
, 5(1(3(2(0(x1))))) -> 5(3(1(5(2(0(x1))))))
, 5(1(3(2(3(x1))))) -> 3(4(3(5(1(2(x1))))))
, 5(1(4(5(2(x1))))) -> 5(1(4(1(5(2(x1))))))
, 5(5(1(3(2(x1))))) -> 3(5(5(4(1(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(0(0(x1))) -> 0(0(1(0(2(x1)))))
, 0(3(2(x1))) -> 4(3(0(2(x1))))
, 0(0(4(2(x1)))) -> 0(4(1(0(2(x1)))))
, 0(0(5(2(x1)))) -> 5(0(2(3(0(x1)))))
, 0(1(3(2(x1)))) -> 0(3(1(0(2(x1)))))
, 0(1(3(2(x1)))) -> 3(1(1(0(2(x1)))))
, 0(1(3(2(x1)))) -> 0(1(4(3(1(2(x1))))))
, 0(4(1(3(x1)))) -> 1(4(3(0(2(2(x1))))))
, 0(4(2(3(x1)))) -> 5(4(3(0(2(x1)))))
, 0(4(5(2(x1)))) -> 5(0(2(2(4(2(x1))))))
, 0(5(1(3(x1)))) -> 3(0(1(5(1(2(x1))))))
, 0(5(3(0(x1)))) -> 5(0(1(4(3(0(x1))))))
, 0(5(3(2(x1)))) -> 5(1(5(0(2(3(x1))))))
, 4(0(2(3(x1)))) -> 3(4(3(0(2(x1)))))
, 4(0(2(3(x1)))) -> 4(3(5(0(2(x1)))))
, 4(4(1(3(x1)))) -> 4(3(4(1(2(2(x1))))))
, 4(5(2(0(x1)))) -> 4(2(1(5(0(2(x1))))))
, 4(5(2(0(x1)))) -> 5(1(0(2(2(4(x1))))))
, 5(1(0(0(x1)))) -> 5(1(0(2(0(x1)))))
, 5(1(0(0(x1)))) -> 5(2(1(0(2(0(x1))))))
, 5(1(3(0(x1)))) -> 5(0(2(1(3(x1)))))
, 5(1(3(2(x1)))) -> 3(0(1(5(1(2(x1))))))
, 5(1(3(2(x1)))) -> 3(1(1(5(2(2(x1))))))
, 5(3(0(0(x1)))) -> 5(0(4(3(0(2(x1))))))
, 0(0(4(1(3(x1))))) -> 4(0(1(0(2(3(x1))))))
, 0(0(4(5(2(x1))))) -> 5(0(1(0(2(4(x1))))))
, 0(0(5(3(2(x1))))) -> 0(1(5(0(2(3(x1))))))
, 0(1(0(5(2(x1))))) -> 1(0(2(5(1(0(x1))))))
, 0(1(4(5(2(x1))))) -> 2(1(5(0(2(4(x1))))))
, 0(3(1(4(0(x1))))) -> 4(1(0(1(0(3(x1))))))
, 0(3(2(0(0(x1))))) -> 0(0(1(0(2(3(x1))))))
, 0(3(4(0(2(x1))))) -> 4(3(0(2(1(0(x1))))))
, 0(3(4(0(2(x1))))) -> 4(3(0(2(3(0(x1))))))
, 0(3(4(4(2(x1))))) -> 4(0(3(4(2(2(x1))))))
, 0(4(2(5(3(x1))))) -> 0(4(3(5(1(2(x1))))))
, 0(5(1(2(0(x1))))) -> 3(0(1(5(0(2(x1))))))
, 4(4(2(2(0(x1))))) -> 4(1(0(2(2(4(x1))))))
, 4(5(1(2(0(x1))))) -> 5(0(4(1(2(2(x1))))))
, 4(5(2(3(2(x1))))) -> 5(4(3(5(2(2(x1))))))
, 5(1(0(3(2(x1))))) -> 5(0(3(1(0(2(x1))))))
, 5(1(0(5(3(x1))))) -> 5(5(0(1(3(1(x1))))))
, 5(1(3(0(0(x1))))) -> 3(5(0(1(2(0(x1))))))
, 5(1(3(0(2(x1))))) -> 3(0(2(1(5(2(x1))))))
, 5(1(3(0(2(x1))))) -> 5(0(1(0(3(2(x1))))))
, 5(1(3(0(2(x1))))) -> 5(0(1(1(2(3(x1))))))
, 5(1(3(2(0(x1))))) -> 5(3(1(5(2(0(x1))))))
, 5(1(3(2(3(x1))))) -> 3(4(3(5(1(2(x1))))))
, 5(1(4(5(2(x1))))) -> 5(1(4(1(5(2(x1))))))
, 5(5(1(3(2(x1))))) -> 3(5(5(4(1(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(5) -> 4
, 0_1(6) -> 1
, 0_1(12) -> 8
, 1_0(2) -> 2
, 1_1(4) -> 7
, 1_1(5) -> 11
, 1_1(7) -> 8
, 1_1(9) -> 6
, 1_1(13) -> 12
, 2_0(2) -> 2
, 2_1(2) -> 5
, 2_1(5) -> 14
, 3_0(2) -> 2
, 3_1(4) -> 3
, 3_1(7) -> 6
, 3_1(8) -> 1
, 3_1(11) -> 10
, 3_1(13) -> 15
, 4_0(2) -> 1
, 4_1(3) -> 1
, 4_1(10) -> 9
, 4_1(15) -> 8
, 5_0(2) -> 1
, 5_1(11) -> 13
, 5_1(14) -> 4}