|
1
|
DIGEST a67e786cf59f0f9bb308946312df06f5
|
|
2
|
FStreamsLib
|
|
3
|
R15:21 Coq.Lists.Streams <> <> lib
|
|
4
|
R32:35 Coq.Lists.List <> <> lib
|
|
5
|
R53:58 Coq.Setoids.Setoid <> <> lib
|
|
6
|
R76:95 Coq.Relations.Relation_Definitions <> <> lib
|
|
7
|
R113:122 Coq.Program.Wf <> <> lib
|
|
8
|
R140:145 Coq.Arith.Wf_nat <> <> lib
|
|
9
|
R163:173 Coq.Wellfounded.Wellfounded <> <> lib
|
|
10
|
def 188:191 <> mapT
|
|
11
|
R243:243 StreamsLib <> F var
|
|
12
|
R245:245 StreamsLib <> B var
|
|
13
|
R234:234 StreamsLib <> F var
|
|
14
|
R236:236 StreamsLib <> A var
|
|
15
|
R227:227 StreamsLib <> B var
|
|
16
|
R222:222 StreamsLib <> A var
|
|
17
|
def 261:266 <> applyT
|
|
18
|
R322:322 StreamsLib <> F var
|
|
19
|
R324:324 StreamsLib <> B var
|
|
20
|
R313:313 StreamsLib <> F var
|
|
21
|
R315:315 StreamsLib <> A var
|
|
22
|
R297:297 StreamsLib <> F var
|
|
23
|
R305:305 StreamsLib <> B var
|
|
24
|
R300:300 StreamsLib <> A var
|
|
25
|
def 340:351 <> option_apply
|
|
26
|
R362:367 StreamsLib <> applyT def
|
|
27
|
R378:378 StreamsLib <> B var
|
|
28
|
R376:376 StreamsLib <> A var
|
|
29
|
R369:374 Coq.Init.Datatypes <> option ind
|
|
30
|
R405:405 StreamsLib <> a var
|
|
31
|
R402:402 StreamsLib <> f var
|
|
32
|
R415:418 Coq.Init.Datatypes <> Some constr
|
|
33
|
R423:426 Coq.Init.Datatypes <> Some constr
|
|
34
|
R433:436 Coq.Init.Datatypes <> Some constr
|
|
35
|
R439:439 StreamsLib <> f var
|
|
36
|
R441:441 StreamsLib <> a var
|
|
37
|
R465:468 Coq.Init.Datatypes <> None constr
|
|
38
|
ax 484:490 <> eqst_eq
|
|
39
|
R513:518 Coq.Lists.Streams <> Stream coind
|
|
40
|
R520:520 StreamsLib <> A var
|
|
41
|
R538:540 Coq.Init.Logic <> :type_scope:x_'='_x not
|
|
42
|
R537:537 StreamsLib <> s var
|
|
43
|
R541:542 StreamsLib <> s' var
|
|
44
|
R524:527 Coq.Lists.Streams <> EqSt coind
|
|
45
|
R531:532 StreamsLib <> s' var
|
|
46
|
R529:529 StreamsLib <> s var
|
|
47
|
prf 554:560 <> inv_inv
|
|
48
|
R580:585 Coq.Lists.Streams <> Stream coind
|
|
49
|
R587:587 StreamsLib <> A var
|
|
50
|
R603:608 Coq.Lists.Streams <> Stream coind
|
|
51
|
R610:610 StreamsLib <> A var
|
|
52
|
R628:633 Coq.Lists.Streams <> ForAll coind
|
|
53
|
R659:659 StreamsLib <> s var
|
|
54
|
R646:651 Coq.Lists.Streams <> ForAll coind
|
|
55
|
R655:656 StreamsLib <> s' var
|
|
56
|
R653:653 StreamsLib <> P var
|
|
57
|
R614:619 Coq.Lists.Streams <> ForAll coind
|
|
58
|
R623:623 StreamsLib <> s var
|
|
59
|
R621:621 StreamsLib <> P var
|
|
60
|
R733:746 Coq.Lists.Streams <> HereAndFurther constr
|
|
61
|
R733:746 Coq.Lists.Streams <> HereAndFurther constr
|
|
62
|
prf 823:829 <> evt_inv
|
|
63
|
R851:856 Coq.Lists.Streams <> Stream coind
|
|
64
|
R858:858 StreamsLib <> A var
|
|
65
|
R874:879 Coq.Lists.Streams <> Stream coind
|
|
66
|
R881:881 StreamsLib <> A var
|
|
67
|
R915:920 Coq.Lists.Streams <> Exists ind
|
|
68
|
R947:947 StreamsLib <> s var
|
|
69
|
R937:940 Coq.Init.Logic <> :type_scope:x_'/\'_x not
|
|
70
|
R933:933 StreamsLib <> P var
|
|
71
|
R935:936 StreamsLib <> s' var
|
|
72
|
R941:941 StreamsLib <> Q var
|
|
73
|
R943:944 StreamsLib <> s' var
|
|
74
|
R901:906 Coq.Lists.Streams <> Exists ind
|
|
75
|
R910:910 StreamsLib <> s var
|
|
76
|
R908:908 StreamsLib <> Q var
|
|
77
|
R887:892 Coq.Lists.Streams <> ForAll coind
|
|
78
|
R896:896 StreamsLib <> s var
|
|
79
|
R894:894 StreamsLib <> P var
|
|
80
|
R977:980 Coq.Lists.Streams <> Here constr
|
|
81
|
R977:980 Coq.Lists.Streams <> Here constr
|
|
82
|
R0:-1 StreamsLib <> y var
|
|
83
|
R1017:1023 Coq.Lists.Streams <> Further constr
|
|
84
|
R1017:1023 Coq.Lists.Streams <> Further constr
|
|
85
|
def 1087:1098 <> ForAll_apply
|
|
86
|
R1112:1117 Coq.Lists.Streams <> Stream coind
|
|
87
|
R1119:1119 StreamsLib <> A var
|
|
88
|
R1196:1201 Coq.Lists.Streams <> ForAll coind
|
|
89
|
R1205:1205 StreamsLib <> s var
|
|
90
|
R1203:1203 StreamsLib <> Q var
|
|
91
|
R1160:1165 Coq.Lists.Streams <> ForAll coind
|
|
92
|
R1189:1189 StreamsLib <> s var
|
|
93
|
R1184:1184 StreamsLib <> Q var
|
|
94
|
R1186:1186 StreamsLib <> s var
|
|
95
|
R1177:1177 StreamsLib <> P var
|
|
96
|
R1179:1179 StreamsLib <> s var
|
|
97
|
R1144:1149 Coq.Lists.Streams <> ForAll coind
|
|
98
|
R1153:1153 StreamsLib <> s var
|
|
99
|
R1151:1151 StreamsLib <> P var
|
|
100
|
R1257:1265 StreamsLib <> always_pq var
|
|
101
|
R1247:1254 StreamsLib <> always_p var
|
|
102
|
R1276:1289 Coq.Lists.Streams <> HereAndFurther constr
|
|
103
|
R1308:1321 Coq.Lists.Streams <> HereAndFurther constr
|
|
104
|
R1343:1356 Coq.Lists.Streams <> HereAndFurther constr
|
|
105
|
R1372:1383 StreamsLib <> ForAll_apply def
|
|
106
|
R1386:1387 Coq.Lists.Streams <> tl def
|
|
107
|
R1389:1389 StreamsLib <> s var
|
|
108
|
R1358:1358 StreamsLib <> s var
|
|
109
|
def 1432:1444 <> necessitation
|
|
110
|
R1455:1460 Coq.Lists.Streams <> Stream coind
|
|
111
|
R1462:1462 StreamsLib <> A var
|
|
112
|
R1488:1488 StreamsLib <> P var
|
|
113
|
R1490:1490 StreamsLib <> s var
|
|
114
|
R1497:1502 Coq.Lists.Streams <> ForAll coind
|
|
115
|
R1506:1506 StreamsLib <> s var
|
|
116
|
R1504:1504 StreamsLib <> P var
|
|
117
|
R1512:1525 Coq.Lists.Streams <> HereAndFurther constr
|
|
118
|
R1536:1548 StreamsLib <> necessitation def
|
|
119
|
R1553:1554 Coq.Lists.Streams <> tl def
|
|
120
|
R1556:1556 StreamsLib <> s var
|
|
121
|
R1550:1550 StreamsLib <> I var
|
|
122
|
R1530:1530 StreamsLib <> I var
|
|
123
|
R1532:1532 StreamsLib <> s var
|
|
124
|
R1527:1527 StreamsLib <> s var
|
|
125
|
def 1573:1588 <> ForAll_reinforce
|
|
126
|
R1602:1607 Coq.Lists.Streams <> Stream coind
|
|
127
|
R1609:1609 StreamsLib <> A var
|
|
128
|
R1670:1675 Coq.Lists.Streams <> ForAll coind
|
|
129
|
R1679:1679 StreamsLib <> s var
|
|
130
|
R1677:1677 StreamsLib <> Q var
|
|
131
|
R1634:1639 Coq.Lists.Streams <> ForAll coind
|
|
132
|
R1663:1663 StreamsLib <> s var
|
|
133
|
R1654:1657 Coq.Init.Logic <> :type_scope:x_'/\'_x not
|
|
134
|
R1651:1651 StreamsLib <> P var
|
|
135
|
R1653:1653 StreamsLib <> s var
|
|
136
|
R1658:1658 StreamsLib <> Q var
|
|
137
|
R1660:1660 StreamsLib <> s var
|
|
138
|
R1705:1716 StreamsLib <> ForAll_apply def
|
|
139
|
R1705:1716 StreamsLib <> ForAll_apply def
|
|
140
|
R1737:1749 StreamsLib <> necessitation def
|
|
141
|
R1737:1749 StreamsLib <> necessitation def
|
|
142
|
R0:-1 StreamsLib <> y var
|
|
143
|
R0:-1 StreamsLib <> y var
|
|
144
|
def 1785:1790 <> concat
|
|
145
|
R1806:1809 Coq.Init.Datatypes <> list ind
|
|
146
|
R1811:1811 StreamsLib <> A var
|
|
147
|
R1824:1829 Coq.Lists.Streams <> Stream coind
|
|
148
|
R1831:1831 StreamsLib <> A var
|
|
149
|
R1836:1841 Coq.Lists.Streams <> Stream coind
|
|
150
|
R1843:1843 StreamsLib <> A var
|
|
151
|
R1849:1862 Coq.Lists.List <> fold_left def
|
|
152
|
R1893:1898 StreamsLib <> suffix var
|
|
153
|
R1886:1891 StreamsLib <> prefix var
|
|
154
|
R1876:1879 Coq.Lists.Streams <> Cons constr
|
|
155
|
R1883:1883 StreamsLib <> q var
|
|
156
|
R1881:1881 StreamsLib <> t var
|
|
157
|
prf 1910:1920 <> eqst_concat
|
|
158
|
R1951:1956 Coq.Lists.Streams <> Stream coind
|
|
159
|
R1958:1958 StreamsLib <> A var
|
|
160
|
R1979:1982 Coq.Lists.Streams <> EqSt coind
|
|
161
|
R2002:2007 StreamsLib <> concat def
|
|
162
|
R2013:2016 StreamsLib <> sfx' var
|
|
163
|
R2009:2011 StreamsLib <> pfx var
|
|
164
|
R1985:1990 StreamsLib <> concat def
|
|
165
|
R1996:1998 StreamsLib <> sfx var
|
|
166
|
R1992:1994 StreamsLib <> pfx var
|
|
167
|
R1962:1965 Coq.Lists.Streams <> EqSt coind
|
|
168
|
R1971:1974 StreamsLib <> sfx' var
|
|
169
|
R1967:1969 StreamsLib <> sfx var
|
|
170
|
R2088:2091 Coq.Lists.Streams <> eqst constr
|
|
171
|
R2088:2091 Coq.Lists.Streams <> eqst constr
|
|
172
|
prf 2135:2145 <> concat_eqst
|
|
173
|
R2181:2186 Coq.Lists.Streams <> Stream coind
|
|
174
|
R2188:2188 StreamsLib <> A var
|
|
175
|
R2284:2287 Coq.Init.Logic <> :type_scope:x_'/\'_x not
|
|
176
|
R2277:2279 Coq.Init.Logic <> :type_scope:x_'='_x not
|
|
177
|
R2274:2276 StreamsLib <> pfx var
|
|
178
|
R2280:2283 StreamsLib <> pfx' var
|
|
179
|
R2288:2291 Coq.Lists.Streams <> EqSt coind
|
|
180
|
R2297:2300 StreamsLib <> sfx' var
|
|
181
|
R2293:2295 StreamsLib <> sfx var
|
|
182
|
R2230:2233 Coq.Lists.Streams <> EqSt coind
|
|
183
|
R2253:2258 StreamsLib <> concat def
|
|
184
|
R2265:2268 StreamsLib <> sfx' var
|
|
185
|
R2260:2263 StreamsLib <> pfx' var
|
|
186
|
R2236:2241 StreamsLib <> concat def
|
|
187
|
R2247:2249 StreamsLib <> sfx var
|
|
188
|
R2243:2245 StreamsLib <> pfx var
|
|
189
|
R2207:2209 Coq.Init.Logic <> :type_scope:x_'='_x not
|
|
190
|
R2192:2202 Coq.Lists.List <> length syndef
|
|
191
|
R2204:2206 StreamsLib <> pfx var
|
|
192
|
R2210:2220 Coq.Lists.List <> length syndef
|
|
193
|
R2222:2225 StreamsLib <> pfx' var
|
|
194
|
R0:-1 StreamsLib <> y var
|
|
195
|
R0:-1 StreamsLib <> y var
|
|
196
|
R0:-1 StreamsLib <> y var
|
|
197
|
R0:-1 StreamsLib <> y var
|
|
198
|
prf 2588:2593 <> evt_id
|
|
199
|
R2613:2618 Coq.Lists.Streams <> Stream coind
|
|
200
|
R2620:2620 StreamsLib <> A var
|
|
201
|
R2624:2629 Coq.Lists.Streams <> Exists ind
|
|
202
|
R2650:2650 StreamsLib <> s var
|
|
203
|
R2643:2645 Coq.Init.Logic <> :type_scope:x_'='_x not
|
|
204
|
R2642:2642 StreamsLib <> s var
|
|
205
|
R2646:2647 StreamsLib <> s' var
|
|
206
|
R2674:2677 Coq.Lists.Streams <> Here constr
|
|
207
|
R2674:2677 Coq.Lists.Streams <> Here constr
|
|
208
|
prf 2707:2716 <> evt_concat
|
|
209
|
R2736:2741 Coq.Lists.Streams <> Stream coind
|
|
210
|
R2743:2743 StreamsLib <> A var
|
|
211
|
R2761:2766 Coq.Lists.Streams <> Stream coind
|
|
212
|
R2768:2768 StreamsLib <> A var
|
|
213
|
R2786:2791 Coq.Lists.Streams <> Exists ind
|
|
214
|
R2796:2801 StreamsLib <> concat def
|
|
215
|
R2805:2805 StreamsLib <> s var
|
|
216
|
R2803:2803 StreamsLib <> p var
|
|
217
|
R2793:2793 StreamsLib <> P var
|
|
218
|
R2772:2777 Coq.Lists.Streams <> Exists ind
|
|
219
|
R2781:2781 StreamsLib <> s var
|
|
220
|
R2779:2779 StreamsLib <> P var
|
|
221
|
R2866:2869 Coq.Lists.Streams <> Cons constr
|
|
222
|
R2866:2869 Coq.Lists.Streams <> Cons constr
|
|
223
|
R2885:2891 Coq.Lists.Streams <> Further constr
|
|
224
|
R2885:2891 Coq.Lists.Streams <> Further constr
|
|
225
|
prf 2918:2927 <> inv_concat
|
|
226
|
R2947:2952 Coq.Lists.Streams <> Stream coind
|
|
227
|
R2954:2954 StreamsLib <> A var
|
|
228
|
R2972:2977 Coq.Lists.Streams <> Stream coind
|
|
229
|
R2979:2979 StreamsLib <> A var
|
|
230
|
R3008:3013 Coq.Lists.Streams <> ForAll coind
|
|
231
|
R3017:3017 StreamsLib <> s var
|
|
232
|
R3015:3015 StreamsLib <> P var
|
|
233
|
R2983:2988 Coq.Lists.Streams <> ForAll coind
|
|
234
|
R2993:2998 StreamsLib <> concat def
|
|
235
|
R3002:3002 StreamsLib <> s var
|
|
236
|
R3000:3000 StreamsLib <> p var
|
|
237
|
R2990:2990 StreamsLib <> P var
|
|
238
|
R3090:3093 Coq.Lists.Streams <> Cons constr
|
|
239
|
R3090:3093 Coq.Lists.Streams <> Cons constr
|
|
240
|
def 3160:3163 <> lift
|
|
241
|
R3174:3174 StreamsLib <> A var
|
|
242
|
R3180:3183 Coq.Lists.Streams <> Cons constr
|
|
243
|
R3188:3191 StreamsLib <> lift def
|
|
244
|
R3193:3193 StreamsLib <> v var
|
|
245
|
R3185:3185 StreamsLib <> v var
|
|
246
|
prf 3204:3210 <> hd_lift
|
|
247
|
R3230:3230 StreamsLib <> A var
|
|
248
|
R3245:3247 Coq.Init.Logic <> :type_scope:x_'='_x not
|
|
249
|
R3234:3235 Coq.Lists.Streams <> hd def
|
|
250
|
R3238:3241 StreamsLib <> lift def
|
|
251
|
R3243:3243 StreamsLib <> v var
|
|
252
|
R3248:3248 StreamsLib <> v var
|
|
253
|
prf 3283:3289 <> tl_lift
|
|
254
|
R3309:3309 StreamsLib <> A var
|
|
255
|
R3324:3326 Coq.Init.Logic <> :type_scope:x_'='_x not
|
|
256
|
R3313:3314 Coq.Lists.Streams <> tl def
|
|
257
|
R3317:3320 StreamsLib <> lift def
|
|
258
|
R3322:3322 StreamsLib <> v var
|
|
259
|
R3327:3330 StreamsLib <> lift def
|
|
260
|
R3332:3332 StreamsLib <> v var
|
|
261
|
def 3372:3376 <> apply
|
|
262
|
R3387:3392 StreamsLib <> applyT def
|
|
263
|
R3403:3403 StreamsLib <> B var
|
|
264
|
R3401:3401 StreamsLib <> A var
|
|
265
|
R3394:3399 Coq.Lists.Streams <> Stream coind
|
|
266
|
R3430:3430 StreamsLib <> a var
|
|
267
|
R3427:3427 StreamsLib <> f var
|
|
268
|
R3441:3444 Coq.Lists.Streams <> Cons constr
|
|
269
|
R3455:3458 Coq.Lists.Streams <> Cons constr
|
|
270
|
R3470:3473 Coq.Lists.Streams <> Cons constr
|
|
271
|
R3484:3488 StreamsLib <> apply def
|
|
272
|
prf 3510:3517 <> hd_apply
|
|
273
|
R3539:3544 Coq.Lists.Streams <> Stream coind
|
|
274
|
R3552:3552 StreamsLib <> B var
|
|
275
|
R3547:3547 StreamsLib <> A var
|
|
276
|
R3561:3566 Coq.Lists.Streams <> Stream coind
|
|
277
|
R3568:3568 StreamsLib <> A var
|
|
278
|
R3586:3588 Coq.Init.Logic <> :type_scope:x_'='_x not
|
|
279
|
R3572:3573 Coq.Lists.Streams <> hd def
|
|
280
|
R3576:3580 StreamsLib <> apply def
|
|
281
|
R3584:3584 StreamsLib <> a var
|
|
282
|
R3582:3582 StreamsLib <> f var
|
|
283
|
R3590:3591 Coq.Lists.Streams <> hd def
|
|
284
|
R3593:3593 StreamsLib <> f var
|
|
285
|
R3597:3598 Coq.Lists.Streams <> hd def
|
|
286
|
R3600:3600 StreamsLib <> a var
|
|
287
|
prf 3660:3667 <> tl_apply
|
|
288
|
R3689:3694 Coq.Lists.Streams <> Stream coind
|
|
289
|
R3702:3702 StreamsLib <> B var
|
|
290
|
R3697:3697 StreamsLib <> A var
|
|
291
|
R3711:3716 Coq.Lists.Streams <> Stream coind
|
|
292
|
R3718:3718 StreamsLib <> A var
|
|
293
|
R3736:3738 Coq.Init.Logic <> :type_scope:x_'='_x not
|
|
294
|
R3722:3723 Coq.Lists.Streams <> tl def
|
|
295
|
R3726:3730 StreamsLib <> apply def
|
|
296
|
R3734:3734 StreamsLib <> a var
|
|
297
|
R3732:3732 StreamsLib <> f var
|
|
298
|
R3739:3743 StreamsLib <> apply def
|
|
299
|
R3753:3754 Coq.Lists.Streams <> tl def
|
|
300
|
R3756:3756 StreamsLib <> a var
|
|
301
|
R3746:3747 Coq.Lists.Streams <> tl def
|
|
302
|
R3749:3749 StreamsLib <> f var
|
|
303
|
prf 3816:3825 <> cons_apply
|
|
304
|
R3853:3853 StreamsLib <> B var
|
|
305
|
R3848:3848 StreamsLib <> A var
|
|
306
|
R3862:3867 Coq.Lists.Streams <> Stream coind
|
|
307
|
R3875:3875 StreamsLib <> B var
|
|
308
|
R3870:3870 StreamsLib <> A var
|
|
309
|
R3885:3885 StreamsLib <> A var
|
|
310
|
R3894:3899 Coq.Lists.Streams <> Stream coind
|
|
311
|
R3901:3901 StreamsLib <> A var
|
|
312
|
R3905:3908 Coq.Lists.Streams <> EqSt coind
|
|
313
|
R3945:3948 Coq.Lists.Streams <> Cons constr
|
|
314
|
R3959:3963 StreamsLib <> apply def
|
|
315
|
R3968:3969 StreamsLib <> a' var
|
|
316
|
R3965:3966 StreamsLib <> f' var
|
|
317
|
R3951:3952 StreamsLib <> f0 var
|
|
318
|
R3954:3955 StreamsLib <> a0 var
|
|
319
|
R3911:3915 StreamsLib <> apply def
|
|
320
|
R3931:3934 Coq.Lists.Streams <> Cons constr
|
|
321
|
R3939:3940 StreamsLib <> a' var
|
|
322
|
R3936:3937 StreamsLib <> a0 var
|
|
323
|
R3918:3921 Coq.Lists.Streams <> Cons constr
|
|
324
|
R3926:3927 StreamsLib <> f' var
|
|
325
|
R3923:3924 StreamsLib <> f0 var
|
|
326
|
R3995:3998 Coq.Lists.Streams <> eqst constr
|
|
327
|
R3995:3998 Coq.Lists.Streams <> eqst constr
|
|
328
|
R4023:4033 Coq.Lists.Streams <> EqSt_reflex thm
|
|
329
|
R4023:4033 Coq.Lists.Streams <> EqSt_reflex thm
|
|
330
|
prf 4048:4057 <> eqst_apply
|
|
331
|
R4082:4087 Coq.Lists.Streams <> Stream coind
|
|
332
|
R4095:4095 StreamsLib <> B var
|
|
333
|
R4090:4090 StreamsLib <> A var
|
|
334
|
R4107:4112 Coq.Lists.Streams <> Stream coind
|
|
335
|
R4114:4114 StreamsLib <> A var
|
|
336
|
R4146:4149 Coq.Lists.Streams <> EqSt coind
|
|
337
|
R4164:4168 StreamsLib <> apply def
|
|
338
|
R4173:4174 StreamsLib <> a' var
|
|
339
|
R4170:4171 StreamsLib <> f' var
|
|
340
|
R4152:4156 StreamsLib <> apply def
|
|
341
|
R4160:4160 StreamsLib <> a var
|
|
342
|
R4158:4158 StreamsLib <> f var
|
|
343
|
R4133:4136 Coq.Lists.Streams <> EqSt coind
|
|
344
|
R4140:4141 StreamsLib <> a' var
|
|
345
|
R4138:4138 StreamsLib <> a var
|
|
346
|
R4120:4123 Coq.Lists.Streams <> EqSt coind
|
|
347
|
R4127:4128 StreamsLib <> f' var
|
|
348
|
R4125:4125 StreamsLib <> f var
|
|
349
|
R4251:4254 Coq.Lists.Streams <> eqst constr
|
|
350
|
R4251:4254 Coq.Lists.Streams <> eqst constr
|
|
351
|
R4266:4273 StreamsLib <> hd_apply thm
|
|
352
|
R4266:4273 StreamsLib <> hd_apply thm
|
|
353
|
R4285:4292 StreamsLib <> hd_apply thm
|
|
354
|
R4285:4292 StreamsLib <> hd_apply thm
|
|
355
|
R4318:4325 StreamsLib <> tl_apply thm
|
|
356
|
R4318:4325 StreamsLib <> tl_apply thm
|
|
357
|
R4337:4344 StreamsLib <> tl_apply thm
|
|
358
|
R4337:4344 StreamsLib <> tl_apply thm
|
|
359
|
prf 4404:4410 <> inv_map
|
|
360
|
R4437:4437 StreamsLib <> B var
|
|
361
|
R4432:4432 StreamsLib <> A var
|
|
362
|
R4447:4452 Coq.Lists.Streams <> Stream coind
|
|
363
|
R4454:4454 StreamsLib <> A var
|
|
364
|
R4489:4494 Coq.Lists.Streams <> ForAll coind
|
|
365
|
R4530:4530 StreamsLib <> s var
|
|
366
|
R4507:4507 StreamsLib <> P var
|
|
367
|
R4510:4514 StreamsLib <> apply def
|
|
368
|
R4525:4526 StreamsLib <> s' var
|
|
369
|
R4517:4520 StreamsLib <> lift def
|
|
370
|
R4522:4522 StreamsLib <> f var
|
|
371
|
R4458:4463 Coq.Lists.Streams <> ForAll coind
|
|
372
|
R4468:4472 StreamsLib <> apply def
|
|
373
|
R4483:4483 StreamsLib <> s var
|
|
374
|
R4475:4478 StreamsLib <> lift def
|
|
375
|
R4480:4480 StreamsLib <> f var
|
|
376
|
R4465:4465 StreamsLib <> P var
|
|
377
|
R4621:4634 Coq.Lists.Streams <> HereAndFurther constr
|
|
378
|
R4621:4634 Coq.Lists.Streams <> HereAndFurther constr
|
|
379
|
prf 4700:4706 <> map_inv
|
|
380
|
R4733:4733 StreamsLib <> B var
|
|
381
|
R4728:4728 StreamsLib <> A var
|
|
382
|
R4743:4748 Coq.Lists.Streams <> Stream coind
|
|
383
|
R4750:4750 StreamsLib <> A var
|
|
384
|
R4800:4805 Coq.Lists.Streams <> ForAll coind
|
|
385
|
R4810:4814 StreamsLib <> apply def
|
|
386
|
R4825:4825 StreamsLib <> s var
|
|
387
|
R4817:4820 StreamsLib <> lift def
|
|
388
|
R4822:4822 StreamsLib <> f var
|
|
389
|
R4807:4807 StreamsLib <> P var
|
|
390
|
R4754:4759 Coq.Lists.Streams <> ForAll coind
|
|
391
|
R4795:4795 StreamsLib <> s var
|
|
392
|
R4772:4772 StreamsLib <> P var
|
|
393
|
R4775:4779 StreamsLib <> apply def
|
|
394
|
R4790:4791 StreamsLib <> s' var
|
|
395
|
R4782:4785 StreamsLib <> lift def
|
|
396
|
R4787:4787 StreamsLib <> f var
|
|
397
|
R4917:4930 Coq.Lists.Streams <> HereAndFurther constr
|
|
398
|
R4917:4930 Coq.Lists.Streams <> HereAndFurther constr
|
|
399
|
prf 4996:5002 <> evt_map
|
|
400
|
R5029:5029 StreamsLib <> B var
|
|
401
|
R5024:5024 StreamsLib <> A var
|
|
402
|
R5039:5044 Coq.Lists.Streams <> Stream coind
|
|
403
|
R5046:5046 StreamsLib <> A var
|
|
404
|
R5081:5086 Coq.Lists.Streams <> Exists ind
|
|
405
|
R5122:5122 StreamsLib <> s var
|
|
406
|
R5099:5099 StreamsLib <> P var
|
|
407
|
R5102:5106 StreamsLib <> apply def
|
|
408
|
R5117:5118 StreamsLib <> s' var
|
|
409
|
R5109:5112 StreamsLib <> lift def
|
|
410
|
R5114:5114 StreamsLib <> f var
|
|
411
|
R5050:5055 Coq.Lists.Streams <> Exists ind
|
|
412
|
R5060:5064 StreamsLib <> apply def
|
|
413
|
R5075:5075 StreamsLib <> s var
|
|
414
|
R5067:5070 StreamsLib <> lift def
|
|
415
|
R5072:5072 StreamsLib <> f var
|
|
416
|
R5057:5057 StreamsLib <> P var
|
|
417
|
R5160:5164 StreamsLib <> apply def
|
|
418
|
R5167:5170 StreamsLib <> lift def
|
|
419
|
R5160:5164 StreamsLib <> apply def
|
|
420
|
R5167:5170 StreamsLib <> lift def
|
|
421
|
R5239:5242 Coq.Lists.Streams <> Here constr
|
|
422
|
R5239:5242 Coq.Lists.Streams <> Here constr
|
|
423
|
R5291:5297 Coq.Lists.Streams <> Further constr
|
|
424
|
R5291:5297 Coq.Lists.Streams <> Further constr
|
|
425
|
R5318:5319 Coq.Lists.Streams <> tl def
|
|
426
|
R5318:5319 Coq.Lists.Streams <> tl def
|
|
427
|
R5338:5344 StreamsLib <> tl_lift thm
|
|
428
|
R5338:5344 StreamsLib <> tl_lift thm
|
|
429
|
R5359:5366 StreamsLib <> tl_apply thm
|
|
430
|
R5359:5366 StreamsLib <> tl_apply thm
|
|
431
|
R5376:5382 Coq.Init.Logic <> f_equal thm
|
|
432
|
R5376:5382 Coq.Init.Logic <> f_equal thm
|
|
433
|
prf 5413:5419 <> map_evt
|
|
434
|
R5446:5446 StreamsLib <> B var
|
|
435
|
R5441:5441 StreamsLib <> A var
|
|
436
|
R5456:5461 Coq.Lists.Streams <> Stream coind
|
|
437
|
R5463:5463 StreamsLib <> A var
|
|
438
|
R5513:5518 Coq.Lists.Streams <> Exists ind
|
|
439
|
R5523:5527 StreamsLib <> apply def
|
|
440
|
R5538:5538 StreamsLib <> s var
|
|
441
|
R5530:5533 StreamsLib <> lift def
|
|
442
|
R5535:5535 StreamsLib <> f var
|
|
443
|
R5520:5520 StreamsLib <> P var
|
|
444
|
R5467:5472 Coq.Lists.Streams <> Exists ind
|
|
445
|
R5508:5508 StreamsLib <> s var
|
|
446
|
R5485:5485 StreamsLib <> P var
|
|
447
|
R5488:5492 StreamsLib <> apply def
|
|
448
|
R5503:5504 StreamsLib <> s' var
|
|
449
|
R5495:5498 StreamsLib <> lift def
|
|
450
|
R5500:5500 StreamsLib <> f var
|
|
451
|
R5596:5599 Coq.Lists.Streams <> Here constr
|
|
452
|
R5596:5599 Coq.Lists.Streams <> Here constr
|
|
453
|
R5620:5626 Coq.Lists.Streams <> Further constr
|
|
454
|
R5620:5626 Coq.Lists.Streams <> Further constr
|
|
455
|
R5638:5645 StreamsLib <> tl_apply thm
|
|
456
|
R5638:5645 StreamsLib <> tl_apply thm
|
|
457
|
R5657:5663 StreamsLib <> tl_lift thm
|
|
458
|
R5657:5663 StreamsLib <> tl_lift thm
|
|
459
|
def 5700:5702 <> zip
|
|
460
|
R5723:5725 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
|
|
461
|
R5715:5720 Coq.Lists.Streams <> Stream coind
|
|
462
|
R5722:5722 StreamsLib <> A var
|
|
463
|
R5726:5731 Coq.Lists.Streams <> Stream coind
|
|
464
|
R5733:5733 StreamsLib <> B var
|
|
465
|
R5739:5743 StreamsLib <> apply def
|
|
466
|
R5789:5791 Coq.Init.Datatypes <> snd def
|
|
467
|
R5793:5793 StreamsLib <> s var
|
|
468
|
R5746:5750 StreamsLib <> apply def
|
|
469
|
R5780:5782 Coq.Init.Datatypes <> fst def
|
|
470
|
R5784:5784 StreamsLib <> s var
|
|
471
|
R5753:5756 StreamsLib <> lift def
|
|
472
|
R5770:5770 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
473
|
R5772:5773 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
474
|
R5775:5775 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
475
|
R5771:5771 StreamsLib <> a var
|
|
476
|
R5774:5774 StreamsLib <> b var
|
|
477
|
prf 5804:5815 <> zip_fst_eqst
|
|
478
|
R5850:5855 Coq.Lists.Streams <> Stream coind
|
|
479
|
R5857:5857 StreamsLib <> A var
|
|
480
|
R5870:5875 Coq.Lists.Streams <> Stream coind
|
|
481
|
R5877:5877 StreamsLib <> B var
|
|
482
|
R5923:5926 Coq.Lists.Streams <> EqSt coind
|
|
483
|
R5931:5933 StreamsLib <> s1' var
|
|
484
|
R5928:5929 StreamsLib <> s1 var
|
|
485
|
R5883:5886 Coq.Lists.Streams <> EqSt coind
|
|
486
|
R5904:5906 StreamsLib <> zip def
|
|
487
|
R5908:5908 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
488
|
R5912:5913 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
489
|
R5917:5917 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
490
|
R5909:5911 StreamsLib <> s1' var
|
|
491
|
R5914:5916 StreamsLib <> s2' var
|
|
492
|
R5889:5891 StreamsLib <> zip def
|
|
493
|
R5893:5893 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
494
|
R5896:5897 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
495
|
R5900:5900 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
496
|
R5894:5895 StreamsLib <> s1 var
|
|
497
|
R5898:5899 StreamsLib <> s2 var
|
|
498
|
R6048:6051 Coq.Lists.Streams <> eqst constr
|
|
499
|
R6048:6051 Coq.Lists.Streams <> eqst constr
|
|
500
|
prf 6167:6173 <> zip_fst
|
|
501
|
R6208:6213 Coq.Lists.Streams <> Stream coind
|
|
502
|
R6215:6215 StreamsLib <> A var
|
|
503
|
R6228:6233 Coq.Lists.Streams <> Stream coind
|
|
504
|
R6235:6235 StreamsLib <> B var
|
|
505
|
R6276:6278 Coq.Init.Logic <> :type_scope:x_'='_x not
|
|
506
|
R6274:6275 StreamsLib <> s1 var
|
|
507
|
R6279:6281 StreamsLib <> s1' var
|
|
508
|
R6253:6255 Coq.Init.Logic <> :type_scope:x_'='_x not
|
|
509
|
R6241:6243 StreamsLib <> zip def
|
|
510
|
R6245:6245 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
511
|
R6248:6249 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
512
|
R6252:6252 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
513
|
R6246:6247 StreamsLib <> s1 var
|
|
514
|
R6250:6251 StreamsLib <> s2 var
|
|
515
|
R6256:6258 StreamsLib <> zip def
|
|
516
|
R6260:6260 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
517
|
R6264:6265 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
518
|
R6269:6269 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
519
|
R6261:6263 StreamsLib <> s1' var
|
|
520
|
R6266:6268 StreamsLib <> s2' var
|
|
521
|
R6305:6311 StreamsLib <> eqst_eq prfax
|
|
522
|
R6305:6311 StreamsLib <> eqst_eq prfax
|
|
523
|
R6321:6332 StreamsLib <> zip_fst_eqst thm
|
|
524
|
R6321:6332 StreamsLib <> zip_fst_eqst thm
|
|
525
|
R6367:6377 Coq.Lists.Streams <> EqSt_reflex thm
|
|
526
|
R6367:6377 Coq.Lists.Streams <> EqSt_reflex thm
|
|
527
|
prf 6392:6403 <> zip_snd_eqst
|
|
528
|
R6438:6443 Coq.Lists.Streams <> Stream coind
|
|
529
|
R6445:6445 StreamsLib <> A var
|
|
530
|
R6458:6463 Coq.Lists.Streams <> Stream coind
|
|
531
|
R6465:6465 StreamsLib <> B var
|
|
532
|
R6511:6514 Coq.Lists.Streams <> EqSt coind
|
|
533
|
R6519:6521 StreamsLib <> s2' var
|
|
534
|
R6516:6517 StreamsLib <> s2 var
|
|
535
|
R6471:6474 Coq.Lists.Streams <> EqSt coind
|
|
536
|
R6492:6494 StreamsLib <> zip def
|
|
537
|
R6496:6496 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
538
|
R6500:6501 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
539
|
R6505:6505 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
540
|
R6497:6499 StreamsLib <> s1' var
|
|
541
|
R6502:6504 StreamsLib <> s2' var
|
|
542
|
R6477:6479 StreamsLib <> zip def
|
|
543
|
R6481:6481 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
544
|
R6484:6485 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
545
|
R6488:6488 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
546
|
R6482:6483 StreamsLib <> s1 var
|
|
547
|
R6486:6487 StreamsLib <> s2 var
|
|
548
|
R6636:6639 Coq.Lists.Streams <> eqst constr
|
|
549
|
R6636:6639 Coq.Lists.Streams <> eqst constr
|
|
550
|
prf 6755:6761 <> zip_snd
|
|
551
|
R6796:6801 Coq.Lists.Streams <> Stream coind
|
|
552
|
R6803:6803 StreamsLib <> A var
|
|
553
|
R6816:6821 Coq.Lists.Streams <> Stream coind
|
|
554
|
R6823:6823 StreamsLib <> B var
|
|
555
|
R6864:6866 Coq.Init.Logic <> :type_scope:x_'='_x not
|
|
556
|
R6862:6863 StreamsLib <> s2 var
|
|
557
|
R6867:6869 StreamsLib <> s2' var
|
|
558
|
R6841:6843 Coq.Init.Logic <> :type_scope:x_'='_x not
|
|
559
|
R6829:6831 StreamsLib <> zip def
|
|
560
|
R6833:6833 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
561
|
R6836:6837 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
562
|
R6840:6840 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
563
|
R6834:6835 StreamsLib <> s1 var
|
|
564
|
R6838:6839 StreamsLib <> s2 var
|
|
565
|
R6844:6846 StreamsLib <> zip def
|
|
566
|
R6848:6848 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
567
|
R6852:6853 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
568
|
R6857:6857 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
569
|
R6849:6851 StreamsLib <> s1' var
|
|
570
|
R6854:6856 StreamsLib <> s2' var
|
|
571
|
R6893:6899 StreamsLib <> eqst_eq prfax
|
|
572
|
R6893:6899 StreamsLib <> eqst_eq prfax
|
|
573
|
R6909:6920 StreamsLib <> zip_snd_eqst thm
|
|
574
|
R6909:6920 StreamsLib <> zip_snd_eqst thm
|
|
575
|
R6955:6965 Coq.Lists.Streams <> EqSt_reflex thm
|
|
576
|
R6955:6965 Coq.Lists.Streams <> EqSt_reflex thm
|
|
577
|
def 6985:6989 <> unzip
|
|
578
|
R7002:7007 Coq.Lists.Streams <> Stream coind
|
|
579
|
R7011:7011 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
|
|
580
|
R7010:7010 StreamsLib <> A var
|
|
581
|
R7012:7012 StreamsLib <> B var
|
|
582
|
R7019:7019 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
583
|
R7045:7046 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
584
|
R7072:7072 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
585
|
R7020:7024 StreamsLib <> apply def
|
|
586
|
R7044:7044 StreamsLib <> s var
|
|
587
|
R7027:7030 StreamsLib <> lift def
|
|
588
|
R7034:7036 Coq.Init.Datatypes <> fst def
|
|
589
|
R7047:7051 StreamsLib <> apply def
|
|
590
|
R7071:7071 StreamsLib <> s var
|
|
591
|
R7054:7057 StreamsLib <> lift def
|
|
592
|
R7061:7063 Coq.Init.Datatypes <> snd def
|
|
593
|
prf 7082:7093 <> fst_zip_eqst
|
|
594
|
R7116:7121 Coq.Lists.Streams <> Stream coind
|
|
595
|
R7123:7123 StreamsLib <> A var
|
|
596
|
R7132:7137 Coq.Lists.Streams <> Stream coind
|
|
597
|
R7139:7139 StreamsLib <> B var
|
|
598
|
R7143:7146 Coq.Lists.Streams <> EqSt coind
|
|
599
|
R7189:7190 StreamsLib <> s1 var
|
|
600
|
R7149:7153 StreamsLib <> apply def
|
|
601
|
R7174:7176 StreamsLib <> zip def
|
|
602
|
R7178:7178 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
603
|
R7181:7182 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
604
|
R7185:7185 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
605
|
R7179:7180 StreamsLib <> s1 var
|
|
606
|
R7183:7184 StreamsLib <> s2 var
|
|
607
|
R7156:7159 StreamsLib <> lift def
|
|
608
|
R7163:7165 Coq.Init.Datatypes <> fst def
|
|
609
|
R7257:7260 Coq.Lists.Streams <> eqst constr
|
|
610
|
R7257:7260 Coq.Lists.Streams <> eqst constr
|
|
611
|
prf 7304:7310 <> fst_zip
|
|
612
|
R7333:7338 Coq.Lists.Streams <> Stream coind
|
|
613
|
R7340:7340 StreamsLib <> A var
|
|
614
|
R7349:7354 Coq.Lists.Streams <> Stream coind
|
|
615
|
R7356:7356 StreamsLib <> B var
|
|
616
|
R7398:7400 Coq.Init.Logic <> :type_scope:x_'='_x not
|
|
617
|
R7360:7364 StreamsLib <> apply def
|
|
618
|
R7385:7387 StreamsLib <> zip def
|
|
619
|
R7389:7389 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
620
|
R7392:7393 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
621
|
R7396:7396 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
622
|
R7390:7391 StreamsLib <> s1 var
|
|
623
|
R7394:7395 StreamsLib <> s2 var
|
|
624
|
R7367:7370 StreamsLib <> lift def
|
|
625
|
R7374:7376 Coq.Init.Datatypes <> fst def
|
|
626
|
R7401:7402 StreamsLib <> s1 var
|
|
627
|
R7426:7432 StreamsLib <> eqst_eq prfax
|
|
628
|
R7426:7432 StreamsLib <> eqst_eq prfax
|
|
629
|
R7441:7452 StreamsLib <> fst_zip_eqst thm
|
|
630
|
R7441:7452 StreamsLib <> fst_zip_eqst thm
|
|
631
|
prf 7467:7478 <> snd_zip_eqst
|
|
632
|
R7501:7506 Coq.Lists.Streams <> Stream coind
|
|
633
|
R7508:7508 StreamsLib <> A var
|
|
634
|
R7517:7522 Coq.Lists.Streams <> Stream coind
|
|
635
|
R7524:7524 StreamsLib <> B var
|
|
636
|
R7528:7531 Coq.Lists.Streams <> EqSt coind
|
|
637
|
R7574:7575 StreamsLib <> s2 var
|
|
638
|
R7534:7538 StreamsLib <> apply def
|
|
639
|
R7559:7561 StreamsLib <> zip def
|
|
640
|
R7563:7563 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
641
|
R7566:7567 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
642
|
R7570:7570 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
643
|
R7564:7565 StreamsLib <> s1 var
|
|
644
|
R7568:7569 StreamsLib <> s2 var
|
|
645
|
R7541:7544 StreamsLib <> lift def
|
|
646
|
R7548:7550 Coq.Init.Datatypes <> snd def
|
|
647
|
R7642:7645 Coq.Lists.Streams <> eqst constr
|
|
648
|
R7642:7645 Coq.Lists.Streams <> eqst constr
|
|
649
|
prf 7689:7695 <> snd_zip
|
|
650
|
R7718:7723 Coq.Lists.Streams <> Stream coind
|
|
651
|
R7725:7725 StreamsLib <> A var
|
|
652
|
R7734:7739 Coq.Lists.Streams <> Stream coind
|
|
653
|
R7741:7741 StreamsLib <> B var
|
|
654
|
R7783:7785 Coq.Init.Logic <> :type_scope:x_'='_x not
|
|
655
|
R7745:7749 StreamsLib <> apply def
|
|
656
|
R7770:7772 StreamsLib <> zip def
|
|
657
|
R7774:7774 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
658
|
R7777:7778 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
659
|
R7781:7781 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
660
|
R7775:7776 StreamsLib <> s1 var
|
|
661
|
R7779:7780 StreamsLib <> s2 var
|
|
662
|
R7752:7755 StreamsLib <> lift def
|
|
663
|
R7759:7761 Coq.Init.Datatypes <> snd def
|
|
664
|
R7786:7787 StreamsLib <> s2 var
|
|
665
|
R7811:7817 StreamsLib <> eqst_eq prfax
|
|
666
|
R7811:7817 StreamsLib <> eqst_eq prfax
|
|
667
|
R7826:7837 StreamsLib <> snd_zip_eqst thm
|
|
668
|
R7826:7837 StreamsLib <> snd_zip_eqst thm
|
|
669
|
prf 7852:7865 <> zip_unzip_eqst
|
|
670
|
R7887:7892 Coq.Lists.Streams <> Stream coind
|
|
671
|
R7896:7896 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
|
|
672
|
R7895:7895 StreamsLib <> A var
|
|
673
|
R7897:7897 StreamsLib <> B var
|
|
674
|
R7902:7905 Coq.Lists.Streams <> EqSt coind
|
|
675
|
R7923:7923 StreamsLib <> s var
|
|
676
|
R7908:7910 StreamsLib <> zip def
|
|
677
|
R7913:7917 StreamsLib <> unzip def
|
|
678
|
R7919:7919 StreamsLib <> s var
|
|
679
|
R7976:7979 Coq.Lists.Streams <> eqst constr
|
|
680
|
R7976:7979 Coq.Lists.Streams <> eqst constr
|
|
681
|
prf 8052:8060 <> zip_unzip
|
|
682
|
R8082:8087 Coq.Lists.Streams <> Stream coind
|
|
683
|
R8091:8091 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
|
|
684
|
R8090:8090 StreamsLib <> A var
|
|
685
|
R8092:8092 StreamsLib <> B var
|
|
686
|
R8110:8112 Coq.Init.Logic <> :type_scope:x_'='_x not
|
|
687
|
R8097:8099 StreamsLib <> zip def
|
|
688
|
R8102:8106 StreamsLib <> unzip def
|
|
689
|
R8108:8108 StreamsLib <> s var
|
|
690
|
R8113:8113 StreamsLib <> s var
|
|
691
|
R8137:8143 StreamsLib <> eqst_eq prfax
|
|
692
|
R8137:8143 StreamsLib <> eqst_eq prfax
|
|
693
|
R8152:8165 StreamsLib <> zip_unzip_eqst thm
|
|
694
|
R8152:8165 StreamsLib <> zip_unzip_eqst thm
|
|
695
|
prf 8182:8192 <> inv_eq_eqst
|
|
696
|
R8215:8220 Coq.Lists.Streams <> Stream coind
|
|
697
|
R8222:8222 StreamsLib <> A var
|
|
698
|
R8292:8295 Coq.Lists.Streams <> EqSt coind
|
|
699
|
R8299:8300 StreamsLib <> s' var
|
|
700
|
R8297:8297 StreamsLib <> s var
|
|
701
|
R8227:8232 Coq.Lists.Streams <> ForAll coind
|
|
702
|
R8276:8278 StreamsLib <> zip def
|
|
703
|
R8280:8280 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
704
|
R8282:8283 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
705
|
R8286:8286 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
706
|
R8281:8281 StreamsLib <> s var
|
|
707
|
R8284:8285 StreamsLib <> s' var
|
|
708
|
R8258:8260 Coq.Init.Logic <> :type_scope:x_'='_x not
|
|
709
|
R8246:8248 Coq.Init.Datatypes <> fst def
|
|
710
|
R8251:8252 Coq.Lists.Streams <> hd def
|
|
711
|
R8254:8256 StreamsLib <> ss' var
|
|
712
|
R8261:8263 Coq.Init.Datatypes <> snd def
|
|
713
|
R8266:8267 Coq.Lists.Streams <> hd def
|
|
714
|
R8269:8271 StreamsLib <> ss' var
|
|
715
|
R8408:8411 Coq.Lists.Streams <> eqst constr
|
|
716
|
R8408:8411 Coq.Lists.Streams <> eqst constr
|
|
717
|
prf 8469:8479 <> eqst_inv_eq
|
|
718
|
R8502:8507 Coq.Lists.Streams <> Stream coind
|
|
719
|
R8509:8509 StreamsLib <> A var
|
|
720
|
R8528:8533 Coq.Lists.Streams <> ForAll coind
|
|
721
|
R8577:8579 StreamsLib <> zip def
|
|
722
|
R8581:8581 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
723
|
R8583:8584 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
724
|
R8587:8587 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
725
|
R8582:8582 StreamsLib <> s var
|
|
726
|
R8585:8586 StreamsLib <> s' var
|
|
727
|
R8559:8561 Coq.Init.Logic <> :type_scope:x_'='_x not
|
|
728
|
R8547:8549 Coq.Init.Datatypes <> fst def
|
|
729
|
R8552:8553 Coq.Lists.Streams <> hd def
|
|
730
|
R8555:8557 StreamsLib <> ss' var
|
|
731
|
R8562:8564 Coq.Init.Datatypes <> snd def
|
|
732
|
R8567:8568 Coq.Lists.Streams <> hd def
|
|
733
|
R8570:8572 StreamsLib <> ss' var
|
|
734
|
R8515:8518 Coq.Lists.Streams <> EqSt coind
|
|
735
|
R8522:8523 StreamsLib <> s' var
|
|
736
|
R8520:8520 StreamsLib <> s var
|
|
737
|
R8696:8709 Coq.Lists.Streams <> HereAndFurther constr
|
|
738
|
R8696:8709 Coq.Lists.Streams <> HereAndFurther constr
|
|
739
|
def 8771:8781 <> history_rec
|
|
740
|
R8795:8798 Coq.Init.Datatypes <> list ind
|
|
741
|
R8800:8800 StreamsLib <> A var
|
|
742
|
R8808:8813 Coq.Lists.Streams <> Stream coind
|
|
743
|
R8815:8815 StreamsLib <> A var
|
|
744
|
R8820:8825 Coq.Lists.Streams <> Stream coind
|
|
745
|
R8834:8836 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
|
|
746
|
R8828:8831 Coq.Init.Datatypes <> list ind
|
|
747
|
R8833:8833 StreamsLib <> A var
|
|
748
|
R8837:8837 StreamsLib <> A var
|
|
749
|
R8850:8850 StreamsLib <> s var
|
|
750
|
R8860:8863 Coq.Lists.Streams <> Cons constr
|
|
751
|
R8874:8877 Coq.Lists.Streams <> Cons constr
|
|
752
|
R8891:8901 StreamsLib <> history_rec def
|
|
753
|
R8904:8907 Coq.Init.Datatypes <> cons constr
|
|
754
|
R8912:8915 StreamsLib <> past var
|
|
755
|
R8879:8879 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
756
|
R8884:8885 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
757
|
R8888:8888 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
|
|
758
|
R8880:8883 StreamsLib <> past var
|
|
759
|
def 8940:8946 <> history
|
|
760
|
R8957:8962 Coq.Lists.Streams <> Stream coind
|
|
761
|
R8964:8964 StreamsLib <> A var
|
|
762
|
R8969:8974 Coq.Lists.Streams <> Stream coind
|
|
763
|
R8983:8985 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
|
|
764
|
R8977:8980 Coq.Init.Datatypes <> list ind
|
|
765
|
R8982:8982 StreamsLib <> A var
|
|
766
|
R8986:8986 StreamsLib <> A var
|
|
767
|
R8992:9002 StreamsLib <> history_rec def
|
|
768
|
R9008:9008 StreamsLib <> s var
|
|
769
|
R9004:9006 Coq.Init.Datatypes <> nil constr
|
|
770
|
prf 9021:9036 <> eqst_history_rec
|
|
771
|
R9058:9061 Coq.Init.Datatypes <> list ind
|
|
772
|
R9063:9063 StreamsLib <> A var
|
|
773
|
R9078:9083 Coq.Lists.Streams <> Stream coind
|
|
774
|
R9085:9085 StreamsLib <> A var
|
|
775
|
R9108:9111 Coq.Lists.Streams <> EqSt coind
|
|
776
|
R9136:9146 StreamsLib <> history_rec def
|
|
777
|
R9152:9155 StreamsLib <> sfx' var
|
|
778
|
R9148:9150 StreamsLib <> pfx var
|
|
779
|
R9114:9124 StreamsLib <> history_rec def
|
|
780
|
R9130:9132 StreamsLib <> sfx var
|
|
781
|
R9126:9128 StreamsLib <> pfx var
|
|
782
|
R9091:9094 Coq.Lists.Streams <> EqSt coind
|
|
783
|
R9100:9103 StreamsLib <> sfx' var
|
|
784
|
R9096:9098 StreamsLib <> sfx var
|
|
785
|
R9305:9308 Coq.Lists.Streams <> eqst constr
|
|
786
|
R9305:9308 Coq.Lists.Streams <> eqst constr
|
|
787
|
prf 9382:9393 <> eqst_history
|
|
788
|
R9420:9425 Coq.Lists.Streams <> Stream coind
|
|
789
|
R9427:9427 StreamsLib <> A var
|
|
790
|
R9450:9453 Coq.Lists.Streams <> EqSt coind
|
|
791
|
R9470:9476 StreamsLib <> history def
|
|
792
|
R9478:9481 StreamsLib <> sfx' var
|
|
793
|
R9456:9462 StreamsLib <> history def
|
|
794
|
R9464:9466 StreamsLib <> sfx var
|
|
795
|
R9433:9436 Coq.Lists.Streams <> EqSt coind
|
|
796
|
R9442:9445 StreamsLib <> sfx' var
|
|
797
|
R9438:9440 StreamsLib <> sfx var
|
|
798
|
R9506:9521 StreamsLib <> eqst_history_rec thm
|
|
799
|
R9506:9521 StreamsLib <> eqst_history_rec thm
|
|
800
|
prf 9550:9566 <> unzip_history_rec
|
|
801
|
R9588:9591 Coq.Init.Datatypes <> list ind
|
|
802
|
R9593:9593 StreamsLib <> A var
|
|
803
|
R9603:9608 Coq.Lists.Streams <> Stream coind
|
|
804
|
R9610:9610 StreamsLib <> A var
|
|
805
|
R9614:9617 Coq.Lists.Streams <> EqSt coind
|
|
806
|
R9655:9657 StreamsLib <> sfx var
|
|
807
|
R9620:9622 Coq.Init.Datatypes <> snd def
|
|
808
|
R9625:9629 StreamsLib <> unzip def
|
|
809
|
R9632:9642 StreamsLib <> history_rec def
|
|
810
|
R9648:9650 StreamsLib <> sfx var
|
|
811
|
R9644:9646 StreamsLib <> pfx var
|
|
812
|
R9725:9728 Coq.Lists.Streams <> eqst constr
|
|
813
|
R9725:9728 Coq.Lists.Streams <> eqst constr
|
|
814
|
prf 9774:9786 <> unzip_history
|
|
815
|
R9806:9811 Coq.Lists.Streams <> Stream coind
|
|
816
|
R9813:9813 StreamsLib <> A var
|
|
817
|
R9817:9820 Coq.Lists.Streams <> EqSt coind
|
|
818
|
R9848:9848 StreamsLib <> s var
|
|
819
|
R9823:9825 Coq.Init.Datatypes <> snd def
|
|
820
|
R9828:9832 StreamsLib <> unzip def
|
|
821
|
R9835:9841 StreamsLib <> history def
|
|
822
|
R9843:9843 StreamsLib <> s var
|
|
823
|
R9865:9871 StreamsLib <> history def
|
|
824
|
R9888:9904 StreamsLib <> unzip_history_rec thm
|
|
825
|
R9888:9904 StreamsLib <> unzip_history_rec thm
|
|
826
|
def 9924:9935 <> History_Spec
|
|
827
|
R9946:9951 Coq.Lists.Streams <> Stream coind
|
|
828
|
R9953:9953 StreamsLib <> A var
|
|
829
|
R10018:10023 Coq.Init.Logic <> :type_scope:x_'/\'_x not
|
|
830
|
R9983:9985 Coq.Init.Logic <> :type_scope:x_'='_x not
|
|
831
|
R9967:9969 Coq.Init.Datatypes <> fst def
|
|
832
|
R9972:9973 Coq.Lists.Streams <> hd def
|
|
833
|
R9976:9977 Coq.Lists.Streams <> tl def
|
|
834
|
R9979:9980 StreamsLib <> s' var
|
|
835
|
R9986:9989 Coq.Init.Datatypes <> cons constr
|
|
836
|
R10006:10008 Coq.Init.Datatypes <> fst def
|
|
837
|
R10011:10012 Coq.Lists.Streams <> hd def
|
|
838
|
R10014:10015 StreamsLib <> s' var
|
|
839
|
R9992:9994 Coq.Init.Datatypes <> snd def
|
|
840
|
R9997:9998 Coq.Lists.Streams <> hd def
|
|
841
|
R10000:10001 StreamsLib <> s' var
|
|
842
|
R10024:10027 Coq.Lists.Streams <> EqSt coind
|
|
843
|
R10081:10081 StreamsLib <> s var
|
|
844
|
R10030:10035 StreamsLib <> concat def
|
|
845
|
R10052:10056 StreamsLib <> apply def
|
|
846
|
R10076:10077 StreamsLib <> s' var
|
|
847
|
R10059:10062 StreamsLib <> lift def
|
|
848
|
R10066:10068 Coq.Init.Datatypes <> snd def
|
|
849
|
R10038:10040 Coq.Init.Datatypes <> fst def
|
|
850
|
R10043:10044 Coq.Lists.Streams <> hd def
|
|
851
|
R10046:10047 StreamsLib <> s' var
|
|
852
|
prf 10093:10108 <> history_rec_spec
|
|
853
|
R10130:10135 Coq.Lists.Streams <> Stream coind
|
|
854
|
R10137:10137 StreamsLib <> A var
|
|
855
|
R10176:10182 Coq.Init.Logic <> :type_scope:x_'/\'_x not
|
|
856
|
R10172:10174 Coq.Init.Logic <> :type_scope:x_'='_x not
|
|
857
|
R10146:10148 Coq.Init.Datatypes <> fst def
|
|
858
|
R10151:10152 Coq.Lists.Streams <> hd def
|
|
859
|
R10155:10165 StreamsLib <> history_rec def
|
|
860
|
R10169:10169 StreamsLib <> s var
|
|
861
|
R10167:10167 StreamsLib <> p var
|
|
862
|
R10175:10175 StreamsLib <> p var
|
|
863
|
R10183:10188 Coq.Lists.Streams <> ForAll coind
|
|
864
|
R10232:10242 StreamsLib <> history_rec def
|
|
865
|
R10246:10246 StreamsLib <> s var
|
|
866
|
R10244:10244 StreamsLib <> p var
|
|
867
|
R10201:10212 StreamsLib <> History_Spec def
|
|
868
|
R10227:10228 StreamsLib <> s' var
|
|
869
|
R10215:10220 StreamsLib <> concat def
|
|
870
|
R10224:10224 StreamsLib <> s var
|
|
871
|
R10222:10222 StreamsLib <> p var
|
|
872
|
R10359:10372 Coq.Lists.Streams <> HereAndFurther constr
|
|
873
|
R10359:10372 Coq.Lists.Streams <> HereAndFurther constr
|
|
874
|
R10436:10446 StreamsLib <> eqst_concat thm
|
|
875
|
R10436:10446 StreamsLib <> eqst_concat thm
|
|
876
|
R10458:10474 StreamsLib <> unzip_history_rec thm
|
|
877
|
R10458:10474 StreamsLib <> unzip_history_rec thm
|
|
878
|
R10494:10497 Coq.Init.Datatypes <> cons constr
|
|
879
|
R10494:10497 Coq.Init.Datatypes <> cons constr
|
|
880
|
prf 10524:10535 <> history_spec
|
|
881
|
R10555:10560 Coq.Lists.Streams <> Stream coind
|
|
882
|
R10562:10562 StreamsLib <> A var
|
|
883
|
R10597:10602 Coq.Init.Logic <> :type_scope:x_'/\'_x not
|
|
884
|
R10591:10593 Coq.Init.Logic <> :type_scope:x_'='_x not
|
|
885
|
R10571:10573 Coq.Init.Datatypes <> fst def
|
|
886
|
R10576:10577 Coq.Lists.Streams <> hd def
|
|
887
|
R10580:10586 StreamsLib <> history def
|
|
888
|
R10588:10588 StreamsLib <> s var
|
|
889
|
R10594:10596 Coq.Init.Datatypes <> nil constr
|
|
890
|
R10603:10608 Coq.Lists.Streams <> ForAll coind
|
|
891
|
R10641:10647 StreamsLib <> history def
|
|
892
|
R10649:10649 StreamsLib <> s var
|
|
893
|
R10621:10632 StreamsLib <> History_Spec def
|
|
894
|
R10636:10637 StreamsLib <> s' var
|
|
895
|
R10634:10634 StreamsLib <> s var
|
|
896
|
R10680:10695 StreamsLib <> history_rec_spec thm
|
|
897
|
R10697:10699 Coq.Init.Datatypes <> nil constr
|
|
898
|
R10680:10695 StreamsLib <> history_rec_spec thm
|
|
899
|
R10697:10699 Coq.Init.Datatypes <> nil constr
|
|
900
|
R0:-1 StreamsLib <> y var
|
|
901
|
prf 10730:10754 <> history_rec_spec_complete
|
|
902
|
R10776:10781 Coq.Lists.Streams <> Stream coind
|
|
903
|
R10783:10783 StreamsLib <> A var
|
|
904
|
R10865:10868 Coq.Lists.Streams <> EqSt coind
|
|
905
|
R10874:10884 StreamsLib <> history_rec def
|
|
906
|
R10888:10888 StreamsLib <> s var
|
|
907
|
R10886:10886 StreamsLib <> p var
|
|
908
|
R10870:10871 StreamsLib <> ps var
|
|
909
|
R10811:10816 Coq.Lists.Streams <> ForAll coind
|
|
910
|
R10859:10860 StreamsLib <> ps var
|
|
911
|
R10829:10840 StreamsLib <> History_Spec def
|
|
912
|
R10855:10856 StreamsLib <> s' var
|
|
913
|
R10843:10848 StreamsLib <> concat def
|
|
914
|
R10852:10852 StreamsLib <> s var
|
|
915
|
R10850:10850 StreamsLib <> p var
|
|
916
|
R10803:10805 Coq.Init.Logic <> :type_scope:x_'='_x not
|
|
917
|
R10792:10794 Coq.Init.Datatypes <> fst def
|
|
918
|
R10797:10798 Coq.Lists.Streams <> hd def
|
|
919
|
R10800:10801 StreamsLib <> ps var
|
|
920
|
R10806:10806 StreamsLib <> p var
|
|
921
|
R11031:11042 StreamsLib <> History_Spec def
|
|
922
|
R11080:11083 Coq.Lists.Streams <> eqst constr
|
|
923
|
R11080:11083 Coq.Lists.Streams <> eqst constr
|
|
924
|
R11147:11158 StreamsLib <> History_Spec def
|
|
925
|
R11212:11222 StreamsLib <> concat_eqst thm
|
|
926
|
R11232:11241 Coq.Init.Logic <> refl_equal syndef
|
|
927
|
R11212:11222 StreamsLib <> concat_eqst thm
|
|
928
|
R11232:11241 Coq.Init.Logic <> refl_equal syndef
|
|
929
|
R11349:11359 StreamsLib <> concat_eqst thm
|
|
930
|
R11369:11378 Coq.Init.Logic <> refl_equal syndef
|
|
931
|
R11349:11359 StreamsLib <> concat_eqst thm
|
|
932
|
R11369:11378 Coq.Init.Logic <> refl_equal syndef
|
|
933
|
prf 11468:11488 <> history_spec_complete
|
|
934
|
R11508:11513 Coq.Lists.Streams <> Stream coind
|
|
935
|
R11515:11515 StreamsLib <> A var
|
|
936
|
R11588:11591 Coq.Lists.Streams <> EqSt coind
|
|
937
|
R11597:11603 StreamsLib <> history def
|
|
938
|
R11605:11605 StreamsLib <> s var
|
|
939
|
R11593:11594 StreamsLib <> ps var
|
|
940
|
R11545:11550 Coq.Lists.Streams <> ForAll coind
|
|
941
|
R11582:11583 StreamsLib <> ps var
|
|
942
|
R11563:11574 StreamsLib <> History_Spec def
|
|
943
|
R11578:11579 StreamsLib <> s' var
|
|
944
|
R11576:11576 StreamsLib <> s var
|
|
945
|
R11535:11537 Coq.Init.Logic <> :type_scope:x_'='_x not
|
|
946
|
R11524:11526 Coq.Init.Datatypes <> fst def
|
|
947
|
R11529:11530 Coq.Lists.Streams <> hd def
|
|
948
|
R11532:11533 StreamsLib <> ps var
|
|
949
|
R11538:11540 Coq.Init.Datatypes <> nil constr
|
|
950
|
R11630:11654 StreamsLib <> history_rec_spec_complete thm
|
|
951
|
R11630:11654 StreamsLib <> history_rec_spec_complete thm
|
|
952
|
prf 11698:11722 <> inv_snd_history_rec_intro
|
|
953
|
R11742:11747 Coq.Lists.Streams <> Stream coind
|
|
954
|
R11749:11749 StreamsLib <> A var
|
|
955
|
R11767:11772 Coq.Lists.Streams <> Stream coind
|
|
956
|
R11774:11774 StreamsLib <> A var
|
|
957
|
R11794:11799 Coq.Lists.Streams <> ForAll coind
|
|
958
|
R11845:11855 StreamsLib <> history_rec def
|
|
959
|
R11859:11859 StreamsLib <> s var
|
|
960
|
R11857:11857 StreamsLib <> p var
|
|
961
|
R11812:11812 StreamsLib <> P var
|
|
962
|
R11815:11819 StreamsLib <> apply def
|
|
963
|
R11839:11840 StreamsLib <> s' var
|
|
964
|
R11822:11825 StreamsLib <> lift def
|
|
965
|
R11829:11831 Coq.Init.Datatypes <> snd def
|
|
966
|
R11780:11785 Coq.Lists.Streams <> ForAll coind
|
|
967
|
R11789:11789 StreamsLib <> s var
|
|
968
|
R11787:11787 StreamsLib <> P var
|
|
969
|
R11884:11890 StreamsLib <> inv_map thm
|
|
970
|
R11884:11890 StreamsLib <> inv_map thm
|
|
971
|
R11905:11911 StreamsLib <> eqst_eq prfax
|
|
972
|
R11918:11934 StreamsLib <> unzip_history_rec thm
|
|
973
|
R11905:11911 StreamsLib <> eqst_eq prfax
|
|
974
|
R11918:11934 StreamsLib <> unzip_history_rec thm
|
|
975
|
prf 11995:12015 <> inv_snd_history_intro
|
|
976
|
R12035:12040 Coq.Lists.Streams <> Stream coind
|
|
977
|
R12042:12042 StreamsLib <> A var
|
|
978
|
R12058:12063 Coq.Lists.Streams <> Stream coind
|
|
979
|
R12065:12065 StreamsLib <> A var
|
|
980
|
R12085:12090 Coq.Lists.Streams <> ForAll coind
|
|
981
|
R12136:12142 StreamsLib <> history def
|
|
982
|
R12144:12144 StreamsLib <> s var
|
|
983
|
R12103:12103 StreamsLib <> P var
|
|
984
|
R12106:12110 StreamsLib <> apply def
|
|
985
|
R12130:12131 StreamsLib <> s' var
|
|
986
|
R12113:12116 StreamsLib <> lift def
|
|
987
|
R12120:12122 Coq.Init.Datatypes <> snd def
|
|
988
|
R12071:12076 Coq.Lists.Streams <> ForAll coind
|
|
989
|
R12080:12080 StreamsLib <> s var
|
|
990
|
R12078:12078 StreamsLib <> P var
|
|
991
|
R12169:12193 StreamsLib <> inv_snd_history_rec_intro thm
|
|
992
|
R12169:12193 StreamsLib <> inv_snd_history_rec_intro thm
|
|
993
|
prf 12222:12245 <> inv_snd_history_rec_elim
|
|
994
|
R12265:12270 Coq.Lists.Streams <> Stream coind
|
|
995
|
R12272:12272 StreamsLib <> A var
|
|
996
|
R12290:12295 Coq.Lists.Streams <> Stream coind
|
|
997
|
R12297:12297 StreamsLib <> A var
|
|
998
|
R12374:12379 Coq.Lists.Streams <> ForAll coind
|
|
999
|
R12383:12383 StreamsLib <> s var
|
|
1000
|
R12381:12381 StreamsLib <> P var
|
|
1001
|
R12303:12308 Coq.Lists.Streams <> ForAll coind
|
|
1002
|
R12354:12364 StreamsLib <> history_rec def
|
|
1003
|
R12368:12368 StreamsLib <> s var
|
|
1004
|
R12366:12366 StreamsLib <> p var
|
|
1005
|
R12321:12321 StreamsLib <> P var
|
|
1006
|
R12324:12328 StreamsLib <> apply def
|
|
1007
|
R12348:12349 StreamsLib <> s' var
|
|
1008
|
R12331:12334 StreamsLib <> lift def
|
|
1009
|
R12338:12340 Coq.Init.Datatypes <> snd def
|
|
1010
|
R12413:12419 StreamsLib <> eqst_eq prfax
|
|
1011
|
R12426:12442 StreamsLib <> unzip_history_rec thm
|
|
1012
|
R12413:12419 StreamsLib <> eqst_eq prfax
|
|
1013
|
R12426:12442 StreamsLib <> unzip_history_rec thm
|
|
1014
|
R12457:12463 StreamsLib <> map_inv thm
|
|
1015
|
R12457:12463 StreamsLib <> map_inv thm
|
|
1016
|
prf 12489:12508 <> inv_snd_history_elim
|
|
1017
|
R12528:12533 Coq.Lists.Streams <> Stream coind
|
|
1018
|
R12535:12535 StreamsLib <> A var
|
|
1019
|
R12551:12556 Coq.Lists.Streams <> Stream coind
|
|
1020
|
R12558:12558 StreamsLib <> A var
|
|
1021
|
R12629:12634 Coq.Lists.Streams <> ForAll coind
|
|
1022
|
R12638:12638 StreamsLib <> s var
|
|
1023
|
R12636:12636 StreamsLib <> P var
|
|
1024
|
R12564:12569 Coq.Lists.Streams <> ForAll coind
|
|
1025
|
R12615:12621 StreamsLib <> history def
|
|
1026
|
R12623:12623 StreamsLib <> s var
|
|
1027
|
R12582:12582 StreamsLib <> P var
|
|
1028
|
R12585:12589 StreamsLib <> apply def
|
|
1029
|
R12609:12610 StreamsLib <> s' var
|
|
1030
|
R12592:12595 StreamsLib <> lift def
|
|
1031
|
R12599:12601 Coq.Init.Datatypes <> snd def
|
|
1032
|
R12698:12700 Coq.Init.Datatypes <> nil constr
|
|
1033
|
R12662:12685 StreamsLib <> inv_snd_history_rec_elim thm
|
|
1034
|
R12698:12700 Coq.Init.Datatypes <> nil constr
|
|
1035
|
R12662:12685 StreamsLib <> inv_snd_history_rec_elim thm
|
|
1036
|
def 12731:12736 <> prefix
|
|
1037
|
R12747:12747 StreamsLib <> A var
|
|
1038
|
R12768:12768 StreamsLib <> A var
|
|
1039
|
R12763:12763 StreamsLib <> A var
|
|
1040
|
R12784:12786 Coq.Init.Datatypes <> nat ind
|
|
1041
|
R12791:12794 Coq.Init.Datatypes <> list ind
|
|
1042
|
R12796:12796 StreamsLib <> A var
|
|
1043
|
R12817:12817 StreamsLib <> k var
|
|
1044
|
R12849:12852 Coq.Init.Logic <> True ind
|
|
1045
|
R12858:12858 Coq.Init.Datatypes <> S constr
|
|
1046
|
R12884:12884 StreamsLib <> p var
|
|
1047
|
R12916:12919 Coq.Init.Logic <> True ind
|
|
1048
|
R12986:12986 StreamsLib <> I var
|
|
1049
|
R13016:13016 Coq.Init.Logic <> :type_scope:x_'/\'_x not
|
|
1050
|
R13023:13028 Coq.Init.Logic <> :type_scope:x_'/\'_x not
|
|
1051
|
R13044:13044 Coq.Init.Logic <> :type_scope:x_'/\'_x not
|
|
1052
|
R13017:13017 StreamsLib <> T var
|
|
1053
|
R13029:13034 StreamsLib <> prefix def
|
|
1054
|
R13038:13038 StreamsLib <> T var
|
|
1055
|
R13036:13036 StreamsLib <> I var
|
|
1056
|
prf 13077:13089 <> prefix_mono_k
|
|
1057
|
R13115:13118 Coq.Init.Datatypes <> list ind
|
|
1058
|
R13120:13120 StreamsLib <> A var
|
|
1059
|
R13146:13151 StreamsLib <> prefix def
|
|
1060
|
R13159:13159 StreamsLib <> p var
|
|
1061
|
R13157:13157 StreamsLib <> k var
|
|
1062
|
R13155:13155 StreamsLib <> T var
|
|
1063
|
R13153:13153 StreamsLib <> I var
|
|
1064
|
R13124:13129 StreamsLib <> prefix def
|
|
1065
|
R13141:13141 StreamsLib <> p var
|
|
1066
|
R13136:13136 Coq.Init.Datatypes <> S constr
|
|
1067
|
R13138:13138 StreamsLib <> k var
|
|
1068
|
R13133:13133 StreamsLib <> T var
|
|
1069
|
R13131:13131 StreamsLib <> I var
|
|
1070
|
R0:-1 StreamsLib <> y var
|
|
1071
|
R0:-1 StreamsLib <> y var
|
|
1072
|
R0:-1 StreamsLib <> y var
|
|
1073
|
R0:-1 StreamsLib <> y var
|
|
1074
|
R0:-1 StreamsLib <> y var
|
|
1075
|
prf 13316:13327 <> prefix_apply
|
|
1076
|
R13350:13350 StreamsLib <> A var
|
|
1077
|
R13374:13374 StreamsLib <> A var
|
|
1078
|
R13369:13369 StreamsLib <> A var
|
|
1079
|
R13392:13395 Coq.Init.Datatypes <> list ind
|
|
1080
|
R13397:13397 StreamsLib <> A var
|
|
1081
|
R13490:13495 StreamsLib <> prefix def
|
|
1082
|
R13505:13505 StreamsLib <> p var
|
|
1083
|
R13503:13503 StreamsLib <> k var
|
|
1084
|
R13500:13501 StreamsLib <> T' var
|
|
1085
|
R13497:13498 StreamsLib <> I' var
|
|
1086
|
R13421:13426 StreamsLib <> prefix def
|
|
1087
|
R13485:13485 StreamsLib <> p var
|
|
1088
|
R13483:13483 StreamsLib <> k var
|
|
1089
|
R13474:13475 StreamsLib <> T' var
|
|
1090
|
R13479:13480 StreamsLib <> s' var
|
|
1091
|
R13477:13477 StreamsLib <> s var
|
|
1092
|
R13464:13464 StreamsLib <> T var
|
|
1093
|
R13468:13469 StreamsLib <> s' var
|
|
1094
|
R13466:13466 StreamsLib <> s var
|
|
1095
|
R13445:13446 StreamsLib <> I' var
|
|
1096
|
R13448:13448 StreamsLib <> s var
|
|
1097
|
R13438:13438 StreamsLib <> I var
|
|
1098
|
R13440:13440 StreamsLib <> s var
|
|
1099
|
R13403:13408 StreamsLib <> prefix def
|
|
1100
|
R13416:13416 StreamsLib <> p var
|
|
1101
|
R13414:13414 StreamsLib <> k var
|
|
1102
|
R13412:13412 StreamsLib <> T var
|
|
1103
|
R13410:13410 StreamsLib <> I var
|
|
1104
|
R0:-1 StreamsLib <> y var
|
|
1105
|
R0:-1 StreamsLib <> y var
|
|
1106
|
prf 13649:13658 <> kinduction
|
|
1107
|
R13678:13678 StreamsLib <> A var
|
|
1108
|
R13696:13701 Coq.Lists.Streams <> Stream coind
|
|
1109
|
R13703:13703 StreamsLib <> A var
|
|
1110
|
R13827:13832 Coq.Lists.Streams <> ForAll coind
|
|
1111
|
R13856:13856 StreamsLib <> s var
|
|
1112
|
R13845:13845 StreamsLib <> P var
|
|
1113
|
R13848:13849 Coq.Lists.Streams <> hd def
|
|
1114
|
R13851:13852 StreamsLib <> s' var
|
|
1115
|
R13711:13716 Coq.Lists.Streams <> ForAll coind
|
|
1116
|
R13812:13818 StreamsLib <> history def
|
|
1117
|
R13820:13820 StreamsLib <> s var
|
|
1118
|
R13794:13794 StreamsLib <> P var
|
|
1119
|
R13797:13799 Coq.Init.Datatypes <> snd def
|
|
1120
|
R13802:13803 Coq.Lists.Streams <> hd def
|
|
1121
|
R13805:13806 StreamsLib <> s' var
|
|
1122
|
R13729:13734 StreamsLib <> prefix def
|
|
1123
|
R13778:13780 Coq.Init.Datatypes <> fst def
|
|
1124
|
R13783:13784 Coq.Lists.Streams <> hd def
|
|
1125
|
R13786:13787 StreamsLib <> s' var
|
|
1126
|
R13775:13775 StreamsLib <> k var
|
|
1127
|
R13768:13768 StreamsLib <> P var
|
|
1128
|
R13770:13772 StreamsLib <> st' var
|
|
1129
|
R13747:13747 StreamsLib <> P var
|
|
1130
|
R13749:13750 StreamsLib <> st var
|
|
1131
|
R13880:13899 StreamsLib <> inv_snd_history_elim thm
|
|
1132
|
R13880:13899 StreamsLib <> inv_snd_history_elim thm
|
|
1133
|
R13946:13948 Coq.Init.Datatypes <> snd def
|
|
1134
|
R13951:13952 Coq.Lists.Streams <> hd def
|
|
1135
|
R13954:13955 StreamsLib <> s' var
|
|
1136
|
R13909:13920 StreamsLib <> ForAll_apply def
|
|
1137
|
R13946:13948 Coq.Init.Datatypes <> snd def
|
|
1138
|
R13951:13952 Coq.Lists.Streams <> hd def
|
|
1139
|
R13954:13955 StreamsLib <> s' var
|
|
1140
|
R13909:13920 StreamsLib <> ForAll_apply def
|
|
1141
|
R14024:14029 StreamsLib <> prefix def
|
|
1142
|
R14073:14075 Coq.Init.Datatypes <> fst def
|
|
1143
|
R14078:14079 Coq.Lists.Streams <> hd def
|
|
1144
|
R14081:14082 StreamsLib <> s' var
|
|
1145
|
R14065:14067 StreamsLib <> st' var
|
|
1146
|
R14044:14045 StreamsLib <> st var
|
|
1147
|
R13971:13982 StreamsLib <> ForAll_apply def
|
|
1148
|
R14024:14029 StreamsLib <> prefix def
|
|
1149
|
R14073:14075 Coq.Init.Datatypes <> fst def
|
|
1150
|
R14078:14079 Coq.Lists.Streams <> hd def
|
|
1151
|
R14081:14082 StreamsLib <> s' var
|
|
1152
|
R14065:14067 StreamsLib <> st' var
|
|
1153
|
R14044:14045 StreamsLib <> st var
|
|
1154
|
R13971:13982 StreamsLib <> ForAll_apply def
|
|
1155
|
R14138:14143 Coq.Lists.Streams <> ForAll coind
|
|
1156
|
R14169:14174 Coq.Lists.Streams <> Stream coind
|
|
1157
|
R14183:14185 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
|
|
1158
|
R14177:14180 Coq.Init.Datatypes <> list ind
|
|
1159
|
R14299:14301 Coq.Init.Datatypes <> snd def
|
|
1160
|
R14304:14305 Coq.Lists.Streams <> hd def
|
|
1161
|
R14307:14308 StreamsLib <> s' var
|
|
1162
|
R14207:14212 StreamsLib <> prefix def
|
|
1163
|
R14280:14282 Coq.Init.Datatypes <> fst def
|
|
1164
|
R14285:14286 Coq.Lists.Streams <> hd def
|
|
1165
|
R14288:14289 StreamsLib <> s' var
|
|
1166
|
R14255:14257 StreamsLib <> st' var
|
|
1167
|
R14231:14232 StreamsLib <> st var
|
|
1168
|
R14100:14115 StreamsLib <> ForAll_reinforce def
|
|
1169
|
R14138:14143 Coq.Lists.Streams <> ForAll coind
|
|
1170
|
R14169:14174 Coq.Lists.Streams <> Stream coind
|
|
1171
|
R14183:14185 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
|
|
1172
|
R14177:14180 Coq.Init.Datatypes <> list ind
|
|
1173
|
R14299:14301 Coq.Init.Datatypes <> snd def
|
|
1174
|
R14304:14305 Coq.Lists.Streams <> hd def
|
|
1175
|
R14307:14308 StreamsLib <> s' var
|
|
1176
|
R14207:14212 StreamsLib <> prefix def
|
|
1177
|
R14280:14282 Coq.Init.Datatypes <> fst def
|
|
1178
|
R14285:14286 Coq.Lists.Streams <> hd def
|
|
1179
|
R14288:14289 StreamsLib <> s' var
|
|
1180
|
R14255:14257 StreamsLib <> st' var
|
|
1181
|
R14231:14232 StreamsLib <> st var
|
|
1182
|
R14100:14115 StreamsLib <> ForAll_reinforce def
|
|
1183
|
R14359:14364 Coq.Lists.Streams <> ForAll coind
|
|
1184
|
R14376:14381 Coq.Lists.Streams <> Stream coind
|
|
1185
|
R14390:14392 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
|
|
1186
|
R14384:14387 Coq.Init.Datatypes <> list ind
|
|
1187
|
R14399:14410 StreamsLib <> History_Spec def
|
|
1188
|
R14414:14415 StreamsLib <> s' var
|
|
1189
|
R14327:14342 StreamsLib <> ForAll_reinforce def
|
|
1190
|
R14359:14364 Coq.Lists.Streams <> ForAll coind
|
|
1191
|
R14376:14381 Coq.Lists.Streams <> Stream coind
|
|
1192
|
R14390:14392 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
|
|
1193
|
R14384:14387 Coq.Init.Datatypes <> list ind
|
|
1194
|
R14399:14410 StreamsLib <> History_Spec def
|
|
1195
|
R14414:14415 StreamsLib <> s' var
|
|
1196
|
R14327:14342 StreamsLib <> ForAll_reinforce def
|
|
1197
|
R14429:14440 Coq.Lists.Streams <> ForAll_coind thm
|
|
1198
|
R14429:14440 Coq.Lists.Streams <> ForAll_coind thm
|
|
1199
|
R14472:14472 StreamsLib <> x var
|
|
1200
|
R14472:14472 StreamsLib <> x var
|
|
1201
|
R0:-1 StreamsLib <> y var
|
|
1202
|
R14646:14657 StreamsLib <> History_Spec def
|
|
1203
|
R0:-1 StreamsLib <> y var
|
|
1204
|
R14925:14937 StreamsLib <> prefix_mono_k thm
|
|
1205
|
R14925:14937 StreamsLib <> prefix_mono_k thm
|
|
1206
|
R0:-1 StreamsLib <> y var
|
|
1207
|
R14998:15009 StreamsLib <> history_spec thm
|
|
1208
|
R14998:15009 StreamsLib <> history_spec thm
|
|
1209
|
R0:-1 StreamsLib <> y var
|
|
1210
|
R15147:15159 StreamsLib <> necessitation def
|
|
1211
|
R15147:15159 StreamsLib <> necessitation def
|
|
1212
|
prf 15208:15218 <> kinduction'
|
|
1213
|
R15239:15239 StreamsLib <> A var
|
|
1214
|
R15260:15265 Coq.Lists.Streams <> Stream coind
|
|
1215
|
R15267:15267 StreamsLib <> A var
|
|
1216
|
R15448:15453 Coq.Lists.Streams <> ForAll coind
|
|
1217
|
R15477:15477 StreamsLib <> s var
|
|
1218
|
R15466:15466 StreamsLib <> P var
|
|
1219
|
R15469:15470 Coq.Lists.Streams <> hd def
|
|
1220
|
R15472:15473 StreamsLib <> s' var
|
|
1221
|
R15341:15346 Coq.Lists.Streams <> ForAll coind
|
|
1222
|
R15441:15442 StreamsLib <> ps var
|
|
1223
|
R15424:15424 StreamsLib <> P var
|
|
1224
|
R15427:15429 Coq.Init.Datatypes <> snd def
|
|
1225
|
R15432:15433 Coq.Lists.Streams <> hd def
|
|
1226
|
R15435:15436 StreamsLib <> s' var
|
|
1227
|
R15359:15364 StreamsLib <> prefix def
|
|
1228
|
R15408:15410 Coq.Init.Datatypes <> fst def
|
|
1229
|
R15413:15414 Coq.Lists.Streams <> hd def
|
|
1230
|
R15416:15417 StreamsLib <> s' var
|
|
1231
|
R15405:15405 StreamsLib <> k var
|
|
1232
|
R15398:15398 StreamsLib <> P var
|
|
1233
|
R15400:15402 StreamsLib <> st' var
|
|
1234
|
R15377:15377 StreamsLib <> P var
|
|
1235
|
R15379:15380 StreamsLib <> st var
|
|
1236
|
R15297:15302 Coq.Lists.Streams <> ForAll coind
|
|
1237
|
R15334:15335 StreamsLib <> ps var
|
|
1238
|
R15315:15326 StreamsLib <> History_Spec def
|
|
1239
|
R15330:15331 StreamsLib <> s' var
|
|
1240
|
R15328:15328 StreamsLib <> s var
|
|
1241
|
R15286:15288 Coq.Init.Logic <> :type_scope:x_'='_x not
|
|
1242
|
R15275:15277 Coq.Init.Datatypes <> fst def
|
|
1243
|
R15280:15281 Coq.Lists.Streams <> hd def
|
|
1244
|
R15283:15284 StreamsLib <> ps var
|
|
1245
|
R15289:15291 Coq.Init.Datatypes <> nil constr
|
|
1246
|
R15504:15510 StreamsLib <> eqst_eq prfax
|
|
1247
|
R15517:15537 StreamsLib <> history_spec_complete thm
|
|
1248
|
R15504:15510 StreamsLib <> eqst_eq prfax
|
|
1249
|
R15517:15537 StreamsLib <> history_spec_complete thm
|
|
1250
|
R15564:15573 StreamsLib <> kinduction thm
|
|
1251
|
R15564:15573 StreamsLib <> kinduction thm
|
|
1252
|
prf 15600:15621 <> inv_prefix_history_rec
|
|
1253
|
R15641:15641 StreamsLib <> A var
|
|
1254
|
R15662:15662 StreamsLib <> A var
|
|
1255
|
R15657:15657 StreamsLib <> A var
|
|
1256
|
R15680:15685 Coq.Lists.Streams <> Stream coind
|
|
1257
|
R15687:15687 StreamsLib <> A var
|
|
1258
|
R15799:15804 Coq.Lists.Streams <> ForAll coind
|
|
1259
|
R15867:15877 StreamsLib <> history_rec def
|
|
1260
|
R15881:15881 StreamsLib <> s var
|
|
1261
|
R15879:15879 StreamsLib <> p var
|
|
1262
|
R15817:15822 StreamsLib <> prefix def
|
|
1263
|
R15831:15834 Coq.Init.Datatypes <> cons constr
|
|
1264
|
R15851:15853 Coq.Init.Datatypes <> fst def
|
|
1265
|
R15856:15857 Coq.Lists.Streams <> hd def
|
|
1266
|
R15859:15860 StreamsLib <> s' var
|
|
1267
|
R15837:15839 Coq.Init.Datatypes <> snd def
|
|
1268
|
R15842:15843 Coq.Lists.Streams <> hd def
|
|
1269
|
R15845:15846 StreamsLib <> s' var
|
|
1270
|
R15828:15828 StreamsLib <> k var
|
|
1271
|
R15826:15826 StreamsLib <> T var
|
|
1272
|
R15824:15824 StreamsLib <> I var
|
|
1273
|
R15764:15769 StreamsLib <> prefix def
|
|
1274
|
R15778:15781 Coq.Init.Datatypes <> cons constr
|
|
1275
|
R15790:15790 StreamsLib <> p var
|
|
1276
|
R15784:15785 Coq.Lists.Streams <> hd def
|
|
1277
|
R15787:15787 StreamsLib <> s var
|
|
1278
|
R15775:15775 StreamsLib <> k var
|
|
1279
|
R15773:15773 StreamsLib <> T var
|
|
1280
|
R15771:15771 StreamsLib <> I var
|
|
1281
|
R15692:15697 Coq.Lists.Streams <> ForAll coind
|
|
1282
|
R15735:15740 StreamsLib <> concat def
|
|
1283
|
R15744:15744 StreamsLib <> s var
|
|
1284
|
R15742:15742 StreamsLib <> p var
|
|
1285
|
R15710:15710 StreamsLib <> T var
|
|
1286
|
R15721:15722 Coq.Lists.Streams <> hd def
|
|
1287
|
R15725:15726 Coq.Lists.Streams <> tl def
|
|
1288
|
R15728:15729 StreamsLib <> s' var
|
|
1289
|
R15713:15714 Coq.Lists.Streams <> hd def
|
|
1290
|
R15716:15717 StreamsLib <> s' var
|
|
1291
|
R15970:15983 Coq.Lists.Streams <> HereAndFurther constr
|
|
1292
|
R15970:15983 Coq.Lists.Streams <> HereAndFurther constr
|
|
1293
|
R16097:16106 StreamsLib <> inv_concat thm
|
|
1294
|
R16097:16106 StreamsLib <> inv_concat thm
|
|
1295
|
R16184:16196 StreamsLib <> prefix_mono_k thm
|
|
1296
|
R16184:16196 StreamsLib <> prefix_mono_k thm
|
|
1297
|
prf 16229:16246 <> inv_prefix_history
|
|
1298
|
R16266:16266 StreamsLib <> A var
|
|
1299
|
R16287:16287 StreamsLib <> A var
|
|
1300
|
R16282:16282 StreamsLib <> A var
|
|
1301
|
R16303:16308 Coq.Lists.Streams <> Stream coind
|
|
1302
|
R16310:16310 StreamsLib <> A var
|
|
1303
|
R16386:16391 Coq.Lists.Streams <> ForAll coind
|
|
1304
|
R16454:16460 StreamsLib <> history def
|
|
1305
|
R16462:16462 StreamsLib <> s var
|
|
1306
|
R16404:16409 StreamsLib <> prefix def
|
|
1307
|
R16418:16421 Coq.Init.Datatypes <> cons constr
|
|
1308
|
R16438:16440 Coq.Init.Datatypes <> fst def
|
|
1309
|
R16443:16444 Coq.Lists.Streams <> hd def
|
|
1310
|
R16446:16447 StreamsLib <> s' var
|
|
1311
|
R16424:16426 Coq.Init.Datatypes <> snd def
|
|
1312
|
R16429:16430 Coq.Lists.Streams <> hd def
|
|
1313
|
R16432:16433 StreamsLib <> s' var
|
|
1314
|
R16415:16415 StreamsLib <> k var
|
|
1315
|
R16413:16413 StreamsLib <> T var
|
|
1316
|
R16411:16411 StreamsLib <> I var
|
|
1317
|
R16327:16332 Coq.Lists.Streams <> ForAll coind
|
|
1318
|
R16369:16369 StreamsLib <> s var
|
|
1319
|
R16345:16345 StreamsLib <> T var
|
|
1320
|
R16356:16357 Coq.Lists.Streams <> hd def
|
|
1321
|
R16360:16361 Coq.Lists.Streams <> tl def
|
|
1322
|
R16363:16364 StreamsLib <> s' var
|
|
1323
|
R16348:16349 Coq.Lists.Streams <> hd def
|
|
1324
|
R16351:16352 StreamsLib <> s' var
|
|
1325
|
R16315:16315 StreamsLib <> I var
|
|
1326
|
R16318:16319 Coq.Lists.Streams <> hd def
|
|
1327
|
R16321:16321 StreamsLib <> s var
|
|
1328
|
R16487:16508 StreamsLib <> inv_prefix_history_rec thm
|
|
1329
|
R16487:16508 StreamsLib <> inv_prefix_history_rec thm
|
|
1330
|
prf 16585:16603 <> inv_prefix_history'
|
|
1331
|
R16623:16623 StreamsLib <> A var
|
|
1332
|
R16644:16644 StreamsLib <> A var
|
|
1333
|
R16639:16639 StreamsLib <> A var
|
|
1334
|
R16660:16665 Coq.Lists.Streams <> Stream coind
|
|
1335
|
R16667:16667 StreamsLib <> A var
|
|
1336
|
R16743:16748 Coq.Lists.Streams <> ForAll coind
|
|
1337
|
R16790:16796 StreamsLib <> history def
|
|
1338
|
R16798:16798 StreamsLib <> s var
|
|
1339
|
R16761:16766 StreamsLib <> prefix def
|
|
1340
|
R16775:16777 Coq.Init.Datatypes <> fst def
|
|
1341
|
R16780:16781 Coq.Lists.Streams <> hd def
|
|
1342
|
R16783:16784 StreamsLib <> s' var
|
|
1343
|
R16772:16772 StreamsLib <> k var
|
|
1344
|
R16770:16770 StreamsLib <> T var
|
|
1345
|
R16768:16768 StreamsLib <> I var
|
|
1346
|
R16684:16689 Coq.Lists.Streams <> ForAll coind
|
|
1347
|
R16726:16726 StreamsLib <> s var
|
|
1348
|
R16702:16702 StreamsLib <> T var
|
|
1349
|
R16713:16714 Coq.Lists.Streams <> hd def
|
|
1350
|
R16717:16718 Coq.Lists.Streams <> tl def
|
|
1351
|
R16720:16721 StreamsLib <> s' var
|
|
1352
|
R16705:16706 Coq.Lists.Streams <> hd def
|
|
1353
|
R16708:16709 StreamsLib <> s' var
|
|
1354
|
R16672:16672 StreamsLib <> I var
|
|
1355
|
R16675:16676 Coq.Lists.Streams <> hd def
|
|
1356
|
R16678:16678 StreamsLib <> s var
|
|
1357
|
R16836:16848 StreamsLib <> necessitation def
|
|
1358
|
R16836:16848 StreamsLib <> necessitation def
|
|
1359
|
R16878:16889 StreamsLib <> ForAll_apply def
|
|
1360
|
R16878:16889 StreamsLib <> ForAll_apply def
|
|
1361
|
R16912:16929 StreamsLib <> inv_prefix_history thm
|
|
1362
|
R16942:16942 Coq.Init.Datatypes <> S constr
|
|
1363
|
R16945:16945 Coq.Init.Datatypes <> S constr
|
|
1364
|
R16939:16939 StreamsLib <> n var
|
|
1365
|
R16937:16937 StreamsLib <> i var
|
|
1366
|
R16912:16929 StreamsLib <> inv_prefix_history thm
|
|
1367
|
R16942:16942 Coq.Init.Datatypes <> S constr
|
|
1368
|
R16945:16945 Coq.Init.Datatypes <> S constr
|
|
1369
|
R16939:16939 StreamsLib <> n var
|
|
1370
|
R16937:16937 StreamsLib <> i var
|
|
1371
|
R16988:17000 StreamsLib <> necessitation def
|
|
1372
|
R16988:17000 StreamsLib <> necessitation def
|
|
1373
|
R0:-1 StreamsLib <> y var
|
|
1374
|
def 17105:17113 <> effective
|
|
1375
|
R17131:17138 Coq.Relations.Relation_Definitions <> relation def
|
|
1376
|
R17140:17140 StreamsLib <> A var
|
|
1377
|
R17161:17162 Coq.Init.Specif <> :type_scope:'{'_x_'}'_'+'_'{'_x_'}' not
|
|
1378
|
R17170:17176 Coq.Init.Specif <> :type_scope:'{'_x_'}'_'+'_'{'_x_'}' not
|
|
1379
|
R17186:17187 Coq.Init.Specif <> :type_scope:'{'_x_'}'_'+'_'{'_x_'}' not
|
|
1380
|
R17163:17163 StreamsLib <> r var
|
|
1381
|
R17168:17169 StreamsLib <> a2 var
|
|
1382
|
R17165:17166 StreamsLib <> a1 var
|
|
1383
|
R17177:17178 Coq.Init.Logic <> :type_scope:'~'_x not
|
|
1384
|
R17179:17179 StreamsLib <> r var
|
|
1385
|
R17184:17185 StreamsLib <> a2 var
|
|
1386
|
R17181:17182 StreamsLib <> a1 var
|
|
1387
|
def 17202:17208 <> lift_hd
|
|
1388
|
R17226:17233 Coq.Relations.Relation_Definitions <> relation def
|
|
1389
|
R17235:17235 StreamsLib <> A var
|
|
1390
|
R17240:17247 Coq.Relations.Relation_Definitions <> relation def
|
|
1391
|
R17250:17255 Coq.Lists.Streams <> Stream coind
|
|
1392
|
R17257:17257 StreamsLib <> A var
|
|
1393
|
R17284:17284 StreamsLib <> r var
|
|
1394
|
R17295:17296 Coq.Lists.Streams <> hd def
|
|
1395
|
R17298:17299 StreamsLib <> s2 var
|
|
1396
|
R17287:17288 Coq.Lists.Streams <> hd def
|
|
1397
|
R17290:17291 StreamsLib <> s1 var
|
|
1398
|
prf 17312:17328 <> lift_hd_effective
|
|
1399
|
R17355:17362 Coq.Relations.Relation_Definitions <> relation def
|
|
1400
|
R17364:17364 StreamsLib <> A var
|
|
1401
|
R17384:17392 StreamsLib <> effective def
|
|
1402
|
R17395:17401 StreamsLib <> lift_hd def
|
|
1403
|
R17403:17403 StreamsLib <> r var
|
|
1404
|
R17369:17377 StreamsLib <> effective def
|
|
1405
|
R17379:17379 StreamsLib <> r var
|
|
1406
|
R17421:17429 StreamsLib <> effective def
|
|
1407
|
R17432:17438 StreamsLib <> lift_hd def
|
|
1408
|
sec 17522:17531 <> FixedPoint
|
|
1409
|
var 17544:17544 FixedPoint A
|
|
1410
|
var 17563:17567 FixedPoint union
|
|
1411
|
R17581:17581 StreamsLib <> FixedPoint.A var
|
|
1412
|
R17576:17576 StreamsLib <> FixedPoint.A var
|
|
1413
|
R17571:17571 StreamsLib <> FixedPoint.A var
|
|
1414
|
var 17594:17595 FixedPoint le
|
|
1415
|
R17599:17606 Coq.Relations.Relation_Definitions <> relation def
|
|
1416
|
R17608:17608 StreamsLib <> FixedPoint.A var
|
|
1417
|
var 17623:17629 FixedPoint le_mono
|
|
1418
|
R17645:17646 StreamsLib <> FixedPoint.le var
|
|
1419
|
R17651:17655 StreamsLib <> FixedPoint.union var
|
|
1420
|
R17659:17659 StreamsLib <> y var
|
|
1421
|
R17657:17657 StreamsLib <> x var
|
|
1422
|
R17648:17648 StreamsLib <> x var
|
|
1423
|
var 17675:17680 FixedPoint le_eff
|
|
1424
|
R17684:17692 StreamsLib <> effective def
|
|
1425
|
R17694:17695 StreamsLib <> FixedPoint.le var
|
|
1426
|
def 17710:17711 <> gt
|
|
1427
|
R17726:17729 Coq.Init.Logic <> :type_scope:x_'/\'_x not
|
|
1428
|
R17720:17721 StreamsLib <> FixedPoint.le var
|
|
1429
|
R17725:17725 StreamsLib <> x var
|
|
1430
|
R17723:17723 StreamsLib <> y var
|
|
1431
|
R17730:17731 Coq.Init.Logic <> :type_scope:'~'_x not
|
|
1432
|
R17732:17733 StreamsLib <> FixedPoint.le var
|
|
1433
|
R17737:17737 StreamsLib <> y var
|
|
1434
|
R17735:17735 StreamsLib <> x var
|
|
1435
|
var 17752:17756 FixedPoint gt_wf
|
|
1436
|
R17760:17771 Coq.Init.Wf <> well_founded def
|
|
1437
|
R17773:17774 StreamsLib <> gt def
|
|
1438
|
fix 17795:17800 <> rec_hd
|
|
1439
|
R17819:17824 Coq.Lists.Streams <> Stream coind
|
|
1440
|
R17826:17826 StreamsLib <> FixedPoint.A var
|
|
1441
|
R17807:17812 Coq.Lists.Streams <> Stream coind
|
|
1442
|
R17814:17814 StreamsLib <> FixedPoint.A var
|
|
1443
|
R17834:17839 Coq.Lists.Streams <> Stream coind
|
|
1444
|
R17841:17841 StreamsLib <> FixedPoint.A var
|
|
1445
|
R17868:17873 Coq.Lists.Streams <> Stream coind
|
|
1446
|
R17875:17875 StreamsLib <> FixedPoint.A var
|
|
1447
|
R17850:17856 StreamsLib <> lift_hd def
|
|
1448
|
R17858:17859 StreamsLib <> gt def
|
|
1449
|
R17891:17895 StreamsLib <> apply def
|
|
1450
|
R17898:17902 StreamsLib <> apply def
|
|
1451
|
R17905:17908 StreamsLib <> lift def
|
|
1452
|
R17910:17914 StreamsLib <> FixedPoint.union var
|
|
1453
|
R17934:17950 StreamsLib <> lift_hd_effective thm
|
|
1454
|
R17959:17960 StreamsLib <> s' var
|
|
1455
|
R17952:17957 StreamsLib <> FixedPoint.le_eff var
|
|
1456
|
R17980:17985 StreamsLib <> rec_hd def
|
|
1457
|
R17989:17990 StreamsLib <> s' var
|
|
1458
|
R17971:17972 StreamsLib <> s' var
|
|
1459
|
R18022:18028 StreamsLib <> lift_hd def
|
|
1460
|
R18039:18046 StreamsLib <> hd_apply thm
|
|
1461
|
R18039:18046 StreamsLib <> hd_apply thm
|
|
1462
|
R18057:18064 StreamsLib <> hd_apply thm
|
|
1463
|
R18057:18064 StreamsLib <> hd_apply thm
|
|
1464
|
R18075:18081 StreamsLib <> hd_lift thm
|
|
1465
|
R18075:18081 StreamsLib <> hd_lift thm
|
|
1466
|
R18091:18092 StreamsLib <> gt def
|
|
1467
|
R18109:18115 StreamsLib <> FixedPoint.le_mono var
|
|
1468
|
R18109:18115 StreamsLib <> FixedPoint.le_mono var
|
|
1469
|
R18127:18133 StreamsLib <> lift_hd def
|
|
1470
|
R18150:18157 StreamsLib <> hd_apply thm
|
|
1471
|
R18150:18157 StreamsLib <> hd_apply thm
|
|
1472
|
R18174:18181 StreamsLib <> hd_apply thm
|
|
1473
|
R18174:18181 StreamsLib <> hd_apply thm
|
|
1474
|
R18198:18204 StreamsLib <> hd_lift thm
|
|
1475
|
R18198:18204 StreamsLib <> hd_lift thm
|
|
1476
|
R18256:18257 Coq.Program.Wf <> MR def
|
|
1477
|
R18266:18281 Coq.Wellfounded.Inverse_Image <> wf_inverse_image thm
|
|
1478
|
R18266:18281 Coq.Wellfounded.Inverse_Image <> wf_inverse_image thm
|
|
1479
|
R18291:18297 StreamsLib <> lift_hd def
|
|
1480
|
R18306:18321 Coq.Wellfounded.Inverse_Image <> wf_inverse_image thm
|
|
1481
|
R18306:18321 Coq.Wellfounded.Inverse_Image <> wf_inverse_image thm
|
|
1482
|
def 18357:18359 <> rec
|
|
1483
|
R18378:18383 Coq.Lists.Streams <> Stream coind
|
|
1484
|
R18385:18385 StreamsLib <> FixedPoint.A var
|
|
1485
|
R18366:18371 Coq.Lists.Streams <> Stream coind
|
|
1486
|
R18373:18373 StreamsLib <> FixedPoint.A var
|
|
1487
|
R18393:18398 Coq.Lists.Streams <> Stream coind
|
|
1488
|
R18400:18400 StreamsLib <> FixedPoint.A var
|
|
1489
|
R18405:18410 Coq.Lists.Streams <> Stream coind
|
|
1490
|
R18412:18412 StreamsLib <> FixedPoint.A var
|
|
1491
|
R18428:18433 StreamsLib <> rec_hd def
|
|
1492
|
R18437:18437 StreamsLib <> s var
|
|
1493
|
R18435:18435 StreamsLib <> f var
|
|
1494
|
R18442:18445 Coq.Lists.Streams <> Cons constr
|
|
1495
|
R18456:18458 StreamsLib <> rec def
|
|
1496
|
R18463:18464 Coq.Lists.Streams <> tl def
|
|
1497
|
R18466:18467 StreamsLib <> s' var
|
|
1498
|
R18460:18460 StreamsLib <> f var
|
|
1499
|
R18448:18449 Coq.Lists.Streams <> hd def
|
|
1500
|
R18451:18452 StreamsLib <> s' var
|
|
1501
|
R18477:18486 StreamsLib FixedPoint <> sec
|