Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / oversampling / wp9.script @ 6a93d814

History | View | Annotate | Download (6.46 KB)

1 6a93d814 xthirioux
(* Generated by Frama-C WP *)
2
3
Goal typed_f_reset_post.
4
Hint default,f_reset,property.
5
Proof.
6
(* auto with zarith. *)
7
Qed.
8
9
Goal typed_f_step_assert.
10
Hint f_step,property.
11
Proof.
12
  auto with zarith.
13
Qed.
14
15
Goal typed_f_step_assert_2.
16
Hint f_step,property.
17
Proof.
18
(* --------------------------------------
19
  
20
From 'typed_f_step_post': 
21
  auto with zarith.
22
*)
23
(* --------------------------------------
24
  
25
From 'typed_f_step_assert': 
26
  auto with zarith.
27
*)
28
Qed.
29
30
Goal typed_f_step_assert_3.
31
Hint f_step,property.
32
Proof.
33
(* --------------------------------------
34
  
35
From 'typed_f_step_post': 
36
  auto with zarith.
37
*)
38
(* --------------------------------------
39
  
40
From 'typed_f_step_assert': 
41
  auto with zarith.
42
*)
43
Qed.
44
45
Goal typed_f_step_assert_4.
46
Hint f_step,property.
47
Proof.
48
(* --------------------------------------
49
  
50
From 'typed_f_step_post': 
51
  auto with zarith.
52
*)
53
(* --------------------------------------
54
  
55
From 'typed_f_step_assert': 
56
  auto with zarith.
57
*)
58
Qed.
59
60
Goal typed_f_step_assert_5.
61
Hint f_step,property.
62
Proof.
63
(* --------------------------------------
64
  
65
From 'typed_f_step_post': 
66
  auto with zarith.
67
*)
68
(* --------------------------------------
69
  
70
From 'typed_f_step_assert': 
71
  auto with zarith.
72
*)
73
Qed.
74
75
Goal typed_f_step_assert_6.
76
Hint f_step,property.
77
Proof.
78
(* --------------------------------------
79
  
80
From 'typed_f_step_post': 
81
  auto with zarith.
82
*)
83
(* --------------------------------------
84
  
85
From 'typed_f_step_assert': 
86
  auto with zarith.
87
*)
88
(* --------------------------------------
89
  
90
From 'typed_f_step_assert_4': 
91
(* --------------------------------------
92
  
93
From 'typed_f_step_post': 
94
  auto with zarith.
95
*)
96
(* --------------------------------------
97
  
98
From 'typed_f_step_assert': 
99
  auto with zarith.
100
*)
101
*)
102
Qed.
103
104
Goal typed_f_step_post.
105
Hint default,f_step,property.
106
Proof.
107
  auto with zarith.
108
Qed.
109
110
Goal typed_g_reset_call_f_reset_pre.
111
Hint g_reset,precond-f_reset.
112
Proof.
113
(* auto with zarith. *)
114
Qed.
115
116
Goal typed_g_reset_post.
117
Hint default,g_reset,property.
118
Proof.
119
(* auto with zarith. *)
120
Qed.
121
122
Goal typed_g_step_assert.
123
Hint g_step,property.
124
Proof.
125
  auto with zarith.
126
Qed.
127
128
Goal typed_g_step_assert_2.
129
Hint g_step,property.
130
Proof.
131
(* --------------------------------------
132
  
133
From 'typed_g_step_assert': 
134
  auto with zarith.
135
*)
136
(* --------------------------------------
137
  
138
From 'typed_g_step_post': 
139
  auto with zarith.
140
*)
141
Qed.
142
143
Goal typed_g_step_assert_3.
144
Hint g_step,property.
145
Proof.
146
(* --------------------------------------
147
  
148
From 'typed_g_step_assert': 
149
  auto with zarith.
150
*)
151
(* --------------------------------------
152
  
153
From 'typed_g_step_post': 
154
  auto with zarith.
155
*)
156
Qed.
157
158
Goal typed_g_step_assert_4.
159
Hint g_step,property.
160
Proof.
161
(* --------------------------------------
162
  
163
From 'typed_g_step_assert': 
164
  auto with zarith.
165
*)
166
(* --------------------------------------
167
  
168
From 'typed_g_step_assert_3': 
169
(* --------------------------------------
170
  
171
From 'typed_g_step_assert': 
172
  auto with zarith.
173
*)
174
(* --------------------------------------
175
  
176
From 'typed_g_step_post': 
177
  auto with zarith.
178
*)
179
*)
180
(* --------------------------------------
181
  
182
From 'typed_g_step_assert_2': 
183
(* --------------------------------------
184
  
185
From 'typed_g_step_assert': 
186
  auto with zarith.
187
*)
188
(* --------------------------------------
189
  
190
From 'typed_g_step_post': 
191
  auto with zarith.
192
*)
193
*)
194
Qed.
195
196
Goal typed_g_step_assert_5.
197
Hint g_step,property.
198
Proof.
199
(* --------------------------------------
200
  
201
From 'typed_g_step_assert': 
202
  auto with zarith.
203
*)
204
(* --------------------------------------
205
  
206
From 'typed_g_step_assert_3': 
207
(* --------------------------------------
208
  
209
From 'typed_g_step_assert': 
210
  auto with zarith.
211
*)
212
(* --------------------------------------
213
  
214
From 'typed_g_step_post': 
215
  auto with zarith.
216
*)
217
*)
218
(* --------------------------------------
219
  
220
From 'typed_g_step_assert_2': 
221
(* --------------------------------------
222
  
223
From 'typed_g_step_assert': 
224
  auto with zarith.
225
*)
226
(* --------------------------------------
227
  
228
From 'typed_g_step_post': 
229
  auto with zarith.
230
*)
231
*)
232
Qed.
233
234
Goal typed_g_step_assert_6.
235
Hint g_step,property.
236
Proof.
237
(* --------------------------------------
238
  
239
From 'typed_g_step_assert': 
240
  auto with zarith.
241
*)
242
(* --------------------------------------
243
  
244
From 'typed_g_step_assert_4': 
245
(* --------------------------------------
246
  
247
From 'typed_g_step_assert': 
248
  auto with zarith.
249
*)
250
(* --------------------------------------
251
  
252
From 'typed_g_step_assert_3': 
253
(* --------------------------------------
254
  
255
From 'typed_g_step_assert': 
256
  auto with zarith.
257
*)
258
(* --------------------------------------
259
  
260
From 'typed_g_step_post': 
261
  auto with zarith.
262
*)
263
*)
264
(* --------------------------------------
265
  
266
From 'typed_g_step_assert_2': 
267
(* --------------------------------------
268
  
269
From 'typed_g_step_assert': 
270
  auto with zarith.
271
*)
272
(* --------------------------------------
273
  
274
From 'typed_g_step_post': 
275
  auto with zarith.
276
*)
277
*)
278
*)
279
(* --------------------------------------
280
  
281
From 'typed_g_step_assert_3': 
282
(* --------------------------------------
283
  
284
From 'typed_g_step_assert': 
285
  auto with zarith.
286
*)
287
(* --------------------------------------
288
  
289
From 'typed_g_step_post': 
290
  auto with zarith.
291
*)
292
*)
293
Qed.
294
295
Goal typed_g_step_assert_7.
296
Hint g_step,property.
297
Proof.
298
(* --------------------------------------
299
  
300
From 'typed_g_step_assert': 
301
  auto with zarith.
302
*)
303
(* --------------------------------------
304
  
305
From 'typed_g_step_assert_4': 
306
(* --------------------------------------
307
  
308
From 'typed_g_step_assert': 
309
  auto with zarith.
310
*)
311
(* --------------------------------------
312
  
313
From 'typed_g_step_assert_3': 
314
(* --------------------------------------
315
  
316
From 'typed_g_step_assert': 
317
  auto with zarith.
318
*)
319
(* --------------------------------------
320
  
321
From 'typed_g_step_post': 
322
  auto with zarith.
323
*)
324
*)
325
(* --------------------------------------
326
  
327
From 'typed_g_step_assert_2': 
328
(* --------------------------------------
329
  
330
From 'typed_g_step_assert': 
331
  auto with zarith.
332
*)
333
(* --------------------------------------
334
  
335
From 'typed_g_step_post': 
336
  auto with zarith.
337
*)
338
*)
339
*)
340
(* --------------------------------------
341
  
342
From 'typed_g_step_assert_3': 
343
(* --------------------------------------
344
  
345
From 'typed_g_step_assert': 
346
  auto with zarith.
347
*)
348
(* --------------------------------------
349
  
350
From 'typed_g_step_post': 
351
  auto with zarith.
352
*)
353
*)
354
Qed.
355
356
Goal typed_g_step_call_f_step_pre.
357
Hint g_step,precond-f_step.
358
Proof.
359
(* auto with zarith. *)
360
Qed.
361
362
Goal typed_g_step_call_f_step_pre_4.
363
Hint g_step,precond-f_step.
364
Proof.
365
(* auto with zarith. *)
366
Qed.
367
368
Goal typed_g_step_post.
369
Hint default,g_step,property.
370
Proof.
371
  auto with zarith.
372
Qed.
373