1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
|
(*************************************************************)
(* This file is distributed under the terms of the *)
(* GNU Lesser General Public License Version 2.1 *)
(*************************************************************)
(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *)
(*************************************************************)
Require Import Lucas.
Eval vm_compute in 2.
Time Eval vm_compute in lucas 2.
Eval vm_compute in 3.
Time Eval vm_compute in lucas 3.
Eval vm_compute in 5.
Time Eval vm_compute in lucas 5.
Eval vm_compute in 7.
Time Eval vm_compute in lucas 7.
Eval vm_compute in 13.
Time Eval vm_compute in lucas 13.
Eval vm_compute in 17.
Time Eval vm_compute in lucas 17.
Eval vm_compute in 19.
Time Eval vm_compute in lucas 19.
Eval vm_compute in 31.
Time Eval vm_compute in lucas 31.
Eval vm_compute in 61.
Time Eval vm_compute in lucas 61.
Eval vm_compute in 89.
Time Eval vm_compute in lucas 89.
Eval vm_compute in 107.
Time Eval vm_compute in lucas 107.
Eval vm_compute in 127.
Time Eval vm_compute in lucas 127.
Eval vm_compute in 521.
Time Eval vm_compute in lucas 521.
Eval vm_compute in 607.
Time Eval vm_compute in lucas 607.
Eval vm_compute in 1279.
Time Eval vm_compute in lucas 1279.
Eval vm_compute in 2203.
Time Eval vm_compute in lucas 2203.
Eval vm_compute in 2281.
Time Eval vm_compute in lucas 2281.
Eval vm_compute in 3217.
Time Eval vm_compute in lucas 3217.
Eval vm_compute in 4253.
Time Eval vm_compute in lucas 4253.
Eval vm_compute in 4423.
Time Eval vm_compute in lucas 4423.
(*
= 3
= 0
Finished transaction in 0. secs (0.01u,0.s)
= 5
= 0
Finished transaction in 0. secs (0.u,0.s)
= 7
= 0
Finished transaction in 0. secs (0.u,0.s)
= 13
= 0
Finished transaction in 0. secs (0.u,0.s)
= 17
= 0
Finished transaction in 0. secs (0.u,0.s)
= 19
= 0
Finished transaction in 0. secs (0.u,0.s)
= 31
= 0
Finished transaction in 0. secs (0.u,0.s)
= 61
= 0
Finished transaction in 0. secs (0.01u,0.s)
= 89
= 0
Finished transaction in 0. secs (0.02u,0.s)
= 107
= 0
Finished transaction in 0. secs (0.02u,0.s)
= 127
= 0
Finished transaction in 0. secs (0.04u,0.s)
= 521
= 0
Finished transaction in 2. secs (1.85u,0.01s)
= 607
= 0
Finished transaction in 3. secs (2.78u,0.07s)
= 1279
= 0
Finished transaction in 21. secs (20.21u,0.26s)
= 2203
= 0
Finished transaction in 94. secs (89.1u,1.05s)
= 2281
= 0
Finished transaction in 102. secs (97.59u,1.1s)
= 3217
= 0
Finished transaction in 244. secs (237.65u,2.39s)
= 4253
= 0
Finished transaction in 506. secs (494.09u,4.65s)
= 4423
= 0
Finished transaction in 572. secs (563.27u,5.45s)
*)
|
