forked from Barry-Jay/lambdaSF
-
Notifications
You must be signed in to change notification settings - Fork 0
/
LamSF_Closed.glob
959 lines (959 loc) · 39 KB
/
LamSF_Closed.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
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
DIGEST 8102099d888fc3bc83207a64d4dcc477
FLamSF_Closed
R1991:1995 Coq.Arith.Arith <> <> lib
R2013:2016 Test <> <> lib
R2034:2040 General <> <> lib
R2059:2061 Coq.Arith.Max <> <> lib
R2080:2090 LamSF_Terms <> <> lib
R2108:2120 LamSF_Tactics <> <> lib
R2138:2160 LamSF_Substitution_term <> <> lib
R2178:2189 SF_reduction <> <> lib
R2207:2221 LamSF_reduction <> <> lib
R2239:2250 LamSF_Normal <> <> lib
R2268:2272 Coq.omega.Omega <> <> lib
def 2307:2312 <> maxvar
R2318:2322 LamSF_Terms <> lamSF ind
R2335:2335 LamSF_Closed <> M var
R2345:2347 LamSF_Terms <> Ref constr
R2354:2354 Coq.Init.Datatypes <> S constr
R2360:2361 LamSF_Terms <> Op constr
R2373:2375 LamSF_Terms <> App constr
R2386:2388 Coq.Arith.Max <> max syndef
R2403:2408 LamSF_Closed <> maxvar def
R2391:2396 LamSF_Closed <> maxvar def
R2416:2418 LamSF_Terms <> Abs constr
R2425:2428 Coq.Init.Peano <> pred syndef
R2431:2436 LamSF_Closed <> maxvar def
def 2459:2464 <> closed
R2479:2481 Coq.Init.Logic <> :type_scope:x_'='_x not
R2471:2476 LamSF_Closed <> maxvar def
R2478:2478 LamSF_Closed <> M var
prf 2493:2507 <> maxvar_lift_rec
R2537:2540 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R2533:2535 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2525:2530 LamSF_Closed <> maxvar def
R2532:2532 LamSF_Closed <> M var
R2536:2536 LamSF_Closed <> k var
R2541:2546 LamSF_Closed <> maxvar def
R2549:2556 LamSF_Terms <> lift_rec def
R2562:2562 LamSF_Closed <> k var
R2560:2560 LamSF_Closed <> n var
R2558:2558 LamSF_Closed <> M var
R2607:2614 LamSF_Terms <> relocate def
R2622:2625 Test <> test def
R2622:2625 Test <> test def
R2687:2690 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R2683:2685 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2668:2671 Coq.Init.Peano <> pred syndef
R2674:2679 LamSF_Closed <> maxvar def
R2691:2694 Coq.Init.Peano <> pred syndef
R2705:2707 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2697:2702 LamSF_Closed <> maxvar def
R2687:2690 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R2683:2685 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2668:2671 Coq.Init.Peano <> pred syndef
R2674:2679 LamSF_Closed <> maxvar def
R2691:2694 Coq.Init.Peano <> pred syndef
R2705:2707 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2697:2702 LamSF_Closed <> maxvar def
R2741:2744 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R2737:2739 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2729:2734 LamSF_Closed <> maxvar def
R2745:2750 LamSF_Closed <> maxvar def
R2753:2760 LamSF_Terms <> lift_rec def
R2765:2765 Coq.Init.Datatypes <> S constr
R2741:2744 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R2737:2739 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2729:2734 LamSF_Closed <> maxvar def
R2745:2750 LamSF_Closed <> maxvar def
R2753:2760 LamSF_Terms <> lift_rec def
R2765:2765 Coq.Init.Datatypes <> S constr
R2806:2813 General <> max_plus thm
R2806:2813 General <> max_plus thm
R2806:2813 General <> max_plus thm
R2825:2837 General <> max_monotonic thm
prf 2854:2875 <> subst_decreases_maxvar
R2931:2934 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R2895:2897 Coq.Arith.Max <> max syndef
R2926:2928 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2918:2923 LamSF_Closed <> maxvar def
R2925:2925 LamSF_Closed <> N var
R2929:2929 LamSF_Closed <> k var
R2900:2903 Coq.Init.Peano <> pred syndef
R2906:2911 LamSF_Closed <> maxvar def
R2913:2913 LamSF_Closed <> M var
R2935:2940 LamSF_Closed <> maxvar def
R2942:2950 LamSF_Terms <> subst_rec def
R2956:2956 LamSF_Closed <> k var
R2954:2954 LamSF_Closed <> N var
R2952:2952 LamSF_Closed <> M var
R3000:3009 LamSF_Terms <> insert_Ref def
R3018:3024 Test <> compare def
R3018:3024 Test <> compare def
R3091:3094 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R3071:3073 Coq.Arith.Max <> max syndef
R3086:3088 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3078:3083 LamSF_Closed <> maxvar def
R3091:3094 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R3071:3073 Coq.Arith.Max <> max syndef
R3086:3088 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3078:3083 LamSF_Closed <> maxvar def
R3109:3118 General <> max_is_max thm
R3137:3140 LamSF_Terms <> lift def
R3149:3163 LamSF_Closed <> maxvar_lift_rec thm
R3149:3163 LamSF_Closed <> maxvar_lift_rec thm
R3193:3202 General <> max_is_max thm
R3224:3227 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R3213:3215 Coq.Arith.Max <> max syndef
R3220:3220 Coq.Init.Datatypes <> S constr
R3228:3230 Coq.Arith.Max <> max syndef
R3224:3227 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R3213:3215 Coq.Arith.Max <> max syndef
R3220:3220 Coq.Init.Datatypes <> S constr
R3228:3230 Coq.Arith.Max <> max syndef
R3249:3261 General <> max_monotonic thm
R3308:3311 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R3288:3290 Coq.Arith.Max <> max syndef
R3303:3305 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3295:3300 LamSF_Closed <> maxvar def
R3320:3322 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3312:3317 LamSF_Closed <> maxvar def
R3308:3311 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R3288:3290 Coq.Arith.Max <> max syndef
R3303:3305 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3295:3300 LamSF_Closed <> maxvar def
R3320:3322 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3312:3317 LamSF_Closed <> maxvar def
R3337:3346 General <> max_is_max thm
R3435:3438 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R3392:3394 Coq.Arith.Max <> max syndef
R3430:3432 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3422:3427 LamSF_Closed <> maxvar def
R3397:3400 Coq.Init.Peano <> pred syndef
R3403:3406 Coq.Init.Peano <> pred syndef
R3409:3414 LamSF_Closed <> maxvar def
R3439:3442 Coq.Init.Peano <> pred syndef
R3444:3446 Coq.Arith.Max <> max syndef
R3475:3478 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3482:3482 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3467:3472 LamSF_Closed <> maxvar def
R3479:3479 Coq.Init.Datatypes <> S constr
R3449:3452 Coq.Init.Peano <> pred syndef
R3455:3460 LamSF_Closed <> maxvar def
R3435:3438 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R3392:3394 Coq.Arith.Max <> max syndef
R3430:3432 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3422:3427 LamSF_Closed <> maxvar def
R3397:3400 Coq.Init.Peano <> pred syndef
R3403:3406 Coq.Init.Peano <> pred syndef
R3409:3414 LamSF_Closed <> maxvar def
R3439:3442 Coq.Init.Peano <> pred syndef
R3444:3446 Coq.Arith.Max <> max syndef
R3475:3478 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3482:3482 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3467:3472 LamSF_Closed <> maxvar def
R3479:3479 Coq.Init.Datatypes <> S constr
R3449:3452 Coq.Init.Peano <> pred syndef
R3455:3460 LamSF_Closed <> maxvar def
R3496:3503 General <> max_pred thm
R3496:3503 General <> max_pred thm
R3496:3503 General <> max_pred thm
R3515:3527 General <> max_monotonic thm
R3585:3588 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R3547:3549 Coq.Arith.Max <> max syndef
R3578:3580 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3570:3575 LamSF_Closed <> maxvar def
R3581:3581 Coq.Init.Datatypes <> S constr
R3552:3555 Coq.Init.Peano <> pred syndef
R3558:3563 LamSF_Closed <> maxvar def
R3589:3594 LamSF_Closed <> maxvar def
R3597:3605 LamSF_Terms <> subst_rec def
R3612:3612 Coq.Init.Datatypes <> S constr
R3585:3588 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R3547:3549 Coq.Arith.Max <> max syndef
R3578:3580 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3570:3575 LamSF_Closed <> maxvar def
R3581:3581 Coq.Init.Datatypes <> S constr
R3552:3555 Coq.Init.Peano <> pred syndef
R3558:3563 LamSF_Closed <> maxvar def
R3589:3594 LamSF_Closed <> maxvar def
R3597:3605 LamSF_Terms <> subst_rec def
R3612:3612 Coq.Init.Datatypes <> S constr
R3688:3691 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R3643:3646 Coq.Init.Peano <> pred syndef
R3649:3651 Coq.Arith.Max <> max syndef
R3680:3682 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3672:3677 LamSF_Closed <> maxvar def
R3683:3683 Coq.Init.Datatypes <> S constr
R3654:3657 Coq.Init.Peano <> pred syndef
R3660:3665 LamSF_Closed <> maxvar def
R3692:3695 Coq.Init.Peano <> pred syndef
R3698:3703 LamSF_Closed <> maxvar def
R3706:3714 LamSF_Terms <> subst_rec def
R3721:3721 Coq.Init.Datatypes <> S constr
R3688:3691 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R3643:3646 Coq.Init.Peano <> pred syndef
R3649:3651 Coq.Arith.Max <> max syndef
R3680:3682 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3672:3677 LamSF_Closed <> maxvar def
R3683:3683 Coq.Init.Datatypes <> S constr
R3654:3657 Coq.Init.Peano <> pred syndef
R3660:3665 LamSF_Closed <> maxvar def
R3692:3695 Coq.Init.Peano <> pred syndef
R3698:3703 LamSF_Closed <> maxvar def
R3706:3714 LamSF_Terms <> subst_rec def
R3721:3721 Coq.Init.Datatypes <> S constr
R3765:3772 General <> max_pred thm
R3765:3772 General <> max_pred thm
R3765:3772 General <> max_pred thm
R3866:3869 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R3783:3785 Coq.Arith.Max <> max syndef
R3828:3830 Coq.Arith.Max <> max syndef
R3860:3862 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3852:3857 LamSF_Closed <> maxvar def
R3833:3836 Coq.Init.Peano <> pred syndef
R3839:3844 LamSF_Closed <> maxvar def
R3787:3789 Coq.Arith.Max <> max syndef
R3819:3821 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3811:3816 LamSF_Closed <> maxvar def
R3792:3795 Coq.Init.Peano <> pred syndef
R3798:3803 LamSF_Closed <> maxvar def
R3870:3872 Coq.Arith.Max <> max syndef
R3903:3908 LamSF_Closed <> maxvar def
R3911:3919 LamSF_Terms <> subst_rec def
R3875:3880 LamSF_Closed <> maxvar def
R3883:3891 LamSF_Terms <> subst_rec def
R3866:3869 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R3783:3785 Coq.Arith.Max <> max syndef
R3828:3830 Coq.Arith.Max <> max syndef
R3860:3862 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3852:3857 LamSF_Closed <> maxvar def
R3833:3836 Coq.Init.Peano <> pred syndef
R3839:3844 LamSF_Closed <> maxvar def
R3787:3789 Coq.Arith.Max <> max syndef
R3819:3821 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3811:3816 LamSF_Closed <> maxvar def
R3792:3795 Coq.Init.Peano <> pred syndef
R3798:3803 LamSF_Closed <> maxvar def
R3870:3872 Coq.Arith.Max <> max syndef
R3903:3908 LamSF_Closed <> maxvar def
R3911:3919 LamSF_Terms <> subst_rec def
R3875:3880 LamSF_Closed <> maxvar def
R3883:3891 LamSF_Terms <> subst_rec def
R3940:3952 General <> max_monotonic thm
R4025:4030 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R3963:3965 Coq.Arith.Max <> max syndef
R4020:4022 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4012:4017 LamSF_Closed <> maxvar def
R3968:3970 Coq.Arith.Max <> max syndef
R3992:3995 Coq.Init.Peano <> pred syndef
R3998:4003 LamSF_Closed <> maxvar def
R3973:3976 Coq.Init.Peano <> pred syndef
R3979:3984 LamSF_Closed <> maxvar def
R4031:4033 Coq.Arith.Max <> max syndef
R4076:4078 Coq.Arith.Max <> max syndef
R4108:4110 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4100:4105 LamSF_Closed <> maxvar def
R4081:4084 Coq.Init.Peano <> pred syndef
R4087:4092 LamSF_Closed <> maxvar def
R4035:4037 Coq.Arith.Max <> max syndef
R4067:4069 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4059:4064 LamSF_Closed <> maxvar def
R4040:4043 Coq.Init.Peano <> pred syndef
R4046:4051 LamSF_Closed <> maxvar def
R4025:4030 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R3963:3965 Coq.Arith.Max <> max syndef
R4020:4022 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4012:4017 LamSF_Closed <> maxvar def
R3968:3970 Coq.Arith.Max <> max syndef
R3992:3995 Coq.Init.Peano <> pred syndef
R3998:4003 LamSF_Closed <> maxvar def
R3973:3976 Coq.Init.Peano <> pred syndef
R3979:3984 LamSF_Closed <> maxvar def
R4031:4033 Coq.Arith.Max <> max syndef
R4076:4078 Coq.Arith.Max <> max syndef
R4108:4110 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4100:4105 LamSF_Closed <> maxvar def
R4081:4084 Coq.Init.Peano <> pred syndef
R4087:4092 LamSF_Closed <> maxvar def
R4035:4037 Coq.Arith.Max <> max syndef
R4067:4069 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4059:4064 LamSF_Closed <> maxvar def
R4040:4043 Coq.Init.Peano <> pred syndef
R4046:4051 LamSF_Closed <> maxvar def
R4137:4144 General <> max_max2 thm
R4155:4167 General <> max_monotonic thm
R4155:4167 General <> max_monotonic thm
R4178:4187 General <> max_is_max thm
R4178:4187 General <> max_is_max thm
def 4210:4218 <> decreases
R4233:4236 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4237:4239 Coq.Init.Datatypes <> nat ind
R4228:4232 LamSF_Terms <> lamSF ind
R4247:4253 LamSF_Tactics <> termred def
R4278:4281 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4288:4291 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R4282:4285 LamSF_Closed <> rank var
R4287:4287 LamSF_Closed <> M var
R4292:4295 LamSF_Closed <> rank var
R4297:4297 LamSF_Closed <> N var
R4271:4273 LamSF_Closed <> red var
R4277:4277 LamSF_Closed <> N var
R4275:4275 LamSF_Closed <> M var
prf 4307:4326 <> decreases_multi_step
R4365:4368 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4369:4377 LamSF_Closed <> decreases def
R4385:4394 LamSF_Tactics <> multi_step ind
R4396:4398 LamSF_Closed <> red var
R4379:4382 LamSF_Closed <> rank var
R4347:4355 LamSF_Closed <> decreases def
R4362:4364 LamSF_Closed <> red var
R4357:4360 LamSF_Closed <> rank var
R4480:4483 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R4480:4483 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R4520:4523 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R4520:4523 Coq.Init.Peano <> :nat_scope:x_'>='_x not
prf 4571:4585 <> lift_rec_closed
R4612:4616 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4641:4643 Coq.Init.Logic <> :type_scope:x_'='_x not
R4627:4634 LamSF_Terms <> lift_rec def
R4640:4640 LamSF_Closed <> k var
R4638:4638 LamSF_Closed <> n var
R4636:4636 LamSF_Closed <> M var
R4644:4644 LamSF_Closed <> M var
R4601:4603 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R4600:4600 LamSF_Closed <> n var
R4604:4609 LamSF_Closed <> maxvar def
R4611:4611 LamSF_Closed <> M var
R4692:4695 LamSF_Terms <> lift def
R4705:4712 LamSF_Terms <> lift_rec def
R4720:4727 LamSF_Terms <> lift_rec def
R4720:4727 LamSF_Terms <> lift_rec def
R4720:4727 LamSF_Terms <> lift_rec def
R4720:4727 LamSF_Terms <> lift_rec def
R4738:4745 LamSF_Terms <> relocate def
R4753:4756 Test <> test def
R4753:4756 Test <> test def
R4850:4853 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R4823:4825 Coq.Arith.Max <> max syndef
R4840:4845 LamSF_Closed <> maxvar def
R4828:4833 LamSF_Closed <> maxvar def
R4854:4859 LamSF_Closed <> maxvar def
R4850:4853 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R4823:4825 Coq.Arith.Max <> max syndef
R4840:4845 LamSF_Closed <> maxvar def
R4828:4833 LamSF_Closed <> maxvar def
R4854:4859 LamSF_Closed <> maxvar def
R4876:4885 General <> max_is_max thm
R4923:4926 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R4896:4898 Coq.Arith.Max <> max syndef
R4913:4918 LamSF_Closed <> maxvar def
R4901:4906 LamSF_Closed <> maxvar def
R4927:4932 LamSF_Closed <> maxvar def
R4923:4926 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R4896:4898 Coq.Arith.Max <> max syndef
R4913:4918 LamSF_Closed <> maxvar def
R4901:4906 LamSF_Closed <> maxvar def
R4927:4932 LamSF_Closed <> maxvar def
R4949:4958 General <> max_is_max thm
prf 5037:5047 <> lift_closed
R5071:5074 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5093:5095 Coq.Init.Logic <> :type_scope:x_'='_x not
R5085:5088 LamSF_Terms <> lift def
R5092:5092 LamSF_Closed <> M var
R5090:5090 LamSF_Closed <> k var
R5096:5096 LamSF_Closed <> M var
R5068:5069 Coq.Init.Logic <> :type_scope:x_'='_x not
R5060:5065 LamSF_Closed <> maxvar def
R5067:5067 LamSF_Closed <> M var
R5126:5140 LamSF_Closed <> lift_rec_closed thm
prf 5164:5179 <> subst_rec_closed
R5207:5210 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5236:5238 Coq.Init.Logic <> :type_scope:x_'='_x not
R5221:5229 LamSF_Terms <> subst_rec def
R5235:5235 LamSF_Closed <> n var
R5233:5233 LamSF_Closed <> N var
R5231:5231 LamSF_Closed <> M var
R5239:5239 LamSF_Closed <> M var
R5196:5198 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R5195:5195 LamSF_Closed <> n var
R5199:5204 LamSF_Closed <> maxvar def
R5206:5206 LamSF_Closed <> M var
R5287:5296 LamSF_Terms <> insert_Ref def
R5305:5311 Test <> compare def
R5305:5311 Test <> compare def
R5444:5447 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R5417:5419 Coq.Arith.Max <> max syndef
R5434:5439 LamSF_Closed <> maxvar def
R5422:5427 LamSF_Closed <> maxvar def
R5448:5453 LamSF_Closed <> maxvar def
R5444:5447 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R5417:5419 Coq.Arith.Max <> max syndef
R5434:5439 LamSF_Closed <> maxvar def
R5422:5427 LamSF_Closed <> maxvar def
R5448:5453 LamSF_Closed <> maxvar def
R5470:5479 General <> max_is_max thm
R5517:5520 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R5490:5492 Coq.Arith.Max <> max syndef
R5507:5512 LamSF_Closed <> maxvar def
R5495:5500 LamSF_Closed <> maxvar def
R5521:5526 LamSF_Closed <> maxvar def
R5517:5520 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R5490:5492 Coq.Arith.Max <> max syndef
R5507:5512 LamSF_Closed <> maxvar def
R5495:5500 LamSF_Closed <> maxvar def
R5521:5526 LamSF_Closed <> maxvar def
R5543:5552 General <> max_is_max thm
prf 5631:5646 <> maxvar_subst_rec
R5674:5677 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5703:5705 Coq.Init.Logic <> :type_scope:x_'='_x not
R5688:5696 LamSF_Terms <> subst_rec def
R5702:5702 LamSF_Closed <> k var
R5700:5700 LamSF_Closed <> N var
R5698:5698 LamSF_Closed <> M var
R5706:5706 LamSF_Closed <> M var
R5669:5672 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R5661:5666 LamSF_Closed <> maxvar def
R5668:5668 LamSF_Closed <> M var
R5673:5673 LamSF_Closed <> k var
R5738:5746 LamSF_Terms <> subst_rec def
R5754:5762 LamSF_Terms <> subst_rec def
R5754:5762 LamSF_Terms <> subst_rec def
R5754:5762 LamSF_Terms <> subst_rec def
R5754:5762 LamSF_Terms <> subst_rec def
R5754:5762 LamSF_Terms <> subst_rec def
R5791:5800 LamSF_Terms <> insert_Ref def
R5808:5814 Test <> compare def
R5808:5814 Test <> compare def
R5929:5932 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R5917:5919 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R5920:5925 LamSF_Closed <> maxvar def
R5934:5936 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R5937:5942 LamSF_Closed <> maxvar def
R5929:5932 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R5917:5919 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R5920:5925 LamSF_Closed <> maxvar def
R5934:5936 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R5937:5942 LamSF_Closed <> maxvar def
R5959:5965 General <> max_max thm
prf 6045:6055 <> maxvar_star
R6083:6085 Coq.Init.Logic <> :type_scope:x_'='_x not
R6068:6073 LamSF_Closed <> maxvar def
R6076:6079 SF_reduction <> star def
R6081:6081 LamSF_Closed <> M var
R6086:6089 Coq.Init.Peano <> pred syndef
R6092:6097 LamSF_Closed <> maxvar def
R6099:6099 LamSF_Closed <> M var
R6165:6172 General <> max_pred thm
R6165:6172 General <> max_pred thm
R6165:6172 General <> max_pred thm
prf 6194:6224 <> left_component_preserves_maxvar
R6248:6252 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6277:6280 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R6253:6258 LamSF_Closed <> maxvar def
R6260:6273 SF_reduction <> left_component def
R6275:6275 LamSF_Closed <> M var
R6281:6286 LamSF_Closed <> maxvar def
R6288:6288 LamSF_Closed <> M var
R6238:6245 SF_reduction <> compound ind
R6247:6247 LamSF_Closed <> M var
R6355:6364 General <> max_is_max thm
prf 6381:6412 <> right_component_preserves_maxvar
R6436:6440 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6466:6469 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R6441:6446 LamSF_Closed <> maxvar def
R6448:6462 SF_reduction <> right_component def
R6464:6464 LamSF_Closed <> M var
R6470:6475 LamSF_Closed <> maxvar def
R6477:6477 LamSF_Closed <> M var
R6426:6433 SF_reduction <> compound ind
R6435:6435 LamSF_Closed <> M var
R6544:6553 General <> max_is_max thm
R6565:6575 LamSF_Closed <> maxvar_star thm
R6565:6575 LamSF_Closed <> maxvar_star thm
R6565:6575 LamSF_Closed <> maxvar_star thm
R6594:6604 LamSF_Closed <> maxvar_star thm
R6594:6604 LamSF_Closed <> maxvar_star thm
R6594:6604 LamSF_Closed <> maxvar_star thm
R6668:6671 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R6659:6661 Coq.Arith.Max <> max syndef
R6668:6671 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R6659:6661 Coq.Arith.Max <> max syndef
R6693:6696 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R6686:6688 Coq.Arith.Max <> max syndef
R6729:6732 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R6810:6813 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R6801:6803 Coq.Arith.Max <> max syndef
R6810:6813 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R6801:6803 Coq.Arith.Max <> max syndef
R6835:6838 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R6828:6830 Coq.Arith.Max <> max syndef
R6871:6874 Coq.Init.Peano <> :nat_scope:x_'>='_x not
prf 6915:6940 <> decreases_maxvar_lamF_red1
R6943:6951 LamSF_Closed <> decreases def
R6960:6969 LamSF_reduction <> lamSF_red1 ind
R6953:6958 LamSF_Closed <> maxvar def
R7070:7073 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7082:7085 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R7074:7079 LamSF_Closed <> maxvar def
R7081:7081 LamSF_Closed <> N var
R7086:7091 LamSF_Closed <> maxvar def
R7093:7093 LamSF_Closed <> M var
R7056:7065 LamSF_reduction <> lamSF_red1 ind
R7069:7069 LamSF_Closed <> N var
R7067:7067 LamSF_Closed <> M var
R7070:7073 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7082:7085 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R7074:7079 LamSF_Closed <> maxvar def
R7081:7081 LamSF_Closed <> N var
R7086:7091 LamSF_Closed <> maxvar def
R7093:7093 LamSF_Closed <> M var
R7056:7065 LamSF_reduction <> lamSF_red1 ind
R7069:7069 LamSF_Closed <> N var
R7067:7067 LamSF_Closed <> M var
R7182:7194 General <> max_monotonic thm
R7182:7194 General <> max_monotonic thm
R7182:7194 General <> max_monotonic thm
R7182:7194 General <> max_monotonic thm
R7182:7194 General <> max_monotonic thm
R7182:7194 General <> max_monotonic thm
R7182:7194 General <> max_monotonic thm
R7182:7194 General <> max_monotonic thm
R7182:7194 General <> max_monotonic thm
R7182:7194 General <> max_monotonic thm
R7182:7194 General <> max_monotonic thm
R7182:7194 General <> max_monotonic thm
R7182:7194 General <> max_monotonic thm
R7182:7194 General <> max_monotonic thm
R7232:7239 General <> max_max2 thm
R7232:7239 General <> max_max2 thm
R7232:7239 General <> max_max2 thm
R7232:7239 General <> max_max2 thm
R7232:7239 General <> max_max2 thm
R7232:7239 General <> max_max2 thm
R7232:7239 General <> max_max2 thm
R7232:7239 General <> max_max2 thm
R7232:7239 General <> max_max2 thm
R7232:7239 General <> max_max2 thm
R7232:7239 General <> max_max2 thm
R7232:7239 General <> max_max2 thm
R7232:7239 General <> max_max2 thm
R7232:7239 General <> max_max2 thm
R7305:7309 LamSF_Terms <> subst def
R7356:7359 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R7320:7322 Coq.Arith.Max <> max syndef
R7351:7353 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7343:7348 LamSF_Closed <> maxvar def
R7325:7328 Coq.Init.Peano <> pred syndef
R7331:7336 LamSF_Closed <> maxvar def
R7360:7365 LamSF_Closed <> maxvar def
R7367:7375 LamSF_Terms <> subst_rec def
R7356:7359 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R7320:7322 Coq.Arith.Max <> max syndef
R7351:7353 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7343:7348 LamSF_Closed <> maxvar def
R7325:7328 Coq.Init.Peano <> pred syndef
R7331:7336 LamSF_Closed <> maxvar def
R7360:7365 LamSF_Closed <> maxvar def
R7367:7375 LamSF_Terms <> subst_rec def
R7394:7415 LamSF_Closed <> subst_decreases_maxvar thm
R7436:7438 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7428:7433 LamSF_Closed <> maxvar def
R7448:7453 LamSF_Closed <> maxvar def
R7436:7438 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7428:7433 LamSF_Closed <> maxvar def
R7448:7453 LamSF_Closed <> maxvar def
R7546:7549 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R7522:7524 Coq.Arith.Max <> max syndef
R7537:7542 LamSF_Closed <> maxvar def
R7526:7531 LamSF_Closed <> maxvar def
R7550:7555 LamSF_Closed <> maxvar def
R7546:7549 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R7522:7524 Coq.Arith.Max <> max syndef
R7537:7542 LamSF_Closed <> maxvar def
R7526:7531 LamSF_Closed <> maxvar def
R7550:7555 LamSF_Closed <> maxvar def
R7609:7639 LamSF_Closed <> left_component_preserves_maxvar thm
R7664:7695 LamSF_Closed <> right_component_preserves_maxvar thm
prf 7711:7735 <> decreases_maxvar_lamF_red
R7739:7747 LamSF_Closed <> decreases def
R7756:7764 LamSF_reduction <> lamSF_red def
R7749:7754 LamSF_Closed <> maxvar def
R7782:7801 LamSF_Closed <> decreases_multi_step thm
R7812:7837 LamSF_Closed <> decreases_maxvar_lamF_red1 thm
prf 7854:7869 <> status_lt_maxvar
R7890:7893 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R7882:7887 LamSF_Tactics <> status def
R7889:7889 LamSF_Closed <> M var
R7894:7899 LamSF_Closed <> maxvar def
R7901:7901 LamSF_Closed <> M var
R7940:7943 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7952:7955 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R7944:7949 LamSF_Tactics <> status def
R7951:7951 LamSF_Closed <> M var
R7956:7961 LamSF_Closed <> maxvar def
R7963:7963 LamSF_Closed <> M var
R7931:7933 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R7930:7930 LamSF_Closed <> p var
R7934:7937 LamSF_Tactics <> rank def
R7939:7939 LamSF_Closed <> M var
R7940:7943 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7952:7955 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R7944:7949 LamSF_Tactics <> status def
R7951:7951 LamSF_Closed <> M var
R7956:7961 LamSF_Closed <> maxvar def
R7963:7963 LamSF_Closed <> M var
R7931:7933 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R7930:7930 LamSF_Closed <> p var
R7934:7937 LamSF_Tactics <> rank def
R7939:7939 LamSF_Closed <> M var
R8027:8028 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R8021:8024 LamSF_Tactics <> rank def
R8027:8028 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R8021:8024 LamSF_Tactics <> rank def
R8043:8055 LamSF_Tactics <> rank_positive thm
R8184:8187 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R8176:8181 LamSF_Tactics <> status def
R8188:8193 LamSF_Closed <> maxvar def
R8184:8187 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R8176:8181 LamSF_Tactics <> status def
R8188:8193 LamSF_Closed <> maxvar def
R8330:8335 LamSF_Closed <> maxvar def
R8330:8335 LamSF_Closed <> maxvar def
R8369:8372 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R8361:8363 Coq.Arith.Max <> max syndef
R8369:8372 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R8361:8363 Coq.Arith.Max <> max syndef
R8495:8500 LamSF_Closed <> maxvar def
R8495:8500 LamSF_Closed <> maxvar def
R8525:8530 LamSF_Closed <> maxvar def
R8525:8530 LamSF_Closed <> maxvar def
R8564:8567 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R8556:8558 Coq.Arith.Max <> max syndef
R8564:8567 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R8556:8558 Coq.Arith.Max <> max syndef
R8595:8600 LamSF_Closed <> maxvar def
R8595:8600 LamSF_Closed <> maxvar def
R8634:8637 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R8626:8628 Coq.Arith.Max <> max syndef
R8634:8637 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R8626:8628 Coq.Arith.Max <> max syndef
R8674:8677 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R8666:8668 Coq.Arith.Max <> max syndef
R8674:8677 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R8666:8668 Coq.Arith.Max <> max syndef
R8707:8710 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R8699:8701 Coq.Arith.Max <> max syndef
R8707:8710 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R8699:8701 Coq.Arith.Max <> max syndef
R8749:8752 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R8732:8734 Coq.Arith.Max <> max syndef
R8737:8739 Coq.Arith.Max <> max syndef
R8753:8755 Coq.Arith.Max <> max syndef
R8749:8752 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R8732:8734 Coq.Arith.Max <> max syndef
R8737:8739 Coq.Arith.Max <> max syndef
R8753:8755 Coq.Arith.Max <> max syndef
R8774:8786 General <> max_monotonic thm
R8899:8904 LamSF_Closed <> maxvar def
R8899:8904 LamSF_Closed <> maxvar def
R8929:8934 LamSF_Closed <> maxvar def
R8929:8934 LamSF_Closed <> maxvar def
R8959:8964 LamSF_Closed <> maxvar def
R8959:8964 LamSF_Closed <> maxvar def
R8998:9001 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R8990:8992 Coq.Arith.Max <> max syndef
R8998:9001 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R8990:8992 Coq.Arith.Max <> max syndef
R9029:9034 LamSF_Closed <> maxvar def
R9029:9034 LamSF_Closed <> maxvar def
R9068:9071 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9060:9062 Coq.Arith.Max <> max syndef
R9068:9071 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9060:9062 Coq.Arith.Max <> max syndef
R9108:9111 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9100:9102 Coq.Arith.Max <> max syndef
R9108:9111 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9100:9102 Coq.Arith.Max <> max syndef
R9141:9144 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9133:9135 Coq.Arith.Max <> max syndef
R9141:9144 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9133:9135 Coq.Arith.Max <> max syndef
R9183:9186 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9166:9168 Coq.Arith.Max <> max syndef
R9171:9173 Coq.Arith.Max <> max syndef
R9187:9189 Coq.Arith.Max <> max syndef
R9183:9186 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9166:9168 Coq.Arith.Max <> max syndef
R9171:9173 Coq.Arith.Max <> max syndef
R9187:9189 Coq.Arith.Max <> max syndef
R9208:9220 General <> max_monotonic thm
R9237:9242 LamSF_Closed <> maxvar def
R9237:9242 LamSF_Closed <> maxvar def
R9267:9272 LamSF_Closed <> maxvar def
R9267:9272 LamSF_Closed <> maxvar def
R9306:9309 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9298:9300 Coq.Arith.Max <> max syndef
R9306:9309 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9298:9300 Coq.Arith.Max <> max syndef
R9346:9349 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9338:9340 Coq.Arith.Max <> max syndef
R9346:9349 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9338:9340 Coq.Arith.Max <> max syndef
R9379:9382 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9371:9373 Coq.Arith.Max <> max syndef
R9379:9382 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9371:9373 Coq.Arith.Max <> max syndef
R9421:9424 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9404:9406 Coq.Arith.Max <> max syndef
R9409:9411 Coq.Arith.Max <> max syndef
R9425:9427 Coq.Arith.Max <> max syndef
R9421:9424 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9404:9406 Coq.Arith.Max <> max syndef
R9409:9411 Coq.Arith.Max <> max syndef
R9425:9427 Coq.Arith.Max <> max syndef
R9446:9458 General <> max_monotonic thm
R9475:9480 LamSF_Closed <> maxvar def
R9475:9480 LamSF_Closed <> maxvar def
R9514:9517 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9506:9508 Coq.Arith.Max <> max syndef
R9514:9517 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9506:9508 Coq.Arith.Max <> max syndef
R9547:9550 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9539:9541 Coq.Arith.Max <> max syndef
R9547:9550 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9539:9541 Coq.Arith.Max <> max syndef
R9589:9592 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9572:9574 Coq.Arith.Max <> max syndef
R9577:9579 Coq.Arith.Max <> max syndef
R9593:9595 Coq.Arith.Max <> max syndef
R9589:9592 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9572:9574 Coq.Arith.Max <> max syndef
R9577:9579 Coq.Arith.Max <> max syndef
R9593:9595 Coq.Arith.Max <> max syndef
R9614:9626 General <> max_monotonic thm
R9652:9655 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9644:9646 Coq.Arith.Max <> max syndef
R9652:9655 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9644:9646 Coq.Arith.Max <> max syndef
R9685:9688 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9677:9679 Coq.Arith.Max <> max syndef
R9685:9688 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9677:9679 Coq.Arith.Max <> max syndef
R9718:9721 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9710:9712 Coq.Arith.Max <> max syndef
R9718:9721 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9710:9712 Coq.Arith.Max <> max syndef
R9760:9763 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9743:9745 Coq.Arith.Max <> max syndef
R9748:9750 Coq.Arith.Max <> max syndef
R9764:9766 Coq.Arith.Max <> max syndef
R9760:9763 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9743:9745 Coq.Arith.Max <> max syndef
R9748:9750 Coq.Arith.Max <> max syndef
R9764:9766 Coq.Arith.Max <> max syndef
R9785:9797 General <> max_monotonic thm
R9825:9828 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9808:9810 Coq.Arith.Max <> max syndef
R9813:9815 Coq.Arith.Max <> max syndef
R9825:9828 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9808:9810 Coq.Arith.Max <> max syndef
R9813:9815 Coq.Arith.Max <> max syndef
R9876:9879 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9850:9852 Coq.Arith.Max <> max syndef
R9855:9857 Coq.Arith.Max <> max syndef
R9860:9862 Coq.Arith.Max <> max syndef
R9880:9882 Coq.Arith.Max <> max syndef
R9876:9879 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9850:9852 Coq.Arith.Max <> max syndef
R9855:9857 Coq.Arith.Max <> max syndef
R9860:9862 Coq.Arith.Max <> max syndef
R9880:9882 Coq.Arith.Max <> max syndef
R9901:9913 General <> max_monotonic thm
R9950:9953 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9924:9926 Coq.Arith.Max <> max syndef
R9929:9931 Coq.Arith.Max <> max syndef
R9934:9936 Coq.Arith.Max <> max syndef
R9950:9953 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9924:9926 Coq.Arith.Max <> max syndef
R9929:9931 Coq.Arith.Max <> max syndef
R9934:9936 Coq.Arith.Max <> max syndef
R10021:10024 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R10012:10017 LamSF_Tactics <> status def
R10025:10030 LamSF_Closed <> maxvar def
R10021:10024 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R10012:10017 LamSF_Tactics <> status def
R10025:10030 LamSF_Closed <> maxvar def
R10086:10089 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R10077:10082 LamSF_Closed <> maxvar def
R10090:10092 Coq.Arith.Max <> max syndef
R10125:10130 LamSF_Closed <> maxvar def
R10095:10097 Coq.Arith.Max <> max syndef
R10112:10117 LamSF_Closed <> maxvar def
R10100:10105 LamSF_Closed <> maxvar def
R10086:10089 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R10077:10082 LamSF_Closed <> maxvar def
R10090:10092 Coq.Arith.Max <> max syndef
R10125:10130 LamSF_Closed <> maxvar def
R10095:10097 Coq.Arith.Max <> max syndef
R10112:10117 LamSF_Closed <> maxvar def
R10100:10105 LamSF_Closed <> maxvar def
R10173:10176 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R10146:10148 Coq.Arith.Max <> max syndef
R10163:10168 LamSF_Closed <> maxvar def
R10151:10156 LamSF_Closed <> maxvar def
R10177:10182 LamSF_Closed <> maxvar def
R10173:10176 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R10146:10148 Coq.Arith.Max <> max syndef
R10163:10168 LamSF_Closed <> maxvar def
R10151:10156 LamSF_Closed <> maxvar def
R10177:10182 LamSF_Closed <> maxvar def
R10251:10254 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R10206:10208 Coq.Arith.Max <> max syndef
R10241:10246 LamSF_Closed <> maxvar def
R10211:10213 Coq.Arith.Max <> max syndef
R10228:10233 LamSF_Closed <> maxvar def
R10216:10221 LamSF_Closed <> maxvar def
R10255:10257 Coq.Arith.Max <> max syndef
R10272:10277 LamSF_Closed <> maxvar def
R10260:10265 LamSF_Closed <> maxvar def
R10251:10254 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R10206:10208 Coq.Arith.Max <> max syndef
R10241:10246 LamSF_Closed <> maxvar def
R10211:10213 Coq.Arith.Max <> max syndef
R10228:10233 LamSF_Closed <> maxvar def
R10216:10221 LamSF_Closed <> maxvar def
R10255:10257 Coq.Arith.Max <> max syndef
R10272:10277 LamSF_Closed <> maxvar def
R10260:10265 LamSF_Closed <> maxvar def
R10371:10373 Coq.Init.Logic <> :type_scope:x_'='_x not
R10327:10332 LamSF_Tactics <> status def
R10334:10336 LamSF_Terms <> App constr
R10339:10341 LamSF_Terms <> App constr
R10344:10346 LamSF_Terms <> App constr
R10349:10351 LamSF_Terms <> App constr
R10374:10379 LamSF_Tactics <> status def
R10383:10385 LamSF_Terms <> App constr
R10388:10390 LamSF_Terms <> App constr
R10393:10395 LamSF_Terms <> App constr
R10371:10373 Coq.Init.Logic <> :type_scope:x_'='_x not
R10327:10332 LamSF_Tactics <> status def
R10334:10336 LamSF_Terms <> App constr
R10339:10341 LamSF_Terms <> App constr
R10344:10346 LamSF_Terms <> App constr
R10349:10351 LamSF_Terms <> App constr
R10374:10379 LamSF_Tactics <> status def
R10383:10385 LamSF_Terms <> App constr
R10388:10390 LamSF_Terms <> App constr
R10393:10395 LamSF_Terms <> App constr
R10481:10493 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R10445:10450 LamSF_Tactics <> status def
R10453:10455 LamSF_Terms <> App constr
R10458:10460 LamSF_Terms <> App constr
R10463:10465 LamSF_Terms <> App constr
R10494:10499 LamSF_Closed <> maxvar def
R10502:10504 LamSF_Terms <> App constr
R10507:10509 LamSF_Terms <> App constr
R10512:10514 LamSF_Terms <> App constr
R10481:10493 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R10445:10450 LamSF_Tactics <> status def
R10453:10455 LamSF_Terms <> App constr
R10458:10460 LamSF_Terms <> App constr
R10463:10465 LamSF_Terms <> App constr
R10494:10499 LamSF_Closed <> maxvar def
R10502:10504 LamSF_Terms <> App constr
R10507:10509 LamSF_Terms <> App constr
R10512:10514 LamSF_Terms <> App constr
R10612:10615 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R10575:10580 LamSF_Closed <> maxvar def
R10584:10586 LamSF_Terms <> App constr
R10589:10591 LamSF_Terms <> App constr
R10594:10596 LamSF_Terms <> App constr
R10616:10621 LamSF_Closed <> maxvar def
R10624:10626 LamSF_Terms <> App constr
R10629:10631 LamSF_Terms <> App constr
R10634:10636 LamSF_Terms <> App constr
R10639:10641 LamSF_Terms <> App constr
R10612:10615 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R10575:10580 LamSF_Closed <> maxvar def
R10584:10586 LamSF_Terms <> App constr
R10589:10591 LamSF_Terms <> App constr
R10594:10596 LamSF_Terms <> App constr
R10616:10621 LamSF_Closed <> maxvar def
R10624:10626 LamSF_Terms <> App constr
R10629:10631 LamSF_Terms <> App constr
R10634:10636 LamSF_Terms <> App constr
R10639:10641 LamSF_Terms <> App constr
R10684:10693 General <> max_is_max thm
def 10722:10728 <> program
R10743:10746 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R10735:10740 LamSF_Normal <> normal ind
R10742:10742 LamSF_Closed <> M var
R10755:10757 Coq.Init.Logic <> :type_scope:x_'='_x not
R10747:10752 LamSF_Closed <> maxvar def
R10754:10754 LamSF_Closed <> M var
prf 10771:10790 <> components_monotonic
R10815:10818 Coq.Init.Logic <> :type_scope:x_'->'_x not
R10828:10833 Coq.Init.Logic <> :type_scope:x_'->'_x not
R10869:10873 Coq.Init.Logic <> :type_scope:x_'->'_x not
R10911:10914 Coq.Init.Logic <> :type_scope:x_'->'_x not
R10916:10918 Coq.Init.Logic <> :type_scope:x_'='_x not
R10915:10915 LamSF_Closed <> M var
R10919:10919 LamSF_Closed <> N var
R10891:10893 Coq.Init.Logic <> :type_scope:x_'='_x not
R10874:10888 SF_reduction <> right_component def
R10890:10890 LamSF_Closed <> M var
R10894:10908 SF_reduction <> right_component def
R10910:10910 LamSF_Closed <> N var
R10850:10852 Coq.Init.Logic <> :type_scope:x_'='_x not
R10834:10847 SF_reduction <> left_component def
R10849:10849 LamSF_Closed <> M var
R10853:10866 SF_reduction <> left_component def
R10868:10868 LamSF_Closed <> N var
R10819:10825 LamSF_Closed <> program def
R10827:10827 LamSF_Closed <> N var
R10806:10812 LamSF_Closed <> program def
R10814:10814 LamSF_Closed <> M var
R10951:10957 LamSF_Closed <> program def
R11245:11245 Coq.Init.Logic <> :type_scope:x_'='_x not
R11245:11245 Coq.Init.Logic <> :type_scope:x_'='_x not
R11258:11271 SF_reduction <> star_monotonic thm
R11343:11350 SF_reduction <> compound ind
R11415:11418 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R11397:11402 LamSF_Tactics <> status def
R11405:11407 LamSF_Terms <> App constr
R11419:11424 LamSF_Closed <> maxvar def
R11427:11429 LamSF_Terms <> App constr
R11415:11418 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R11397:11402 LamSF_Tactics <> status def
R11405:11407 LamSF_Terms <> App constr
R11419:11424 LamSF_Closed <> maxvar def
R11427:11429 LamSF_Terms <> App constr
R11450:11465 LamSF_Closed <> status_lt_maxvar thm
def 11545:11554 <> factorable
R11561:11561 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R11580:11584 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R11562:11568 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R11570:11571 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R11573:11575 Coq.Init.Logic <> :type_scope:x_'='_x not
R11572:11572 LamSF_Closed <> M var
R11576:11577 LamSF_Terms <> Op constr
R11579:11579 LamSF_Closed <> o var
R11585:11592 SF_reduction <> compound ind
R11594:11594 LamSF_Closed <> M var
prf 11606:11628 <> programs_are_factorable
R11651:11655 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11656:11665 LamSF_Closed <> factorable def
R11667:11667 LamSF_Closed <> M var
R11642:11648 LamSF_Closed <> program def
R11650:11650 LamSF_Closed <> M var
R11686:11692 LamSF_Closed <> program def
R11695:11704 LamSF_Closed <> factorable def
R11726:11746 LamSF_Normal <> not_active_factorable thm
R11765:11768 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R11757:11762 LamSF_Tactics <> status def
R11769:11774 LamSF_Closed <> maxvar def
R11765:11768 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R11757:11762 LamSF_Tactics <> status def
R11769:11774 LamSF_Closed <> maxvar def
R11790:11805 LamSF_Closed <> status_lt_maxvar thm