forked from Barry-Jay/lambdaSF
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathLamSF_Normal.glob
375 lines (375 loc) · 15.3 KB
/
LamSF_Normal.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
DIGEST 9c348eff8f48ca5b37fdbba99bee6a13
FLamSF_Normal
R1990:1994 Coq.Arith.Arith <> <> lib
R2012:2018 General <> <> lib
R2036:2038 Coq.Arith.Max <> <> lib
R2057:2060 Test <> <> lib
R2078:2088 LamSF_Terms <> <> lib
R2106:2118 LamSF_Tactics <> <> lib
R2136:2158 LamSF_Substitution_term <> <> lib
R2176:2187 SF_reduction <> <> lib
R2205:2219 LamSF_reduction <> <> lib
R2237:2241 Coq.omega.Omega <> <> lib
ind 2277:2282 <> normal
constr 2306:2311 <> nf_ref
constr 2342:2346 <> nf_op
constr 2376:2381 <> nf_abs
constr 2424:2432 <> nf_active
constr 2555:2565 <> nf_compound
R2291:2294 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2286:2290 LamSF_Terms <> lamSF ind
R2325:2330 LamSF_Normal <> normal ind
R2333:2335 LamSF_Terms <> Ref constr
R2337:2337 LamSF_Normal <> n var
R2360:2365 LamSF_Normal <> normal ind
R2368:2369 LamSF_Terms <> Op constr
R2371:2371 LamSF_Normal <> o var
R2403:2406 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2407:2412 LamSF_Normal <> normal ind
R2415:2417 LamSF_Terms <> Abs constr
R2419:2419 LamSF_Normal <> M var
R2395:2400 LamSF_Normal <> normal ind
R2402:2402 LamSF_Normal <> M var
R2459:2462 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2472:2506 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2528:2531 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2532:2537 LamSF_Normal <> normal ind
R2540:2542 LamSF_Terms <> App constr
R2547:2548 LamSF_Normal <> M2 var
R2544:2545 LamSF_Normal <> M1 var
R2525:2526 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R2507:2512 LamSF_Tactics <> status def
R2515:2517 LamSF_Terms <> App constr
R2522:2523 LamSF_Normal <> M2 var
R2519:2520 LamSF_Normal <> M1 var
R2463:2468 LamSF_Normal <> normal ind
R2470:2471 LamSF_Normal <> M2 var
R2450:2455 LamSF_Normal <> normal ind
R2457:2458 LamSF_Normal <> M1 var
R2592:2595 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2605:2639 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2660:2663 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2664:2669 LamSF_Normal <> normal ind
R2672:2674 LamSF_Terms <> App constr
R2679:2680 LamSF_Normal <> M2 var
R2676:2677 LamSF_Normal <> M1 var
R2640:2647 SF_reduction <> compound ind
R2650:2652 LamSF_Terms <> App constr
R2657:2658 LamSF_Normal <> M2 var
R2654:2655 LamSF_Normal <> M1 var
R2596:2601 LamSF_Normal <> normal ind
R2603:2604 LamSF_Normal <> M2 var
R2583:2588 LamSF_Normal <> normal ind
R2590:2591 LamSF_Normal <> M1 var
prf 2753:2777 <> lift_rec_preserves_normal
R2799:2803 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2816:2821 LamSF_Normal <> normal ind
R2823:2830 LamSF_Terms <> lift_rec def
R2836:2836 LamSF_Normal <> k var
R2834:2834 LamSF_Normal <> n var
R2832:2832 LamSF_Normal <> M var
R2791:2796 LamSF_Normal <> normal ind
R2798:2798 LamSF_Normal <> M var
R2896:2904 LamSF_Normal <> nf_active constr
R2975:2977 Coq.Init.Logic <> :type_scope:x_'='_x not
R2942:2947 LamSF_Tactics <> status def
R2950:2957 LamSF_Terms <> lift_rec def
R2960:2962 LamSF_Terms <> App constr
R2978:2985 LamSF_Terms <> relocate def
R3008:3008 Coq.Init.Datatypes <> S constr
R2987:2992 LamSF_Tactics <> status def
R2995:2997 LamSF_Terms <> App constr
R2975:2977 Coq.Init.Logic <> :type_scope:x_'='_x not
R2942:2947 LamSF_Tactics <> status def
R2950:2957 LamSF_Terms <> lift_rec def
R2960:2962 LamSF_Terms <> App constr
R2978:2985 LamSF_Terms <> relocate def
R3008:3008 Coq.Init.Datatypes <> S constr
R2987:2992 LamSF_Tactics <> status def
R2995:2997 LamSF_Terms <> App constr
R3026:3050 LamSF_Tactics <> lift_rec_preserves_status thm
R3061:3068 LamSF_Terms <> lift_rec def
R3082:3089 LamSF_Terms <> lift_rec def
R3082:3089 LamSF_Terms <> lift_rec def
R3119:3126 LamSF_Terms <> relocate def
R3135:3138 Test <> test def
R3147:3152 LamSF_Tactics <> status def
R3155:3157 LamSF_Terms <> App constr
R3141:3141 Coq.Init.Datatypes <> S constr
R3135:3138 Test <> test def
R3147:3152 LamSF_Tactics <> status def
R3155:3157 LamSF_Terms <> App constr
R3141:3141 Coq.Init.Datatypes <> S constr
prf 3203:3223 <> not_active_factorable
R3246:3249 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3262:3266 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3267:3267 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R3286:3290 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R3268:3274 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R3276:3277 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R3279:3281 Coq.Init.Logic <> :type_scope:x_'='_x not
R3278:3278 LamSF_Normal <> M var
R3282:3283 LamSF_Terms <> Op constr
R3285:3285 LamSF_Normal <> o var
R3291:3298 SF_reduction <> compound ind
R3300:3300 LamSF_Normal <> M var
R3258:3260 Coq.Init.Logic <> :type_scope:x_'='_x not
R3250:3255 LamSF_Tactics <> status def
R3257:3257 LamSF_Normal <> M var
R3238:3243 LamSF_Normal <> normal ind
R3245:3245 LamSF_Normal <> M var
R3385:3388 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R3381:3383 Coq.Init.Logic <> :type_scope:x_'='_x not
R3373:3378 LamSF_Tactics <> status def
R3397:3399 Coq.Init.Logic <> :type_scope:x_'='_x not
R3389:3394 LamSF_Tactics <> status def
R3385:3388 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R3381:3383 Coq.Init.Logic <> :type_scope:x_'='_x not
R3373:3378 LamSF_Tactics <> status def
R3397:3399 Coq.Init.Logic <> :type_scope:x_'='_x not
R3389:3394 LamSF_Tactics <> status def
R3489:3507 SF_reduction <> abs_active_compound constr
prf 3545:3555 <> normal_star
R3578:3581 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3582:3587 LamSF_Normal <> normal ind
R3590:3593 SF_reduction <> star def
R3595:3595 LamSF_Normal <> M var
R3570:3575 LamSF_Normal <> normal ind
R3577:3577 LamSF_Normal <> M var
prf 3704:3721 <> normal_component_l
R3743:3746 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3747:3752 LamSF_Normal <> normal ind
R3755:3768 SF_reduction <> left_component def
R3770:3770 LamSF_Normal <> M var
R3735:3740 LamSF_Normal <> normal ind
R3742:3742 LamSF_Normal <> M var
prf 3856:3873 <> normal_component_r
R3895:3898 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3899:3904 LamSF_Normal <> normal ind
R3907:3921 SF_reduction <> right_component def
R3923:3923 LamSF_Normal <> M var
R3887:3892 LamSF_Normal <> normal ind
R3894:3894 LamSF_Normal <> M var
R4014:4024 LamSF_Normal <> nf_compound constr
R4037:4047 LamSF_Normal <> normal_star thm
def 4068:4078 <> irreducible
R4087:4093 LamSF_Tactics <> termred def
R4116:4119 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4120:4124 Coq.Init.Logic <> False ind
R4109:4111 LamSF_Normal <> red var
R4115:4115 LamSF_Normal <> N var
R4113:4113 LamSF_Normal <> M var
prf 4135:4149 <> ref_irreducible
R4163:4173 LamSF_Normal <> irreducible def
R4183:4192 LamSF_reduction <> lamSF_red1 ind
R4176:4178 LamSF_Terms <> Ref constr
R4180:4180 LamSF_Normal <> n var
prf 4260:4277 <> active_irreducible
R4302:4306 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4348:4352 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4395:4398 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4399:4409 LamSF_Normal <> irreducible def
R4413:4422 LamSF_reduction <> lamSF_red1 ind
R4411:4411 LamSF_Normal <> M var
R4353:4363 LamSF_Normal <> irreducible def
R4385:4394 LamSF_reduction <> lamSF_red1 ind
R4366:4380 SF_reduction <> right_component def
R4382:4382 LamSF_Normal <> M var
R4307:4317 LamSF_Normal <> irreducible def
R4338:4347 LamSF_reduction <> lamSF_red1 ind
R4320:4333 SF_reduction <> left_component def
R4335:4335 LamSF_Normal <> M var
R4299:4300 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R4291:4296 LamSF_Tactics <> status def
R4298:4298 LamSF_Normal <> M var
R4556:4565 LamSF_reduction <> lamSF_red1 ind
R4578:4581 SF_reduction <> star def
R4568:4571 SF_reduction <> star def
R4556:4565 LamSF_reduction <> lamSF_red1 ind
R4578:4581 SF_reduction <> star def
R4568:4571 SF_reduction <> star def
R4598:4629 LamSF_reduction <> lamSF_red1_preserves_star_active thm
R4676:4678 Coq.Init.Logic <> :type_scope:x_'='_x not
R4668:4673 LamSF_Tactics <> status def
R4676:4678 Coq.Init.Logic <> :type_scope:x_'='_x not
R4668:4673 LamSF_Tactics <> status def
R4693:4711 SF_reduction <> compound_not_active thm
prf 4737:4756 <> compound_irreducible
R4780:4784 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4826:4830 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4873:4876 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4877:4887 LamSF_Normal <> irreducible def
R4891:4900 LamSF_reduction <> lamSF_red1 ind
R4889:4889 LamSF_Normal <> M var
R4831:4841 LamSF_Normal <> irreducible def
R4863:4872 LamSF_reduction <> lamSF_red1 ind
R4844:4858 SF_reduction <> right_component def
R4860:4860 LamSF_Normal <> M var
R4785:4795 LamSF_Normal <> irreducible def
R4816:4825 LamSF_reduction <> lamSF_red1 ind
R4798:4811 SF_reduction <> left_component def
R4813:4813 LamSF_Normal <> M var
R4770:4777 SF_reduction <> compound ind
R4779:4779 LamSF_Normal <> M var
R5449:5458 LamSF_reduction <> lamSF_red1 ind
R5477:5479 LamSF_Terms <> Abs constr
R5482:5485 SF_reduction <> star def
R5461:5463 LamSF_Terms <> Abs constr
R5466:5469 SF_reduction <> star def
R5449:5458 LamSF_reduction <> lamSF_red1 ind
R5477:5479 LamSF_Terms <> Abs constr
R5482:5485 SF_reduction <> star def
R5461:5463 LamSF_Terms <> Abs constr
R5466:5469 SF_reduction <> star def
R5504:5516 LamSF_reduction <> abs_lamSF_red constr
R5528:5561 LamSF_reduction <> lamSF_red1_preserves_star_compound thm
R5652:5661 LamSF_reduction <> lamSF_red1 ind
R5679:5681 LamSF_Terms <> Abs constr
R5684:5687 SF_reduction <> star def
R5664:5666 LamSF_Terms <> Abs constr
R5669:5672 SF_reduction <> star def
R5652:5661 LamSF_reduction <> lamSF_red1 ind
R5679:5681 LamSF_Terms <> Abs constr
R5684:5687 SF_reduction <> star def
R5664:5666 LamSF_Terms <> Abs constr
R5669:5672 SF_reduction <> star def
R5706:5718 LamSF_reduction <> abs_lamSF_red constr
R5730:5761 LamSF_reduction <> lamSF_red1_preserves_star_active thm
R5844:5853 LamSF_reduction <> lamSF_red1 ind
R5866:5869 SF_reduction <> star def
R5857:5860 SF_reduction <> star def
R5844:5853 LamSF_reduction <> lamSF_red1 ind
R5866:5869 SF_reduction <> star def
R5857:5860 SF_reduction <> star def
R5886:5917 LamSF_reduction <> lamSF_red1_preserves_star_active thm
prf 5963:5977 <> abs_irreducible
R6016:6020 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6021:6031 LamSF_Normal <> irreducible def
R6041:6050 LamSF_reduction <> lamSF_red1 ind
R6034:6036 LamSF_Terms <> Abs constr
R6038:6038 LamSF_Normal <> M var
R5992:6002 LamSF_Normal <> irreducible def
R6006:6015 LamSF_reduction <> lamSF_red1 ind
R6004:6004 LamSF_Normal <> M var
prf 6117:6137 <> normal_is_irreducible
R6159:6162 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6163:6173 LamSF_Normal <> irreducible def
R6177:6186 LamSF_reduction <> lamSF_red1 ind
R6175:6175 LamSF_Normal <> M var
R6151:6156 LamSF_Normal <> normal ind
R6158:6158 LamSF_Normal <> M var
R6248:6262 LamSF_Normal <> ref_irreducible thm
R6304:6318 LamSF_Normal <> abs_irreducible thm
R6329:6346 LamSF_Normal <> active_irreducible thm
R6359:6378 LamSF_Normal <> compound_irreducible thm
prf 6475:6482 <> progress
R6499:6503 LamSF_Terms <> lamSF ind
R6515:6519 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R6544:6544 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R6507:6512 LamSF_Normal <> normal ind
R6514:6514 LamSF_Normal <> M var
R6520:6526 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R6528:6529 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R6530:6539 LamSF_reduction <> lamSF_red1 ind
R6543:6543 LamSF_Normal <> N var
R6541:6541 LamSF_Normal <> M var
R6708:6716 LamSF_Normal <> nf_active constr
R6761:6769 LamSF_Normal <> nf_active constr
R7071:7079 LamSF_Normal <> nf_active constr
R7181:7184 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R7177:7179 Coq.Init.Logic <> :type_scope:x_'='_x not
R7168:7173 LamSF_Tactics <> status def
R7198:7201 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R7194:7196 Coq.Init.Logic <> :type_scope:x_'='_x not
R7185:7190 LamSF_Tactics <> status def
R7211:7212 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R7202:7207 LamSF_Tactics <> status def
R7181:7184 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R7177:7179 Coq.Init.Logic <> :type_scope:x_'='_x not
R7168:7173 LamSF_Tactics <> status def
R7198:7201 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R7194:7196 Coq.Init.Logic <> :type_scope:x_'='_x not
R7185:7190 LamSF_Tactics <> status def
R7211:7212 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R7202:7207 LamSF_Tactics <> status def
R7248:7268 LamSF_Normal <> not_active_factorable thm
R7248:7268 LamSF_Normal <> not_active_factorable thm
R7404:7407 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R7396:7398 Coq.Init.Logic <> :type_scope:x_'='_x not
R7399:7401 LamSF_Terms <> Ref constr
R7410:7413 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R7414:7416 LamSF_Terms <> Ref constr
R7404:7407 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R7396:7398 Coq.Init.Logic <> :type_scope:x_'='_x not
R7399:7401 LamSF_Terms <> Ref constr
R7410:7413 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R7414:7416 LamSF_Terms <> Ref constr
R7432:7454 LamSF_Terms <> decidable_term_equality thm
R7502:7509 SF_reduction <> compound ind
R7512:7514 LamSF_Terms <> Abs constr
R7502:7509 SF_reduction <> compound ind
R7512:7514 LamSF_Terms <> Abs constr
R7531:7549 SF_reduction <> abs_active_compound constr
R7591:7599 LamSF_Normal <> nf_active constr
prf 7637:7657 <> irreducible_is_normal
R7695:7698 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7699:7704 LamSF_Normal <> normal ind
R7706:7706 LamSF_Normal <> M var
R7671:7681 LamSF_Normal <> irreducible def
R7685:7694 LamSF_reduction <> lamSF_red1 ind
R7683:7683 LamSF_Normal <> M var
R7733:7740 LamSF_Normal <> progress thm
R7733:7740 LamSF_Normal <> progress thm
R7764:7768 Coq.Init.Logic <> False ind
R7764:7768 Coq.Init.Logic <> False ind
prf 7806:7827 <> irreducible_iff_normal
R7864:7868 Coq.Init.Logic <> :type_scope:x_'<->'_x not
R7840:7850 LamSF_Normal <> irreducible def
R7854:7863 LamSF_reduction <> lamSF_red1 ind
R7852:7852 LamSF_Normal <> M var
R7869:7874 LamSF_Normal <> normal ind
R7876:7876 LamSF_Normal <> M var
R7906:7926 LamSF_Normal <> irreducible_is_normal thm
R7937:7957 LamSF_Normal <> normal_is_irreducible thm
prf 7974:7989 <> normal_is_stable
R8010:8013 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8037:8040 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8042:8044 Coq.Init.Logic <> :type_scope:x_'='_x not
R8041:8041 LamSF_Normal <> N var
R8045:8045 LamSF_Normal <> M var
R8024:8032 LamSF_reduction <> lamSF_red def
R8036:8036 LamSF_Normal <> N var
R8034:8034 LamSF_Normal <> M var
R8002:8007 LamSF_Normal <> normal ind
R8009:8009 LamSF_Normal <> M var
R8087:8095 LamSF_reduction <> lamSF_red def
R8087:8095 LamSF_reduction <> lamSF_red def
R8106:8110 Coq.Init.Logic <> False ind
R8106:8110 Coq.Init.Logic <> False ind
R8123:8143 LamSF_Normal <> normal_is_irreducible thm
prf 8167:8169 <> unf
R8199:8202 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8216:8219 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8228:8231 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8240:8243 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8245:8247 Coq.Init.Logic <> :type_scope:x_'='_x not
R8244:8244 LamSF_Normal <> N var
R8248:8248 LamSF_Normal <> P var
R8232:8237 LamSF_Normal <> normal ind
R8239:8239 LamSF_Normal <> P var
R8220:8225 LamSF_Normal <> normal ind
R8227:8227 LamSF_Normal <> N var
R8203:8211 LamSF_reduction <> lamSF_red def
R8215:8215 LamSF_Normal <> P var
R8213:8213 LamSF_Normal <> M var
R8186:8194 LamSF_reduction <> lamSF_red def
R8198:8198 LamSF_Normal <> N var
R8196:8196 LamSF_Normal <> M var
R8277:8293 LamSF_reduction <> diamond_lamSF_red thm
R8277:8293 LamSF_reduction <> diamond_lamSF_red thm
R8326:8326 Coq.Init.Logic <> :type_scope:x_'='_x not
R8326:8326 Coq.Init.Logic <> :type_scope:x_'='_x not
R8341:8356 LamSF_Normal <> normal_is_stable thm
R8369:8369 Coq.Init.Logic <> :type_scope:x_'='_x not
R8369:8369 Coq.Init.Logic <> :type_scope:x_'='_x not
R8384:8399 LamSF_Normal <> normal_is_stable thm