-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathLamSF_Cube.glob
366 lines (366 loc) · 13.7 KB
/
LamSF_Cube.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
DIGEST 2f4eb227527ea8c6a4c92a7e0dafb1e9
FLamSF_Cube
R2282:2286 Coq.Arith.Arith <> <> lib
R2304:2314 LamSF_Terms <> <> lib
R2332:2338 General <> <> lib
R2356:2369 Beta_Reduction <> <> lib
R2387:2399 LamSF_Redexes <> <> lib
R2417:2420 Test <> <> lib
R2438:2455 LamSF_Substitution <> <> lib
R2473:2487 LamSF_Residuals <> <> lib
ind 2733:2738 <> compat
constr 2787:2796 <> Compat_Var
constr 2845:2855 <> Compat_Oper
constr 2904:2913 <> Compat_Ap1
constr 3116:3125 <> Compat_Ap2
constr 3342:3351 <> Compat_Fun
R2764:2770 LamSF_Redexes <> redexes ind
R2753:2759 LamSF_Redexes <> redexes ind
R2742:2748 LamSF_Redexes <> redexes ind
R2810:2815 LamSF_Cube <> compat ind
R2834:2836 LamSF_Redexes <> Var constr
R2838:2838 LamSF_Cube <> i var
R2826:2828 LamSF_Redexes <> Var constr
R2830:2830 LamSF_Cube <> i var
R2818:2820 LamSF_Redexes <> Var constr
R2822:2822 LamSF_Cube <> i var
R2869:2874 LamSF_Cube <> compat ind
R2893:2895 LamSF_Redexes <> Opp constr
R2897:2897 LamSF_Cube <> o var
R2885:2887 LamSF_Redexes <> Opp constr
R2889:2889 LamSF_Cube <> o var
R2877:2879 LamSF_Redexes <> Opp constr
R2881:2881 LamSF_Cube <> o var
R2941:2947 LamSF_Redexes <> redexes ind
R2999:3005 LamSF_Redexes <> redexes ind
R3051:3054 Coq.Init.Datatypes <> bool ind
R3058:3063 LamSF_Cube <> compat ind
R3100:3101 LamSF_Redexes <> Ap constr
R3108:3109 LamSF_Cube <> W2 var
R3105:3106 LamSF_Cube <> W1 var
R3103:3103 LamSF_Cube <> b var
R3083:3084 LamSF_Redexes <> Ap constr
R3095:3096 LamSF_Cube <> V2 var
R3092:3093 LamSF_Cube <> V1 var
R3086:3090 Coq.Init.Datatypes <> false constr
R3066:3067 LamSF_Redexes <> Ap constr
R3078:3079 LamSF_Cube <> U2 var
R3075:3076 LamSF_Cube <> U1 var
R3069:3073 Coq.Init.Datatypes <> false constr
R3014:3019 LamSF_Cube <> compat ind
R3027:3028 LamSF_Cube <> W2 var
R3024:3025 LamSF_Cube <> V2 var
R3021:3022 LamSF_Cube <> U2 var
R2956:2961 LamSF_Cube <> compat ind
R2969:2970 LamSF_Cube <> W1 var
R2966:2967 LamSF_Cube <> V1 var
R2963:2964 LamSF_Cube <> U1 var
R3202:3208 LamSF_Redexes <> redexes ind
R3257:3260 Coq.Init.Datatypes <> bool ind
R3270:3275 LamSF_Cube <> compat ind
R3319:3320 LamSF_Redexes <> Ap constr
R3334:3335 LamSF_Cube <> W2 var
R3326:3328 LamSF_Redexes <> Fun constr
R3330:3331 LamSF_Cube <> W1 var
R3322:3323 LamSF_Cube <> b' var
R3300:3301 LamSF_Redexes <> Ap constr
R3314:3315 LamSF_Cube <> V2 var
R3306:3308 LamSF_Redexes <> Fun constr
R3310:3311 LamSF_Cube <> V1 var
R3303:3303 LamSF_Cube <> b var
R3278:3279 LamSF_Redexes <> Ap constr
R3295:3296 LamSF_Cube <> U2 var
R3287:3289 LamSF_Redexes <> Fun constr
R3291:3292 LamSF_Cube <> U1 var
R3281:3284 Coq.Init.Datatypes <> true constr
R3217:3222 LamSF_Cube <> compat ind
R3230:3231 LamSF_Cube <> W2 var
R3227:3228 LamSF_Cube <> V2 var
R3224:3225 LamSF_Cube <> U2 var
R3159:3164 LamSF_Cube <> compat ind
R3172:3173 LamSF_Cube <> W1 var
R3169:3170 LamSF_Cube <> V1 var
R3166:3167 LamSF_Cube <> U1 var
R3391:3396 LamSF_Cube <> compat ind
R3415:3417 LamSF_Redexes <> Fun constr
R3419:3419 LamSF_Cube <> W var
R3407:3409 LamSF_Redexes <> Fun constr
R3411:3411 LamSF_Cube <> V var
R3399:3401 LamSF_Redexes <> Fun constr
R3403:3403 LamSF_Cube <> U var
R3375:3380 LamSF_Cube <> compat ind
R3386:3386 LamSF_Cube <> W var
R3384:3384 LamSF_Cube <> V var
R3382:3382 LamSF_Cube <> U var
R3438:3447 LamSF_Cube <> Compat_Var constr
R3449:3459 LamSF_Cube <> Compat_Oper constr
R3461:3470 LamSF_Cube <> Compat_Ap1 constr
R3472:3481 LamSF_Cube <> Compat_Ap2 constr
R3483:3492 LamSF_Cube <> Compat_Fun constr
prf 3502:3513 <> compat_intro
R3534:3540 LamSF_Redexes <> redexes ind
R3580:3586 LamSF_Redexes <> redexes ind
R3595:3603 LamSF_Residuals <> residuals ind
R3609:3610 LamSF_Cube <> WV var
R3607:3607 LamSF_Cube <> V var
R3605:3605 LamSF_Cube <> W var
R3618:3620 LamSF_Redexes <> sub ind
R3624:3624 LamSF_Cube <> U var
R3622:3622 LamSF_Cube <> V var
R3628:3633 LamSF_Cube <> compat ind
R3639:3639 LamSF_Cube <> W var
R3637:3637 LamSF_Cube <> V var
R3635:3635 LamSF_Cube <> U var
R3544:3552 LamSF_Residuals <> residuals ind
R3558:3559 LamSF_Cube <> WU var
R3556:3556 LamSF_Cube <> U var
R3554:3554 LamSF_Cube <> W var
R3742:3742 Coq.Init.Datatypes <> S constr
R3841:3850 LamSF_Cube <> Compat_Ap1 constr
R3904:3913 LamSF_Cube <> Compat_Fun constr
R3986:3995 LamSF_Cube <> Compat_Ap2 constr
R4122:4131 LamSF_Cube <> Compat_Ap2 constr
R4210:4219 LamSF_Cube <> Compat_Ap2 constr
R4298:4307 LamSF_Cube <> Compat_Ap2 constr
prf 4323:4328 <> prism0
R4348:4354 LamSF_Redexes <> redexes ind
R4388:4394 LamSF_Redexes <> redexes ind
R4403:4411 LamSF_Residuals <> residuals ind
R4417:4418 LamSF_Cube <> UV var
R4415:4415 LamSF_Cube <> V var
R4413:4413 LamSF_Cube <> U var
R4430:4436 LamSF_Redexes <> redexes ind
R4448:4456 LamSF_Residuals <> residuals ind
R4462:4463 LamSF_Cube <> WU var
R4460:4460 LamSF_Cube <> U var
R4458:4458 LamSF_Cube <> W var
R4472:4480 LamSF_Residuals <> residuals ind
R4486:4487 LamSF_Cube <> WV var
R4484:4484 LamSF_Cube <> V var
R4482:4482 LamSF_Cube <> W var
R4493:4501 LamSF_Residuals <> residuals ind
R4509:4510 LamSF_Cube <> WU var
R4506:4507 LamSF_Cube <> UV var
R4503:4504 LamSF_Cube <> WV var
R4358:4363 LamSF_Cube <> compat ind
R4369:4369 LamSF_Cube <> W var
R4367:4367 LamSF_Cube <> V var
R4365:4365 LamSF_Cube <> U var
R4734:4740 LamSF_Substitution <> subst_r def
R4751:4769 LamSF_Residuals <> residuals_subst_rec thm
prf 5432:5437 <> prism1
R5457:5463 LamSF_Redexes <> redexes ind
R5491:5497 LamSF_Redexes <> redexes ind
R5534:5540 LamSF_Redexes <> redexes ind
R5577:5583 LamSF_Redexes <> redexes ind
R5606:5614 LamSF_Residuals <> residuals ind
R5622:5623 LamSF_Cube <> WU var
R5619:5620 LamSF_Cube <> UV var
R5616:5617 LamSF_Cube <> WV var
R5586:5594 LamSF_Residuals <> residuals ind
R5600:5601 LamSF_Cube <> WU var
R5598:5598 LamSF_Cube <> U var
R5596:5596 LamSF_Cube <> W var
R5544:5552 LamSF_Residuals <> residuals ind
R5558:5559 LamSF_Cube <> WV var
R5556:5556 LamSF_Cube <> V var
R5554:5554 LamSF_Cube <> W var
R5501:5509 LamSF_Residuals <> residuals ind
R5515:5516 LamSF_Cube <> UV var
R5513:5513 LamSF_Cube <> V var
R5511:5511 LamSF_Cube <> U var
R5467:5469 LamSF_Redexes <> sub ind
R5473:5473 LamSF_Cube <> U var
R5471:5471 LamSF_Cube <> V var
R5647:5652 LamSF_Cube <> prism0 thm
R5647:5652 LamSF_Cube <> prism0 thm
R5678:5689 LamSF_Cube <> compat_intro thm
R5678:5689 LamSF_Cube <> compat_intro thm
prf 5775:5780 <> prism2
R5800:5806 LamSF_Redexes <> redexes ind
R5848:5854 LamSF_Redexes <> redexes ind
R5891:5897 LamSF_Redexes <> redexes ind
R5934:5940 LamSF_Redexes <> redexes ind
R5965:5973 LamSF_Residuals <> residuals ind
R5979:5980 LamSF_Cube <> WU var
R5977:5977 LamSF_Cube <> U var
R5975:5975 LamSF_Cube <> W var
R5943:5951 LamSF_Residuals <> residuals ind
R5959:5960 LamSF_Cube <> WU var
R5956:5957 LamSF_Cube <> UV var
R5953:5954 LamSF_Cube <> WV var
R5901:5909 LamSF_Residuals <> residuals ind
R5915:5916 LamSF_Cube <> WV var
R5913:5913 LamSF_Cube <> V var
R5911:5911 LamSF_Cube <> W var
R5858:5866 LamSF_Residuals <> residuals ind
R5872:5873 LamSF_Cube <> UV var
R5870:5870 LamSF_Cube <> V var
R5868:5868 LamSF_Cube <> U var
R5822:5828 LamSF_Redexes <> regular def
R5830:5830 LamSF_Cube <> U var
R5810:5812 LamSF_Redexes <> sub ind
R5816:5816 LamSF_Cube <> U var
R5814:5814 LamSF_Cube <> V var
R6004:6018 LamSF_Residuals <> residuals_intro thm
R6004:6018 LamSF_Residuals <> residuals_intro thm
R6055:6072 LamSF_Residuals <> residuals_function thm
R6055:6072 LamSF_Residuals <> residuals_function thm
R6109:6114 LamSF_Cube <> prism1 thm
R6109:6114 LamSF_Cube <> prism1 thm
R6143:6152 LamSF_Redexes <> comp_trans thm
R6143:6152 LamSF_Redexes <> comp_trans thm
R6168:6181 LamSF_Residuals <> residuals_comp thm
R6168:6181 LamSF_Residuals <> residuals_comp thm
R6207:6214 LamSF_Redexes <> comp_sym thm
R6223:6236 LamSF_Residuals <> residuals_comp thm
R6207:6214 LamSF_Redexes <> comp_sym thm
R6223:6236 LamSF_Residuals <> residuals_comp thm
prf 6270:6274 <> prism
R6294:6300 LamSF_Redexes <> redexes ind
R6328:6334 LamSF_Redexes <> redexes ind
R6371:6377 LamSF_Redexes <> redexes ind
R6414:6420 LamSF_Redexes <> redexes ind
R6439:6443 Coq.Init.Logic <> :type_scope:x_'<->'_x not
R6423:6431 LamSF_Residuals <> residuals ind
R6437:6438 LamSF_Cube <> WU var
R6435:6435 LamSF_Cube <> U var
R6433:6433 LamSF_Cube <> W var
R6453:6456 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R6444:6450 LamSF_Redexes <> regular def
R6452:6452 LamSF_Cube <> U var
R6457:6465 LamSF_Residuals <> residuals ind
R6473:6474 LamSF_Cube <> WU var
R6470:6471 LamSF_Cube <> UV var
R6467:6468 LamSF_Cube <> WV var
R6381:6389 LamSF_Residuals <> residuals ind
R6395:6396 LamSF_Cube <> WV var
R6393:6393 LamSF_Cube <> V var
R6391:6391 LamSF_Cube <> W var
R6338:6346 LamSF_Residuals <> residuals ind
R6352:6353 LamSF_Cube <> UV var
R6350:6350 LamSF_Cube <> V var
R6348:6348 LamSF_Cube <> U var
R6304:6306 LamSF_Redexes <> sub ind
R6310:6310 LamSF_Cube <> U var
R6308:6308 LamSF_Cube <> V var
R6499:6501 Coq.Init.Logic <> iff def
R6539:6555 LamSF_Residuals <> residuals_regular thm
R6539:6555 LamSF_Residuals <> residuals_regular thm
R6583:6588 LamSF_Cube <> prism1 thm
R6583:6588 LamSF_Cube <> prism1 thm
R6645:6650 LamSF_Cube <> prism2 thm
R6645:6650 LamSF_Cube <> prism2 thm
prf 7151:7154 <> cube
R7178:7184 LamSF_Redexes <> redexes ind
R7251:7257 LamSF_Redexes <> redexes ind
R7325:7333 LamSF_Residuals <> residuals ind
R7341:7343 LamSF_Cube <> WUV var
R7338:7339 LamSF_Cube <> UV var
R7335:7336 LamSF_Cube <> WV var
R7305:7313 LamSF_Residuals <> residuals ind
R7319:7320 LamSF_Cube <> WV var
R7317:7317 LamSF_Cube <> V var
R7315:7315 LamSF_Cube <> W var
R7282:7290 LamSF_Residuals <> residuals ind
R7298:7300 LamSF_Cube <> WUV var
R7295:7296 LamSF_Cube <> VU var
R7292:7293 LamSF_Cube <> WU var
R7261:7269 LamSF_Residuals <> residuals ind
R7275:7276 LamSF_Cube <> WU var
R7273:7273 LamSF_Cube <> U var
R7271:7271 LamSF_Cube <> W var
R7209:7217 LamSF_Residuals <> residuals ind
R7223:7224 LamSF_Cube <> VU var
R7221:7221 LamSF_Cube <> U var
R7219:7219 LamSF_Cube <> V var
R7188:7196 LamSF_Residuals <> residuals ind
R7202:7203 LamSF_Cube <> UV var
R7200:7200 LamSF_Cube <> V var
R7198:7198 LamSF_Cube <> U var
R7366:7369 LamSF_Redexes <> comp ind
R7366:7369 LamSF_Redexes <> comp ind
R7386:7399 LamSF_Residuals <> residuals_comp thm
R7386:7399 LamSF_Residuals <> residuals_comp thm
R7434:7446 LamSF_Redexes <> union_defined thm
R7434:7446 LamSF_Redexes <> union_defined thm
R7476:7481 LamSF_Cube <> prism1 thm
R7476:7481 LamSF_Cube <> prism1 thm
R7510:7516 LamSF_Redexes <> union_r thm
R7510:7516 LamSF_Redexes <> union_r thm
R7541:7552 LamSF_Residuals <> preservation thm
R7541:7552 LamSF_Residuals <> preservation thm
R7577:7582 LamSF_Cube <> prism2 thm
R7577:7582 LamSF_Cube <> prism2 thm
R7613:7619 LamSF_Redexes <> union_l thm
R7613:7619 LamSF_Redexes <> union_l thm
R7644:7665 LamSF_Redexes <> union_preserve_regular thm
R7644:7665 LamSF_Redexes <> union_preserve_regular thm
R7692:7708 LamSF_Residuals <> residuals_regular thm
R7692:7708 LamSF_Residuals <> residuals_regular thm
R7736:7752 LamSF_Residuals <> residuals_regular thm
R7736:7752 LamSF_Residuals <> residuals_regular thm
R7780:7791 LamSF_Residuals <> preservation thm
R7780:7791 LamSF_Residuals <> preservation thm
R7816:7824 LamSF_Redexes <> union_sym thm
R7816:7824 LamSF_Redexes <> union_sym thm
prf 7884:7889 <> paving
R7915:7921 LamSF_Redexes <> redexes ind
R7967:7973 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R7986:7991 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R8085:8085 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R7979:7985 LamSF_Redexes <> redexes ind
R7992:7998 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R8011:8019 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R8084:8084 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R8004:8010 LamSF_Redexes <> redexes ind
R8020:8026 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R8040:8041 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R8033:8039 LamSF_Redexes <> redexes ind
R8061:8064 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R8042:8050 LamSF_Residuals <> residuals ind
R8058:8060 LamSF_Cube <> WUV var
R8055:8056 LamSF_Cube <> VU var
R8052:8053 LamSF_Cube <> WU var
R8065:8073 LamSF_Residuals <> residuals ind
R8081:8083 LamSF_Cube <> WUV var
R8078:8079 LamSF_Cube <> UV var
R8075:8076 LamSF_Cube <> WV var
R7946:7954 LamSF_Residuals <> residuals ind
R7960:7961 LamSF_Cube <> WV var
R7958:7958 LamSF_Cube <> V var
R7956:7956 LamSF_Cube <> W var
R7925:7933 LamSF_Residuals <> residuals ind
R7939:7940 LamSF_Cube <> WU var
R7937:7937 LamSF_Cube <> U var
R7935:7935 LamSF_Cube <> W var
R8109:8123 LamSF_Residuals <> residuals_intro thm
R8109:8123 LamSF_Residuals <> residuals_intro thm
R8162:8176 LamSF_Residuals <> residuals_intro thm
R8162:8176 LamSF_Residuals <> residuals_intro thm
R8215:8229 LamSF_Residuals <> residuals_intro thm
R8215:8229 LamSF_Residuals <> residuals_intro thm
R8288:8291 LamSF_Cube <> cube thm
R8288:8291 LamSF_Cube <> cube thm
R8326:8346 LamSF_Residuals <> mutual_residuals_comp thm
R8326:8346 LamSF_Residuals <> mutual_residuals_comp thm
R8375:8400 LamSF_Residuals <> residuals_preserve_regular thm
R8375:8400 LamSF_Residuals <> residuals_preserve_regular thm
R8427:8443 LamSF_Residuals <> residuals_regular thm
R8427:8443 LamSF_Residuals <> residuals_regular thm
R8471:8478 LamSF_Redexes <> comp_sym thm
R8487:8500 LamSF_Residuals <> residuals_comp thm
R8471:8478 LamSF_Redexes <> comp_sym thm
R8487:8500 LamSF_Residuals <> residuals_comp thm
R8526:8542 LamSF_Residuals <> residuals_regular thm
R8526:8542 LamSF_Residuals <> residuals_regular thm
R8570:8579 LamSF_Redexes <> comp_trans thm
R8570:8579 LamSF_Redexes <> comp_trans thm
R8595:8602 LamSF_Redexes <> comp_sym thm
R8611:8624 LamSF_Residuals <> residuals_comp thm
R8595:8602 LamSF_Redexes <> comp_sym thm
R8611:8624 LamSF_Residuals <> residuals_comp thm
R8650:8663 LamSF_Residuals <> residuals_comp thm
R8650:8663 LamSF_Residuals <> residuals_comp thm
R8689:8705 LamSF_Residuals <> residuals_regular thm
R8689:8705 LamSF_Residuals <> residuals_regular thm