Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / lustre.glob @ 6a93d814

History | View | Annotate | Download (30.1 KB)

1
DIGEST 1249f251c4c818f242231930be50bcc9
2
Flustre
3
R15:19 Coq.Arith.Arith <> <> lib
4
R37:41 Coq.omega.Omega <> <> lib
5
R59:62 Coq.Bool.Bool <> <> lib
6
R80:90 Coq.Arith.Compare_dec <> <> lib
7
R108:113 Coq.Arith.Wf_nat <> <> lib
8
R131:141 Coq.Wellfounded.Wellfounded <> <> lib
9
R159:178 Coq.Relations.Relation_Definitions <> <> lib
10
R196:201 Coq.funind.Recdef <> <> lib
11
R219:228 StreamsLib <> <> lib
12
def 243:251 <> effective
13
R269:276 Coq.Relations.Relation_Definitions <> relation def
14
R278:278 lustre <> A var
15
R299:300 Coq.Init.Specif <> :type_scope:'{'_x_'}'_'+'_'{'_x_'}' not
16
R308:314 Coq.Init.Specif <> :type_scope:'{'_x_'}'_'+'_'{'_x_'}' not
17
R324:325 Coq.Init.Specif <> :type_scope:'{'_x_'}'_'+'_'{'_x_'}' not
18
R301:301 lustre <> r var
19
R306:307 lustre <> a2 var
20
R303:304 lustre <> a1 var
21
R315:316 Coq.Init.Logic <> :type_scope:'~'_x not
22
R317:317 lustre <> r var
23
R322:323 lustre <> a2 var
24
R319:320 lustre <> a1 var
25
ind 339:345 <> element
26
constr 370:372 <> Bot
27
constr 389:391 <> Elt
28
constr 413:415 <> Top
29
R377:383 lustre <> element ind
30
R401:407 lustre <> element ind
31
R420:426 lustre <> element ind
32
def 443:453 <> measure_elt
33
R465:471 lustre <> element ind
34
R473:473 lustre <> A var
35
R478:480 Coq.Init.Datatypes <> nat ind
36
R492:492 lustre <> e var
37
R502:504 lustre <> Bot constr
38
R516:518 lustre <> Elt constr
39
R530:532 lustre <> Top constr
40
def 559:567 <> union_elt
41
R580:588 lustre <> effective def
42
R605:607 Coq.Init.Logic <> :type_scope:x_'='_x not
43
R604:604 lustre <> x var
44
R608:608 lustre <> y var
45
R590:590 lustre <> A var
46
R622:628 lustre <> element ind
47
R630:630 lustre <> A var
48
R636:642 lustre <> element ind
49
R644:644 lustre <> A var
50
R656:656 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
51
R659:660 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
52
R663:663 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
53
R657:658 lustre <> e1 var
54
R661:662 lustre <> e2 var
55
R673:673 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
56
R677:681 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
57
R683:688 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
58
R674:676 lustre <> Bot constr
59
R693:694 lustre <> e2 var
60
R699:699 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
61
R701:707 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
62
R711:714 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
63
R708:710 lustre <> Bot constr
64
R719:720 lustre <> e1 var
65
R725:725 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
66
R732:733 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
67
R740:740 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
68
R726:728 lustre <> Elt constr
69
R734:736 lustre <> Elt constr
70
R748:750 lustre <> eqA var
71
R775:777 lustre <> Top constr
72
R763:765 lustre <> Elt constr
73
R782:782 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
74
R784:790 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
75
R792:797 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
76
R802:804 lustre <> Top constr
77
def 824:832 <> apply_elt
78
R847:853 lustre <> element ind
79
R861:861 lustre <> B var
80
R856:856 lustre <> A var
81
R872:878 lustre <> element ind
82
R880:880 lustre <> A var
83
R886:892 lustre <> element ind
84
R894:894 lustre <> B var
85
R906:906 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
86
R909:910 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
87
R913:913 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
88
R907:908 lustre <> ef var
89
R911:912 lustre <> ex var
90
R923:923 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
91
R927:930 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
92
R932:936 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
93
R924:926 lustre <> Top constr
94
R941:943 lustre <> Top constr
95
R948:948 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
96
R950:955 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
97
R959:961 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
98
R956:958 lustre <> Top constr
99
R966:968 lustre <> Top constr
100
R973:973 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
101
R977:980 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
102
R982:986 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
103
R974:976 lustre <> Bot constr
104
R991:993 lustre <> Bot constr
105
R998:998 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
106
R1000:1005 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
107
R1009:1011 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
108
R1006:1008 lustre <> Bot constr
109
R1016:1018 lustre <> Bot constr
110
R1023:1023 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
111
R1029:1030 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
112
R1036:1036 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
113
R1024:1026 lustre <> Elt constr
114
R1031:1033 lustre <> Elt constr
115
R1041:1043 lustre <> Elt constr
116
def 1069:1077 <> merge_elt
117
R1093:1099 lustre <> element ind
118
R1101:1101 lustre <> A var
119
R1107:1113 lustre <> element ind
120
R1115:1115 lustre <> A var
121
R1127:1127 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
122
R1130:1131 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
123
R1134:1134 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
124
R1128:1129 lustre <> e1 var
125
R1132:1133 lustre <> e2 var
126
R1144:1144 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
127
R1148:1152 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
128
R1154:1159 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
129
R1145:1147 lustre <> Bot constr
130
R1164:1165 lustre <> e2 var
131
R1170:1170 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
132
R1172:1178 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
133
R1182:1185 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
134
R1179:1181 lustre <> Bot constr
135
R1190:1191 lustre <> e1 var
136
R1196:1196 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
137
R1198:1204 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
138
R1206:1211 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
139
R1216:1218 lustre <> Top constr
140
def 1238:1245 <> when_elt
141
R1258:1264 lustre <> element ind
142
R1266:1266 lustre <> A var
143
R1276:1282 lustre <> element ind
144
R1284:1287 Coq.Init.Datatypes <> bool ind
145
R1293:1299 lustre <> element ind
146
R1301:1301 lustre <> A var
147
R1313:1313 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
148
R1316:1317 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
149
R1320:1320 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
150
R1314:1315 lustre <> e1 var
151
R1318:1319 lustre <> e2 var
152
R1330:1330 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
153
R1332:1338 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
154
R1342:1347 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
155
R1339:1341 lustre <> Top constr
156
R1352:1354 lustre <> Top constr
157
R1359:1359 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
158
R1363:1367 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
159
R1369:1376 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
160
R1360:1362 lustre <> Top constr
161
R1381:1383 lustre <> Top constr
162
R1388:1388 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
163
R1390:1396 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
164
R1405:1405 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
165
R1397:1399 lustre <> Elt constr
166
R1401:1404 Coq.Init.Datatypes <> true constr
167
R1410:1411 lustre <> e1 var
168
R1416:1416 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
169
R1418:1424 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
170
R1426:1433 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
171
R1438:1440 lustre <> Bot constr
172
def 1460:1466 <> ite_elt
173
R1479:1485 lustre <> element ind
174
R1487:1490 Coq.Init.Datatypes <> bool ind
175
R1500:1506 lustre <> element ind
176
R1508:1508 lustre <> A var
177
R1518:1524 lustre <> element ind
178
R1526:1526 lustre <> A var
179
R1532:1538 lustre <> element ind
180
R1540:1540 lustre <> A var
181
R1552:1552 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
182
R1555:1556 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
183
R1559:1560 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
184
R1563:1563 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
185
R1553:1554 lustre <> e1 var
186
R1557:1558 lustre <> e2 var
187
R1561:1562 lustre <> e3 var
188
R1573:1573 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
189
R1577:1584 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
190
R1586:1589 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
191
R1591:1593 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
192
R1574:1576 lustre <> Top constr
193
R1598:1600 lustre <> Top constr
194
R1605:1605 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
195
R1607:1616 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
196
R1620:1621 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
197
R1623:1625 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
198
R1617:1619 lustre <> Top constr
199
R1630:1632 lustre <> Top constr
200
R1637:1637 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
201
R1639:1648 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
202
R1650:1653 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
203
R1657:1657 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
204
R1654:1656 lustre <> Top constr
205
R1662:1664 lustre <> Top constr
206
R1669:1669 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
207
R1678:1680 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
208
R1682:1685 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
209
R1687:1689 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
210
R1670:1672 lustre <> Elt constr
211
R1674:1677 Coq.Init.Datatypes <> true constr
212
R1694:1695 lustre <> e2 var
213
R1700:1700 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
214
R1710:1711 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
215
R1713:1716 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
216
R1718:1720 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
217
R1701:1703 lustre <> Elt constr
218
R1705:1709 Coq.Init.Datatypes <> false constr
219
R1725:1726 lustre <> e3 var
220
R1731:1731 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
221
R1735:1742 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
222
R1744:1747 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
223
R1749:1751 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
224
R1732:1734 lustre <> Bot constr
225
R1756:1758 lustre <> Bot constr
226
def 1778:1782 <> undef
227
R1791:1794 StreamsLib <> lift def
228
R1798:1800 lustre <> Bot constr
229
R1802:1802 lustre <> A var
230
def 1816:1820 <> slice
231
R1831:1836 Coq.Lists.Streams <> Stream coind
232
R1840:1846 lustre <> element ind
233
R1848:1848 lustre <> A var
234
R1857:1859 Coq.Init.Datatypes <> nat ind
235
R1875:1880 Coq.Lists.Streams <> Stream coind
236
R1884:1890 lustre <> element ind
237
R1892:1892 lustre <> A var
238
R1905:1905 lustre <> n var
239
R1915:1915 Coq.Init.Datatypes <> O constr
240
R1922:1926 lustre <> undef def
241
R1931:1931 Coq.Init.Datatypes <> S constr
242
R1938:1941 Coq.Lists.Streams <> Cons constr
243
R1951:1955 lustre <> slice def
244
R1958:1959 Coq.Lists.Streams <> tl def
245
R1961:1961 lustre <> s var
246
R1944:1945 Coq.Lists.Streams <> hd def
247
R1947:1947 lustre <> s var
248
prf 1982:1992 <> slice_bisim
249
R2016:2021 Coq.Lists.Streams <> Stream coind
250
R2025:2031 lustre <> element ind
251
R2033:2033 lustre <> A var
252
R2062:2065 Coq.Lists.Streams <> EqSt coind
253
R2081:2085 lustre <> slice def
254
R2090:2090 lustre <> n var
255
R2087:2088 lustre <> s2 var
256
R2068:2072 lustre <> slice def
257
R2077:2077 lustre <> n var
258
R2074:2075 lustre <> s1 var
259
R2038:2041 Coq.Lists.Streams <> EqSt coind
260
R2046:2047 lustre <> s2 var
261
R2043:2044 lustre <> s1 var
262
R2174:2184 Coq.Lists.Streams <> EqSt_reflex thm
263
R2174:2184 Coq.Lists.Streams <> EqSt_reflex thm
264
R2210:2213 Coq.Lists.Streams <> eqst constr
265
R2210:2213 Coq.Lists.Streams <> eqst constr
266
def 2275:2284 <> bisim_upto
267
R2295:2297 Coq.Init.Datatypes <> nat ind
268
R2302:2309 Coq.Relations.Relation_Definitions <> relation def
269
R2312:2317 Coq.Lists.Streams <> Stream coind
270
R2321:2327 lustre <> element ind
271
R2329:2329 lustre <> A var
272
R2357:2360 Coq.Lists.Streams <> EqSt coind
273
R2376:2380 lustre <> slice def
274
R2385:2385 lustre <> n var
275
R2382:2383 lustre <> s2 var
276
R2363:2367 lustre <> slice def
277
R2372:2372 lustre <> n var
278
R2369:2370 lustre <> s1 var
279
prf 2398:2413 <> bisim_bisim_upto
280
R2437:2442 Coq.Lists.Streams <> Stream coind
281
R2446:2452 lustre <> element ind
282
R2454:2454 lustre <> A var
283
R2485:2494 lustre <> bisim_upto def
284
R2501:2502 lustre <> s2 var
285
R2498:2499 lustre <> s1 var
286
R2496:2496 lustre <> n var
287
R2461:2464 Coq.Lists.Streams <> EqSt coind
288
R2469:2470 lustre <> s2 var
289
R2466:2467 lustre <> s1 var
290
R2519:2528 lustre <> bisim_upto def
291
R2604:2614 Coq.Lists.Streams <> EqSt_reflex thm
292
R2604:2614 Coq.Lists.Streams <> EqSt_reflex thm
293
R2640:2643 Coq.Lists.Streams <> eqst constr
294
R2640:2643 Coq.Lists.Streams <> eqst constr
295
prf 2702:2717 <> bisim_upto_bisim
296
R2741:2746 Coq.Lists.Streams <> Stream coind
297
R2750:2756 lustre <> element ind
298
R2758:2758 lustre <> A var
299
R2799:2802 Coq.Lists.Streams <> EqSt coind
300
R2807:2808 lustre <> s2 var
301
R2804:2805 lustre <> s1 var
302
R2776:2785 lustre <> bisim_upto def
303
R2792:2793 lustre <> s2 var
304
R2789:2790 lustre <> s1 var
305
R2787:2787 lustre <> n var
306
R2825:2834 lustre <> bisim_upto def
307
R2890:2893 Coq.Lists.Streams <> eqst constr
308
R2890:2893 Coq.Lists.Streams <> eqst constr
309
R2964:2964 Coq.Init.Datatypes <> S constr
310
R2964:2964 Coq.Init.Datatypes <> S constr
311
def 3003:3009 <> lift_hd
312
R3027:3034 Coq.Relations.Relation_Definitions <> relation def
313
R3036:3036 lustre <> A var
314
R3041:3048 Coq.Relations.Relation_Definitions <> relation def
315
R3051:3056 Coq.Lists.Streams <> Stream coind
316
R3058:3058 lustre <> A var
317
R3085:3085 lustre <> r var
318
R3096:3097 Coq.Lists.Streams <> hd def
319
R3099:3100 lustre <> s2 var
320
R3088:3089 Coq.Lists.Streams <> hd def
321
R3091:3092 lustre <> s1 var
322
prf 3113:3126 <> lift_effective
323
R3153:3160 Coq.Relations.Relation_Definitions <> relation def
324
R3162:3162 lustre <> A var
325
R3184:3192 lustre <> effective def
326
R3206:3212 lustre <> lift_hd def
327
R3216:3216 lustre <> r var
328
R3214:3214 lustre <> A var
329
R3195:3200 Coq.Lists.Streams <> Stream coind
330
R3202:3202 lustre <> A var
331
R3167:3175 lustre <> effective def
332
R3179:3179 lustre <> r var
333
R3177:3177 lustre <> A var
334
R3234:3242 lustre <> effective def
335
R3245:3251 lustre <> lift_hd def
336
def 3338:3343 <> le_elt
337
R3359:3365 lustre <> element ind
338
R3367:3367 lustre <> A var
339
R3388:3391 Coq.Init.Peano <> :nat_scope:x_'>='_x not
340
R3374:3384 lustre <> measure_elt def
341
R3386:3387 lustre <> e1 var
342
R3392:3402 lustre <> measure_elt def
343
R3404:3405 lustre <> e2 var
344
def 3420:3425 <> lt_elt
345
R3441:3447 lustre <> element ind
346
R3449:3449 lustre <> A var
347
R3470:3472 Coq.Init.Peano <> :nat_scope:x_'>'_x not
348
R3456:3466 lustre <> measure_elt def
349
R3468:3469 lustre <> e1 var
350
R3473:3483 lustre <> measure_elt def
351
R3485:3486 lustre <> e2 var
352
prf 3498:3510 <> not_le_lt_elt
353
R3535:3541 lustre <> element ind
354
R3543:3543 lustre <> A var
355
R3566:3571 lustre <> lt_elt def
356
R3576:3577 lustre <> e1 var
357
R3573:3574 lustre <> e2 var
358
R3548:3549 Coq.Init.Logic <> :type_scope:'~'_x not
359
R3550:3555 lustre <> le_elt def
360
R3560:3561 lustre <> e2 var
361
R3557:3558 lustre <> e1 var
362
R3594:3599 lustre <> le_elt def
363
R3602:3607 lustre <> lt_elt def
364
prf 3639:3651 <> lt_not_le_elt
365
R3676:3682 lustre <> element ind
366
R3684:3684 lustre <> A var
367
R3705:3706 Coq.Init.Logic <> :type_scope:'~'_x not
368
R3707:3712 lustre <> le_elt def
369
R3717:3718 lustre <> e1 var
370
R3714:3715 lustre <> e2 var
371
R3689:3694 lustre <> lt_elt def
372
R3699:3700 lustre <> e2 var
373
R3696:3697 lustre <> e1 var
374
R3735:3740 lustre <> le_elt def
375
R3743:3748 lustre <> lt_elt def
376
def 3783:3788 <> gt_elt
377
R3804:3810 lustre <> element ind
378
R3812:3812 lustre <> A var
379
R3818:3823 lustre <> lt_elt def
380
R3828:3829 lustre <> e1 var
381
R3825:3826 lustre <> e2 var
382
prf 3841:3850 <> le_elt_dec
383
R3875:3881 lustre <> element ind
384
R3883:3883 lustre <> A var
385
R3887:3888 Coq.Init.Specif <> :type_scope:'{'_x_'}'_'+'_'{'_x_'}' not
386
R3901:3907 Coq.Init.Specif <> :type_scope:'{'_x_'}'_'+'_'{'_x_'}' not
387
R3920:3921 Coq.Init.Specif <> :type_scope:'{'_x_'}'_'+'_'{'_x_'}' not
388
R3889:3894 lustre <> le_elt def
389
R3899:3900 lustre <> e2 var
390
R3896:3897 lustre <> e1 var
391
R3908:3913 lustre <> lt_elt def
392
R3918:3919 lustre <> e1 var
393
R3915:3916 lustre <> e2 var
394
R3938:3943 lustre <> lt_elt def
395
R3946:3951 lustre <> le_elt def
396
R3954:3955 Coq.Init.Peano <> ge def
397
R3980:3988 Coq.Arith.Compare_dec <> le_lt_dec def
398
R3980:3988 Coq.Arith.Compare_dec <> le_lt_dec def
399
prf 4005:4020 <> le_elt_effective
400
R4036:4044 lustre <> effective def
401
R4059:4064 lustre <> le_elt def
402
R4048:4054 lustre <> element ind
403
R4056:4056 lustre <> A var
404
R4081:4089 lustre <> effective def
405
R4126:4135 lustre <> le_elt_dec thm
406
R4126:4135 lustre <> le_elt_dec thm
407
R4180:4192 lustre <> lt_not_le_elt thm
408
R4180:4192 lustre <> lt_not_le_elt thm
409
prf 4225:4234 <> gt_elt_acc
410
R4250:4261 Coq.Init.Wf <> well_founded def
411
R4265:4270 lustre <> gt_elt def
412
R4272:4272 lustre <> A var
413
R4290:4295 lustre <> gt_elt def
414
R4298:4303 lustre <> lt_elt def
415
R4330:4351 Coq.Arith.Wf_nat <> well_founded_lt_compat thm
416
R4330:4351 Coq.Arith.Wf_nat <> well_founded_lt_compat thm
417
R4361:4362 Coq.Init.Peano <> gt def
418
prf 4410:4418 <> gt_hd_acc
419
R4434:4445 Coq.Init.Wf <> well_founded def
420
R4448:4454 lustre <> lift_hd def
421
R4469:4474 lustre <> gt_elt def
422
R4458:4464 lustre <> element ind
423
R4466:4466 lustre <> A var
424
R4501:4507 lustre <> lift_hd def
425
R4516:4531 Coq.Wellfounded.Inverse_Image <> wf_inverse_image thm
426
R4516:4531 Coq.Wellfounded.Inverse_Image <> wf_inverse_image thm
427
R4540:4549 lustre <> gt_elt_acc thm
428
R4540:4549 lustre <> gt_elt_acc thm
429
mod 4565:4570 <> Signal
430
def 4585:4585 Signal t
431
R4592:4597 Coq.Lists.Streams <> Stream coind
432
R4601:4607 lustre Signal element ind
433
R4609:4609 lustre <> A var
434
def 4625:4629 Signal clock
435
R4634:4639 Coq.Lists.Streams <> Stream coind
436
R4641:4644 Coq.Init.Datatypes <> bool ind
437
def 4898:4902 Signal union
438
R4921:4921 lustre Signal t def
439
R4923:4923 lustre <> A var
440
R4929:4933 StreamsLib <> apply def
441
R4969:4970 lustre <> s2 var
442
R4936:4940 StreamsLib <> apply def
443
R4965:4966 lustre <> s1 var
444
R4943:4946 StreamsLib <> lift def
445
R4949:4957 lustre Signal union_elt def
446
R4959:4961 lustre <> eqA var
447
R5008:5008 lustre Signal t def
448
R5010:5010 lustre <> A var
449
R5001:5001 lustre Signal t def
450
R5003:5003 lustre <> A var
451
R5018:5018 lustre Signal t def
452
R5020:5020 lustre <> A var
453
R5064:5064 lustre Signal t def
454
R5066:5066 lustre <> A var
455
R5082:5086 lustre Signal union def
456
R5095:5095 lustre <> f var
457
R5097:5097 lustre <> s var
458
R5092:5092 lustre <> s var
459
R5088:5090 lustre <> eqA var
460
R5108:5121 lustre Signal lift_effective thm
461
R5147:5147 lustre <> s var
462
R5144:5145 lustre <> s' var
463
R5127:5142 lustre Signal le_elt_effective thm
464
R5165:5170 lustre <> rec_hd def
465
R5180:5181 lustre <> s' var
466
R5178:5178 lustre <> f var
467
R5174:5176 lustre <> eqA var
468
R5172:5172 lustre <> A var
469
R5156:5157 lustre <> s' var
470
R0:-1 lustre <> A var
471
R0:-1 lustre <> y var
472
R0:-1 lustre <> x var
473
R0:-1 lustre <> A var
474
R0:-1 lustre <> A var
475
R0:-1 lustre <> A var
476
R0:-1 lustre <> A var
477
R0:-1 lustre <> A var
478
R0:-1 lustre <> A var
479
R0:-1 lustre <> A var
480
R0:-1 lustre <> y var
481
R0:-1 lustre <> x var
482
R0:-1 lustre <> A var
483
R0:-1 lustre <> A var
484
R0:-1 lustre <> A var
485
R0:-1 lustre <> A var
486
R0:-1 lustre <> A var
487
R5082:5086 lustre Signal union def
488
R5095:5095 lustre <> f var
489
R5097:5097 lustre <> s var
490
R5092:5092 lustre <> s var
491
R5088:5090 lustre <> eqA var
492
R5108:5121 lustre Signal lift_effective thm
493
R5147:5147 lustre <> s var
494
R5144:5145 lustre <> s' var
495
R5127:5142 lustre Signal le_elt_effective thm
496
R5165:5170 lustre <> rec_hd def
497
R5180:5181 lustre <> s' var
498
R5178:5178 lustre <> f var
499
R5174:5176 lustre <> eqA var
500
R5172:5172 lustre <> A var
501
R5156:5157 lustre <> s' var
502
R0:-1 lustre <> A var
503
R0:-1 lustre <> y var
504
R0:-1 lustre <> x var
505
R0:-1 lustre <> A var
506
R0:-1 lustre <> A var
507
R0:-1 lustre <> A var
508
R0:-1 lustre <> A var
509
R0:-1 lustre <> A var
510
R0:-1 lustre <> A var
511
R0:-1 lustre <> A var
512
R0:-1 lustre <> y var
513
R0:-1 lustre <> x var
514
R0:-1 lustre <> A var
515
R0:-1 lustre <> A var
516
R0:-1 lustre <> A var
517
R0:-1 lustre <> A var
518
R0:-1 lustre <> A var
519
R5082:5086 lustre Signal union def
520
R5095:5095 lustre <> f var
521
R5097:5097 lustre <> s var
522
R5092:5092 lustre <> s var
523
R5088:5090 lustre <> eqA var
524
R5108:5121 lustre Signal lift_effective thm
525
R5147:5147 lustre <> s var
526
R5144:5145 lustre <> s' var
527
R5127:5142 lustre Signal le_elt_effective thm
528
R5165:5170 lustre <> rec_hd def
529
R5180:5181 lustre <> s' var
530
R5178:5178 lustre <> f var
531
R5174:5176 lustre <> eqA var
532
R5172:5172 lustre <> A var
533
R5156:5157 lustre <> s' var
534
R0:-1 lustre <> rec_hd def
535
R0:-1 lustre <> s var
536
R0:-1 lustre <> f var
537
R0:-1 lustre <> eqA var
538
R0:-1 lustre <> A var
539
R5029:5035 lustre Signal lift_hd def
540
R5050:5055 lustre Signal gt_elt def
541
R5039:5045 lustre Signal element ind
542
R5208:5214 lustre Signal lift_hd def
543
R5238:5244 lustre Signal lift_hd def
544
R5263:5268 lustre Signal gt_elt def
545
R5286:5298 lustre Signal not_le_lt_elt thm
546
R5286:5298 lustre Signal not_le_lt_elt thm
547
R5332:5340 lustre Signal gt_hd_acc thm
548
R5332:5340 lustre Signal gt_hd_acc thm
549
R0:-1 lustre <> A var
550
R0:-1 lustre <> x var
551
R0:-1 lustre <> y var
552
R0:-1 lustre <> A var
553
R0:-1 lustre <> A var
554
R0:-1 lustre <> A var
555
R0:-1 lustre <> A var
556
R0:-1 lustre <> A var
557
def 5360:5362 Signal rec
558
R5384:5384 lustre Signal t def
559
R5386:5386 lustre <> A var
560
R5377:5377 lustre Signal t def
561
R5379:5379 lustre <> A var
562
R5394:5394 lustre Signal t def
563
R5396:5396 lustre <> A var
564
R5401:5401 lustre Signal t def
565
R5403:5403 lustre <> A var
566
R5419:5424 lustre Signal rec_hd thm
567
R5434:5434 lustre <> s var
568
R5432:5432 lustre <> f var
569
R5428:5430 lustre <> eqA var
570
R5426:5426 lustre <> A var
571
R5439:5442 Coq.Lists.Streams <> Cons constr
572
R5453:5455 lustre <> rec def
573
R5464:5465 Coq.Lists.Streams <> tl def
574
R5467:5468 lustre <> s' var
575
R5461:5461 lustre <> f var
576
R5457:5459 lustre <> eqA var
577
R5445:5446 Coq.Lists.Streams <> hd def
578
R5448:5449 lustre <> s' var
579
def 5485:5488 Signal loop
580
R5510:5510 lustre Signal t def
581
R5512:5512 lustre <> A var
582
R5503:5503 lustre Signal t def
583
R5505:5505 lustre <> A var
584
R5517:5517 lustre Signal t def
585
R5519:5519 lustre <> A var
586
R5525:5527 lustre Signal rec def
587
R5535:5539 lustre Signal undef def
588
R5533:5533 lustre <> f var
589
R5529:5531 lustre <> eqA var
590
def 5554:5560 Signal correct
591
R5571:5571 lustre Signal t def
592
R5573:5573 lustre <> A var
593
R5579:5584 Coq.Lists.Streams <> ForAll coind
594
R5610:5610 lustre <> s var
595
R5596:5597 Coq.Init.Logic <> :type_scope:'~'_x not
596
R5602:5604 Coq.Init.Logic <> :type_scope:x_'='_x not
597
R5598:5599 Coq.Lists.Streams <> hd def
598
R5601:5601 lustre <> s var
599
R5605:5607 lustre Signal Top constr
600
def 5625:5630 Signal _arrow
601
R5635:5638 Coq.Lists.Streams <> Cons constr
602
R5652:5655 StreamsLib <> lift def
603
R5658:5660 lustre Signal Elt constr
604
R5662:5666 Coq.Init.Datatypes <> false constr
605
R5641:5643 lustre Signal Elt constr
606
R5645:5648 Coq.Init.Datatypes <> true constr
607
def 5683:5685 Signal ite
608
R5699:5699 lustre Signal t def
609
R5701:5704 Coq.Init.Datatypes <> bool ind
610
R5724:5724 lustre Signal t def
611
R5726:5726 lustre <> A var
612
R5733:5737 StreamsLib <> apply def
613
R5787:5792 lustre <> s_else var
614
R5740:5744 StreamsLib <> apply def
615
R5779:5784 lustre <> s_then var
616
R5747:5751 StreamsLib <> apply def
617
R5773:5776 lustre <> s_if var
618
R5754:5757 StreamsLib <> lift def
619
R5761:5767 lustre Signal ite_elt def
620
R5769:5769 lustre <> A var
621
prf 5802:5807 Signal hd_ite
622
R5836:5836 lustre Signal t def
623
R5838:5841 Coq.Init.Datatypes <> bool ind
624
R5853:5853 lustre Signal t def
625
R5855:5855 lustre <> A var
626
R5877:5879 Coq.Init.Logic <> :type_scope:x_'='_x not
627
R5860:5861 Coq.Lists.Streams <> hd def
628
R5864:5866 lustre Signal ite def
629
R5874:5875 lustre <> es var
630
R5871:5872 lustre <> ts var
631
R5868:5869 lustre <> cs var
632
R5880:5886 lustre Signal ite_elt def
633
R5905:5906 Coq.Lists.Streams <> hd def
634
R5908:5909 lustre <> es var
635
R5897:5898 Coq.Lists.Streams <> hd def
636
R5900:5901 lustre <> ts var
637
R5889:5890 Coq.Lists.Streams <> hd def
638
R5892:5893 lustre <> cs var
639
prf 5984:5989 Signal tl_ite
640
R6018:6018 lustre Signal t def
641
R6020:6023 Coq.Init.Datatypes <> bool ind
642
R6035:6035 lustre Signal t def
643
R6037:6037 lustre <> A var
644
R6059:6061 Coq.Init.Logic <> :type_scope:x_'='_x not
645
R6042:6043 Coq.Lists.Streams <> tl def
646
R6046:6048 lustre Signal ite def
647
R6056:6057 lustre <> es var
648
R6053:6054 lustre <> ts var
649
R6050:6051 lustre <> cs var
650
R6062:6064 lustre Signal ite def
651
R6083:6084 Coq.Lists.Streams <> tl def
652
R6086:6087 lustre <> es var
653
R6075:6076 Coq.Lists.Streams <> tl def
654
R6078:6079 lustre <> ts var
655
R6067:6068 Coq.Lists.Streams <> tl def
656
R6070:6071 lustre <> cs var
657
prf 6164:6171 Signal eqst_ite
658
R6203:6203 lustre Signal t def
659
R6205:6208 Coq.Init.Datatypes <> bool ind
660
R6226:6226 lustre Signal t def
661
R6228:6228 lustre <> A var
662
R6275:6278 Coq.Lists.Streams <> EqSt coind
663
R6296:6298 lustre Signal ite def
664
R6306:6307 lustre <> e2 var
665
R6303:6304 lustre <> t2 var
666
R6300:6301 lustre <> c2 var
667
R6281:6283 lustre Signal ite def
668
R6291:6292 lustre <> e1 var
669
R6288:6289 lustre <> t1 var
670
R6285:6286 lustre <> c1 var
671
R6261:6264 Coq.Lists.Streams <> EqSt coind
672
R6269:6270 lustre <> e2 var
673
R6266:6267 lustre <> e1 var
674
R6247:6250 Coq.Lists.Streams <> EqSt coind
675
R6255:6256 lustre <> t2 var
676
R6252:6253 lustre <> t1 var
677
R6233:6236 Coq.Lists.Streams <> EqSt coind
678
R6241:6242 lustre <> c2 var
679
R6238:6239 lustre <> c1 var
680
R6332:6341 StreamsLib <> eqst_apply thm
681
R6332:6341 StreamsLib <> eqst_apply thm
682
R6351:6360 StreamsLib <> eqst_apply thm
683
R6351:6360 StreamsLib <> eqst_apply thm
684
R6371:6380 StreamsLib <> eqst_apply thm
685
R6371:6380 StreamsLib <> eqst_apply thm
686
R6392:6402 Coq.Lists.Streams <> EqSt_reflex thm
687
R6392:6402 Coq.Lists.Streams <> EqSt_reflex thm
688
R6461:6466 lustre <> <> mod
689
R6485:6488 Coq.Bool.Bool <> <> lib
690
def 6503:6506 <> bnot
691
R6513:6518 Coq.Lists.Streams <> Stream coind
692
R6520:6523 Coq.Init.Datatypes <> bool ind
693
R6529:6533 StreamsLib <> apply def
694
R6547:6547 lustre <> s var
695
R6536:6539 StreamsLib <> lift def
696
R6541:6544 Coq.Init.Datatypes <> negb def
697
def 6562:6565 <> band
698
R6576:6581 Coq.Lists.Streams <> Stream coind
699
R6583:6586 Coq.Init.Datatypes <> bool ind
700
R6592:6596 StreamsLib <> apply def
701
R6621:6622 lustre <> s2 var
702
R6599:6603 StreamsLib <> apply def
703
R6617:6618 lustre <> s1 var
704
R6606:6609 StreamsLib <> lift def
705
R6611:6614 Coq.Init.Datatypes <> andb def
706
def 6637:6639 <> bor
707
R6650:6655 Coq.Lists.Streams <> Stream coind
708
R6657:6660 Coq.Init.Datatypes <> bool ind
709
R6666:6670 StreamsLib <> apply def
710
R6694:6695 lustre <> s2 var
711
R6673:6677 StreamsLib <> apply def
712
R6690:6691 lustre <> s1 var
713
R6680:6683 StreamsLib <> lift def
714
R6685:6687 Coq.Init.Datatypes <> orb def
715
R6714:6719 Coq.ZArith.ZArith <> <> lib
716
def 6734:6738 <> iplus
717
R6749:6754 Coq.Lists.Streams <> Stream coind
718
R6756:6756 Coq.Numbers.BinNums <> Z ind
719
R6762:6766 StreamsLib <> apply def
720
R6813:6814 lustre <> s2 var
721
R6769:6773 StreamsLib <> apply def
722
R6809:6810 lustre <> s1 var
723
R6776:6779 StreamsLib <> lift def
724
R6798:6800 Coq.ZArith.BinInt <> :Z_scope:x_'+'_x not
725
R6796:6797 lustre <> i1 var
726
R6801:6802 lustre <> i2 var
727
def 6829:6834 <> iminus
728
R6845:6850 Coq.Lists.Streams <> Stream coind
729
R6852:6852 Coq.Numbers.BinNums <> Z ind
730
R6858:6862 StreamsLib <> apply def
731
R6909:6910 lustre <> s2 var
732
R6865:6869 StreamsLib <> apply def
733
R6905:6906 lustre <> s1 var
734
R6872:6875 StreamsLib <> lift def
735
R6894:6896 Coq.ZArith.BinInt <> :Z_scope:x_'-'_x not
736
R6892:6893 lustre <> i1 var
737
R6897:6898 lustre <> i2 var
738
def 6925:6929 <> imult
739
R6940:6945 Coq.Lists.Streams <> Stream coind
740
R6947:6947 Coq.Numbers.BinNums <> Z ind
741
R6953:6957 StreamsLib <> apply def
742
R7004:7005 lustre <> s2 var
743
R6960:6964 StreamsLib <> apply def
744
R7000:7001 lustre <> s1 var
745
R6967:6970 StreamsLib <> lift def
746
R6989:6991 Coq.ZArith.BinInt <> :Z_scope:x_'*'_x not
747
R6987:6988 lustre <> i1 var
748
R6992:6993 lustre <> i2 var
749
def 7020:7023 <> idiv
750
R7034:7039 Coq.Lists.Streams <> Stream coind
751
R7041:7041 Coq.Numbers.BinNums <> Z ind
752
R7047:7051 StreamsLib <> apply def
753
R7098:7099 lustre <> s2 var
754
R7054:7058 StreamsLib <> apply def
755
R7094:7095 lustre <> s1 var
756
R7061:7064 StreamsLib <> lift def
757
R7083:7085 Coq.ZArith.BinInt <> :Z_scope:x_'/'_x not
758
R7081:7082 lustre <> i1 var
759
R7086:7087 lustre <> i2 var
760
def 7114:7117 <> imod
761
R7128:7133 Coq.Lists.Streams <> Stream coind
762
R7135:7135 Coq.Numbers.BinNums <> Z ind
763
R7141:7145 StreamsLib <> apply def
764
R7191:7192 lustre <> s2 var
765
R7148:7152 StreamsLib <> apply def
766
R7187:7188 lustre <> s1 var
767
R7155:7158 StreamsLib <> lift def
768
R7174:7177 Coq.ZArith.Zdiv <> Zmod syndef
769
R7182:7183 lustre <> i2 var
770
R7179:7180 lustre <> i1 var
771
def 7207:7209 <> ieq
772
R7220:7225 Coq.Lists.Streams <> Stream coind
773
R7227:7227 Coq.Numbers.BinNums <> Z ind
774
R7233:7237 StreamsLib <> apply def
775
R7324:7325 lustre <> s2 var
776
R7240:7244 StreamsLib <> apply def
777
R7320:7321 lustre <> s1 var
778
R7247:7250 StreamsLib <> lift def
779
R7275:7278 Coq.ZArith.BinInt <> :Z_scope:x_'?='_x not
780
R7273:7274 lustre <> i1 var
781
R7279:7280 lustre <> i2 var
782
R7290:7291 Coq.Init.Datatypes <> Eq constr
783
R7296:7299 Coq.Init.Datatypes <> true constr
784
R7308:7312 Coq.Init.Datatypes <> false constr
785
def 7340:7342 <> ilt
786
R7353:7358 Coq.Lists.Streams <> Stream coind
787
R7360:7360 Coq.Numbers.BinNums <> Z ind
788
R7366:7370 StreamsLib <> apply def
789
R7457:7458 lustre <> s2 var
790
R7373:7377 StreamsLib <> apply def
791
R7453:7454 lustre <> s1 var
792
R7380:7383 StreamsLib <> lift def
793
R7408:7411 Coq.ZArith.BinInt <> :Z_scope:x_'?='_x not
794
R7406:7407 lustre <> i1 var
795
R7412:7413 lustre <> i2 var
796
R7423:7424 Coq.Init.Datatypes <> Lt constr
797
R7429:7432 Coq.Init.Datatypes <> true constr
798
R7441:7445 Coq.Init.Datatypes <> false constr
799
def 7513:7519 <> denot_f
800
R7532:7537 Coq.Lists.Streams <> Stream coind
801
R7539:7539 Coq.Numbers.BinNums <> Z ind
802
R7546:7546 Coq.Init.Logic <> :type_scope:x_'/\'_x not
803
R7574:7579 Coq.Init.Logic <> :type_scope:x_'/\'_x not
804
R7641:7641 Coq.Init.Logic <> :type_scope:x_'/\'_x not
805
R7547:7550 Coq.Lists.Streams <> EqSt coind
806
R7555:7559 lustre <> iplus def
807
R7564:7567 StreamsLib <> lift def
808
R7561:7561 lustre <> x var
809
R7552:7552 lustre <> y var
810
R7580:7583 Coq.Lists.Streams <> EqSt coind
811
R7590:7594 lustre <> iplus def
812
R7631:7634 StreamsLib <> lift def