forked from Barry-Jay/lambdaSF
-
Notifications
You must be signed in to change notification settings - Fork 0
/
LamSF_Simulation.glob
261 lines (261 loc) · 10.2 KB
/
LamSF_Simulation.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
DIGEST 012a3caedfef62d25c3aa2f6628d3555
FLamSF_Simulation
R2329:2333 Coq.Arith.Arith <> <> lib
R2351:2357 General <> <> lib
R2375:2385 LamSF_Terms <> <> lib
R2403:2415 LamSF_Tactics <> <> lib
R2433:2446 Beta_Reduction <> <> lib
R2464:2476 LamSF_Redexes <> <> lib
R2494:2497 Test <> <> lib
R2515:2525 LamSF_Marks <> <> lib
R2543:2560 LamSF_Substitution <> <> lib
R2578:2592 LamSF_Residuals <> <> lib
prf 2634:2646 <> mark_lift_rec
R2663:2667 LamSF_Terms <> lamSF ind
R2677:2679 Coq.Init.Datatypes <> nat ind
R2707:2709 Coq.Init.Logic <> :type_scope:x_'='_x not
R2684:2693 LamSF_Substitution <> lift_rec_r def
R2706:2706 LamSF_Simulation <> n var
R2704:2704 LamSF_Simulation <> k var
R2696:2699 LamSF_Marks <> mark def
R2701:2701 LamSF_Simulation <> M var
R2710:2713 LamSF_Marks <> mark def
R2716:2723 LamSF_Terms <> lift_rec def
R2729:2729 LamSF_Simulation <> n var
R2727:2727 LamSF_Simulation <> k var
R2725:2725 LamSF_Simulation <> M var
prf 2783:2791 <> mark_lift
R2808:2812 LamSF_Terms <> lamSF ind
R2820:2822 Coq.Init.Datatypes <> nat ind
R2843:2845 Coq.Init.Logic <> :type_scope:x_'='_x not
R2826:2831 LamSF_Substitution <> lift_r def
R2836:2839 LamSF_Marks <> mark def
R2841:2841 LamSF_Simulation <> M var
R2833:2833 LamSF_Simulation <> n var
R2846:2849 LamSF_Marks <> mark def
R2852:2855 LamSF_Terms <> lift def
R2859:2859 LamSF_Simulation <> M var
R2857:2857 LamSF_Simulation <> n var
R2877:2880 LamSF_Terms <> lift def
R2898:2903 LamSF_Substitution <> lift_r def
R2928:2940 LamSF_Simulation <> mark_lift_rec thm
R2928:2940 LamSF_Simulation <> mark_lift_rec thm
prf 2955:2968 <> mark_subst_rec
R2987:2991 LamSF_Terms <> lamSF ind
R2999:3001 Coq.Init.Datatypes <> nat ind
R3037:3039 Coq.Init.Logic <> :type_scope:x_'='_x not
R3006:3016 LamSF_Substitution <> subst_rec_r def
R3036:3036 LamSF_Simulation <> n var
R3028:3031 LamSF_Marks <> mark def
R3033:3033 LamSF_Simulation <> N var
R3019:3022 LamSF_Marks <> mark def
R3024:3024 LamSF_Simulation <> M var
R3040:3043 LamSF_Marks <> mark def
R3046:3054 LamSF_Terms <> subst_rec def
R3060:3060 LamSF_Simulation <> n var
R3058:3058 LamSF_Simulation <> N var
R3056:3056 LamSF_Simulation <> M var
R3124:3133 LamSF_Substitution <> insert_Var def
R3136:3145 LamSF_Terms <> insert_Ref def
R3162:3168 Test <> compare def
R3162:3168 Test <> compare def
R3217:3225 LamSF_Simulation <> mark_lift thm
R3217:3225 LamSF_Simulation <> mark_lift thm
R3217:3225 LamSF_Simulation <> mark_lift thm
prf 3255:3264 <> mark_subst
R3282:3286 LamSF_Terms <> lamSF ind
R3314:3316 Coq.Init.Logic <> :type_scope:x_'='_x not
R3289:3295 LamSF_Substitution <> subst_r def
R3307:3310 LamSF_Marks <> mark def
R3312:3312 LamSF_Simulation <> N var
R3298:3301 LamSF_Marks <> mark def
R3303:3303 LamSF_Simulation <> M var
R3317:3320 LamSF_Marks <> mark def
R3323:3327 LamSF_Terms <> subst def
R3331:3331 LamSF_Simulation <> N var
R3329:3329 LamSF_Simulation <> M var
R3349:3353 LamSF_Terms <> subst def
R3371:3377 LamSF_Substitution <> subst_r def
R3402:3415 LamSF_Simulation <> mark_subst_rec thm
R3402:3415 LamSF_Simulation <> mark_subst_rec thm
def 3473:3481 <> simulates
R3489:3495 LamSF_Tactics <> termred def
R3525:3528 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3529:3535 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R3537:3538 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R3539:3547 LamSF_Residuals <> residuals ind
R3561:3564 LamSF_Marks <> mark def
R3566:3567 LamSF_Simulation <> M' var
R3558:3558 LamSF_Simulation <> V var
R3550:3553 LamSF_Marks <> mark def
R3555:3555 LamSF_Simulation <> M var
R3517:3519 LamSF_Simulation <> red var
R3523:3524 LamSF_Simulation <> M' var
R3521:3521 LamSF_Simulation <> M var
prf 3579:3588 <> simulation
R3618:3621 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3622:3628 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R3630:3631 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R3632:3640 LamSF_Residuals <> residuals ind
R3654:3657 LamSF_Marks <> mark def
R3659:3660 LamSF_Simulation <> M' var
R3651:3651 LamSF_Simulation <> V var
R3643:3646 LamSF_Marks <> mark def
R3648:3648 LamSF_Simulation <> M var
R3605:3612 Beta_Reduction <> par_red1 ind
R3616:3617 LamSF_Simulation <> M' var
R3614:3614 LamSF_Simulation <> M var
R3710:3714 LamSF_Terms <> subst def
R3728:3741 LamSF_Simulation <> mark_subst_rec thm
R3728:3741 LamSF_Simulation <> mark_subst_rec thm
R3728:3741 LamSF_Simulation <> mark_subst_rec thm
R3751:3752 LamSF_Redexes <> Ap constr
R3760:3762 LamSF_Redexes <> Fun constr
R3754:3757 Coq.Init.Datatypes <> true constr
R3751:3752 LamSF_Redexes <> Ap constr
R3760:3762 LamSF_Redexes <> Fun constr
R3754:3757 Coq.Init.Datatypes <> true constr
R3780:3788 LamSF_Residuals <> Res_redex constr
prf 3837:3851 <> unmark_lift_rec
R3868:3874 LamSF_Redexes <> redexes ind
R3884:3886 Coq.Init.Datatypes <> nat ind
R3914:3916 Coq.Init.Logic <> :type_scope:x_'='_x not
R3891:3898 LamSF_Terms <> lift_rec def
R3913:3913 LamSF_Simulation <> n var
R3911:3911 LamSF_Simulation <> k var
R3901:3906 LamSF_Marks <> unmark def
R3908:3908 LamSF_Simulation <> U var
R3917:3922 LamSF_Marks <> unmark def
R3925:3934 LamSF_Substitution <> lift_rec_r def
R3940:3940 LamSF_Simulation <> n var
R3938:3938 LamSF_Simulation <> k var
R3936:3936 LamSF_Simulation <> U var
prf 4031:4041 <> unmark_lift
R4058:4064 LamSF_Redexes <> redexes ind
R4072:4074 Coq.Init.Datatypes <> nat ind
R4095:4097 Coq.Init.Logic <> :type_scope:x_'='_x not
R4078:4081 LamSF_Terms <> lift def
R4086:4091 LamSF_Marks <> unmark def
R4093:4093 LamSF_Simulation <> U var
R4083:4083 LamSF_Simulation <> n var
R4098:4103 LamSF_Marks <> unmark def
R4106:4111 LamSF_Substitution <> lift_r def
R4115:4115 LamSF_Simulation <> U var
R4113:4113 LamSF_Simulation <> n var
R4133:4136 LamSF_Terms <> lift def
R4154:4159 LamSF_Substitution <> lift_r def
R4184:4198 LamSF_Simulation <> unmark_lift_rec thm
R4184:4198 LamSF_Simulation <> unmark_lift_rec thm
prf 4213:4228 <> unmark_subst_rec
R4247:4253 LamSF_Redexes <> redexes ind
R4261:4263 Coq.Init.Datatypes <> nat ind
R4301:4303 Coq.Init.Logic <> :type_scope:x_'='_x not
R4268:4276 LamSF_Terms <> subst_rec def
R4300:4300 LamSF_Simulation <> n var
R4290:4295 LamSF_Marks <> unmark def
R4297:4297 LamSF_Simulation <> V var
R4279:4284 LamSF_Marks <> unmark def
R4286:4286 LamSF_Simulation <> U var
R4304:4309 LamSF_Marks <> unmark def
R4312:4322 LamSF_Substitution <> subst_rec_r def
R4328:4328 LamSF_Simulation <> n var
R4326:4326 LamSF_Simulation <> V var
R4324:4324 LamSF_Simulation <> U var
R4392:4401 LamSF_Substitution <> insert_Var def
R4404:4413 LamSF_Terms <> insert_Ref def
R4430:4436 Test <> compare def
R4430:4436 Test <> compare def
R4485:4495 LamSF_Simulation <> unmark_lift thm
R4485:4495 LamSF_Simulation <> unmark_lift thm
R4485:4495 LamSF_Simulation <> unmark_lift thm
prf 4525:4536 <> unmark_subst
R4554:4560 LamSF_Redexes <> redexes ind
R4590:4592 Coq.Init.Logic <> :type_scope:x_'='_x not
R4563:4567 LamSF_Terms <> subst def
R4581:4586 LamSF_Marks <> unmark def
R4588:4588 LamSF_Simulation <> V var
R4570:4575 LamSF_Marks <> unmark def
R4577:4577 LamSF_Simulation <> U var
R4593:4598 LamSF_Marks <> unmark def
R4601:4607 LamSF_Substitution <> subst_r def
R4611:4611 LamSF_Simulation <> V var
R4609:4609 LamSF_Simulation <> U var
R4629:4633 LamSF_Terms <> subst def
R4651:4657 LamSF_Substitution <> subst_r def
R4682:4697 LamSF_Simulation <> unmark_subst_rec thm
R4682:4697 LamSF_Simulation <> unmark_subst_rec thm
prf 4712:4723 <> completeness
R4743:4749 LamSF_Redexes <> redexes ind
R4767:4770 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4771:4778 Beta_Reduction <> par_red1 ind
R4792:4797 LamSF_Marks <> unmark def
R4799:4799 LamSF_Simulation <> W var
R4781:4786 LamSF_Marks <> unmark def
R4788:4788 LamSF_Simulation <> U var
R4752:4760 LamSF_Residuals <> residuals ind
R4766:4766 LamSF_Simulation <> W var
R4764:4764 LamSF_Simulation <> V var
R4762:4762 LamSF_Simulation <> U var
R4864:4869 LamSF_Marks <> unmark def
R4872:4878 LamSF_Substitution <> subst_r def
R4895:4899 LamSF_Terms <> subst def
R4914:4919 LamSF_Marks <> unmark def
R4902:4907 LamSF_Marks <> unmark def
R4864:4869 LamSF_Marks <> unmark def
R4872:4878 LamSF_Substitution <> subst_r def
R4895:4899 LamSF_Terms <> subst def
R4914:4919 LamSF_Marks <> unmark def
R4902:4907 LamSF_Marks <> unmark def
R4936:4943 Beta_Reduction <> beta_red constr
R4954:4958 LamSF_Terms <> subst def
R4961:4967 LamSF_Substitution <> subst_r def
R4990:5005 LamSF_Simulation <> unmark_subst_rec thm
R4990:5005 LamSF_Simulation <> unmark_subst_rec thm
R4990:5005 LamSF_Simulation <> unmark_subst_rec thm
def 5195:5203 <> reduction
R5210:5214 LamSF_Terms <> lamSF ind
R5222:5228 LamSF_Redexes <> redexes ind
R5236:5240 LamSF_Terms <> lamSF ind
R5248:5256 LamSF_Residuals <> residuals ind
R5270:5273 LamSF_Marks <> mark def
R5275:5275 LamSF_Simulation <> N var
R5267:5267 LamSF_Simulation <> U var
R5259:5262 LamSF_Marks <> mark def
R5264:5264 LamSF_Simulation <> M var
prf 5286:5303 <> reduction_function
R5324:5328 LamSF_Terms <> lamSF ind
R5336:5342 LamSF_Redexes <> redexes ind
R5362:5365 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5381:5384 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5386:5388 Coq.Init.Logic <> :type_scope:x_'='_x not
R5385:5385 LamSF_Simulation <> N var
R5389:5389 LamSF_Simulation <> P var
R5366:5374 LamSF_Simulation <> reduction def
R5380:5380 LamSF_Simulation <> P var
R5378:5378 LamSF_Simulation <> U var
R5376:5376 LamSF_Simulation <> M var
R5347:5355 LamSF_Simulation <> reduction def
R5361:5361 LamSF_Simulation <> N var
R5359:5359 LamSF_Simulation <> U var
R5357:5357 LamSF_Simulation <> M var
R5406:5414 LamSF_Simulation <> reduction def
R5438:5441 LamSF_Redexes <> comp ind
R5453:5456 LamSF_Marks <> mark def
R5444:5447 LamSF_Marks <> mark def
R5438:5441 LamSF_Redexes <> comp ind
R5453:5456 LamSF_Marks <> mark def
R5444:5447 LamSF_Marks <> mark def
R5479:5485 LamSF_Marks <> inverse thm
R5500:5506 LamSF_Marks <> inverse thm
R5518:5531 LamSF_Marks <> comp_unmark_eq thm
R5479:5485 LamSF_Marks <> inverse thm
R5479:5485 LamSF_Marks <> inverse thm
R5500:5506 LamSF_Marks <> inverse thm
R5500:5506 LamSF_Marks <> inverse thm
R5518:5531 LamSF_Marks <> comp_unmark_eq thm
R5580:5583 LamSF_Marks <> mark def
R5589:5592 LamSF_Marks <> mark def
R5550:5570 LamSF_Residuals <> mutual_residuals_comp thm
R5580:5583 LamSF_Marks <> mark def
R5589:5592 LamSF_Marks <> mark def
R5550:5570 LamSF_Residuals <> mutual_residuals_comp thm