-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathProbLogic.glob
320 lines (320 loc) · 11.7 KB
/
ProbLogic.glob
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
DIGEST 69c002cf62921cc9873fb8f572b1ca25
FProbLogic
R52:68 Coq.QArith.QArith <> <> lib
ax 130:130 <> i
ax 172:172 <> W
def 217:222 <> action
R228:231 Coq.Init.Logic <> :type_scope:x_'->'_x not
R232:235 Coq.Init.Datatypes <> list ind
R237:237 ProbLogic <> W defax
R227:227 ProbLogic <> W defax
def 287:287 <> o
R293:296 Coq.Init.Logic <> :type_scope:x_'->'_x not
R292:292 ProbLogic <> W defax
def 342:347 <> mequal
R364:364 ProbLogic <> A var
R377:377 ProbLogic <> W defax
R383:385 Coq.Init.Logic <> :type_scope:x_'='_x not
R382:382 ProbLogic <> x var
R386:386 ProbLogic <> y var
R411:416 ProbLogic <> mequal def
not 398:398 <> ::x_'m='_x
def 471:474 <> mnot
R480:480 ProbLogic <> o def
R486:486 ProbLogic <> W defax
R492:494 Coq.Init.Logic <> :type_scope:'~'_x not
R498:498 Coq.Init.Logic <> :type_scope:'~'_x not
R495:495 ProbLogic <> p var
R497:497 ProbLogic <> w var
R522:525 ProbLogic <> mnot def
not 510:510 <> ::'m~'_x
def 578:581 <> mand
R588:588 ProbLogic <> o def
R594:594 ProbLogic <> W defax
R600:600 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R604:609 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R613:613 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R601:601 ProbLogic <> p var
R603:603 ProbLogic <> w var
R610:610 ProbLogic <> q var
R612:612 ProbLogic <> w var
R639:642 ProbLogic <> mand def
not 625:625 <> ::x_'m/\'_x
def 697:699 <> mor
R706:706 ProbLogic <> o def
R712:712 ProbLogic <> W defax
R718:718 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R722:727 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R731:731 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R719:719 ProbLogic <> p var
R721:721 ProbLogic <> w var
R728:728 ProbLogic <> q var
R730:730 ProbLogic <> w var
R757:759 ProbLogic <> mor def
not 743:743 <> ::x_'m\/'_x
def 814:821 <> mimplies
R828:828 ProbLogic <> o def
R833:833 ProbLogic <> W defax
R839:839 Coq.Init.Logic <> :type_scope:x_'->'_x not
R843:848 Coq.Init.Logic <> :type_scope:x_'->'_x not
R852:852 Coq.Init.Logic <> :type_scope:x_'->'_x not
R849:849 ProbLogic <> q var
R851:851 ProbLogic <> w var
R840:840 ProbLogic <> p var
R842:842 ProbLogic <> w var
R878:885 ProbLogic <> mimplies def
not 864:864 <> ::x_'m->'_x
def 940:945 <> mequiv
R952:952 ProbLogic <> o def
R957:957 ProbLogic <> W defax
R963:963 Coq.Init.Logic <> :type_scope:x_'<->'_x not
R967:973 Coq.Init.Logic <> :type_scope:x_'<->'_x not
R977:977 Coq.Init.Logic <> :type_scope:x_'<->'_x not
R964:964 ProbLogic <> p var
R966:966 ProbLogic <> w var
R974:974 ProbLogic <> q var
R976:976 ProbLogic <> w var
R1004:1009 ProbLogic <> mequiv def
not 989:989 <> ::x_'m<->'_x
def 1090:1090 <> A
R1106:1109 Coq.Init.Logic <> :type_scope:x_'->'_x not
R1110:1110 ProbLogic <> o def
R1105:1105 ProbLogic <> t var
R1116:1116 ProbLogic <> W defax
R1132:1132 ProbLogic <> p var
R1136:1136 ProbLogic <> w var
R1134:1134 ProbLogic <> x var
R1171:1171 ProbLogic <> A def
not 1148:1148 <> :type_scope:'mforall'_x_','_x
R1283:1283 ProbLogic <> A def
not 1257:1257 <> :type_scope:'mforall'_x_':'_x_','_x
def 1434:1434 <> E
R1450:1453 Coq.Init.Logic <> :type_scope:x_'->'_x not
R1454:1454 ProbLogic <> o def
R1449:1449 ProbLogic <> t var
R1460:1460 ProbLogic <> W defax
R1466:1472 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R1474:1475 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R1476:1476 ProbLogic <> p var
R1480:1480 ProbLogic <> w var
R1478:1478 ProbLogic <> x var
R1514:1514 ProbLogic <> E def
not 1492:1492 <> :type_scope:'mexists'_x_','_x
R1626:1626 ProbLogic <> E def
not 1600:1600 <> :type_scope:'mexists'_x_':'_x_','_x
def 1775:1779 <> is_in
R1795:1795 ProbLogic <> A var
R1802:1805 Coq.Init.Datatypes <> list ind
R1807:1807 ProbLogic <> A var
R1819:1819 ProbLogic <> l var
R1831:1833 Coq.Init.Datatypes <> nil constr
R1838:1842 Coq.Init.Logic <> False ind
R1849:1852 Coq.Init.Datatypes <> cons constr
R1870:1874 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R1887:1887 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R1866:1868 Coq.Init.Logic <> :type_scope:x_'='_x not
R1865:1865 ProbLogic <> x var
R1875:1879 ProbLogic <> is_in def
R1881:1881 ProbLogic <> x var
def 1952:1952 <> r
R1958:1958 ProbLogic <> W defax
R1965:1970 ProbLogic <> action def
R1978:1978 ProbLogic <> W defax
R1985:1989 ProbLogic <> is_in def
R1995:1995 ProbLogic <> a var
R1997:1997 ProbLogic <> w var
R1991:1992 ProbLogic <> w1 var
def 2054:2056 <> box
R2062:2067 ProbLogic <> action def
R2074:2074 ProbLogic <> o def
R2100:2100 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2109:2114 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2119:2119 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2115:2115 ProbLogic <> p var
R2117:2118 ProbLogic <> w1 var
R2101:2101 ProbLogic <> r def
R2107:2108 ProbLogic <> w1 var
R2105:2105 ProbLogic <> a var
R2103:2103 ProbLogic <> w var
def 2170:2172 <> dia
R2178:2183 ProbLogic <> action def
R2190:2190 ProbLogic <> o def
R2205:2211 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R2214:2215 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R2216:2216 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R2225:2230 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R2235:2235 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R2217:2217 ProbLogic <> r def
R2223:2224 ProbLogic <> w1 var
R2221:2221 ProbLogic <> a var
R2219:2219 ProbLogic <> w var
R2231:2231 ProbLogic <> p var
R2233:2234 ProbLogic <> w1 var
def 2283:2284 <> At
R2290:2290 ProbLogic <> W defax
R2297:2297 ProbLogic <> o def
R2310:2310 ProbLogic <> W defax
R2316:2316 ProbLogic <> f var
R2318:2318 ProbLogic <> s var
def 2380:2380 <> V
R2386:2386 ProbLogic <> o def
R2402:2402 ProbLogic <> p var
R2404:2404 ProbLogic <> w var
R2428:2428 ProbLogic <> V def
not 2416:2416 <> ::'['_x_']'
R2466:2466 ProbLogic <> V def
R2466:2466 ProbLogic <> V def
R2702:2704 ProbLogic <> box def
R2702:2704 ProbLogic <> box def
R3088:3093 ProbLogic <> mequal def
R3095:3102 ProbLogic <> mimplies def
R3104:3107 ProbLogic <> mnot def
R3109:3111 ProbLogic <> mor def
R3113:3116 ProbLogic <> mand def
R3118:3120 ProbLogic <> dia def
R3122:3124 ProbLogic <> box def
R3126:3126 ProbLogic <> A def
R3128:3128 ProbLogic <> E def
R3130:3130 ProbLogic <> V def
ax 3185:3187 <> dec
R3201:3201 ProbLogic <> o def
R3208:3208 ProbLogic <> W defax
R3212:3212 Coq.Init.Specif <> :type_scope:'{'_x_'}'_'+'_'{'_x_'}' not
R3216:3220 Coq.Init.Specif <> :type_scope:'{'_x_'}'_'+'_'{'_x_'}' not
R3228:3228 Coq.Init.Specif <> :type_scope:'{'_x_'}'_'+'_'{'_x_'}' not
R3213:3213 ProbLogic <> f var
R3215:3215 ProbLogic <> w var
R3221:3223 Coq.Init.Logic <> :type_scope:'~'_x not
R3227:3227 Coq.Init.Logic <> :type_scope:'~'_x not
R3224:3224 ProbLogic <> f var
R3226:3226 ProbLogic <> w var
ax 3242:3248 <> decProp
R3267:3267 Coq.Init.Specif <> :type_scope:'{'_x_'}'_'+'_'{'_x_'}' not
R3269:3273 Coq.Init.Specif <> :type_scope:'{'_x_'}'_'+'_'{'_x_'}' not
R3276:3276 Coq.Init.Specif <> :type_scope:'{'_x_'}'_'+'_'{'_x_'}' not
R3268:3268 ProbLogic <> f var
R3274:3274 Coq.Init.Logic <> :type_scope:'~'_x not
R3275:3275 ProbLogic <> f var
def 3291:3293 <> map
R3315:3318 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3319:3320 ProbLogic <> T2 var
R3313:3314 ProbLogic <> T1 var
R3327:3330 Coq.Init.Datatypes <> list ind
R3332:3333 ProbLogic <> T1 var
R3345:3345 ProbLogic <> l var
R3357:3359 Coq.Init.Datatypes <> nil constr
R3364:3366 Coq.Init.Datatypes <> nil constr
R3373:3376 Coq.Init.Datatypes <> cons constr
R3393:3396 Coq.Init.Datatypes <> cons constr
R3408:3410 ProbLogic <> map def
R3412:3412 ProbLogic <> f var
R3399:3399 ProbLogic <> f var
def 3436:3444 <> summation
R3450:3453 Coq.Init.Datatypes <> list ind
R3455:3455 Coq.QArith.QArith_base <> Q rec
R3467:3467 ProbLogic <> l var
R3478:3480 Coq.Init.Datatypes <> nil constr
R3492:3495 Coq.Init.Datatypes <> cons constr
R3515:3518 Coq.QArith.QArith_base <> :Q_scope:x_'+'_x not
R3533:3533 Coq.QArith.QArith_base <> :Q_scope:x_'+'_x not
R3519:3527 ProbLogic <> summation def
def 3551:3554 <> prob
R3560:3560 ProbLogic <> o def
R3567:3570 Coq.Init.Datatypes <> list ind
R3572:3577 ProbLogic <> action def
R3584:3584 ProbLogic <> W defax
R3596:3596 ProbLogic <> l var
R3607:3609 Coq.Init.Datatypes <> nil constr
R3618:3620 ProbLogic <> dec defax
R3624:3624 ProbLogic <> w var
R3622:3622 ProbLogic <> f var
R3646:3649 Coq.Init.Datatypes <> cons constr
R3662:3662 Coq.QArith.QArith_base <> :Q_scope:x_'/'_x not
R3698:3702 Coq.QArith.QArith_base <> :Q_scope:x_'/'_x not
R3733:3734 Coq.QArith.QArith_base <> :Q_scope:x_'/'_x not
R3663:3671 ProbLogic <> summation def
R3674:3676 ProbLogic <> map def
R3695:3695 ProbLogic <> w var
R3679:3682 ProbLogic <> prob def
R3684:3684 ProbLogic <> f var
R3703:3703 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R3728:3731 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R3704:3711 Coq.ZArith.BinInt Z of_nat def
R3714:3719 Coq.Init.Datatypes <> length def
R3724:3724 ProbLogic <> w var
def 3755:3762 <> probPred
R3768:3768 ProbLogic <> o def
R3775:3778 Coq.Init.Datatypes <> list ind
R3780:3785 ProbLogic <> action def
R3796:3796 Coq.QArith.QArith_base <> Q rec
R3803:3803 ProbLogic <> W defax
R3809:3809 Coq.QArith.QArith_base <> :Q_scope:x_'=='_x not
R3820:3824 Coq.QArith.QArith_base <> :Q_scope:x_'=='_x not
R3810:3813 ProbLogic <> prob def
R3819:3819 ProbLogic <> w var
R3817:3817 ProbLogic <> l var
R3815:3815 ProbLogic <> f var
R3825:3829 ProbLogic <> value var
prf 3868:3873 <> mp_dia
R3876:3876 ProbLogic <> ::'['_x_']' not
R3955:3955 ProbLogic <> ::'['_x_']' not
R3877:3884 ProbLogic <> :type_scope:'mforall'_x_','_x not
R3886:3887 ProbLogic <> :type_scope:'mforall'_x_','_x not
R3888:3895 ProbLogic <> :type_scope:'mforall'_x_','_x not
R3897:3898 ProbLogic <> :type_scope:'mforall'_x_','_x not
R3899:3906 ProbLogic <> :type_scope:'mforall'_x_','_x not
R3908:3909 ProbLogic <> :type_scope:'mforall'_x_','_x not
R3910:3910 ProbLogic <> ::x_'m->'_x not
R3918:3923 ProbLogic <> ::x_'m->'_x not
R3911:3913 ProbLogic <> dia def
R3924:3924 ProbLogic <> ::x_'m->'_x not
R3940:3946 ProbLogic <> ::x_'m->'_x not
R3954:3954 ProbLogic <> ::x_'m->'_x not
R3925:3927 ProbLogic <> box def
R3933:3937 ProbLogic <> ::x_'m->'_x not
R3947:3949 ProbLogic <> dia def
prf 4126:4140 <> not_dia_box_not
R4143:4143 ProbLogic <> ::'['_x_']' not
R4199:4199 ProbLogic <> ::'['_x_']' not
R4144:4151 ProbLogic <> :type_scope:'mforall'_x_','_x not
R4153:4154 ProbLogic <> :type_scope:'mforall'_x_','_x not
R4155:4162 ProbLogic <> :type_scope:'mforall'_x_','_x not
R4164:4165 ProbLogic <> :type_scope:'mforall'_x_','_x not
R4166:4166 ProbLogic <> ::x_'m->'_x not
R4179:4185 ProbLogic <> ::x_'m->'_x not
R4198:4198 ProbLogic <> ::x_'m->'_x not
R4167:4170 ProbLogic <> ::'m~'_x not
R4178:4178 ProbLogic <> ::'m~'_x not
R4171:4173 ProbLogic <> dia def
R4186:4188 ProbLogic <> box def
R4193:4195 ProbLogic <> ::'m~'_x not
prf 4356:4370 <> box_not_not_dia
R4373:4374 ProbLogic <> ::'['_x_']' not
R4430:4431 ProbLogic <> ::'['_x_']' not
R4375:4382 ProbLogic <> :type_scope:'mforall'_x_','_x not
R4384:4385 ProbLogic <> :type_scope:'mforall'_x_','_x not
R4386:4393 ProbLogic <> :type_scope:'mforall'_x_','_x not
R4395:4396 ProbLogic <> :type_scope:'mforall'_x_','_x not
R4397:4397 ProbLogic <> ::x_'m->'_x not
R4410:4416 ProbLogic <> ::x_'m->'_x not
R4429:4429 ProbLogic <> ::x_'m->'_x not
R4398:4400 ProbLogic <> box def
R4405:4407 ProbLogic <> ::'m~'_x not
R4417:4420 ProbLogic <> ::'m~'_x not
R4428:4428 ProbLogic <> ::'m~'_x not
R4421:4423 ProbLogic <> dia def
prf 4602:4616 <> dia_not_not_box
R4619:4620 ProbLogic <> ::'['_x_']' not
R4676:4677 ProbLogic <> ::'['_x_']' not
R4621:4628 ProbLogic <> :type_scope:'mforall'_x_','_x not
R4630:4631 ProbLogic <> :type_scope:'mforall'_x_','_x not
R4632:4639 ProbLogic <> :type_scope:'mforall'_x_','_x not
R4641:4642 ProbLogic <> :type_scope:'mforall'_x_','_x not
R4643:4643 ProbLogic <> ::x_'m->'_x not
R4656:4662 ProbLogic <> ::x_'m->'_x not
R4675:4675 ProbLogic <> ::x_'m->'_x not
R4644:4646 ProbLogic <> dia def
R4651:4653 ProbLogic <> ::'m~'_x not
R4663:4666 ProbLogic <> ::'m~'_x not
R4674:4674 ProbLogic <> ::'m~'_x not
R4667:4669 ProbLogic <> box def