-
Notifications
You must be signed in to change notification settings - Fork 3
/
LamSF_Eval.glob
417 lines (417 loc) · 15.4 KB
/
LamSF_Eval.glob
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
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
DIGEST f70af769e1e7feb17aaf81f6146c7975
FLamSF_Eval
R1990:1994 Coq.Arith.Arith <> <> lib
R2012:2014 Coq.Arith.Max <> <> lib
R2033:2036 Test <> <> lib
R2054:2060 General <> <> lib
R2079:2089 LamSF_Terms <> <> lib
R2107:2119 LamSF_Tactics <> <> lib
R2137:2159 LamSF_Substitution_term <> <> lib
R2177:2188 SF_reduction <> <> lib
R2206:2220 LamSF_reduction <> <> lib
R2238:2249 LamSF_Normal <> <> lib
R2267:2278 LamSF_Closed <> <> lib
R2327:2335 LamSF_reduction <> lamSF_red def
R2327:2335 LamSF_reduction <> lamSF_red def
R2364:2366 Coq.Init.Logic <> :type_scope:x_'='_x not
R2520:2528 LamSF_reduction <> lamSF_red def
R2520:2528 LamSF_reduction <> lamSF_red def
R2543:2551 LamSF_reduction <> lamSF_red def
R2543:2551 LamSF_reduction <> lamSF_red def
R2573:2589 LamSF_reduction <> diamond_lamSF_red thm
def 3107:3114 <> eval_app
R3130:3130 LamSF_Eval <> M var
R3140:3142 LamSF_Terms <> App constr
R3145:3147 LamSF_Terms <> App constr
R3150:3151 LamSF_Terms <> Op constr
R3153:3155 LamSF_Terms <> Sop constr
R3169:3171 LamSF_Terms <> App constr
R3185:3187 LamSF_Terms <> App constr
R3192:3192 LamSF_Eval <> N var
R3174:3176 LamSF_Terms <> App constr
R3181:3181 LamSF_Eval <> N var
R3197:3199 LamSF_Terms <> App constr
R3202:3204 LamSF_Terms <> App constr
R3207:3208 LamSF_Terms <> Op constr
R3210:3212 LamSF_Terms <> Fop constr
R3216:3217 LamSF_Terms <> Op constr
R3235:3237 LamSF_Terms <> App constr
R3240:3242 LamSF_Terms <> App constr
R3245:3246 LamSF_Terms <> Op constr
R3248:3250 LamSF_Terms <> Fop constr
R3254:3256 LamSF_Terms <> App constr
R3259:3260 LamSF_Terms <> Op constr
R3275:3277 LamSF_Terms <> App constr
R3280:3282 LamSF_Terms <> App constr
R3287:3288 LamSF_Terms <> Op constr
R3284:3284 LamSF_Eval <> N var
R3299:3301 LamSF_Terms <> App constr
R3304:3306 LamSF_Terms <> App constr
R3309:3310 LamSF_Terms <> Op constr
R3312:3314 LamSF_Terms <> Fop constr
R3318:3320 LamSF_Terms <> App constr
R3323:3325 LamSF_Terms <> App constr
R3328:3329 LamSF_Terms <> Op constr
R3348:3350 LamSF_Terms <> App constr
R3353:3355 LamSF_Terms <> App constr
R3360:3362 LamSF_Terms <> App constr
R3365:3366 LamSF_Terms <> Op constr
R3357:3357 LamSF_Eval <> N var
R3381:3383 LamSF_Terms <> App constr
R3386:3388 LamSF_Terms <> App constr
R3391:3392 LamSF_Terms <> Op constr
R3394:3396 LamSF_Terms <> Fop constr
R3400:3402 LamSF_Terms <> Abs constr
R3405:3407 LamSF_Terms <> Ref constr
R3419:3421 LamSF_Terms <> App constr
R3441:3444 SF_reduction <> star def
R3447:3449 LamSF_Terms <> Ref constr
R3424:3426 LamSF_Terms <> App constr
R3430:3437 SF_reduction <> abs_left def
R3428:3428 LamSF_Eval <> N var
R3457:3459 LamSF_Terms <> App constr
R3462:3464 LamSF_Terms <> App constr
R3467:3468 LamSF_Terms <> Op constr
R3470:3472 LamSF_Terms <> Fop constr
R3476:3478 LamSF_Terms <> Abs constr
R3481:3482 LamSF_Terms <> Op constr
R3494:3496 LamSF_Terms <> App constr
R3516:3519 SF_reduction <> star def
R3522:3523 LamSF_Terms <> Op constr
R3499:3501 LamSF_Terms <> App constr
R3505:3512 SF_reduction <> abs_left def
R3503:3503 LamSF_Eval <> N var
R3531:3533 LamSF_Terms <> Abs constr
R3541:3545 LamSF_Terms <> subst def
R3547:3547 LamSF_Eval <> N var
R3559:3561 LamSF_Terms <> App constr
R3565:3565 LamSF_Eval <> N var
prf 3580:3598 <> eval_app_from_lamSF
R3614:3622 LamSF_reduction <> lamSF_red def
R3635:3642 LamSF_Eval <> eval_app def
R3646:3646 LamSF_Eval <> N var
R3644:3644 LamSF_Eval <> M var
R3625:3627 LamSF_Terms <> App constr
R3631:3631 LamSF_Eval <> N var
R3629:3629 LamSF_Eval <> M var
R3817:3836 LamSF_reduction <> f_compound_lamSF_red constr
R3863:3882 LamSF_reduction <> f_compound_lamSF_red constr
R3928:3947 LamSF_reduction <> f_compound_lamSF_red constr
R3993:4012 LamSF_reduction <> f_compound_lamSF_red constr
def 4033:4037 <> eval0
R4043:4047 LamSF_Terms <> lamSF ind
R4059:4059 LamSF_Eval <> M var
R4069:4071 LamSF_Terms <> Ref constr
R4078:4080 LamSF_Terms <> Ref constr
R4087:4088 LamSF_Terms <> Op constr
R4095:4096 LamSF_Terms <> Op constr
R4102:4104 LamSF_Terms <> Abs constr
R4112:4114 LamSF_Terms <> Abs constr
R4121:4123 LamSF_Terms <> App constr
R4126:4127 LamSF_Terms <> Op constr
R4129:4131 LamSF_Terms <> Fop constr
R4141:4143 LamSF_Terms <> App constr
R4155:4159 LamSF_Eval <> eval0 def
R4146:4147 LamSF_Terms <> Op constr
R4149:4151 LamSF_Terms <> Fop constr
R4168:4170 LamSF_Terms <> App constr
R4182:4189 LamSF_Eval <> eval_app def
R4192:4196 LamSF_Eval <> eval0 def
prf 4219:4234 <> eval0_from_lamSF
R4248:4256 LamSF_reduction <> lamSF_red def
R4261:4265 LamSF_Eval <> eval0 def
R4267:4267 LamSF_Eval <> M var
R4258:4258 LamSF_Eval <> M var
R4330:4332 LamSF_Terms <> App constr
R4335:4339 LamSF_Eval <> eval0 def
R4309:4322 LamSF_Tactics <> transitive_red thm
R4330:4332 LamSF_Terms <> App constr
R4335:4339 LamSF_Eval <> eval0 def
R4309:4322 LamSF_Tactics <> transitive_red thm
R4389:4396 LamSF_Eval <> eval_app def
R4399:4403 LamSF_Eval <> eval0 def
R4368:4381 LamSF_Tactics <> transitive_red thm
R4389:4396 LamSF_Eval <> eval_app def
R4399:4403 LamSF_Eval <> eval0 def
R4368:4381 LamSF_Tactics <> transitive_red thm
R4423:4441 LamSF_Eval <> eval_app_from_lamSF thm
R4490:4512 LamSF_reduction <> preserves_app_lamSF_red thm
R4579:4587 LamSF_reduction <> lamSF_red def
R4579:4587 LamSF_reduction <> lamSF_red def
R4620:4629 LamSF_Tactics <> multi_step ind
R4631:4640 LamSF_reduction <> lamSF_red1 ind
R4620:4629 LamSF_Tactics <> multi_step ind
R4631:4640 LamSF_reduction <> lamSF_red1 ind
R4680:4684 LamSF_Eval <> eval0 def
R4659:4672 LamSF_Tactics <> transitive_red thm
R4730:4734 LamSF_Eval <> eval0 def
R4737:4744 LamSF_Eval <> eval_app def
R4755:4759 LamSF_Terms <> subst def
def 4831:4833 <> not
R4840:4842 LamSF_Terms <> App constr
R4868:4871 SF_reduction <> k_op def
R4845:4847 LamSF_Terms <> App constr
R4852:4854 LamSF_Terms <> App constr
R4861:4864 SF_reduction <> i_op def
R4856:4859 SF_reduction <> k_op def
R4849:4849 LamSF_Eval <> M var
prf 4881:4888 <> not_true
R4892:4900 LamSF_reduction <> lamSF_red def
R4914:4916 LamSF_Terms <> App constr
R4923:4926 SF_reduction <> i_op def
R4918:4921 SF_reduction <> k_op def
R4903:4905 LamSF_Eval <> not def
R4907:4910 SF_reduction <> k_op def
R4944:4946 LamSF_Eval <> not def
prf 4975:4983 <> not_false
R4987:4995 LamSF_reduction <> lamSF_red def
R5019:5022 SF_reduction <> k_op def
R4998:5000 LamSF_Eval <> not def
R5003:5005 LamSF_Terms <> App constr
R5012:5015 SF_reduction <> i_op def
R5007:5010 SF_reduction <> k_op def
def 5076:5078 <> iff
R5087:5089 LamSF_Terms <> App constr
R5102:5104 LamSF_Eval <> not def
R5106:5106 LamSF_Eval <> N var
R5092:5094 LamSF_Terms <> App constr
R5098:5098 LamSF_Eval <> N var
R5096:5096 LamSF_Eval <> M var
prf 5118:5126 <> true_true
R5130:5138 LamSF_reduction <> lamSF_red def
R5156:5159 SF_reduction <> k_op def
R5141:5143 LamSF_Eval <> iff def
R5150:5153 SF_reduction <> k_op def
R5145:5148 SF_reduction <> k_op def
R5177:5179 LamSF_Eval <> iff def
R5189:5191 LamSF_Eval <> not def
prf 5230:5239 <> true_false
R5243:5251 LamSF_reduction <> lamSF_red def
R5281:5283 LamSF_Terms <> App constr
R5290:5293 SF_reduction <> i_op def
R5285:5288 SF_reduction <> k_op def
R5254:5256 LamSF_Eval <> iff def
R5264:5266 LamSF_Terms <> App constr
R5273:5276 SF_reduction <> i_op def
R5268:5271 SF_reduction <> k_op def
R5258:5261 SF_reduction <> k_op def
R5312:5314 LamSF_Eval <> iff def
R5324:5326 LamSF_Eval <> not def
prf 5365:5374 <> false_true
R5378:5386 LamSF_reduction <> lamSF_red def
R5416:5418 LamSF_Terms <> App constr
R5425:5428 SF_reduction <> i_op def
R5420:5423 SF_reduction <> k_op def
R5389:5391 LamSF_Eval <> iff def
R5409:5412 SF_reduction <> k_op def
R5394:5396 LamSF_Terms <> App constr
R5403:5406 SF_reduction <> i_op def
R5398:5401 SF_reduction <> k_op def
R5447:5449 LamSF_Eval <> iff def
R5459:5461 LamSF_Eval <> not def
prf 5539:5549 <> false_false
R5553:5561 LamSF_reduction <> lamSF_red def
R5601:5604 SF_reduction <> k_op def
R5564:5566 LamSF_Eval <> iff def
R5585:5587 LamSF_Terms <> App constr
R5594:5597 SF_reduction <> i_op def
R5589:5592 SF_reduction <> k_op def
R5569:5571 LamSF_Terms <> App constr
R5578:5581 SF_reduction <> i_op def
R5573:5576 SF_reduction <> k_op def
R5622:5624 LamSF_Eval <> iff def
R5627:5629 LamSF_Eval <> not def
def 5699:5710 <> little_omega
R5715:5717 LamSF_Terms <> Abs constr
R5720:5722 LamSF_Terms <> Abs constr
R5725:5727 LamSF_Terms <> App constr
R5738:5740 LamSF_Terms <> App constr
R5765:5767 LamSF_Terms <> Ref constr
R5743:5745 LamSF_Terms <> App constr
R5756:5758 LamSF_Terms <> Ref constr
R5748:5750 LamSF_Terms <> Ref constr
R5730:5732 LamSF_Terms <> Ref constr
def 5787:5790 <> fix1
R5849:5851 LamSF_Terms <> Abs constr
R5853:5855 LamSF_Terms <> App constr
R6197:6200 SF_reduction <> i_op def
R5858:5860 LamSF_Terms <> App constr
R5882:5884 LamSF_Terms <> App constr
R5960:5962 LamSF_Terms <> App constr
R6167:6169 LamSF_Terms <> App constr
R6177:6179 LamSF_Terms <> Ref constr
R6171:6174 SF_reduction <> k_op def
R5965:5967 LamSF_Terms <> App constr
R6004:6006 LamSF_Terms <> App constr
R6117:6119 LamSF_Terms <> App constr
R6126:6137 LamSF_Eval <> little_omega def
R6121:6124 SF_reduction <> k_op def
R6009:6011 LamSF_Terms <> App constr
R6058:6060 LamSF_Terms <> App constr
R6067:6078 LamSF_Eval <> little_omega def
R6062:6065 SF_reduction <> k_op def
R6013:6016 SF_reduction <> s_op def
R5969:5972 SF_reduction <> s_op def
R5887:5889 LamSF_Terms <> App constr
R5921:5923 LamSF_Terms <> App constr
R5931:5933 LamSF_Terms <> Ref constr
R5925:5928 SF_reduction <> k_op def
R5891:5894 SF_reduction <> s_op def
R5862:5865 SF_reduction <> s_op def
def 6219:6226 <> fixpoint
R6231:6233 LamSF_Terms <> App constr
R6248:6259 LamSF_Eval <> little_omega def
R6235:6246 LamSF_Eval <> little_omega def
prf 6271:6280 <> fix1_check
R6295:6303 LamSF_reduction <> lamSF_red def
R6368:6370 LamSF_Terms <> App constr
R6420:6420 LamSF_Eval <> N var
R6373:6375 LamSF_Terms <> App constr
R6380:6382 LamSF_Terms <> App constr
R6416:6416 LamSF_Eval <> M var
R6385:6387 LamSF_Terms <> App constr
R6402:6413 LamSF_Eval <> little_omega def
R6389:6400 LamSF_Eval <> little_omega def
R6377:6377 LamSF_Eval <> M var
R6306:6308 LamSF_Terms <> App constr
R6323:6323 LamSF_Eval <> N var
R6311:6313 LamSF_Terms <> App constr
R6320:6320 LamSF_Eval <> M var
R6315:6318 LamSF_Eval <> fix1 def
R6451:6454 LamSF_Eval <> fix1 def
R6508:6520 LamSF_Substitution_term <> lift_rec_null thm
R6508:6520 LamSF_Substitution_term <> lift_rec_null thm
R6508:6520 LamSF_Substitution_term <> lift_rec_null thm
R6531:6553 LamSF_reduction <> preserves_app_lamSF_red thm
R6591:6602 LamSF_Eval <> little_omega def
R6591:6602 LamSF_Eval <> little_omega def
R6628:6636 LamSF_reduction <> lamSF_red def
R6639:6641 LamSF_Terms <> App constr
R6644:6646 LamSF_Terms <> App constr
R6649:6651 LamSF_Terms <> App constr
R6654:6656 LamSF_Terms <> App constr
R6668:6669 LamSF_Terms <> Op constr
R6671:6673 LamSF_Terms <> Fop constr
R6659:6660 LamSF_Terms <> Op constr
R6662:6664 LamSF_Terms <> Fop constr
R6628:6636 LamSF_reduction <> lamSF_red def
R6639:6641 LamSF_Terms <> App constr
R6644:6646 LamSF_Terms <> App constr
R6649:6651 LamSF_Terms <> App constr
R6654:6656 LamSF_Terms <> App constr
R6668:6669 LamSF_Terms <> Op constr
R6671:6673 LamSF_Terms <> Fop constr
R6659:6660 LamSF_Terms <> Op constr
R6662:6664 LamSF_Terms <> Fop constr
R6720:6722 LamSF_Terms <> App constr
R6699:6712 LamSF_Tactics <> transitive_red thm
R6720:6722 LamSF_Terms <> App constr
R6699:6712 LamSF_Tactics <> transitive_red thm
R6743:6765 LamSF_reduction <> preserves_app_lamSF_red thm
R6777:6799 LamSF_reduction <> preserves_app_lamSF_red thm
R6851:6860 LamSF_Tactics <> multi_step ind
R6874:6876 LamSF_Terms <> App constr
R6879:6881 LamSF_Terms <> App constr
R6884:6886 LamSF_Terms <> App constr
R6889:6891 LamSF_Terms <> App constr
R6917:6928 LamSF_Eval <> little_omega def
R6894:6896 LamSF_Terms <> App constr
R6908:6909 LamSF_Terms <> Op constr
R6911:6913 LamSF_Terms <> Fop constr
R6899:6900 LamSF_Terms <> Op constr
R6902:6904 LamSF_Terms <> Fop constr
R6862:6871 LamSF_reduction <> lamSF_red1 ind
R6851:6860 LamSF_Tactics <> multi_step ind
R6874:6876 LamSF_Terms <> App constr
R6879:6881 LamSF_Terms <> App constr
R6884:6886 LamSF_Terms <> App constr
R6889:6891 LamSF_Terms <> App constr
R6917:6928 LamSF_Eval <> little_omega def
R6894:6896 LamSF_Terms <> App constr
R6908:6909 LamSF_Terms <> Op constr
R6911:6913 LamSF_Terms <> Fop constr
R6899:6900 LamSF_Terms <> Op constr
R6902:6904 LamSF_Terms <> Fop constr
R6862:6871 LamSF_reduction <> lamSF_red1 ind
R6975:6977 LamSF_Terms <> App constr
R6980:6982 LamSF_Terms <> App constr
R6984:6995 LamSF_Eval <> little_omega def
R6954:6967 LamSF_Tactics <> transitive_red thm
R6975:6977 LamSF_Terms <> App constr
R6980:6982 LamSF_Terms <> App constr
R6984:6995 LamSF_Eval <> little_omega def
R6954:6967 LamSF_Tactics <> transitive_red thm
R7017:7039 LamSF_reduction <> preserves_app_lamSF_red thm
R7051:7073 LamSF_reduction <> preserves_app_lamSF_red thm
prf 7092:7106 <> fixpoint_closed
R7125:7127 Coq.Init.Logic <> :type_scope:x_'='_x not
R7110:7115 LamSF_Closed <> maxvar def
R7117:7124 LamSF_Eval <> fixpoint def
R7146:7153 LamSF_Eval <> fixpoint def
prf 7180:7184 <> fixes
R7198:7206 LamSF_reduction <> lamSF_red def
R7226:7228 LamSF_Terms <> App constr
R7233:7235 LamSF_Terms <> App constr
R7246:7246 LamSF_Eval <> f var
R7237:7244 LamSF_Eval <> fixpoint def
R7230:7230 LamSF_Eval <> f var
R7209:7211 LamSF_Terms <> App constr
R7222:7222 LamSF_Eval <> f var
R7213:7220 LamSF_Eval <> fixpoint def
R7276:7283 LamSF_Eval <> fixpoint def
R7293:7304 LamSF_Eval <> little_omega def
R7333:7337 LamSF_Terms <> subst def
R7391:7403 LamSF_Substitution_term <> lift_rec_null thm
R7391:7403 LamSF_Substitution_term <> lift_rec_null thm
R7391:7403 LamSF_Substitution_term <> lift_rec_null thm
R7459:7467 LamSF_reduction <> lamSF_red def
R7470:7472 LamSF_Terms <> App constr
R7475:7477 LamSF_Terms <> App constr
R7479:7486 LamSF_Eval <> fixpoint def
R7459:7467 LamSF_reduction <> lamSF_red def
R7470:7472 LamSF_Terms <> App constr
R7475:7477 LamSF_Terms <> App constr
R7479:7486 LamSF_Eval <> fixpoint def
R7621:7629 LamSF_reduction <> lamSF_red def
R7632:7634 LamSF_Terms <> App constr
R7637:7639 LamSF_Terms <> App constr
R7642:7644 LamSF_Terms <> App constr
R7646:7653 LamSF_Eval <> fixpoint def
R7621:7629 LamSF_reduction <> lamSF_red def
R7632:7634 LamSF_Terms <> App constr
R7637:7639 LamSF_Terms <> App constr
R7642:7644 LamSF_Terms <> App constr
R7646:7653 LamSF_Eval <> fixpoint def
R7834:7842 LamSF_reduction <> lamSF_red def
R7845:7847 LamSF_Terms <> App constr
R7850:7852 LamSF_Terms <> App constr
R7855:7857 LamSF_Terms <> App constr
R7860:7862 LamSF_Terms <> App constr
R7864:7871 LamSF_Eval <> fixpoint def
R7834:7842 LamSF_reduction <> lamSF_red def
R7845:7847 LamSF_Terms <> App constr
R7850:7852 LamSF_Terms <> App constr
R7855:7857 LamSF_Terms <> App constr
R7860:7862 LamSF_Terms <> App constr
R7864:7871 LamSF_Eval <> fixpoint def
R7923:7925 LamSF_Terms <> App constr
R7928:7930 LamSF_Terms <> App constr
R7933:7935 LamSF_Terms <> App constr
R7938:7940 LamSF_Terms <> App constr
R7945:7947 LamSF_Terms <> App constr
R7949:7956 LamSF_Eval <> fixpoint def
R7902:7915 LamSF_Tactics <> transitive_red thm
R7701:7703 LamSF_Terms <> App constr
R7706:7708 LamSF_Terms <> App constr
R7711:7713 LamSF_Terms <> App constr
R7718:7720 LamSF_Terms <> App constr
R7722:7729 LamSF_Eval <> fixpoint def
R7680:7693 LamSF_Tactics <> transitive_red thm
R7530:7532 LamSF_Terms <> App constr
R7535:7537 LamSF_Terms <> App constr
R7542:7544 LamSF_Terms <> App constr
R7546:7553 LamSF_Eval <> fixpoint def
R7509:7522 LamSF_Tactics <> transitive_red thm
R8156:8165 LamSF_Terms <> insert_Ref def
R8175:8178 LamSF_Terms <> lift def
R8194:8208 LamSF_Closed <> lift_rec_closed thm