Tool CaT
stdout:
YES(?,O(n^1))
Problem:
0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))
0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x1)))))))))))))
Proof:
Bounds Processor:
bound: 2
enrichment: match
automaton:
final states: {3}
transitions:
11(22) -> 23*
11(24) -> 25*
11(19) -> 20*
11(21) -> 22*
11(16) -> 17*
21(15) -> 16*
21(32) -> 33*
21(26) -> 27*
21(23) -> 24*
21(18) -> 19*
01(20) -> 21*
01(17) -> 18*
12(52) -> 53*
12(54) -> 55*
12(49) -> 50*
12(51) -> 52*
12(46) -> 47*
00(2) -> 3*
00(1) -> 3*
22(60) -> 61*
22(45) -> 46*
22(58) -> 59*
22(53) -> 54*
22(48) -> 49*
10(2) -> 1*
10(1) -> 1*
02(50) -> 51*
02(47) -> 48*
20(2) -> 2*
20(1) -> 2*
1 -> 26*
2 -> 15*
21 -> 32*
24 -> 45*
25 -> 18,3
27 -> 16*
33 -> 19*
51 -> 58*
54 -> 60*
55 -> 21,32
59 -> 49*
61 -> 46*
problem:
QedTool IRC1
stdout:
YES(?,O(n^1))
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(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))
, 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(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(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))
, 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(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_1(7) -> 6
, 0_1(10) -> 9
, 0_2(16) -> 15
, 0_2(19) -> 18
, 1_0(2) -> 2
, 1_1(3) -> 1
, 1_1(3) -> 9
, 1_1(5) -> 4
, 1_1(6) -> 5
, 1_1(8) -> 7
, 1_1(11) -> 10
, 1_2(12) -> 6
, 1_2(14) -> 13
, 1_2(15) -> 14
, 1_2(17) -> 16
, 1_2(20) -> 19
, 2_0(2) -> 2
, 2_1(2) -> 11
, 2_1(4) -> 3
, 2_1(6) -> 8
, 2_1(9) -> 8
, 2_2(3) -> 20
, 2_2(12) -> 17
, 2_2(13) -> 12
, 2_2(15) -> 17
, 2_2(18) -> 17}Tool RC1
stdout:
YES(?,O(n^1))
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(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))
, 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(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(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))
, 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(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_1(7) -> 6
, 0_1(10) -> 9
, 0_2(16) -> 15
, 0_2(19) -> 18
, 1_0(2) -> 2
, 1_1(3) -> 1
, 1_1(3) -> 9
, 1_1(5) -> 4
, 1_1(6) -> 5
, 1_1(8) -> 7
, 1_1(11) -> 10
, 1_2(12) -> 6
, 1_2(14) -> 13
, 1_2(15) -> 14
, 1_2(17) -> 16
, 1_2(20) -> 19
, 2_0(2) -> 2
, 2_1(2) -> 11
, 2_1(4) -> 3
, 2_1(6) -> 8
, 2_1(9) -> 8
, 2_2(3) -> 20
, 2_2(12) -> 17
, 2_2(13) -> 12
, 2_2(15) -> 17
, 2_2(18) -> 17}