-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathBeta_Reduction.glob
143 lines (143 loc) · 5.87 KB
/
Beta_Reduction.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
DIGEST b4bad27b73880da3f682a413203b08b5
FBeta_Reduction
R2136:2140 Coq.Arith.Arith <> <> lib
R2158:2164 General <> <> lib
R2182:2185 Test <> <> lib
R2203:2213 LamSF_Terms <> <> lib
R2231:2243 LamSF_Tactics <> <> lib
R2261:2283 LamSF_Substitution_term <> <> lib
R2301:2305 Coq.omega.Omega <> <> lib
ind 2350:2357 <> par_red1
constr 2376:2383 <> beta_red
constr 2501:2511 <> ref_par_red
constr 2554:2563 <> op_par_red
constr 2604:2614 <> app_par_red
constr 2740:2750 <> abs_par_red
R2360:2366 LamSF_Tactics <> termred def
R2418:2421 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2435:2457 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2458:2465 Beta_Reduction <> par_red1 ind
R2484:2488 LamSF_Terms <> subst def
R2493:2494 Beta_Reduction <> M' var
R2490:2491 Beta_Reduction <> N' var
R2468:2470 LamSF_Terms <> App constr
R2480:2480 Beta_Reduction <> N var
R2473:2475 LamSF_Terms <> Abs constr
R2477:2477 Beta_Reduction <> M var
R2422:2429 Beta_Reduction <> par_red1 ind
R2433:2434 Beta_Reduction <> N' var
R2431:2431 Beta_Reduction <> N var
R2405:2412 Beta_Reduction <> par_red1 ind
R2416:2417 Beta_Reduction <> M' var
R2414:2414 Beta_Reduction <> M var
R2525:2532 Beta_Reduction <> par_red1 ind
R2543:2545 LamSF_Terms <> Ref constr
R2547:2547 Beta_Reduction <> i var
R2535:2537 LamSF_Terms <> Ref constr
R2539:2539 Beta_Reduction <> i var
R2577:2584 Beta_Reduction <> par_red1 ind
R2594:2595 LamSF_Terms <> Op constr
R2597:2597 Beta_Reduction <> o var
R2587:2588 LamSF_Terms <> Op constr
R2590:2590 Beta_Reduction <> o var
R2657:2666 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2681:2685 LamSF_Terms <> lamSF ind
R2701:2704 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2705:2712 Beta_Reduction <> par_red1 ind
R2725:2727 LamSF_Terms <> App constr
R2732:2733 Beta_Reduction <> N' var
R2729:2730 Beta_Reduction <> M' var
R2715:2717 LamSF_Terms <> App constr
R2721:2721 Beta_Reduction <> N var
R2719:2719 Beta_Reduction <> M var
R2688:2695 Beta_Reduction <> par_red1 ind
R2699:2700 Beta_Reduction <> N' var
R2697:2697 Beta_Reduction <> N var
R2644:2651 Beta_Reduction <> par_red1 ind
R2655:2656 Beta_Reduction <> M' var
R2653:2653 Beta_Reduction <> M var
R2786:2789 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2790:2797 Beta_Reduction <> par_red1 ind
R2808:2810 LamSF_Terms <> Abs constr
R2812:2813 Beta_Reduction <> M' var
R2800:2802 LamSF_Terms <> Abs constr
R2804:2804 Beta_Reduction <> M var
R2773:2780 Beta_Reduction <> par_red1 ind
R2784:2785 Beta_Reduction <> M' var
R2782:2782 Beta_Reduction <> M var
def 2904:2910 <> par_red
R2915:2924 LamSF_Tactics <> multi_step ind
R2926:2933 Beta_Reduction <> par_red1 ind
prf 2944:2956 <> refl_par_red1
R2959:2968 LamSF_Tactics <> reflective def
R2970:2977 Beta_Reduction <> par_red1 ind
prf 3060:3086 <> lift_rec_preserves_par_red1
R3091:3108 LamSF_Tactics <> lift_rec_preserves def
R3110:3117 Beta_Reduction <> par_red1 ind
R3163:3167 LamSF_Terms <> subst def
R3180:3180 Coq.Init.Logic <> :type_scope:x_'='_x not
R3182:3182 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3180:3180 Coq.Init.Logic <> :type_scope:x_'='_x not
R3182:3182 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3222:3239 LamSF_Substitution_term <> lift_rec_subst_rec thm
R3222:3239 LamSF_Substitution_term <> lift_rec_subst_rec thm
R3222:3239 LamSF_Substitution_term <> lift_rec_subst_rec thm
R3262:3269 Beta_Reduction <> beta_red constr
prf 3330:3355 <> lift_rec_preserves_par_red
R3361:3378 LamSF_Tactics <> lift_rec_preserves def
R3380:3386 Beta_Reduction <> par_red def
R3409:3437 LamSF_Tactics <> lift_rec_preserves_multi_step thm
prf 3453:3480 <> subst_rec_preserves_par_red1
R3484:3502 LamSF_Tactics <> subst_rec_preserves def
R3504:3511 Beta_Reduction <> par_red1 ind
R3584:3588 LamSF_Terms <> subst def
R3612:3614 Coq.Init.Logic <> :type_scope:x_'='_x not
R3616:3616 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3612:3614 Coq.Init.Logic <> :type_scope:x_'='_x not
R3616:3616 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3657:3675 LamSF_Substitution_term <> subst_rec_subst_rec thm
R3657:3675 LamSF_Substitution_term <> subst_rec_subst_rec thm
R3657:3675 LamSF_Substitution_term <> subst_rec_subst_rec thm
R3686:3693 Beta_Reduction <> beta_red constr
R3706:3715 LamSF_Terms <> insert_Ref def
R3723:3729 Test <> compare def
R3723:3729 Test <> compare def
R3777:3780 LamSF_Terms <> lift def
prf 3803:3829 <> preserves_lift_rec_par_red1
R3833:3850 LamSF_Tactics <> preserves_lift_rec def
R3852:3859 Beta_Reduction <> par_red1 ind
R4006:4010 LamSF_Terms <> subst def
R4006:4010 LamSF_Terms <> subst def
R4027:4031 LamSF_Terms <> subst def
R4060:4060 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4060:4060 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4083:4100 LamSF_Substitution_term <> lift_rec_subst_rec thm
R4083:4100 LamSF_Substitution_term <> lift_rec_subst_rec thm
R4083:4100 LamSF_Substitution_term <> lift_rec_subst_rec thm
R4167:4169 LamSF_Terms <> App constr
R4167:4169 LamSF_Terms <> App constr
R4237:4239 LamSF_Terms <> Abs constr
R4237:4239 LamSF_Terms <> Abs constr
prf 4258:4281 <> par_red1_preserves_lift1
R4310:4313 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4340:4343 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4344:4350 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R4353:4354 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R4369:4372 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R4355:4362 Beta_Reduction <> par_red1 ind
R4367:4368 Beta_Reduction <> N0 var
R4364:4365 Beta_Reduction <> M0 var
R4382:4384 Coq.Init.Logic <> :type_scope:x_'='_x not
R4373:4376 LamSF_Terms <> lift def
R4380:4381 Beta_Reduction <> N0 var
R4385:4385 Beta_Reduction <> N var
R4325:4325 Coq.Init.Logic <> :type_scope:x_'='_x not
R4335:4338 Coq.Init.Logic <> :type_scope:x_'='_x not
R4326:4329 LamSF_Terms <> lift def
R4333:4334 Beta_Reduction <> M0 var
R4339:4339 Beta_Reduction <> M var
R4298:4305 Beta_Reduction <> par_red1 ind
R4309:4309 Beta_Reduction <> N var
R4307:4307 Beta_Reduction <> M var
R4414:4417 LamSF_Terms <> lift def
R4433:4459 Beta_Reduction <> preserves_lift_rec_par_red1 thm