forked from Barry-Jay/lambdaSF
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathLamSF_Residuals.glob
368 lines (368 loc) · 14.6 KB
/
LamSF_Residuals.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
DIGEST c6158e25ed02972c6281cd172379b404
FLamSF_Residuals
R2282:2286 Coq.Arith.Arith <> <> lib
R2304:2307 Test <> <> lib
R2325:2331 General <> <> lib
R2349:2359 LamSF_Terms <> <> lib
R2377:2394 LamSF_Substitution <> <> lib
R2412:2424 LamSF_Redexes <> <> lib
R2442:2446 Coq.omega.Omega <> <> lib
ind 2688:2696 <> residuals
constr 2745:2752 <> Res_Oper
constr 2804:2810 <> Res_Var
constr 2862:2867 <> Res_Ap
constr 3076:3082 <> Res_Fun
constr 3170:3178 <> Res_redex
R2707:2710 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2718:2721 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2729:2732 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2722:2728 LamSF_Redexes <> redexes ind
R2711:2717 LamSF_Redexes <> redexes ind
R2700:2706 LamSF_Redexes <> redexes ind
R2766:2774 LamSF_Residuals <> residuals ind
R2793:2795 LamSF_Redexes <> Opp constr
R2797:2797 LamSF_Residuals <> o var
R2785:2787 LamSF_Redexes <> Opp constr
R2789:2789 LamSF_Residuals <> o var
R2777:2779 LamSF_Redexes <> Opp constr
R2781:2781 LamSF_Residuals <> o var
R2824:2832 LamSF_Residuals <> residuals ind
R2851:2853 LamSF_Redexes <> Var constr
R2855:2855 LamSF_Residuals <> i var
R2843:2845 LamSF_Redexes <> Var constr
R2847:2847 LamSF_Residuals <> i var
R2835:2837 LamSF_Redexes <> Var constr
R2839:2839 LamSF_Residuals <> i var
R2895:2901 LamSF_Redexes <> redexes ind
R2928:2937 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2956:2962 LamSF_Redexes <> redexes ind
R2989:2998 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3011:3014 Coq.Init.Datatypes <> bool ind
R3018:3026 LamSF_Residuals <> residuals ind
R3059:3060 LamSF_Redexes <> Ap constr
R3067:3068 LamSF_Residuals <> W2 var
R3064:3065 LamSF_Residuals <> W1 var
R3062:3062 LamSF_Residuals <> b var
R3042:3043 LamSF_Redexes <> Ap constr
R3054:3055 LamSF_Residuals <> V2 var
R3051:3052 LamSF_Residuals <> V1 var
R3045:3049 Coq.Init.Datatypes <> false constr
R3029:3030 LamSF_Redexes <> Ap constr
R3037:3038 LamSF_Residuals <> U2 var
R3034:3035 LamSF_Residuals <> U1 var
R3032:3032 LamSF_Residuals <> b var
R2971:2979 LamSF_Residuals <> residuals ind
R2987:2988 LamSF_Residuals <> W2 var
R2984:2985 LamSF_Residuals <> V2 var
R2981:2982 LamSF_Residuals <> U2 var
R2910:2918 LamSF_Residuals <> residuals ind
R2926:2927 LamSF_Residuals <> W1 var
R2923:2924 LamSF_Residuals <> V1 var
R2920:2921 LamSF_Residuals <> U1 var
R3128:3131 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3132:3140 LamSF_Residuals <> residuals ind
R3159:3161 LamSF_Redexes <> Fun constr
R3163:3163 LamSF_Residuals <> W var
R3151:3153 LamSF_Redexes <> Fun constr
R3155:3155 LamSF_Residuals <> V var
R3143:3145 LamSF_Redexes <> Fun constr
R3147:3147 LamSF_Residuals <> U var
R3113:3121 LamSF_Residuals <> residuals ind
R3127:3127 LamSF_Residuals <> W var
R3125:3125 LamSF_Residuals <> V var
R3123:3123 LamSF_Residuals <> U var
R3206:3212 LamSF_Redexes <> redexes ind
R3239:3248 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3267:3273 LamSF_Redexes <> redexes ind
R3300:3309 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3322:3325 Coq.Init.Datatypes <> bool ind
R3335:3343 LamSF_Residuals <> residuals ind
R3387:3393 LamSF_Substitution <> subst_r def
R3398:3399 LamSF_Residuals <> W1 var
R3395:3396 LamSF_Residuals <> W2 var
R3365:3366 LamSF_Redexes <> Ap constr
R3382:3383 LamSF_Residuals <> V2 var
R3374:3376 LamSF_Redexes <> Fun constr
R3378:3379 LamSF_Residuals <> V1 var
R3368:3371 Coq.Init.Datatypes <> true constr
R3346:3347 LamSF_Redexes <> Ap constr
R3360:3361 LamSF_Residuals <> U2 var
R3352:3354 LamSF_Redexes <> Fun constr
R3356:3357 LamSF_Residuals <> U1 var
R3349:3349 LamSF_Residuals <> b var
R3282:3290 LamSF_Residuals <> residuals ind
R3298:3299 LamSF_Residuals <> W2 var
R3295:3296 LamSF_Residuals <> V2 var
R3292:3293 LamSF_Residuals <> U2 var
R3221:3229 LamSF_Residuals <> residuals ind
R3237:3238 LamSF_Residuals <> W1 var
R3234:3235 LamSF_Residuals <> V1 var
R3231:3232 LamSF_Residuals <> U1 var
prf 3468:3485 <> residuals_function
R3505:3511 LamSF_Redexes <> redexes ind
R3530:3533 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3547:3553 LamSF_Redexes <> redexes ind
R3561:3569 LamSF_Residuals <> residuals ind
R3575:3576 LamSF_Residuals <> W' var
R3573:3573 LamSF_Residuals <> V var
R3571:3571 LamSF_Residuals <> U var
R3582:3584 Coq.Init.Logic <> :type_scope:x_'='_x not
R3580:3581 LamSF_Residuals <> W' var
R3585:3585 LamSF_Residuals <> W var
R3515:3523 LamSF_Residuals <> residuals ind
R3529:3529 LamSF_Residuals <> W var
R3527:3527 LamSF_Residuals <> V var
R3525:3525 LamSF_Residuals <> U var
prf 3910:3927 <> residuals_lift_rec
R3950:3956 LamSF_Redexes <> redexes ind
R3978:3982 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3996:3998 Coq.Init.Datatypes <> nat ind
R4002:4010 LamSF_Residuals <> residuals ind
R4053:4062 LamSF_Substitution <> lift_rec_r def
R4069:4069 LamSF_Residuals <> k var
R4067:4067 LamSF_Residuals <> n var
R4064:4065 LamSF_Residuals <> U3 var
R4033:4042 LamSF_Substitution <> lift_rec_r def
R4049:4049 LamSF_Residuals <> k var
R4047:4047 LamSF_Residuals <> n var
R4044:4045 LamSF_Residuals <> U2 var
R4013:4022 LamSF_Substitution <> lift_rec_r def
R4029:4029 LamSF_Residuals <> k var
R4027:4027 LamSF_Residuals <> n var
R4024:4025 LamSF_Residuals <> U1 var
R3960:3968 LamSF_Residuals <> residuals ind
R3976:3977 LamSF_Residuals <> U3 var
R3973:3974 LamSF_Residuals <> U2 var
R3970:3971 LamSF_Residuals <> U1 var
R4159:4161 Coq.Init.Logic <> :type_scope:x_'='_x not
R4163:4163 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4159:4161 Coq.Init.Logic <> :type_scope:x_'='_x not
R4163:4163 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4203:4209 LamSF_Substitution <> subst_r def
R4221:4238 LamSF_Substitution <> lift_rec_subst_rec thm
R4221:4238 LamSF_Substitution <> lift_rec_subst_rec thm
R4221:4238 LamSF_Substitution <> lift_rec_subst_rec thm
R4250:4258 LamSF_Residuals <> Res_redex constr
prf 4273:4286 <> residuals_lift
R4309:4315 LamSF_Redexes <> redexes ind
R4337:4341 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4353:4355 Coq.Init.Datatypes <> nat ind
R4358:4366 LamSF_Residuals <> residuals ind
R4397:4402 LamSF_Substitution <> lift_r def
R4406:4407 LamSF_Residuals <> U3 var
R4404:4404 LamSF_Residuals <> k var
R4383:4388 LamSF_Substitution <> lift_r def
R4392:4393 LamSF_Residuals <> U2 var
R4390:4390 LamSF_Residuals <> k var
R4369:4374 LamSF_Substitution <> lift_r def
R4378:4379 LamSF_Residuals <> U1 var
R4376:4376 LamSF_Residuals <> k var
R4319:4327 LamSF_Residuals <> residuals ind
R4335:4336 LamSF_Residuals <> U3 var
R4332:4333 LamSF_Residuals <> U2 var
R4329:4330 LamSF_Residuals <> U1 var
R4425:4430 LamSF_Substitution <> lift_r def
R4455:4472 LamSF_Residuals <> residuals_lift_rec thm
R4455:4472 LamSF_Residuals <> residuals_lift_rec thm
prf 4536:4554 <> residuals_subst_rec
R4577:4583 LamSF_Redexes <> redexes ind
R4605:4608 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4646:4650 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4662:4664 Coq.Init.Datatypes <> nat ind
R4668:4676 LamSF_Residuals <> residuals ind
R4723:4733 LamSF_Substitution <> subst_rec_r def
R4741:4741 LamSF_Residuals <> k var
R4738:4739 LamSF_Residuals <> V3 var
R4735:4736 LamSF_Residuals <> U3 var
R4701:4711 LamSF_Substitution <> subst_rec_r def
R4719:4719 LamSF_Residuals <> k var
R4716:4717 LamSF_Residuals <> V2 var
R4713:4714 LamSF_Residuals <> U2 var
R4679:4689 LamSF_Substitution <> subst_rec_r def
R4697:4697 LamSF_Residuals <> k var
R4694:4695 LamSF_Residuals <> V1 var
R4691:4692 LamSF_Residuals <> U1 var
R4628:4636 LamSF_Residuals <> residuals ind
R4644:4645 LamSF_Residuals <> V3 var
R4641:4642 LamSF_Residuals <> V2 var
R4638:4639 LamSF_Residuals <> V1 var
R4587:4595 LamSF_Residuals <> residuals ind
R4603:4604 LamSF_Residuals <> U3 var
R4600:4601 LamSF_Residuals <> U2 var
R4597:4598 LamSF_Residuals <> U1 var
R4823:4832 LamSF_Substitution <> insert_Var def
R4849:4855 Test <> compare def
R4849:4855 Test <> compare def
R4924:4930 LamSF_Substitution <> subst_r def
R4942:4944 Coq.Init.Logic <> :type_scope:x_'='_x not
R4946:4946 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4942:4944 Coq.Init.Logic <> :type_scope:x_'='_x not
R4946:4946 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4981:4999 LamSF_Substitution <> subst_rec_subst_rec thm
R4981:4999 LamSF_Substitution <> subst_rec_subst_rec thm
R4981:4999 LamSF_Substitution <> subst_rec_subst_rec thm
R5027:5035 LamSF_Residuals <> Res_redex constr
prf 5177:5187 <> commutation
R5219:5225 LamSF_Redexes <> redexes ind
R5247:5251 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5270:5274 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5275:5283 LamSF_Residuals <> residuals ind
R5318:5324 LamSF_Substitution <> subst_r def
R5329:5330 LamSF_Residuals <> U3 var
R5326:5327 LamSF_Residuals <> V3 var
R5302:5308 LamSF_Substitution <> subst_r def
R5313:5314 LamSF_Residuals <> U2 var
R5310:5311 LamSF_Residuals <> V2 var
R5286:5292 LamSF_Substitution <> subst_r def
R5297:5298 LamSF_Residuals <> U1 var
R5294:5295 LamSF_Residuals <> V1 var
R5252:5260 LamSF_Residuals <> residuals ind
R5268:5269 LamSF_Residuals <> V3 var
R5265:5266 LamSF_Residuals <> V2 var
R5262:5263 LamSF_Residuals <> V1 var
R5229:5237 LamSF_Residuals <> residuals ind
R5245:5246 LamSF_Residuals <> U3 var
R5242:5243 LamSF_Residuals <> U2 var
R5239:5240 LamSF_Residuals <> U1 var
R5348:5354 LamSF_Substitution <> subst_r def
prf 5394:5407 <> residuals_comp
R5426:5432 LamSF_Redexes <> redexes ind
R5450:5453 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5454:5457 LamSF_Redexes <> comp ind
R5461:5461 LamSF_Residuals <> V var
R5459:5459 LamSF_Residuals <> U var
R5435:5443 LamSF_Residuals <> residuals ind
R5449:5449 LamSF_Residuals <> W var
R5447:5447 LamSF_Residuals <> V var
R5445:5445 LamSF_Residuals <> U var
prf 5535:5547 <> preservation1
R5568:5574 LamSF_Redexes <> redexes ind
R5594:5598 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5611:5617 LamSF_Redexes <> redexes ind
R5627:5631 LamSF_Redexes <> union ind
R5637:5637 LamSF_Residuals <> T var
R5635:5635 LamSF_Residuals <> V var
R5633:5633 LamSF_Residuals <> U var
R5641:5649 LamSF_Residuals <> residuals ind
R5655:5656 LamSF_Residuals <> UV var
R5653:5653 LamSF_Residuals <> V var
R5651:5651 LamSF_Residuals <> T var
R5578:5586 LamSF_Residuals <> residuals ind
R5592:5593 LamSF_Residuals <> UV var
R5590:5590 LamSF_Residuals <> V var
R5588:5588 LamSF_Residuals <> U var
R5811:5819 LamSF_Redexes <> max_false thm
R5811:5819 LamSF_Redexes <> max_false thm
R5811:5819 LamSF_Redexes <> max_false thm
prf 5885:5896 <> preservation
R5919:5925 LamSF_Redexes <> redexes ind
R5940:5943 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5960:5963 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5964:5972 LamSF_Residuals <> residuals ind
R5978:5979 LamSF_Residuals <> UV var
R5976:5976 LamSF_Residuals <> V var
R5974:5974 LamSF_Residuals <> W var
R5944:5952 LamSF_Residuals <> residuals ind
R5958:5959 LamSF_Residuals <> UV var
R5956:5956 LamSF_Residuals <> V var
R5954:5954 LamSF_Residuals <> U var
R5929:5933 LamSF_Redexes <> union ind
R5939:5939 LamSF_Residuals <> W var
R5937:5937 LamSF_Residuals <> V var
R5935:5935 LamSF_Residuals <> U var
R6003:6015 LamSF_Residuals <> preservation1 thm
R6003:6015 LamSF_Residuals <> preservation1 thm
prf 6054:6074 <> mutual_residuals_comp
R6096:6102 LamSF_Redexes <> redexes ind
R6111:6119 LamSF_Residuals <> residuals ind
R6125:6126 LamSF_Residuals <> UW var
R6123:6123 LamSF_Residuals <> W var
R6121:6121 LamSF_Residuals <> U var
R6141:6147 LamSF_Redexes <> redexes ind
R6156:6164 LamSF_Residuals <> residuals ind
R6170:6171 LamSF_Residuals <> VW var
R6168:6168 LamSF_Residuals <> W var
R6166:6166 LamSF_Residuals <> V var
R6175:6178 LamSF_Redexes <> comp ind
R6183:6184 LamSF_Residuals <> VW var
R6180:6181 LamSF_Residuals <> UW var
R6417:6424 LamSF_Redexes <> Comp_Fun constr
R6501:6507 LamSF_Redexes <> Comp_Ap constr
R6501:6507 LamSF_Redexes <> Comp_Ap constr
R6586:6604 LamSF_Substitution <> subst_preserve_comp thm
R6586:6604 LamSF_Substitution <> subst_preserve_comp thm
R6614:6622 LamSF_Residuals <> residuals ind
R6643:6645 LamSF_Redexes <> Fun constr
R6634:6636 LamSF_Redexes <> Fun constr
R6625:6627 LamSF_Redexes <> Fun constr
R6614:6622 LamSF_Residuals <> residuals ind
R6643:6645 LamSF_Redexes <> Fun constr
R6634:6636 LamSF_Redexes <> Fun constr
R6625:6627 LamSF_Redexes <> Fun constr
R6661:6667 LamSF_Residuals <> Res_Fun constr
R6678:6686 LamSF_Residuals <> residuals ind
R6707:6709 LamSF_Redexes <> Fun constr
R6698:6700 LamSF_Redexes <> Fun constr
R6689:6691 LamSF_Redexes <> Fun constr
R6678:6686 LamSF_Residuals <> residuals ind
R6707:6709 LamSF_Redexes <> Fun constr
R6698:6700 LamSF_Redexes <> Fun constr
R6689:6691 LamSF_Redexes <> Fun constr
R6725:6731 LamSF_Residuals <> Res_Fun constr
R6741:6744 LamSF_Redexes <> comp ind
R6756:6758 LamSF_Redexes <> Fun constr
R6747:6749 LamSF_Redexes <> Fun constr
R6811:6813 LamSF_Redexes <> Fun constr
R6802:6804 LamSF_Redexes <> Fun constr
R6790:6792 LamSF_Redexes <> Fun constr
R6781:6783 LamSF_Redexes <> Fun constr
R6741:6744 LamSF_Redexes <> comp ind
R6756:6758 LamSF_Redexes <> Fun constr
R6747:6749 LamSF_Redexes <> Fun constr
R6811:6813 LamSF_Redexes <> Fun constr
R6802:6804 LamSF_Redexes <> Fun constr
R6790:6792 LamSF_Redexes <> Fun constr
R6781:6783 LamSF_Redexes <> Fun constr
prf 6928:6944 <> residuals_regular
R6964:6970 LamSF_Redexes <> redexes ind
R6988:6991 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6992:6998 LamSF_Redexes <> regular def
R7000:7000 LamSF_Residuals <> V var
R6973:6981 LamSF_Residuals <> residuals ind
R6987:6987 LamSF_Residuals <> W var
R6985:6985 LamSF_Residuals <> V var
R6983:6983 LamSF_Residuals <> U var
prf 7201:7215 <> residuals_intro
R7233:7239 LamSF_Redexes <> redexes ind
R7251:7254 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7264:7267 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7268:7274 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R7286:7287 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R7279:7285 LamSF_Redexes <> redexes ind
R7288:7296 LamSF_Residuals <> residuals ind
R7302:7302 LamSF_Residuals <> W var
R7300:7300 LamSF_Residuals <> V var
R7298:7298 LamSF_Residuals <> U var
R7255:7261 LamSF_Redexes <> regular def
R7263:7263 LamSF_Residuals <> V var
R7243:7246 LamSF_Redexes <> comp ind
R7250:7250 LamSF_Residuals <> V var
R7248:7248 LamSF_Residuals <> U var
R7450:7451 LamSF_Redexes <> Ap constr
R7450:7451 LamSF_Redexes <> Ap constr
R7565:7571 LamSF_Substitution <> subst_r def
R7565:7571 LamSF_Substitution <> subst_r def
prf 7629:7654 <> residuals_preserve_regular
R7674:7680 LamSF_Redexes <> redexes ind
R7698:7701 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7711:7714 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7715:7721 LamSF_Redexes <> regular def
R7723:7723 LamSF_Residuals <> W var
R7702:7708 LamSF_Redexes <> regular def
R7710:7710 LamSF_Residuals <> U var
R7683:7691 LamSF_Residuals <> residuals ind
R7697:7697 LamSF_Residuals <> W var
R7695:7695 LamSF_Residuals <> V var
R7693:7693 LamSF_Residuals <> U var
R7952:7977 LamSF_Substitution <> subst_rec_preserve_regular thm
R7952:7977 LamSF_Substitution <> subst_rec_preserve_regular thm