-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathLamSF_Eval.glob
225 lines (225 loc) · 8.05 KB
/
LamSF_Eval.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
DIGEST 6f01e63a81cd28079afef495cbdea1d7
FLamSF_Eval
R1990:1994 Coq.Arith.Arith <> <> lib
R2012:2014 Coq.Arith.Max <> <> lib
R2033:2036 Test <> <> lib
R2054:2060 General <> <> lib
R2079:2089 LamSF_Terms <> <> lib
R2107:2119 LamSF_Tactics <> <> lib
R2137:2159 LamSF_Substitution_term <> <> lib
R2177:2186 Components <> <> lib
R2204:2212 Compounds <> <> lib
R2230:2244 LamSF_reduction <> <> lib
R2262:2273 LamSF_Closed <> <> lib
R2307:2315 LamSF_Terms <> subst_rec def
R2323:2331 LamSF_Terms <> subst_rec def
R2365:2377 LamSF_Substitution_term <> lift_rec_null thm
R2422:2431 LamSF_Tactics <> multi_step ind
R2445:2447 LamSF_Terms <> App constr
R2450:2452 LamSF_Terms <> App constr
R2455:2456 LamSF_Terms <> Op constr
R2458:2460 LamSF_Terms <> Gop constr
R2433:2442 LamSF_reduction <> lamSF_red1 ind
R2422:2431 LamSF_Tactics <> multi_step ind
R2445:2447 LamSF_Terms <> App constr
R2450:2452 LamSF_Terms <> App constr
R2455:2456 LamSF_Terms <> Op constr
R2458:2460 LamSF_Terms <> Gop constr
R2433:2442 LamSF_reduction <> lamSF_red1 ind
R2498:2500 LamSF_Terms <> App constr
R2530:2544 Components <> right_component def
R2503:2505 LamSF_Terms <> App constr
R2510:2523 Components <> left_component def
R2483:2490 LamSF_Tactics <> succ_red constr
R2634:2642 LamSF_reduction <> lamSF_red def
R2634:2642 LamSF_reduction <> lamSF_red def
R2671:2680 LamSF_Tactics <> multi_step ind
R2702:2704 LamSF_Terms <> Ref constr
R2694:2696 LamSF_Terms <> Ref constr
R2682:2691 LamSF_reduction <> lamSF_red1 ind
R2671:2680 LamSF_Tactics <> multi_step ind
R2702:2704 LamSF_Terms <> Ref constr
R2694:2696 LamSF_Terms <> Ref constr
R2682:2691 LamSF_reduction <> lamSF_red1 ind
R2731:2740 LamSF_Tactics <> multi_step ind
R2764:2766 LamSF_Terms <> App constr
R2754:2756 LamSF_Terms <> App constr
R2742:2751 LamSF_reduction <> lamSF_red1 ind
R2731:2740 LamSF_Tactics <> multi_step ind
R2764:2766 LamSF_Terms <> App constr
R2754:2756 LamSF_Terms <> App constr
R2742:2751 LamSF_reduction <> lamSF_red1 ind
R2825:2834 LamSF_Tactics <> multi_step ind
R2856:2858 LamSF_Terms <> Abs constr
R2848:2850 LamSF_Terms <> Abs constr
R2836:2845 LamSF_reduction <> lamSF_red1 ind
R2825:2834 LamSF_Tactics <> multi_step ind
R2856:2858 LamSF_Terms <> Abs constr
R2848:2850 LamSF_Terms <> Abs constr
R2836:2845 LamSF_reduction <> lamSF_red1 ind
R2914:2923 LamSF_reduction <> lamSF_red1 ind
R2934:2936 LamSF_Terms <> Abs constr
R2926:2928 LamSF_Terms <> Abs constr
R2914:2923 LamSF_reduction <> lamSF_red1 ind
R2934:2936 LamSF_Terms <> Abs constr
R2926:2928 LamSF_Terms <> Abs constr
def 3021:3028 <> eval_app
R3044:3044 LamSF_Eval <> M var
R3054:3056 LamSF_Terms <> App constr
R3059:3061 LamSF_Terms <> App constr
R3064:3065 LamSF_Terms <> Op constr
R3067:3069 LamSF_Terms <> Sop constr
R3083:3085 LamSF_Terms <> App constr
R3099:3101 LamSF_Terms <> App constr
R3106:3106 LamSF_Eval <> N var
R3088:3090 LamSF_Terms <> App constr
R3095:3095 LamSF_Eval <> N var
R3111:3113 LamSF_Terms <> App constr
R3116:3118 LamSF_Terms <> App constr
R3121:3122 LamSF_Terms <> Op constr
R3124:3126 LamSF_Terms <> Aop constr
R3140:3142 LamSF_Terms <> App constr
R3156:3156 LamSF_Eval <> N var
R3145:3147 LamSF_Terms <> App constr
R3160:3162 LamSF_Terms <> App constr
R3165:3166 LamSF_Terms <> Op constr
R3168:3170 LamSF_Terms <> Kop constr
R3185:3186 LamSF_Terms <> Op constr
R3188:3190 LamSF_Terms <> Yop constr
R3196:3198 LamSF_Terms <> App constr
R3203:3205 LamSF_Terms <> App constr
R3231:3231 LamSF_Eval <> N var
R3208:3210 LamSF_Terms <> App constr
R3222:3223 LamSF_Terms <> Op constr
R3225:3227 LamSF_Terms <> Yop constr
R3213:3214 LamSF_Terms <> Op constr
R3216:3218 LamSF_Terms <> Aop constr
R3200:3200 LamSF_Eval <> N var
R3236:3238 LamSF_Terms <> Abs constr
R3246:3250 LamSF_Terms <> subst def
R3252:3252 LamSF_Eval <> N var
R3264:3266 LamSF_Terms <> App constr
R3270:3270 LamSF_Eval <> N var
prf 3285:3303 <> eval_app_from_lamSF
R3319:3327 LamSF_reduction <> lamSF_red def
R3340:3347 LamSF_Eval <> eval_app def
R3351:3351 LamSF_Eval <> N var
R3349:3349 LamSF_Eval <> M var
R3330:3332 LamSF_Terms <> App constr
R3336:3336 LamSF_Eval <> N var
R3334:3334 LamSF_Eval <> M var
R3447:3454 LamSF_Tactics <> zero_red constr
def 3625:3629 <> eval0
R3635:3639 LamSF_Terms <> lamSF ind
R3651:3651 LamSF_Eval <> M var
R3661:3663 LamSF_Terms <> Ref constr
R3670:3672 LamSF_Terms <> Ref constr
R3679:3680 LamSF_Terms <> Op constr
R3687:3688 LamSF_Terms <> Op constr
R3694:3696 LamSF_Terms <> Abs constr
R3704:3706 LamSF_Terms <> Abs constr
R3713:3715 LamSF_Terms <> App constr
R3727:3734 LamSF_Eval <> eval_app def
R3737:3741 LamSF_Eval <> eval0 def
prf 3764:3779 <> eval0_from_lamSF
R3793:3801 LamSF_reduction <> lamSF_red def
R3806:3810 LamSF_Eval <> eval0 def
R3812:3812 LamSF_Eval <> M var
R3803:3803 LamSF_Eval <> M var
R3875:3877 LamSF_Terms <> App constr
R3880:3884 LamSF_Eval <> eval0 def
R3854:3867 LamSF_Tactics <> transitive_red thm
R3875:3877 LamSF_Terms <> App constr
R3880:3884 LamSF_Eval <> eval0 def
R3854:3867 LamSF_Tactics <> transitive_red thm
R3903:3925 LamSF_reduction <> preserves_app_lamSF_red thm
R3937:3955 LamSF_Eval <> eval_app_from_lamSF thm
R4022:4030 LamSF_reduction <> lamSF_red def
R4022:4030 LamSF_reduction <> lamSF_red def
R4063:4072 LamSF_Tactics <> multi_step ind
R4074:4083 LamSF_reduction <> lamSF_red1 ind
R4063:4072 LamSF_Tactics <> multi_step ind
R4074:4083 LamSF_reduction <> lamSF_red1 ind
R4123:4127 LamSF_Eval <> eval0 def
R4102:4115 LamSF_Tactics <> transitive_red thm
R4173:4177 LamSF_Eval <> eval0 def
R4180:4187 LamSF_Eval <> eval_app def
R4198:4202 LamSF_Terms <> subst def
def 4274:4276 <> not
R4283:4285 LamSF_Terms <> App constr
R4311:4314 Components <> k_op def
R4288:4290 LamSF_Terms <> App constr
R4295:4297 LamSF_Terms <> App constr
R4304:4307 Components <> i_op def
R4299:4302 Components <> k_op def
R4292:4292 LamSF_Eval <> M var
prf 4324:4331 <> not_true
R4335:4343 LamSF_reduction <> lamSF_red def
R4357:4359 LamSF_Terms <> App constr
R4366:4369 Components <> i_op def
R4361:4364 Components <> k_op def
R4346:4348 LamSF_Eval <> not def
R4350:4353 Components <> k_op def
R4387:4389 LamSF_Eval <> not def
prf 4418:4426 <> not_false
R4430:4438 LamSF_reduction <> lamSF_red def
R4462:4465 Components <> k_op def
R4441:4443 LamSF_Eval <> not def
R4446:4448 LamSF_Terms <> App constr
R4455:4458 Components <> i_op def
R4450:4453 Components <> k_op def
def 4519:4521 <> iff
R4530:4532 LamSF_Terms <> App constr
R4545:4547 LamSF_Eval <> not def
R4549:4549 LamSF_Eval <> N var
R4535:4537 LamSF_Terms <> App constr
R4541:4541 LamSF_Eval <> N var
R4539:4539 LamSF_Eval <> M var
prf 4561:4569 <> true_true
R4573:4581 LamSF_reduction <> lamSF_red def
R4599:4602 Components <> k_op def
R4584:4586 LamSF_Eval <> iff def
R4593:4596 Components <> k_op def
R4588:4591 Components <> k_op def
R4620:4622 LamSF_Eval <> iff def
R4632:4634 LamSF_Eval <> not def
prf 4673:4682 <> true_false
R4686:4694 LamSF_reduction <> lamSF_red def
R4724:4726 LamSF_Terms <> App constr
R4733:4736 Components <> i_op def
R4728:4731 Components <> k_op def
R4697:4699 LamSF_Eval <> iff def
R4707:4709 LamSF_Terms <> App constr
R4716:4719 Components <> i_op def
R4711:4714 Components <> k_op def
R4701:4704 Components <> k_op def
R4755:4757 LamSF_Eval <> iff def
R4767:4769 LamSF_Eval <> not def
prf 4808:4817 <> false_true
R4821:4829 LamSF_reduction <> lamSF_red def
R4859:4861 LamSF_Terms <> App constr
R4868:4871 Components <> i_op def
R4863:4866 Components <> k_op def
R4832:4834 LamSF_Eval <> iff def
R4852:4855 Components <> k_op def
R4837:4839 LamSF_Terms <> App constr
R4846:4849 Components <> i_op def
R4841:4844 Components <> k_op def
R4890:4892 LamSF_Eval <> iff def
R4902:4904 LamSF_Eval <> not def
prf 4982:4992 <> false_false
R4996:5004 LamSF_reduction <> lamSF_red def
R5044:5047 Components <> k_op def
R5007:5009 LamSF_Eval <> iff def
R5028:5030 LamSF_Terms <> App constr
R5037:5040 Components <> i_op def
R5032:5035 Components <> k_op def
R5012:5014 LamSF_Terms <> App constr
R5021:5024 Components <> i_op def
R5016:5019 Components <> k_op def
R5065:5067 LamSF_Eval <> iff def
R5070:5072 LamSF_Eval <> not def
R5168:5177 LamSF_Terms <> insert_Ref def
R5187:5190 LamSF_Terms <> lift def
R5206:5220 LamSF_Closed <> lift_rec_closed thm
R5290:5299 LamSF_Terms <> insert_Ref def