Tool CaT
stdout:
YES(?,O(n^1))
Problem:
twoto(0(x1)) -> p(p(s(s(s(p(p(p(s(s(s(0(p(p(s(s(x1))))))))))))))))
twoto(s(x1)) ->
p(p(s(s(p(p(p(s(s(s(twice(p(p(s(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))
twice(0(x1)) -> p(s(p(s(0(s(p(s(s(s(s(p(s(x1)))))))))))))
twice(s(x1)) -> s(p(p(p(p(s(s(s(s(s(twice(p(s(p(s(p(s(p(s(x1)))))))))))))))))))
p(p(s(x1))) -> p(x1)
p(s(x1)) -> x1
p(0(x1)) -> 0(s(s(s(s(p(s(x1)))))))
0(x1) -> x1
Proof:
Bounds Processor:
bound: 2
enrichment: match
automaton:
final states: {5,4,3,2}
transitions:
s1(65) -> 66*
s1(60) -> 61*
s1(55) -> 56*
s1(50) -> 51*
s1(45) -> 46*
s1(40) -> 41*
s1(35) -> 36*
s1(67) -> 68*
s1(62) -> 63*
s1(74) -> 75*
s1(69) -> 70*
s1(49) -> 50*
s1(44) -> 45*
s1(39) -> 40*
s1(66) -> 67*
s1(56) -> 57*
s1(51) -> 52*
s1(68) -> 69*
s1(38) -> 39*
s1(33) -> 34*
p1(70) -> 71*
p1(72) -> 73*
p1(57) -> 58*
p1(52) -> 53*
p1(47) -> 48*
p1(42) -> 43*
p1(54) -> 55*
p1(34) -> 35*
p1(71) -> 72*
p1(61) -> 62*
p1(46) -> 47*
p1(41) -> 42*
p1(36) -> 37*
p1(73) -> 74*
p1(63) -> 64*
p1(58) -> 59*
p1(53) -> 54*
p1(43) -> 44*
twice1(64) -> 65*
twice1(48) -> 49*
twoto1(37) -> 38*
p2(122) -> 123*
p2(102) -> 103*
p2(124) -> 125*
p2(114) -> 115*
p2(104) -> 105*
p2(94) -> 95*
p2(116) -> 117*
p2(96) -> 97*
p2(110) -> 111*
twoto0(1) -> 2*
00(1) -> 5*
p0(1) -> 4*
s0(1) -> 1*
twice0(1) -> 3*
1 -> 5,4,33
33 -> 35*
35 -> 37*
37 -> 60*
38 -> 117*
39 -> 95,43,116
40 -> 42,94
44 -> 111,48
45 -> 47,110
49 -> 115,55,97
50 -> 103,54,114
51 -> 53,102
55 -> 97*
56 -> 58,96
59 -> 38,2
60 -> 62*
62 -> 64*
66 -> 125,74
67 -> 123,73,124
68 -> 105,122
69 -> 71,104
75 -> 65,3
95 -> 43*
97 -> 59*
103 -> 54*
105 -> 72*
111 -> 48*
115 -> 55*
117 -> 44*
123 -> 73*
125 -> 74*
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:
{ twoto(0(x1)) ->
p(p(s(s(s(p(p(p(s(s(s(0(p(p(s(s(x1))))))))))))))))
, twoto(s(x1)) ->
p(p(s(s(p(p(p(s(s(s(twice(p(p(s(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))
, twice(0(x1)) -> p(s(p(s(0(s(p(s(s(s(s(p(s(x1)))))))))))))
, twice(s(x1)) ->
s(p(p(p(p(s(s(s(s(s(twice(p(s(p(s(p(s(p(s(x1)))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(p(s(x1)))))))
, 0(x1) -> 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:
{ twoto(0(x1)) ->
p(p(s(s(s(p(p(p(s(s(s(0(p(p(s(s(x1))))))))))))))))
, twoto(s(x1)) ->
p(p(s(s(p(p(p(s(s(s(twice(p(p(s(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))
, twice(0(x1)) -> p(s(p(s(0(s(p(s(s(s(s(p(s(x1)))))))))))))
, twice(s(x1)) ->
s(p(p(p(p(s(s(s(s(s(twice(p(s(p(s(p(s(p(s(x1)))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(p(s(x1)))))))
, 0(x1) -> x1}
Proof Output:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ twoto_0(4) -> 1
, twoto_1(27) -> 16
, twoto_1(27) -> 20
, twoto_1(27) -> 26
, 0_0(4) -> 2
, p_0(4) -> 3
, p_1(6) -> 1
, p_1(6) -> 16
, p_1(6) -> 20
, p_1(6) -> 26
, p_1(7) -> 6
, p_1(10) -> 1
, p_1(10) -> 9
, p_1(10) -> 16
, p_1(10) -> 20
, p_1(10) -> 26
, p_1(11) -> 10
, p_1(12) -> 11
, p_1(17) -> 16
, p_1(18) -> 17
, p_1(21) -> 16
, p_1(21) -> 20
, p_1(22) -> 21
, p_1(23) -> 22
, p_1(28) -> 27
, p_1(28) -> 41
, p_1(28) -> 43
, p_1(30) -> 27
, p_1(30) -> 29
, p_1(30) -> 41
, p_1(30) -> 43
, p_1(32) -> 31
, p_1(33) -> 32
, p_1(34) -> 33
, p_1(35) -> 34
, p_1(42) -> 41
, p_1(44) -> 41
, p_1(44) -> 43
, p_2(8) -> 1
, p_2(8) -> 16
, p_2(8) -> 20
, p_2(8) -> 26
, p_2(13) -> 10
, p_2(14) -> 1
, p_2(14) -> 9
, p_2(14) -> 16
, p_2(14) -> 20
, p_2(14) -> 26
, p_2(19) -> 16
, p_2(24) -> 21
, p_2(25) -> 16
, p_2(25) -> 20
, p_2(36) -> 33
, p_2(37) -> 32
, p_2(38) -> 31
, s_0(4) -> 2
, s_0(4) -> 3
, s_0(4) -> 4
, s_0(4) -> 27
, s_0(4) -> 29
, s_0(4) -> 41
, s_0(4) -> 43
, s_1(4) -> 30
, s_1(8) -> 7
, s_1(9) -> 6
, s_1(9) -> 8
, s_1(13) -> 12
, s_1(14) -> 11
, s_1(14) -> 13
, s_1(15) -> 10
, s_1(15) -> 14
, s_1(19) -> 18
, s_1(20) -> 17
, s_1(20) -> 19
, s_1(24) -> 23
, s_1(25) -> 22
, s_1(25) -> 24
, s_1(26) -> 21
, s_1(26) -> 25
, s_1(27) -> 44
, s_1(29) -> 28
, s_1(31) -> 5
, s_1(31) -> 40
, s_1(36) -> 35
, s_1(37) -> 34
, s_1(37) -> 36
, s_1(38) -> 33
, s_1(38) -> 37
, s_1(39) -> 32
, s_1(39) -> 38
, s_1(40) -> 31
, s_1(40) -> 39
, s_1(43) -> 42
, twice_0(4) -> 5
, twice_1(16) -> 1
, twice_1(16) -> 9
, twice_1(16) -> 15
, twice_1(16) -> 16
, twice_1(16) -> 20
, twice_1(16) -> 26
, twice_1(41) -> 40}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:
{ twoto(0(x1)) ->
p(p(s(s(s(p(p(p(s(s(s(0(p(p(s(s(x1))))))))))))))))
, twoto(s(x1)) ->
p(p(s(s(p(p(p(s(s(s(twice(p(p(s(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))
, twice(0(x1)) -> p(s(p(s(0(s(p(s(s(s(s(p(s(x1)))))))))))))
, twice(s(x1)) ->
s(p(p(p(p(s(s(s(s(s(twice(p(s(p(s(p(s(p(s(x1)))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(p(s(x1)))))))
, 0(x1) -> 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:
{ twoto(0(x1)) ->
p(p(s(s(s(p(p(p(s(s(s(0(p(p(s(s(x1))))))))))))))))
, twoto(s(x1)) ->
p(p(s(s(p(p(p(s(s(s(twice(p(p(s(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))
, twice(0(x1)) -> p(s(p(s(0(s(p(s(s(s(s(p(s(x1)))))))))))))
, twice(s(x1)) ->
s(p(p(p(p(s(s(s(s(s(twice(p(s(p(s(p(s(p(s(x1)))))))))))))))))))
, p(p(s(x1))) -> p(x1)
, p(s(x1)) -> x1
, p(0(x1)) -> 0(s(s(s(s(p(s(x1)))))))
, 0(x1) -> x1}
Proof Output:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ twoto_0(2) -> 1
, twoto_1(24) -> 13
, twoto_1(24) -> 17
, twoto_1(24) -> 23
, 0_0(2) -> 1
, p_0(2) -> 1
, p_1(3) -> 1
, p_1(3) -> 13
, p_1(3) -> 17
, p_1(3) -> 23
, p_1(4) -> 3
, p_1(7) -> 1
, p_1(7) -> 6
, p_1(7) -> 13
, p_1(7) -> 17
, p_1(7) -> 23
, p_1(8) -> 7
, p_1(9) -> 8
, p_1(14) -> 13
, p_1(15) -> 14
, p_1(18) -> 13
, p_1(18) -> 17
, p_1(19) -> 18
, p_1(20) -> 19
, p_1(25) -> 24
, p_1(25) -> 38
, p_1(25) -> 40
, p_1(27) -> 24
, p_1(27) -> 26
, p_1(27) -> 38
, p_1(27) -> 40
, p_1(29) -> 28
, p_1(30) -> 29
, p_1(31) -> 30
, p_1(32) -> 31
, p_1(39) -> 38
, p_1(41) -> 38
, p_1(41) -> 40
, p_2(5) -> 1
, p_2(5) -> 13
, p_2(5) -> 17
, p_2(5) -> 23
, p_2(10) -> 7
, p_2(11) -> 1
, p_2(11) -> 6
, p_2(11) -> 13
, p_2(11) -> 17
, p_2(11) -> 23
, p_2(16) -> 13
, p_2(21) -> 18
, p_2(22) -> 13
, p_2(22) -> 17
, p_2(33) -> 30
, p_2(34) -> 29
, p_2(35) -> 28
, s_0(2) -> 1
, s_0(2) -> 2
, s_0(2) -> 24
, s_0(2) -> 26
, s_0(2) -> 38
, s_0(2) -> 40
, s_1(2) -> 27
, s_1(5) -> 4
, s_1(6) -> 3
, s_1(6) -> 5
, s_1(10) -> 9
, s_1(11) -> 8
, s_1(11) -> 10
, s_1(12) -> 7
, s_1(12) -> 11
, s_1(16) -> 15
, s_1(17) -> 14
, s_1(17) -> 16
, s_1(21) -> 20
, s_1(22) -> 19
, s_1(22) -> 21
, s_1(23) -> 18
, s_1(23) -> 22
, s_1(24) -> 41
, s_1(26) -> 25
, s_1(28) -> 1
, s_1(28) -> 37
, s_1(33) -> 32
, s_1(34) -> 31
, s_1(34) -> 33
, s_1(35) -> 30
, s_1(35) -> 34
, s_1(36) -> 29
, s_1(36) -> 35
, s_1(37) -> 28
, s_1(37) -> 36
, s_1(40) -> 39
, twice_0(2) -> 1
, twice_1(13) -> 1
, twice_1(13) -> 6
, twice_1(13) -> 12
, twice_1(13) -> 13
, twice_1(13) -> 17
, twice_1(13) -> 23
, twice_1(38) -> 37}