forked from Barry-Jay/lambdaSF
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathCombinators.glob
705 lines (705 loc) · 28.6 KB
/
Combinators.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
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
DIGEST 818fdb217954e2c2638fc483d146b3a7
FCombinators
R1992:1996 Coq.Arith.Arith <> <> lib
R2014:2016 Coq.Arith.Max <> <> lib
R2035:2038 Test <> <> lib
R2056:2062 General <> <> lib
R2081:2091 LamSF_Terms <> <> lib
R2109:2131 LamSF_Substitution_term <> <> lib
R2149:2161 LamSF_Tactics <> <> lib
R2179:2192 Beta_Reduction <> <> lib
R2210:2225 LamSF_Confluence <> <> lib
R2243:2254 SF_reduction <> <> lib
R2272:2286 LamSF_reduction <> <> lib
R2304:2315 LamSF_Normal <> <> lib
R2333:2344 LamSF_Closed <> <> lib
R2362:2371 LamSF_Eval <> <> lib
R2389:2393 Equal <> <> lib
R2411:2415 Coq.omega.Omega <> <> lib
R2473:2477 LamSF_Terms <> subst def
R2487:2495 LamSF_Terms <> subst_rec def
R2503:2511 LamSF_Terms <> subst_rec def
R2546:2558 LamSF_Substitution_term <> lift_rec_null thm
def 2575:2579 <> abs_K
R2584:2586 LamSF_Terms <> Abs constr
R2589:2591 LamSF_Terms <> Abs constr
R2594:2596 LamSF_Terms <> Ref constr
def 2615:2619 <> abs_S
R2625:2627 LamSF_Terms <> Abs constr
R2629:2631 LamSF_Terms <> Abs constr
R2634:2636 LamSF_Terms <> Abs constr
R2639:2641 LamSF_Terms <> App constr
R2666:2668 LamSF_Terms <> App constr
R2679:2681 LamSF_Terms <> Ref constr
R2671:2673 LamSF_Terms <> Ref constr
R2644:2646 LamSF_Terms <> App constr
R2657:2659 LamSF_Terms <> Ref constr
R2649:2651 LamSF_Terms <> Ref constr
ind 2705:2714 <> combinator
constr 2738:2744 <> comb_op
constr 2778:2785 <> comb_app
R2723:2726 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2718:2722 LamSF_Terms <> lamSF ind
R2758:2767 Combinators <> combinator ind
R2770:2771 LamSF_Terms <> Op constr
R2773:2773 Combinators <> o var
R2813:2816 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2829:2832 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2833:2842 Combinators <> combinator ind
R2845:2847 LamSF_Terms <> App constr
R2851:2851 Combinators <> N var
R2849:2849 Combinators <> M var
R2817:2826 Combinators <> combinator ind
R2828:2828 Combinators <> N var
R2801:2810 Combinators <> combinator ind
R2812:2812 Combinators <> M var
prf 2896:2915 <> combinator_decidable
R2940:2944 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R2966:2966 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R2928:2937 Combinators <> combinator ind
R2939:2939 Combinators <> M var
R2957:2960 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2961:2965 Coq.Init.Logic <> False ind
R2945:2954 Combinators <> combinator ind
R2956:2956 Combinators <> M var
def 3221:3229 <> star_comb
R3234:3236 LamSF_Terms <> Abs constr
R3239:3241 LamSF_Terms <> App constr
R3286:3288 LamSF_Terms <> App constr
R3295:3298 SF_reduction <> i_op def
R3290:3293 SF_reduction <> k_op def
R3244:3246 LamSF_Terms <> App constr
R3279:3282 SF_reduction <> k_op def
R3249:3251 LamSF_Terms <> App constr
R3259:3261 LamSF_Terms <> App constr
R3270:3272 LamSF_Terms <> Ref constr
R3263:3267 Combinators <> abs_K def
R3253:3256 SF_reduction <> f_op def
prf 3311:3324 <> star_comb_star
R3346:3349 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3362:3365 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3366:3374 LamSF_reduction <> lamSF_red def
R3395:3398 SF_reduction <> star def
R3400:3400 Combinators <> M var
R3377:3379 LamSF_Terms <> App constr
R3391:3391 Combinators <> M var
R3381:3389 Combinators <> star_comb def
R3358:3360 Coq.Init.Logic <> :type_scope:x_'='_x not
R3350:3355 LamSF_Closed <> maxvar def
R3357:3357 Combinators <> M var
R3338:3343 LamSF_Normal <> normal ind
R3345:3345 Combinators <> M var
R3433:3441 Combinators <> star_comb def
R3475:3479 Combinators <> abs_K def
R3489:3497 LamSF_Terms <> subst_rec def
R3505:3513 LamSF_Terms <> subst_rec def
R3505:3513 LamSF_Terms <> subst_rec def
R3555:3557 LamSF_Terms <> App constr
R3656:3658 LamSF_Terms <> App constr
R3696:3698 LamSF_Terms <> App constr
R3754:3756 LamSF_Terms <> App constr
R3768:3769 LamSF_Terms <> Op constr
R3771:3773 LamSF_Terms <> Fop constr
R3759:3760 LamSF_Terms <> Op constr
R3762:3764 LamSF_Terms <> Fop constr
R3701:3703 LamSF_Terms <> App constr
R3715:3717 LamSF_Terms <> App constr
R3729:3730 LamSF_Terms <> Op constr
R3732:3734 LamSF_Terms <> Fop constr
R3720:3721 LamSF_Terms <> Op constr
R3723:3725 LamSF_Terms <> Fop constr
R3706:3707 LamSF_Terms <> Op constr
R3709:3711 LamSF_Terms <> Sop constr
R3661:3663 LamSF_Terms <> App constr
R3675:3676 LamSF_Terms <> Op constr
R3678:3680 LamSF_Terms <> Fop constr
R3666:3667 LamSF_Terms <> Op constr
R3669:3671 LamSF_Terms <> Fop constr
R3568:3570 LamSF_Terms <> App constr
R3623:3625 LamSF_Terms <> App constr
R3637:3638 LamSF_Terms <> Op constr
R3640:3642 LamSF_Terms <> Fop constr
R3628:3629 LamSF_Terms <> Op constr
R3631:3633 LamSF_Terms <> Fop constr
R3573:3575 LamSF_Terms <> App constr
R3587:3591 LamSF_Terms <> subst def
R3596:3598 LamSF_Terms <> Abs constr
R3601:3603 LamSF_Terms <> Ref constr
R3578:3579 LamSF_Terms <> Op constr
R3581:3583 LamSF_Terms <> Fop constr
R3539:3546 LamSF_Tactics <> succ_red constr
R3555:3557 LamSF_Terms <> App constr
R3656:3658 LamSF_Terms <> App constr
R3696:3698 LamSF_Terms <> App constr
R3754:3756 LamSF_Terms <> App constr
R3768:3769 LamSF_Terms <> Op constr
R3771:3773 LamSF_Terms <> Fop constr
R3759:3760 LamSF_Terms <> Op constr
R3762:3764 LamSF_Terms <> Fop constr
R3701:3703 LamSF_Terms <> App constr
R3715:3717 LamSF_Terms <> App constr
R3729:3730 LamSF_Terms <> Op constr
R3732:3734 LamSF_Terms <> Fop constr
R3720:3721 LamSF_Terms <> Op constr
R3723:3725 LamSF_Terms <> Fop constr
R3706:3707 LamSF_Terms <> Op constr
R3709:3711 LamSF_Terms <> Sop constr
R3661:3663 LamSF_Terms <> App constr
R3675:3676 LamSF_Terms <> Op constr
R3678:3680 LamSF_Terms <> Fop constr
R3666:3667 LamSF_Terms <> Op constr
R3669:3671 LamSF_Terms <> Fop constr
R3568:3570 LamSF_Terms <> App constr
R3623:3625 LamSF_Terms <> App constr
R3637:3638 LamSF_Terms <> Op constr
R3640:3642 LamSF_Terms <> Fop constr
R3628:3629 LamSF_Terms <> Op constr
R3631:3633 LamSF_Terms <> Fop constr
R3573:3575 LamSF_Terms <> App constr
R3587:3591 LamSF_Terms <> subst def
R3596:3598 LamSF_Terms <> Abs constr
R3601:3603 LamSF_Terms <> Ref constr
R3578:3579 LamSF_Terms <> Op constr
R3581:3583 LamSF_Terms <> Fop constr
R3539:3546 LamSF_Tactics <> succ_red constr
R3790:3803 LamSF_reduction <> appl_lamSF_red constr
R3814:3818 LamSF_Terms <> subst def
R3828:3836 LamSF_Terms <> subst_rec def
R3844:3852 LamSF_Terms <> subst_rec def
R3844:3852 LamSF_Terms <> subst_rec def
R3880:3894 LamSF_Closed <> lift_rec_closed thm
R3880:3894 LamSF_Closed <> lift_rec_closed thm
R3880:3894 LamSF_Closed <> lift_rec_closed thm
R3880:3894 LamSF_Closed <> lift_rec_closed thm
R3930:3932 LamSF_Terms <> App constr
R3982:3996 SF_reduction <> right_component def
R3999:4001 LamSF_Terms <> Abs constr
R3935:3937 LamSF_Terms <> App constr
R3956:3969 SF_reduction <> left_component def
R3972:3974 LamSF_Terms <> Abs constr
R3940:3942 LamSF_Terms <> App constr
R3949:3952 SF_reduction <> i_op def
R3944:3947 SF_reduction <> k_op def
R3915:3922 LamSF_Tactics <> succ_red constr
R3930:3932 LamSF_Terms <> App constr
R3982:3996 SF_reduction <> right_component def
R3999:4001 LamSF_Terms <> Abs constr
R3935:3937 LamSF_Terms <> App constr
R3956:3969 SF_reduction <> left_component def
R3972:3974 LamSF_Terms <> Abs constr
R3940:3942 LamSF_Terms <> App constr
R3949:3952 SF_reduction <> i_op def
R3944:3947 SF_reduction <> k_op def
R3915:3922 LamSF_Tactics <> succ_red constr
R4018:4037 LamSF_reduction <> f_compound_lamSF_red constr
R4048:4048 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R4071:4075 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R4049:4055 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R4057:4058 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R4064:4066 Coq.Init.Logic <> :type_scope:x_'='_x not
R4059:4061 LamSF_Terms <> Abs constr
R4067:4068 LamSF_Terms <> Op constr
R4070:4070 Combinators <> o var
R4076:4083 SF_reduction <> compound ind
R4086:4088 LamSF_Terms <> Abs constr
R4048:4048 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R4071:4075 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R4049:4055 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R4057:4058 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R4064:4066 Coq.Init.Logic <> :type_scope:x_'='_x not
R4059:4061 LamSF_Terms <> Abs constr
R4067:4068 LamSF_Terms <> Op constr
R4070:4070 Combinators <> o var
R4076:4083 SF_reduction <> compound ind
R4086:4088 LamSF_Terms <> Abs constr
R4104:4124 LamSF_Normal <> not_active_factorable thm
R4149:4152 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R4135:4140 LamSF_Tactics <> status def
R4143:4145 LamSF_Terms <> Abs constr
R4153:4158 LamSF_Closed <> maxvar def
R4161:4163 LamSF_Terms <> Abs constr
R4149:4152 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R4135:4140 LamSF_Tactics <> status def
R4143:4145 LamSF_Terms <> Abs constr
R4153:4158 LamSF_Closed <> maxvar def
R4161:4163 LamSF_Terms <> Abs constr
R4180:4195 LamSF_Closed <> status_lt_maxvar thm
prf 4316:4332 <> maxvar_combinator
R4358:4361 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4362:4367 LamSF_Closed <> closed def
R4369:4369 Combinators <> M var
R4346:4355 Combinators <> combinator ind
R4357:4357 Combinators <> M var
R4386:4391 LamSF_Closed <> closed def
def 4495:4504 <> is_comb_fn
R4509:4511 LamSF_Terms <> Abs constr
R4514:4516 LamSF_Terms <> Abs constr
R4520:4522 LamSF_Terms <> App constr
R4555:4557 LamSF_Terms <> Abs constr
R4560:4562 LamSF_Terms <> Abs constr
R4566:4568 LamSF_Terms <> App constr
R4628:4630 LamSF_Terms <> App constr
R4683:4685 LamSF_Terms <> App constr
R4692:4695 SF_reduction <> i_op def
R4687:4690 SF_reduction <> k_op def
R4633:4635 LamSF_Terms <> App constr
R4660:4662 LamSF_Terms <> App constr
R4673:4675 LamSF_Terms <> Ref constr
R4665:4667 LamSF_Terms <> Ref constr
R4638:4640 LamSF_Terms <> App constr
R4651:4653 LamSF_Terms <> Ref constr
R4643:4645 LamSF_Terms <> Ref constr
R4571:4573 LamSF_Terms <> App constr
R4611:4613 LamSF_Terms <> App constr
R4620:4623 SF_reduction <> i_op def
R4615:4618 SF_reduction <> k_op def
R4576:4578 LamSF_Terms <> App constr
R4602:4604 LamSF_Terms <> Ref constr
R4581:4583 LamSF_Terms <> App constr
R4591:4598 SF_reduction <> abs_left def
R4585:4589 Equal <> equal def
R4525:4527 LamSF_Terms <> App constr
R4548:4551 SF_reduction <> k_op def
R4530:4532 LamSF_Terms <> App constr
R4540:4542 LamSF_Terms <> Ref constr
R4534:4537 SF_reduction <> f_op def
def 4718:4724 <> is_comb
R4729:4731 LamSF_Terms <> App constr
R4742:4751 Combinators <> is_comb_fn def
R4733:4740 LamSF_Eval <> fixpoint def
prf 4764:4775 <> is_comb_true
R4797:4800 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4813:4816 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4817:4825 LamSF_reduction <> lamSF_red def
R4843:4846 SF_reduction <> k_op def
R4828:4830 LamSF_Terms <> App constr
R4840:4840 Combinators <> M var
R4832:4838 Combinators <> is_comb def
R4801:4810 Combinators <> combinator ind
R4812:4812 Combinators <> M var
R4788:4794 LamSF_Closed <> program def
R4796:4796 Combinators <> M var
R4865:4871 LamSF_Closed <> program def
R4927:4933 Combinators <> is_comb def
R4950:4956 Combinators <> is_comb def
R4950:4956 Combinators <> is_comb def
R4966:4975 Combinators <> is_comb_fn def
R4998:5006 LamSF_Terms <> subst_rec def
R5014:5022 LamSF_Terms <> subst_rec def
R5014:5022 LamSF_Terms <> subst_rec def
R5106:5109 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R5090:5095 LamSF_Tactics <> status def
R5098:5100 LamSF_Terms <> App constr
R5110:5115 LamSF_Closed <> maxvar def
R5118:5120 LamSF_Terms <> App constr
R5106:5109 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R5090:5095 LamSF_Tactics <> status def
R5098:5100 LamSF_Terms <> App constr
R5110:5115 LamSF_Closed <> maxvar def
R5118:5120 LamSF_Terms <> App constr
R5139:5154 LamSF_Closed <> status_lt_maxvar thm
R5195:5201 Combinators <> is_comb def
R5218:5224 Combinators <> is_comb def
R5218:5224 Combinators <> is_comb def
R5234:5243 Combinators <> is_comb_fn def
R5266:5274 LamSF_Terms <> subst_rec def
R5282:5290 LamSF_Terms <> subst_rec def
R5282:5290 LamSF_Terms <> subst_rec def
R5317:5329 LamSF_Substitution_term <> lift_rec_null thm
R5317:5329 LamSF_Substitution_term <> lift_rec_null thm
R5317:5329 LamSF_Substitution_term <> lift_rec_null thm
R5340:5352 LamSF_Substitution_term <> lift_rec_null thm
R5340:5352 LamSF_Substitution_term <> lift_rec_null thm
R5340:5352 LamSF_Substitution_term <> lift_rec_null thm
R5372:5387 LamSF_Closed <> subst_rec_closed thm
R5389:5393 Equal <> equal def
R5372:5387 LamSF_Closed <> subst_rec_closed thm
R5389:5393 Equal <> equal def
R5372:5387 LamSF_Closed <> subst_rec_closed thm
R5389:5393 Equal <> equal def
R5372:5387 LamSF_Closed <> subst_rec_closed thm
R5389:5393 Equal <> equal def
R5372:5387 LamSF_Closed <> subst_rec_closed thm
R5389:5393 Equal <> equal def
R5423:5440 LamSF_Substitution_term <> subst_rec_lift_rec thm
R5423:5440 LamSF_Substitution_term <> subst_rec_lift_rec thm
R5423:5440 LamSF_Substitution_term <> subst_rec_lift_rec thm
R5423:5440 LamSF_Substitution_term <> subst_rec_lift_rec thm
R5423:5440 LamSF_Substitution_term <> subst_rec_lift_rec thm
R5476:5490 LamSF_Closed <> lift_rec_closed thm
R5476:5490 LamSF_Closed <> lift_rec_closed thm
R5476:5490 LamSF_Closed <> lift_rec_closed thm
R5476:5490 LamSF_Closed <> lift_rec_closed thm
R5540:5549 LamSF_Tactics <> multi_step ind
R5563:5565 LamSF_Terms <> App constr
R5551:5560 LamSF_reduction <> lamSF_red1 ind
R5540:5549 LamSF_Tactics <> multi_step ind
R5563:5565 LamSF_Terms <> App constr
R5551:5560 LamSF_reduction <> lamSF_red1 ind
R5601:5603 LamSF_Terms <> App constr
R5642:5656 SF_reduction <> right_component def
R5659:5661 LamSF_Terms <> App constr
R5606:5608 LamSF_Terms <> App constr
R5614:5627 SF_reduction <> left_component def
R5630:5632 LamSF_Terms <> App constr
R5586:5593 LamSF_Tactics <> succ_red constr
R5601:5603 LamSF_Terms <> App constr
R5642:5656 SF_reduction <> right_component def
R5659:5661 LamSF_Terms <> App constr
R5606:5608 LamSF_Terms <> App constr
R5614:5627 SF_reduction <> left_component def
R5630:5632 LamSF_Terms <> App constr
R5586:5593 LamSF_Tactics <> succ_red constr
R5684:5703 LamSF_reduction <> f_compound_lamSF_red constr
R5735:5750 LamSF_Closed <> subst_rec_closed thm
R5752:5756 Equal <> equal def
R5735:5750 LamSF_Closed <> subst_rec_closed thm
R5752:5756 Equal <> equal def
R5735:5750 LamSF_Closed <> subst_rec_closed thm
R5752:5756 Equal <> equal def
R5735:5750 LamSF_Closed <> subst_rec_closed thm
R5752:5756 Equal <> equal def
R5735:5750 LamSF_Closed <> subst_rec_closed thm
R5752:5756 Equal <> equal def
R5785:5798 SF_reduction <> left_component def
R5801:5815 SF_reduction <> right_component def
R5827:5844 LamSF_Substitution_term <> subst_rec_lift_rec thm
R5827:5844 LamSF_Substitution_term <> subst_rec_lift_rec thm
R5827:5844 LamSF_Substitution_term <> subst_rec_lift_rec thm
R5827:5844 LamSF_Substitution_term <> subst_rec_lift_rec thm
R5827:5844 LamSF_Substitution_term <> subst_rec_lift_rec thm
R5880:5892 LamSF_Substitution_term <> lift_rec_null thm
R5880:5892 LamSF_Substitution_term <> lift_rec_null thm
R5880:5892 LamSF_Substitution_term <> lift_rec_null thm
R5917:5926 LamSF_Tactics <> multi_step ind
R5940:5942 LamSF_Terms <> App constr
R5945:5947 LamSF_Terms <> App constr
R5928:5937 LamSF_reduction <> lamSF_red1 ind
R5917:5926 LamSF_Tactics <> multi_step ind
R5940:5942 LamSF_Terms <> App constr
R5945:5947 LamSF_Terms <> App constr
R5928:5937 LamSF_reduction <> lamSF_red1 ind
R5991:5993 LamSF_Terms <> App constr
R5996:5998 LamSF_Terms <> App constr
R6001:6003 LamSF_Terms <> App constr
R6010:6013 SF_reduction <> i_op def
R6005:6008 SF_reduction <> k_op def
R5970:5983 LamSF_Tactics <> transitive_red thm
R5991:5993 LamSF_Terms <> App constr
R5996:5998 LamSF_Terms <> App constr
R6001:6003 LamSF_Terms <> App constr
R6010:6013 SF_reduction <> i_op def
R6005:6008 SF_reduction <> k_op def
R5970:5983 LamSF_Tactics <> transitive_red thm
R6036:6058 LamSF_reduction <> preserves_app_lamSF_red thm
R6070:6092 LamSF_reduction <> preserves_app_lamSF_red thm
R6104:6119 Equal <> unequal_programs thm
R6205:6220 LamSF_Closed <> subst_rec_closed thm
R6205:6220 LamSF_Closed <> subst_rec_closed thm
R6205:6220 LamSF_Closed <> subst_rec_closed thm
R6205:6220 LamSF_Closed <> subst_rec_closed thm
R6205:6220 LamSF_Closed <> subst_rec_closed thm
R6205:6220 LamSF_Closed <> subst_rec_closed thm
R6205:6220 LamSF_Closed <> subst_rec_closed thm
R6205:6220 LamSF_Closed <> subst_rec_closed thm
R6276:6278 LamSF_Terms <> App constr
R6297:6299 LamSF_Terms <> App constr
R6306:6309 SF_reduction <> i_op def
R6301:6304 SF_reduction <> k_op def
R6281:6283 LamSF_Terms <> App constr
R6290:6293 SF_reduction <> k_op def
R6285:6288 SF_reduction <> k_op def
R6255:6268 LamSF_Tactics <> transitive_red thm
R6276:6278 LamSF_Terms <> App constr
R6297:6299 LamSF_Terms <> App constr
R6306:6309 SF_reduction <> i_op def
R6301:6304 SF_reduction <> k_op def
R6281:6283 LamSF_Terms <> App constr
R6290:6293 SF_reduction <> k_op def
R6285:6288 SF_reduction <> k_op def
R6255:6268 LamSF_Tactics <> transitive_red thm
R6322:6344 LamSF_reduction <> preserves_app_lamSF_red thm
prf 6389:6401 <> is_comb_false
R6423:6426 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6427:6427 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6449:6453 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6454:6462 LamSF_reduction <> lamSF_red def
R6481:6483 LamSF_Terms <> App constr
R6490:6493 SF_reduction <> i_op def
R6485:6488 SF_reduction <> k_op def
R6465:6467 LamSF_Terms <> App constr
R6477:6477 Combinators <> M var
R6469:6475 Combinators <> is_comb def
R6440:6443 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6444:6448 Coq.Init.Logic <> False ind
R6428:6437 Combinators <> combinator ind
R6439:6439 Combinators <> M var
R6414:6420 LamSF_Closed <> program def
R6422:6422 Combinators <> M var
R6513:6519 LamSF_Closed <> program def
R6604:6608 Coq.Init.Logic <> False ind
R6604:6608 Coq.Init.Logic <> False ind
R6649:6655 Combinators <> is_comb def
R6672:6678 Combinators <> is_comb def
R6672:6678 Combinators <> is_comb def
R6688:6697 Combinators <> is_comb_fn def
R6720:6728 LamSF_Terms <> subst_rec def
R6736:6744 LamSF_Terms <> subst_rec def
R6736:6744 LamSF_Terms <> subst_rec def
R6771:6783 LamSF_Substitution_term <> lift_rec_null thm
R6771:6783 LamSF_Substitution_term <> lift_rec_null thm
R6771:6783 LamSF_Substitution_term <> lift_rec_null thm
R6809:6818 LamSF_Tactics <> multi_step ind
R6832:6834 LamSF_Terms <> App constr
R6820:6829 LamSF_reduction <> lamSF_red1 ind
R6809:6818 LamSF_Tactics <> multi_step ind
R6832:6834 LamSF_Terms <> App constr
R6820:6829 LamSF_reduction <> lamSF_red1 ind
R6869:6871 LamSF_Terms <> App constr
R6907:6921 SF_reduction <> right_component def
R6924:6926 LamSF_Terms <> Abs constr
R6874:6876 LamSF_Terms <> App constr
R6881:6894 SF_reduction <> left_component def
R6897:6899 LamSF_Terms <> Abs constr
R6854:6861 LamSF_Tactics <> succ_red constr
R6869:6871 LamSF_Terms <> App constr
R6907:6921 SF_reduction <> right_component def
R6924:6926 LamSF_Terms <> Abs constr
R6874:6876 LamSF_Terms <> App constr
R6881:6894 SF_reduction <> left_component def
R6897:6899 LamSF_Terms <> Abs constr
R6854:6861 LamSF_Tactics <> succ_red constr
R6947:6966 LamSF_reduction <> f_compound_lamSF_red constr
R6977:6986 LamSF_Closed <> factorable def
R6989:6991 LamSF_Terms <> Abs constr
R6977:6986 LamSF_Closed <> factorable def
R6989:6991 LamSF_Terms <> Abs constr
R7008:7030 LamSF_Closed <> programs_are_factorable thm
R7099:7114 LamSF_Closed <> subst_rec_closed thm
R7116:7120 Equal <> equal def
R7099:7114 LamSF_Closed <> subst_rec_closed thm
R7116:7120 Equal <> equal def
R7099:7114 LamSF_Closed <> subst_rec_closed thm
R7116:7120 Equal <> equal def
R7099:7114 LamSF_Closed <> subst_rec_closed thm
R7116:7120 Equal <> equal def
R7099:7114 LamSF_Closed <> subst_rec_closed thm
R7116:7120 Equal <> equal def
R7150:7167 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7150:7167 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7150:7167 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7150:7167 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7150:7167 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7203:7215 LamSF_Substitution_term <> lift_rec_null thm
R7203:7215 LamSF_Substitution_term <> lift_rec_null thm
R7203:7215 LamSF_Substitution_term <> lift_rec_null thm
R7225:7238 SF_reduction <> left_component def
R7241:7255 SF_reduction <> right_component def
R7293:7302 LamSF_Tactics <> multi_step ind
R7316:7318 LamSF_Terms <> App constr
R7321:7323 LamSF_Terms <> App constr
R7304:7313 LamSF_reduction <> lamSF_red1 ind
R7293:7302 LamSF_Tactics <> multi_step ind
R7316:7318 LamSF_Terms <> App constr
R7321:7323 LamSF_Terms <> App constr
R7304:7313 LamSF_reduction <> lamSF_red1 ind
R7367:7369 LamSF_Terms <> App constr
R7372:7374 LamSF_Terms <> App constr
R7376:7379 SF_reduction <> k_op def
R7346:7359 LamSF_Tactics <> transitive_red thm
R7367:7369 LamSF_Terms <> App constr
R7372:7374 LamSF_Terms <> App constr
R7376:7379 SF_reduction <> k_op def
R7346:7359 LamSF_Tactics <> transitive_red thm
R7401:7423 LamSF_reduction <> preserves_app_lamSF_red thm
R7435:7457 LamSF_reduction <> preserves_app_lamSF_red thm
R7469:7482 Equal <> equal_programs thm
R7550:7553 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R7532:7537 LamSF_Tactics <> status def
R7540:7542 LamSF_Terms <> App constr
R7554:7559 LamSF_Closed <> maxvar def
R7562:7564 LamSF_Terms <> App constr
R7550:7553 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R7532:7537 LamSF_Tactics <> status def
R7540:7542 LamSF_Terms <> App constr
R7554:7559 LamSF_Closed <> maxvar def
R7562:7564 LamSF_Terms <> App constr
R7585:7600 LamSF_Closed <> status_lt_maxvar thm
R7627:7633 Combinators <> is_comb def
R7650:7656 Combinators <> is_comb def
R7650:7656 Combinators <> is_comb def
R7666:7675 Combinators <> is_comb_fn def
R7698:7706 LamSF_Terms <> subst_rec def
R7714:7722 LamSF_Terms <> subst_rec def
R7714:7722 LamSF_Terms <> subst_rec def
R7749:7761 LamSF_Substitution_term <> lift_rec_null thm
R7749:7761 LamSF_Substitution_term <> lift_rec_null thm
R7749:7761 LamSF_Substitution_term <> lift_rec_null thm
R7772:7784 LamSF_Substitution_term <> lift_rec_null thm
R7772:7784 LamSF_Substitution_term <> lift_rec_null thm
R7772:7784 LamSF_Substitution_term <> lift_rec_null thm
R7804:7819 LamSF_Closed <> subst_rec_closed thm
R7821:7825 Equal <> equal def
R7804:7819 LamSF_Closed <> subst_rec_closed thm
R7821:7825 Equal <> equal def
R7804:7819 LamSF_Closed <> subst_rec_closed thm
R7821:7825 Equal <> equal def
R7804:7819 LamSF_Closed <> subst_rec_closed thm
R7821:7825 Equal <> equal def
R7804:7819 LamSF_Closed <> subst_rec_closed thm
R7821:7825 Equal <> equal def
R7855:7872 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7855:7872 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7855:7872 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7855:7872 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7855:7872 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7908:7922 LamSF_Closed <> lift_rec_closed thm
R7908:7922 LamSF_Closed <> lift_rec_closed thm
R7908:7922 LamSF_Closed <> lift_rec_closed thm
R7908:7922 LamSF_Closed <> lift_rec_closed thm
R7972:7981 LamSF_Tactics <> multi_step ind
R7995:7997 LamSF_Terms <> App constr
R7983:7992 LamSF_reduction <> lamSF_red1 ind
R7972:7981 LamSF_Tactics <> multi_step ind
R7995:7997 LamSF_Terms <> App constr
R7983:7992 LamSF_reduction <> lamSF_red1 ind
R8032:8034 LamSF_Terms <> App constr
R8074:8088 SF_reduction <> right_component def
R8091:8093 LamSF_Terms <> App constr
R8037:8039 LamSF_Terms <> App constr
R8044:8057 SF_reduction <> left_component def
R8060:8062 LamSF_Terms <> App constr
R8017:8024 LamSF_Tactics <> succ_red constr
R8032:8034 LamSF_Terms <> App constr
R8074:8088 SF_reduction <> right_component def
R8091:8093 LamSF_Terms <> App constr
R8037:8039 LamSF_Terms <> App constr
R8044:8057 SF_reduction <> left_component def
R8060:8062 LamSF_Terms <> App constr
R8017:8024 LamSF_Tactics <> succ_red constr
R8118:8137 LamSF_reduction <> f_compound_lamSF_red constr
R8170:8185 LamSF_Closed <> subst_rec_closed thm
R8187:8191 Equal <> equal def
R8170:8185 LamSF_Closed <> subst_rec_closed thm
R8187:8191 Equal <> equal def
R8170:8185 LamSF_Closed <> subst_rec_closed thm
R8187:8191 Equal <> equal def
R8170:8185 LamSF_Closed <> subst_rec_closed thm
R8187:8191 Equal <> equal def
R8170:8185 LamSF_Closed <> subst_rec_closed thm
R8187:8191 Equal <> equal def
R8220:8233 SF_reduction <> left_component def
R8236:8250 SF_reduction <> right_component def
R8262:8279 LamSF_Substitution_term <> subst_rec_lift_rec thm
R8262:8279 LamSF_Substitution_term <> subst_rec_lift_rec thm
R8262:8279 LamSF_Substitution_term <> subst_rec_lift_rec thm
R8262:8279 LamSF_Substitution_term <> subst_rec_lift_rec thm
R8262:8279 LamSF_Substitution_term <> subst_rec_lift_rec thm
R8315:8327 LamSF_Substitution_term <> lift_rec_null thm
R8315:8327 LamSF_Substitution_term <> lift_rec_null thm
R8315:8327 LamSF_Substitution_term <> lift_rec_null thm
R8352:8361 LamSF_Tactics <> multi_step ind
R8375:8377 LamSF_Terms <> App constr
R8380:8382 LamSF_Terms <> App constr
R8363:8372 LamSF_reduction <> lamSF_red1 ind
R8352:8361 LamSF_Tactics <> multi_step ind
R8375:8377 LamSF_Terms <> App constr
R8380:8382 LamSF_Terms <> App constr
R8363:8372 LamSF_reduction <> lamSF_red1 ind
R8426:8428 LamSF_Terms <> App constr
R8431:8433 LamSF_Terms <> App constr
R8436:8438 LamSF_Terms <> App constr
R8445:8448 SF_reduction <> i_op def
R8440:8443 SF_reduction <> k_op def
R8405:8418 LamSF_Tactics <> transitive_red thm
R8426:8428 LamSF_Terms <> App constr
R8431:8433 LamSF_Terms <> App constr
R8436:8438 LamSF_Terms <> App constr
R8445:8448 SF_reduction <> i_op def
R8440:8443 SF_reduction <> k_op def
R8405:8418 LamSF_Tactics <> transitive_red thm
R8471:8493 LamSF_reduction <> preserves_app_lamSF_red thm
R8505:8527 LamSF_reduction <> preserves_app_lamSF_red thm
R8539:8554 Equal <> unequal_programs thm
R8660:8675 LamSF_Closed <> subst_rec_closed thm
R8660:8675 LamSF_Closed <> subst_rec_closed thm
R8660:8675 LamSF_Closed <> subst_rec_closed thm
R8660:8675 LamSF_Closed <> subst_rec_closed thm
R8660:8675 LamSF_Closed <> subst_rec_closed thm
R8660:8675 LamSF_Closed <> subst_rec_closed thm
R8660:8675 LamSF_Closed <> subst_rec_closed thm
R8660:8675 LamSF_Closed <> subst_rec_closed thm
R8747:8751 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8774:8774 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8734:8743 Combinators <> combinator ind
R8765:8768 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8769:8773 Coq.Init.Logic <> False ind
R8752:8761 Combinators <> combinator ind
R8747:8751 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8774:8774 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8734:8743 Combinators <> combinator ind
R8765:8768 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8769:8773 Coq.Init.Logic <> False ind
R8752:8761 Combinators <> combinator ind
R8788:8807 Combinators <> combinator_decidable thm
R8846:8850 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8873:8873 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8833:8842 Combinators <> combinator ind
R8864:8867 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8868:8872 Coq.Init.Logic <> False ind
R8851:8860 Combinators <> combinator ind
R8846:8850 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8873:8873 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8833:8842 Combinators <> combinator ind
R8864:8867 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8868:8872 Coq.Init.Logic <> False ind
R8851:8860 Combinators <> combinator ind
R8887:8906 Combinators <> combinator_decidable thm
R8931:8935 Coq.Init.Logic <> False ind
R8931:8935 Coq.Init.Logic <> False ind
R8985:8987 LamSF_Terms <> App constr
R9017:9019 LamSF_Terms <> App constr
R9026:9029 SF_reduction <> i_op def
R9021:9024 SF_reduction <> k_op def
R8990:8992 LamSF_Terms <> App constr
R9000:9002 LamSF_Terms <> App constr
R9009:9012 SF_reduction <> i_op def
R9004:9007 SF_reduction <> k_op def
R8994:8997 SF_reduction <> k_op def
R8964:8977 LamSF_Tactics <> transitive_red thm
R8985:8987 LamSF_Terms <> App constr
R9017:9019 LamSF_Terms <> App constr
R9026:9029 SF_reduction <> i_op def
R9021:9024 SF_reduction <> k_op def
R8990:8992 LamSF_Terms <> App constr
R9000:9002 LamSF_Terms <> App constr
R9009:9012 SF_reduction <> i_op def
R9004:9007 SF_reduction <> k_op def
R8994:8997 SF_reduction <> k_op def
R8964:8977 LamSF_Tactics <> transitive_red thm
R9043:9065 LamSF_reduction <> preserves_app_lamSF_red thm
R9077:9099 LamSF_reduction <> preserves_app_lamSF_red thm
R9111:9122 Combinators <> is_comb_true thm
R9192:9194 LamSF_Terms <> App constr
R9236:9238 LamSF_Terms <> App constr
R9245:9248 SF_reduction <> i_op def
R9240:9243 SF_reduction <> k_op def
R9197:9199 LamSF_Terms <> App constr
R9218:9220 LamSF_Terms <> App constr
R9222:9228 Combinators <> is_comb def
R9202:9204 LamSF_Terms <> App constr
R9211:9214 SF_reduction <> i_op def
R9206:9209 SF_reduction <> k_op def
R9171:9184 LamSF_Tactics <> transitive_red thm
R9192:9194 LamSF_Terms <> App constr
R9236:9238 LamSF_Terms <> App constr
R9245:9248 SF_reduction <> i_op def
R9240:9243 SF_reduction <> k_op def
R9197:9199 LamSF_Terms <> App constr
R9218:9220 LamSF_Terms <> App constr
R9222:9228 Combinators <> is_comb def
R9202:9204 LamSF_Terms <> App constr
R9211:9214 SF_reduction <> i_op def
R9206:9209 SF_reduction <> k_op def
R9171:9184 LamSF_Tactics <> transitive_red thm
R9262:9284 LamSF_reduction <> preserves_app_lamSF_red thm