OAI/Analysis/MutuallyUnbiased/MixedSemantics/Canonical3.lean

GitHub source file

786 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.raw384 line 20
2. def OAI.MUB6.Certificate.MixedSemantics.raw384Labels line 21
3. def OAI.MUB6.Certificate.MixedSemantics.raw384step0 line 23
4. def OAI.MUB6.Certificate.MixedSemantics.raw384step0Labels line 24
5. def OAI.MUB6.Certificate.MixedSemantics.raw384step1 line 26
6. def OAI.MUB6.Certificate.MixedSemantics.raw384step1Labels line 27
7. theorem OAI.MUB6.Certificate.MixedSemantics.canonical384 line 29
8. def OAI.MUB6.Certificate.MixedSemantics.raw385 line 44
9. def OAI.MUB6.Certificate.MixedSemantics.raw385Labels line 45
10. def OAI.MUB6.Certificate.MixedSemantics.raw385step0 line 47
11. def OAI.MUB6.Certificate.MixedSemantics.raw385step0Labels line 48
12. theorem OAI.MUB6.Certificate.MixedSemantics.canonical385 line 50
13. def OAI.MUB6.Certificate.MixedSemantics.raw386 line 60
14. def OAI.MUB6.Certificate.MixedSemantics.raw386Labels line 61
15. def OAI.MUB6.Certificate.MixedSemantics.raw386step0 line 63
16. def OAI.MUB6.Certificate.MixedSemantics.raw386step0Labels line 64
17. def OAI.MUB6.Certificate.MixedSemantics.raw386step1 line 66
18. def OAI.MUB6.Certificate.MixedSemantics.raw386step1Labels line 67
19. theorem OAI.MUB6.Certificate.MixedSemantics.canonical386 line 69
20. def OAI.MUB6.Certificate.MixedSemantics.raw387 line 84
21. def OAI.MUB6.Certificate.MixedSemantics.raw387Labels line 85
22. def OAI.MUB6.Certificate.MixedSemantics.raw387step0 line 87
23. def OAI.MUB6.Certificate.MixedSemantics.raw387step0Labels line 88
24. theorem OAI.MUB6.Certificate.MixedSemantics.canonical387 line 90
25. def OAI.MUB6.Certificate.MixedSemantics.raw388 line 100
26. def OAI.MUB6.Certificate.MixedSemantics.raw388Labels line 101
27. def OAI.MUB6.Certificate.MixedSemantics.raw388step0 line 103
28. def OAI.MUB6.Certificate.MixedSemantics.raw388step0Labels line 104
29. def OAI.MUB6.Certificate.MixedSemantics.raw388step1 line 106
30. def OAI.MUB6.Certificate.MixedSemantics.raw388step1Labels line 107
31. theorem OAI.MUB6.Certificate.MixedSemantics.canonical388 line 109
32. def OAI.MUB6.Certificate.MixedSemantics.raw389 line 124
33. def OAI.MUB6.Certificate.MixedSemantics.raw389Labels line 125
34. def OAI.MUB6.Certificate.MixedSemantics.raw389step0 line 127
35. def OAI.MUB6.Certificate.MixedSemantics.raw389step0Labels line 128
36. theorem OAI.MUB6.Certificate.MixedSemantics.canonical389 line 130
37. def OAI.MUB6.Certificate.MixedSemantics.raw390 line 140
38. def OAI.MUB6.Certificate.MixedSemantics.raw390Labels line 141
39. def OAI.MUB6.Certificate.MixedSemantics.raw390step0 line 143
40. def OAI.MUB6.Certificate.MixedSemantics.raw390step0Labels line 144
41. def OAI.MUB6.Certificate.MixedSemantics.raw390step1 line 146
42. def OAI.MUB6.Certificate.MixedSemantics.raw390step1Labels line 147
43. theorem OAI.MUB6.Certificate.MixedSemantics.canonical390 line 149
44. def OAI.MUB6.Certificate.MixedSemantics.raw391 line 164
45. def OAI.MUB6.Certificate.MixedSemantics.raw391Labels line 165
46. def OAI.MUB6.Certificate.MixedSemantics.raw391step0 line 167
47. def OAI.MUB6.Certificate.MixedSemantics.raw391step0Labels line 168
48. theorem OAI.MUB6.Certificate.MixedSemantics.canonical391 line 170
49. def OAI.MUB6.Certificate.MixedSemantics.raw392 line 180
50. def OAI.MUB6.Certificate.MixedSemantics.raw392Labels line 181
51. def OAI.MUB6.Certificate.MixedSemantics.raw392step0 line 183
52. def OAI.MUB6.Certificate.MixedSemantics.raw392step0Labels line 184
53. def OAI.MUB6.Certificate.MixedSemantics.raw392step1 line 186
54. def OAI.MUB6.Certificate.MixedSemantics.raw392step1Labels line 187
55. theorem OAI.MUB6.Certificate.MixedSemantics.canonical392 line 189
56. def OAI.MUB6.Certificate.MixedSemantics.raw393 line 204
57. def OAI.MUB6.Certificate.MixedSemantics.raw393Labels line 205
58. def OAI.MUB6.Certificate.MixedSemantics.raw393step0 line 207
59. def OAI.MUB6.Certificate.MixedSemantics.raw393step0Labels line 208
60. theorem OAI.MUB6.Certificate.MixedSemantics.canonical393 line 210
61. def OAI.MUB6.Certificate.MixedSemantics.raw394 line 220
62. def OAI.MUB6.Certificate.MixedSemantics.raw394Labels line 221
63. def OAI.MUB6.Certificate.MixedSemantics.raw394step0 line 223
64. def OAI.MUB6.Certificate.MixedSemantics.raw394step0Labels line 224
65. def OAI.MUB6.Certificate.MixedSemantics.raw394step1 line 226
66. def OAI.MUB6.Certificate.MixedSemantics.raw394step1Labels line 227
67. theorem OAI.MUB6.Certificate.MixedSemantics.canonical394 line 229
68. def OAI.MUB6.Certificate.MixedSemantics.raw395 line 244
69. def OAI.MUB6.Certificate.MixedSemantics.raw395Labels line 245
70. def OAI.MUB6.Certificate.MixedSemantics.raw395step0 line 247
71. def OAI.MUB6.Certificate.MixedSemantics.raw395step0Labels line 248
72. theorem OAI.MUB6.Certificate.MixedSemantics.canonical395 line 250
73. def OAI.MUB6.Certificate.MixedSemantics.raw396 line 260
74. def OAI.MUB6.Certificate.MixedSemantics.raw396Labels line 261
75. def OAI.MUB6.Certificate.MixedSemantics.raw396step0 line 263
76. def OAI.MUB6.Certificate.MixedSemantics.raw396step0Labels line 264
77. def OAI.MUB6.Certificate.MixedSemantics.raw396step1 line 266
78. def OAI.MUB6.Certificate.MixedSemantics.raw396step1Labels line 267
79. theorem OAI.MUB6.Certificate.MixedSemantics.canonical396 line 269
80. def OAI.MUB6.Certificate.MixedSemantics.raw397 line 284
81. def OAI.MUB6.Certificate.MixedSemantics.raw397Labels line 285
82. def OAI.MUB6.Certificate.MixedSemantics.raw397step0 line 287
83. def OAI.MUB6.Certificate.MixedSemantics.raw397step0Labels line 288
84. theorem OAI.MUB6.Certificate.MixedSemantics.canonical397 line 290
85. def OAI.MUB6.Certificate.MixedSemantics.raw398 line 300
86. def OAI.MUB6.Certificate.MixedSemantics.raw398Labels line 301
87. def OAI.MUB6.Certificate.MixedSemantics.raw398step0 line 303
88. def OAI.MUB6.Certificate.MixedSemantics.raw398step0Labels line 304
89. def OAI.MUB6.Certificate.MixedSemantics.raw398step1 line 306
90. def OAI.MUB6.Certificate.MixedSemantics.raw398step1Labels line 307
91. theorem OAI.MUB6.Certificate.MixedSemantics.canonical398 line 309
92. def OAI.MUB6.Certificate.MixedSemantics.raw399 line 324
93. def OAI.MUB6.Certificate.MixedSemantics.raw399Labels line 325
94. def OAI.MUB6.Certificate.MixedSemantics.raw399step0 line 327
95. def OAI.MUB6.Certificate.MixedSemantics.raw399step0Labels line 328
96. theorem OAI.MUB6.Certificate.MixedSemantics.canonical399 line 330
97. def OAI.MUB6.Certificate.MixedSemantics.raw400 line 340
98. def OAI.MUB6.Certificate.MixedSemantics.raw400Labels line 341
99. def OAI.MUB6.Certificate.MixedSemantics.raw400step0 line 343
100. def OAI.MUB6.Certificate.MixedSemantics.raw400step0Labels line 344
101. def OAI.MUB6.Certificate.MixedSemantics.raw400step1 line 346
102. def OAI.MUB6.Certificate.MixedSemantics.raw400step1Labels line 347
103. theorem OAI.MUB6.Certificate.MixedSemantics.canonical400 line 349
104. def OAI.MUB6.Certificate.MixedSemantics.raw401 line 364
105. def OAI.MUB6.Certificate.MixedSemantics.raw401Labels line 365
106. def OAI.MUB6.Certificate.MixedSemantics.raw401step0 line 367
107. def OAI.MUB6.Certificate.MixedSemantics.raw401step0Labels line 368
108. theorem OAI.MUB6.Certificate.MixedSemantics.canonical401 line 370
109. def OAI.MUB6.Certificate.MixedSemantics.raw402 line 380
110. def OAI.MUB6.Certificate.MixedSemantics.raw402Labels line 381
111. def OAI.MUB6.Certificate.MixedSemantics.raw402step0 line 383
112. def OAI.MUB6.Certificate.MixedSemantics.raw402step0Labels line 384
113. def OAI.MUB6.Certificate.MixedSemantics.raw402step1 line 386
114. def OAI.MUB6.Certificate.MixedSemantics.raw402step1Labels line 387
115. theorem OAI.MUB6.Certificate.MixedSemantics.canonical402 line 389
116. def OAI.MUB6.Certificate.MixedSemantics.raw403 line 404
117. def OAI.MUB6.Certificate.MixedSemantics.raw403Labels line 405
118. def OAI.MUB6.Certificate.MixedSemantics.raw403step0 line 407
119. def OAI.MUB6.Certificate.MixedSemantics.raw403step0Labels line 408
120. theorem OAI.MUB6.Certificate.MixedSemantics.canonical403 line 410
121. def OAI.MUB6.Certificate.MixedSemantics.raw404 line 420
122. def OAI.MUB6.Certificate.MixedSemantics.raw404Labels line 421
123. def OAI.MUB6.Certificate.MixedSemantics.raw404step0 line 423
124. def OAI.MUB6.Certificate.MixedSemantics.raw404step0Labels line 424
125. def OAI.MUB6.Certificate.MixedSemantics.raw404step1 line 426
126. def OAI.MUB6.Certificate.MixedSemantics.raw404step1Labels line 427
127. theorem OAI.MUB6.Certificate.MixedSemantics.canonical404 line 429
128. def OAI.MUB6.Certificate.MixedSemantics.raw405 line 444
129. def OAI.MUB6.Certificate.MixedSemantics.raw405Labels line 445
130. def OAI.MUB6.Certificate.MixedSemantics.raw405step0 line 447
131. def OAI.MUB6.Certificate.MixedSemantics.raw405step0Labels line 448
132. theorem OAI.MUB6.Certificate.MixedSemantics.canonical405 line 450
133. def OAI.MUB6.Certificate.MixedSemantics.raw406 line 460
134. def OAI.MUB6.Certificate.MixedSemantics.raw406Labels line 461
135. def OAI.MUB6.Certificate.MixedSemantics.raw406step0 line 463
136. def OAI.MUB6.Certificate.MixedSemantics.raw406step0Labels line 464
137. def OAI.MUB6.Certificate.MixedSemantics.raw406step1 line 466
138. def OAI.MUB6.Certificate.MixedSemantics.raw406step1Labels line 467
139. theorem OAI.MUB6.Certificate.MixedSemantics.canonical406 line 469
140. def OAI.MUB6.Certificate.MixedSemantics.raw407 line 484
141. def OAI.MUB6.Certificate.MixedSemantics.raw407Labels line 485
142. def OAI.MUB6.Certificate.MixedSemantics.raw407step0 line 487
143. def OAI.MUB6.Certificate.MixedSemantics.raw407step0Labels line 488
144. theorem OAI.MUB6.Certificate.MixedSemantics.canonical407 line 490
145. def OAI.MUB6.Certificate.MixedSemantics.raw408 line 500
146. def OAI.MUB6.Certificate.MixedSemantics.raw408Labels line 501
147. def OAI.MUB6.Certificate.MixedSemantics.raw408step0 line 503
148. def OAI.MUB6.Certificate.MixedSemantics.raw408step0Labels line 504
149. def OAI.MUB6.Certificate.MixedSemantics.raw408step1 line 506
150. def OAI.MUB6.Certificate.MixedSemantics.raw408step1Labels line 507
151. theorem OAI.MUB6.Certificate.MixedSemantics.canonical408 line 509
152. def OAI.MUB6.Certificate.MixedSemantics.raw409 line 524
153. def OAI.MUB6.Certificate.MixedSemantics.raw409Labels line 525
154. def OAI.MUB6.Certificate.MixedSemantics.raw409step0 line 527
155. def OAI.MUB6.Certificate.MixedSemantics.raw409step0Labels line 528
156. theorem OAI.MUB6.Certificate.MixedSemantics.canonical409 line 530
157. def OAI.MUB6.Certificate.MixedSemantics.raw410 line 540
158. def OAI.MUB6.Certificate.MixedSemantics.raw410Labels line 541
159. def OAI.MUB6.Certificate.MixedSemantics.raw410step0 line 543
160. def OAI.MUB6.Certificate.MixedSemantics.raw410step0Labels line 544
161. def OAI.MUB6.Certificate.MixedSemantics.raw410step1 line 546
162. def OAI.MUB6.Certificate.MixedSemantics.raw410step1Labels line 547
163. theorem OAI.MUB6.Certificate.MixedSemantics.canonical410 line 549
164. def OAI.MUB6.Certificate.MixedSemantics.raw411 line 564
165. def OAI.MUB6.Certificate.MixedSemantics.raw411Labels line 565
166. def OAI.MUB6.Certificate.MixedSemantics.raw411step0 line 567
167. def OAI.MUB6.Certificate.MixedSemantics.raw411step0Labels line 568
168. theorem OAI.MUB6.Certificate.MixedSemantics.canonical411 line 570
169. def OAI.MUB6.Certificate.MixedSemantics.raw412 line 580
170. def OAI.MUB6.Certificate.MixedSemantics.raw412Labels line 581
171. def OAI.MUB6.Certificate.MixedSemantics.raw412step0 line 583
172. def OAI.MUB6.Certificate.MixedSemantics.raw412step0Labels line 584
173. def OAI.MUB6.Certificate.MixedSemantics.raw412step1 line 586
174. def OAI.MUB6.Certificate.MixedSemantics.raw412step1Labels line 587
175. theorem OAI.MUB6.Certificate.MixedSemantics.canonical412 line 589
176. def OAI.MUB6.Certificate.MixedSemantics.raw413 line 604
177. def OAI.MUB6.Certificate.MixedSemantics.raw413Labels line 605
178. def OAI.MUB6.Certificate.MixedSemantics.raw413step0 line 607
179. def OAI.MUB6.Certificate.MixedSemantics.raw413step0Labels line 608
180. theorem OAI.MUB6.Certificate.MixedSemantics.canonical413 line 610
181. def OAI.MUB6.Certificate.MixedSemantics.raw414 line 620
182. def OAI.MUB6.Certificate.MixedSemantics.raw414Labels line 621
183. def OAI.MUB6.Certificate.MixedSemantics.raw414step0 line 623
184. def OAI.MUB6.Certificate.MixedSemantics.raw414step0Labels line 624
185. def OAI.MUB6.Certificate.MixedSemantics.raw414step1 line 626
186. def OAI.MUB6.Certificate.MixedSemantics.raw414step1Labels line 627
187. theorem OAI.MUB6.Certificate.MixedSemantics.canonical414 line 629
188. def OAI.MUB6.Certificate.MixedSemantics.raw415 line 644
189. def OAI.MUB6.Certificate.MixedSemantics.raw415Labels line 645
190. def OAI.MUB6.Certificate.MixedSemantics.raw415step0 line 647
191. def OAI.MUB6.Certificate.MixedSemantics.raw415step0Labels line 648
192. theorem OAI.MUB6.Certificate.MixedSemantics.canonical415 line 650
193. def OAI.MUB6.Certificate.MixedSemantics.raw416 line 660
194. def OAI.MUB6.Certificate.MixedSemantics.raw416Labels line 661
195. def OAI.MUB6.Certificate.MixedSemantics.raw416step0 line 663
196. def OAI.MUB6.Certificate.MixedSemantics.raw416step0Labels line 664
197. def OAI.MUB6.Certificate.MixedSemantics.raw416step1 line 666
198. def OAI.MUB6.Certificate.MixedSemantics.raw416step1Labels line 667
199. theorem OAI.MUB6.Certificate.MixedSemantics.canonical416 line 669
200. def OAI.MUB6.Certificate.MixedSemantics.raw417 line 684
201. def OAI.MUB6.Certificate.MixedSemantics.raw417Labels line 685
202. def OAI.MUB6.Certificate.MixedSemantics.raw417step0 line 687
203. def OAI.MUB6.Certificate.MixedSemantics.raw417step0Labels line 688
204. theorem OAI.MUB6.Certificate.MixedSemantics.canonical417 line 690
205. def OAI.MUB6.Certificate.MixedSemantics.raw418 line 700
206. def OAI.MUB6.Certificate.MixedSemantics.raw418Labels line 701
207. def OAI.MUB6.Certificate.MixedSemantics.raw418step0 line 703
208. def OAI.MUB6.Certificate.MixedSemantics.raw418step0Labels line 704
209. def OAI.MUB6.Certificate.MixedSemantics.raw418step1 line 706
210. def OAI.MUB6.Certificate.MixedSemantics.raw418step1Labels line 707
211. theorem OAI.MUB6.Certificate.MixedSemantics.canonical418 line 709
212. def OAI.MUB6.Certificate.MixedSemantics.raw419 line 724
213. def OAI.MUB6.Certificate.MixedSemantics.raw419Labels line 725
214. def OAI.MUB6.Certificate.MixedSemantics.raw419step0 line 727
215. def OAI.MUB6.Certificate.MixedSemantics.raw419step0Labels line 728
216. theorem OAI.MUB6.Certificate.MixedSemantics.canonical419 line 730
217. def OAI.MUB6.Certificate.MixedSemantics.raw420 line 740
218. def OAI.MUB6.Certificate.MixedSemantics.raw420Labels line 741
219. def OAI.MUB6.Certificate.MixedSemantics.raw420step0 line 743
220. def OAI.MUB6.Certificate.MixedSemantics.raw420step0Labels line 744
221. def OAI.MUB6.Certificate.MixedSemantics.raw420step1 line 746
222. def OAI.MUB6.Certificate.MixedSemantics.raw420step1Labels line 747
223. theorem OAI.MUB6.Certificate.MixedSemantics.canonical420 line 749
224. def OAI.MUB6.Certificate.MixedSemantics.raw421 line 764
225. def OAI.MUB6.Certificate.MixedSemantics.raw421Labels line 765
226. def OAI.MUB6.Certificate.MixedSemantics.raw421step0 line 767
227. def OAI.MUB6.Certificate.MixedSemantics.raw421step0Labels line 768
228. theorem OAI.MUB6.Certificate.MixedSemantics.canonical421 line 770
229. def OAI.MUB6.Certificate.MixedSemantics.raw422 line 780
230. def OAI.MUB6.Certificate.MixedSemantics.raw422Labels line 781
231. def OAI.MUB6.Certificate.MixedSemantics.raw422step0 line 783
232. def OAI.MUB6.Certificate.MixedSemantics.raw422step0Labels line 784
233. def OAI.MUB6.Certificate.MixedSemantics.raw422step1 line 786
234. def OAI.MUB6.Certificate.MixedSemantics.raw422step1Labels line 787
235. theorem OAI.MUB6.Certificate.MixedSemantics.canonical422 line 789
236. def OAI.MUB6.Certificate.MixedSemantics.raw423 line 804
237. def OAI.MUB6.Certificate.MixedSemantics.raw423Labels line 805
238. def OAI.MUB6.Certificate.MixedSemantics.raw423step0 line 807
239. def OAI.MUB6.Certificate.MixedSemantics.raw423step0Labels line 808
240. def OAI.MUB6.Certificate.MixedSemantics.raw423step1 line 810
241. def OAI.MUB6.Certificate.MixedSemantics.raw423step1Labels line 811
242. theorem OAI.MUB6.Certificate.MixedSemantics.canonical423 line 813
243. def OAI.MUB6.Certificate.MixedSemantics.raw424 line 828
244. def OAI.MUB6.Certificate.MixedSemantics.raw424Labels line 829
245. def OAI.MUB6.Certificate.MixedSemantics.raw424step0 line 831
246. def OAI.MUB6.Certificate.MixedSemantics.raw424step0Labels line 832
247. def OAI.MUB6.Certificate.MixedSemantics.raw424step1 line 834
248. def OAI.MUB6.Certificate.MixedSemantics.raw424step1Labels line 835
249. theorem OAI.MUB6.Certificate.MixedSemantics.canonical424 line 837
250. def OAI.MUB6.Certificate.MixedSemantics.raw425 line 852
251. def OAI.MUB6.Certificate.MixedSemantics.raw425Labels line 853
252. def OAI.MUB6.Certificate.MixedSemantics.raw425step0 line 855
253. def OAI.MUB6.Certificate.MixedSemantics.raw425step0Labels line 856
254. def OAI.MUB6.Certificate.MixedSemantics.raw425step1 line 858
255. def OAI.MUB6.Certificate.MixedSemantics.raw425step1Labels line 859
256. theorem OAI.MUB6.Certificate.MixedSemantics.canonical425 line 861
257. def OAI.MUB6.Certificate.MixedSemantics.raw426 line 876
258. def OAI.MUB6.Certificate.MixedSemantics.raw426Labels line 877
259. def OAI.MUB6.Certificate.MixedSemantics.raw426step0 line 879
260. def OAI.MUB6.Certificate.MixedSemantics.raw426step0Labels line 880
261. def OAI.MUB6.Certificate.MixedSemantics.raw426step1 line 882
262. def OAI.MUB6.Certificate.MixedSemantics.raw426step1Labels line 883
263. theorem OAI.MUB6.Certificate.MixedSemantics.canonical426 line 885
264. def OAI.MUB6.Certificate.MixedSemantics.raw427 line 900
265. def OAI.MUB6.Certificate.MixedSemantics.raw427Labels line 901
266. def OAI.MUB6.Certificate.MixedSemantics.raw427step0 line 903
267. def OAI.MUB6.Certificate.MixedSemantics.raw427step0Labels line 904
268. theorem OAI.MUB6.Certificate.MixedSemantics.canonical427 line 906
269. def OAI.MUB6.Certificate.MixedSemantics.raw428 line 916
270. def OAI.MUB6.Certificate.MixedSemantics.raw428Labels line 917
271. def OAI.MUB6.Certificate.MixedSemantics.raw428step0 line 919
272. def OAI.MUB6.Certificate.MixedSemantics.raw428step0Labels line 920
273. def OAI.MUB6.Certificate.MixedSemantics.raw428step1 line 922
274. def OAI.MUB6.Certificate.MixedSemantics.raw428step1Labels line 923
275. theorem OAI.MUB6.Certificate.MixedSemantics.canonical428 line 925
276. def OAI.MUB6.Certificate.MixedSemantics.raw429 line 940
277. def OAI.MUB6.Certificate.MixedSemantics.raw429Labels line 941
278. def OAI.MUB6.Certificate.MixedSemantics.raw429step0 line 943
279. def OAI.MUB6.Certificate.MixedSemantics.raw429step0Labels line 944
280. theorem OAI.MUB6.Certificate.MixedSemantics.canonical429 line 946
281. def OAI.MUB6.Certificate.MixedSemantics.raw430 line 956
282. def OAI.MUB6.Certificate.MixedSemantics.raw430Labels line 957
283. def OAI.MUB6.Certificate.MixedSemantics.raw430step0 line 959
284. def OAI.MUB6.Certificate.MixedSemantics.raw430step0Labels line 960
285. def OAI.MUB6.Certificate.MixedSemantics.raw430step1 line 962
286. def OAI.MUB6.Certificate.MixedSemantics.raw430step1Labels line 963
287. theorem OAI.MUB6.Certificate.MixedSemantics.canonical430 line 965
288. def OAI.MUB6.Certificate.MixedSemantics.raw431 line 980
289. def OAI.MUB6.Certificate.MixedSemantics.raw431Labels line 981
290. def OAI.MUB6.Certificate.MixedSemantics.raw431step0 line 983
291. def OAI.MUB6.Certificate.MixedSemantics.raw431step0Labels line 984
292. theorem OAI.MUB6.Certificate.MixedSemantics.canonical431 line 986
293. def OAI.MUB6.Certificate.MixedSemantics.raw432 line 996
294. def OAI.MUB6.Certificate.MixedSemantics.raw432Labels line 997
295. def OAI.MUB6.Certificate.MixedSemantics.raw432step0 line 999
296. def OAI.MUB6.Certificate.MixedSemantics.raw432step0Labels line 1000
297. def OAI.MUB6.Certificate.MixedSemantics.raw432step1 line 1002
298. def OAI.MUB6.Certificate.MixedSemantics.raw432step1Labels line 1003
299. theorem OAI.MUB6.Certificate.MixedSemantics.canonical432 line 1005
300. def OAI.MUB6.Certificate.MixedSemantics.raw433 line 1020
301. def OAI.MUB6.Certificate.MixedSemantics.raw433Labels line 1021
302. def OAI.MUB6.Certificate.MixedSemantics.raw433step0 line 1023
303. def OAI.MUB6.Certificate.MixedSemantics.raw433step0Labels line 1024
304. theorem OAI.MUB6.Certificate.MixedSemantics.canonical433 line 1026
305. def OAI.MUB6.Certificate.MixedSemantics.raw434 line 1036
306. def OAI.MUB6.Certificate.MixedSemantics.raw434Labels line 1037
307. def OAI.MUB6.Certificate.MixedSemantics.raw434step0 line 1039
308. def OAI.MUB6.Certificate.MixedSemantics.raw434step0Labels line 1040
309. def OAI.MUB6.Certificate.MixedSemantics.raw434step1 line 1042
310. def OAI.MUB6.Certificate.MixedSemantics.raw434step1Labels line 1043
311. theorem OAI.MUB6.Certificate.MixedSemantics.canonical434 line 1045
312. def OAI.MUB6.Certificate.MixedSemantics.raw435 line 1060
313. def OAI.MUB6.Certificate.MixedSemantics.raw435Labels line 1061
314. def OAI.MUB6.Certificate.MixedSemantics.raw435step0 line 1063
315. def OAI.MUB6.Certificate.MixedSemantics.raw435step0Labels line 1064
316. theorem OAI.MUB6.Certificate.MixedSemantics.canonical435 line 1066
317. def OAI.MUB6.Certificate.MixedSemantics.raw436 line 1076
318. def OAI.MUB6.Certificate.MixedSemantics.raw436Labels line 1077
319. def OAI.MUB6.Certificate.MixedSemantics.raw436step0 line 1079
320. def OAI.MUB6.Certificate.MixedSemantics.raw436step0Labels line 1080
321. def OAI.MUB6.Certificate.MixedSemantics.raw436step1 line 1082
322. def OAI.MUB6.Certificate.MixedSemantics.raw436step1Labels line 1083
323. theorem OAI.MUB6.Certificate.MixedSemantics.canonical436 line 1085
324. def OAI.MUB6.Certificate.MixedSemantics.raw437 line 1100
325. def OAI.MUB6.Certificate.MixedSemantics.raw437Labels line 1101
326. def OAI.MUB6.Certificate.MixedSemantics.raw437step0 line 1103
327. def OAI.MUB6.Certificate.MixedSemantics.raw437step0Labels line 1104
328. theorem OAI.MUB6.Certificate.MixedSemantics.canonical437 line 1106
329. def OAI.MUB6.Certificate.MixedSemantics.raw438 line 1116
330. def OAI.MUB6.Certificate.MixedSemantics.raw438Labels line 1117
331. def OAI.MUB6.Certificate.MixedSemantics.raw438step0 line 1119
332. def OAI.MUB6.Certificate.MixedSemantics.raw438step0Labels line 1120
333. def OAI.MUB6.Certificate.MixedSemantics.raw438step1 line 1122
334. def OAI.MUB6.Certificate.MixedSemantics.raw438step1Labels line 1123
335. theorem OAI.MUB6.Certificate.MixedSemantics.canonical438 line 1125
336. def OAI.MUB6.Certificate.MixedSemantics.raw439 line 1140
337. def OAI.MUB6.Certificate.MixedSemantics.raw439Labels line 1141
338. def OAI.MUB6.Certificate.MixedSemantics.raw439step0 line 1143
339. def OAI.MUB6.Certificate.MixedSemantics.raw439step0Labels line 1144
340. theorem OAI.MUB6.Certificate.MixedSemantics.canonical439 line 1146
341. def OAI.MUB6.Certificate.MixedSemantics.raw440 line 1156
342. def OAI.MUB6.Certificate.MixedSemantics.raw440Labels line 1157
343. def OAI.MUB6.Certificate.MixedSemantics.raw440step0 line 1159
344. def OAI.MUB6.Certificate.MixedSemantics.raw440step0Labels line 1160
345. def OAI.MUB6.Certificate.MixedSemantics.raw440step1 line 1162
346. def OAI.MUB6.Certificate.MixedSemantics.raw440step1Labels line 1163
347. theorem OAI.MUB6.Certificate.MixedSemantics.canonical440 line 1165
348. def OAI.MUB6.Certificate.MixedSemantics.raw441 line 1180
349. def OAI.MUB6.Certificate.MixedSemantics.raw441Labels line 1181
350. def OAI.MUB6.Certificate.MixedSemantics.raw441step0 line 1183
351. def OAI.MUB6.Certificate.MixedSemantics.raw441step0Labels line 1184
352. theorem OAI.MUB6.Certificate.MixedSemantics.canonical441 line 1186
353. def OAI.MUB6.Certificate.MixedSemantics.raw442 line 1196
354. def OAI.MUB6.Certificate.MixedSemantics.raw442Labels line 1197
355. def OAI.MUB6.Certificate.MixedSemantics.raw442step0 line 1199
356. def OAI.MUB6.Certificate.MixedSemantics.raw442step0Labels line 1200
357. def OAI.MUB6.Certificate.MixedSemantics.raw442step1 line 1202
358. def OAI.MUB6.Certificate.MixedSemantics.raw442step1Labels line 1203
359. theorem OAI.MUB6.Certificate.MixedSemantics.canonical442 line 1205
360. def OAI.MUB6.Certificate.MixedSemantics.raw443 line 1220
361. def OAI.MUB6.Certificate.MixedSemantics.raw443Labels line 1221
362. def OAI.MUB6.Certificate.MixedSemantics.raw443step0 line 1223
363. def OAI.MUB6.Certificate.MixedSemantics.raw443step0Labels line 1224
364. theorem OAI.MUB6.Certificate.MixedSemantics.canonical443 line 1226
365. def OAI.MUB6.Certificate.MixedSemantics.raw444 line 1236
366. def OAI.MUB6.Certificate.MixedSemantics.raw444Labels line 1237
367. def OAI.MUB6.Certificate.MixedSemantics.raw444step0 line 1239
368. def OAI.MUB6.Certificate.MixedSemantics.raw444step0Labels line 1240
369. def OAI.MUB6.Certificate.MixedSemantics.raw444step1 line 1242
370. def OAI.MUB6.Certificate.MixedSemantics.raw444step1Labels line 1243
371. theorem OAI.MUB6.Certificate.MixedSemantics.canonical444 line 1245
372. def OAI.MUB6.Certificate.MixedSemantics.raw445 line 1260
373. def OAI.MUB6.Certificate.MixedSemantics.raw445Labels line 1261
374. def OAI.MUB6.Certificate.MixedSemantics.raw445step0 line 1263
375. def OAI.MUB6.Certificate.MixedSemantics.raw445step0Labels line 1264
376. theorem OAI.MUB6.Certificate.MixedSemantics.canonical445 line 1266
377. def OAI.MUB6.Certificate.MixedSemantics.raw446 line 1276
378. def OAI.MUB6.Certificate.MixedSemantics.raw446Labels line 1277
379. def OAI.MUB6.Certificate.MixedSemantics.raw446step0 line 1279
380. def OAI.MUB6.Certificate.MixedSemantics.raw446step0Labels line 1280
381. def OAI.MUB6.Certificate.MixedSemantics.raw446step1 line 1282
382. def OAI.MUB6.Certificate.MixedSemantics.raw446step1Labels line 1283
383. theorem OAI.MUB6.Certificate.MixedSemantics.canonical446 line 1285
384. def OAI.MUB6.Certificate.MixedSemantics.raw447 line 1300
385. def OAI.MUB6.Certificate.MixedSemantics.raw447Labels line 1301
386. def OAI.MUB6.Certificate.MixedSemantics.raw447step0 line 1303
387. def OAI.MUB6.Certificate.MixedSemantics.raw447step0Labels line 1304
388. theorem OAI.MUB6.Certificate.MixedSemantics.canonical447 line 1306
389. def OAI.MUB6.Certificate.MixedSemantics.raw448 line 1316
390. def OAI.MUB6.Certificate.MixedSemantics.raw448Labels line 1317
391. def OAI.MUB6.Certificate.MixedSemantics.raw448step0 line 1319
392. def OAI.MUB6.Certificate.MixedSemantics.raw448step0Labels line 1320
393. def OAI.MUB6.Certificate.MixedSemantics.raw448step1 line 1322
394. def OAI.MUB6.Certificate.MixedSemantics.raw448step1Labels line 1323
395. theorem OAI.MUB6.Certificate.MixedSemantics.canonical448 line 1325
396. def OAI.MUB6.Certificate.MixedSemantics.raw449 line 1340
397. def OAI.MUB6.Certificate.MixedSemantics.raw449Labels line 1341
398. def OAI.MUB6.Certificate.MixedSemantics.raw449step0 line 1343
399. def OAI.MUB6.Certificate.MixedSemantics.raw449step0Labels line 1344
400. theorem OAI.MUB6.Certificate.MixedSemantics.canonical449 line 1346
401. def OAI.MUB6.Certificate.MixedSemantics.raw450 line 1356
402. def OAI.MUB6.Certificate.MixedSemantics.raw450Labels line 1357
403. def OAI.MUB6.Certificate.MixedSemantics.raw450step0 line 1359
404. def OAI.MUB6.Certificate.MixedSemantics.raw450step0Labels line 1360
405. def OAI.MUB6.Certificate.MixedSemantics.raw450step1 line 1362
406. def OAI.MUB6.Certificate.MixedSemantics.raw450step1Labels line 1363
407. theorem OAI.MUB6.Certificate.MixedSemantics.canonical450 line 1365
408. def OAI.MUB6.Certificate.MixedSemantics.raw451 line 1380
409. def OAI.MUB6.Certificate.MixedSemantics.raw451Labels line 1381
410. def OAI.MUB6.Certificate.MixedSemantics.raw451step0 line 1383
411. def OAI.MUB6.Certificate.MixedSemantics.raw451step0Labels line 1384
412. theorem OAI.MUB6.Certificate.MixedSemantics.canonical451 line 1386
413. def OAI.MUB6.Certificate.MixedSemantics.raw452 line 1396
414. def OAI.MUB6.Certificate.MixedSemantics.raw452Labels line 1397
415. def OAI.MUB6.Certificate.MixedSemantics.raw452step0 line 1399
416. def OAI.MUB6.Certificate.MixedSemantics.raw452step0Labels line 1400
417. def OAI.MUB6.Certificate.MixedSemantics.raw452step1 line 1402
418. def OAI.MUB6.Certificate.MixedSemantics.raw452step1Labels line 1403
419. theorem OAI.MUB6.Certificate.MixedSemantics.canonical452 line 1405
420. def OAI.MUB6.Certificate.MixedSemantics.raw453 line 1420
421. def OAI.MUB6.Certificate.MixedSemantics.raw453Labels line 1421
422. def OAI.MUB6.Certificate.MixedSemantics.raw453step0 line 1423
423. def OAI.MUB6.Certificate.MixedSemantics.raw453step0Labels line 1424
424. theorem OAI.MUB6.Certificate.MixedSemantics.canonical453 line 1426
425. def OAI.MUB6.Certificate.MixedSemantics.raw454 line 1436
426. def OAI.MUB6.Certificate.MixedSemantics.raw454Labels line 1437
427. def OAI.MUB6.Certificate.MixedSemantics.raw454step0 line 1439
428. def OAI.MUB6.Certificate.MixedSemantics.raw454step0Labels line 1440
429. def OAI.MUB6.Certificate.MixedSemantics.raw454step1 line 1442
430. def OAI.MUB6.Certificate.MixedSemantics.raw454step1Labels line 1443
431. theorem OAI.MUB6.Certificate.MixedSemantics.canonical454 line 1445
432. def OAI.MUB6.Certificate.MixedSemantics.raw455 line 1460
433. def OAI.MUB6.Certificate.MixedSemantics.raw455Labels line 1461
434. def OAI.MUB6.Certificate.MixedSemantics.raw455step0 line 1463
435. def OAI.MUB6.Certificate.MixedSemantics.raw455step0Labels line 1464
436. theorem OAI.MUB6.Certificate.MixedSemantics.canonical455 line 1466
437. def OAI.MUB6.Certificate.MixedSemantics.raw456 line 1476
438. def OAI.MUB6.Certificate.MixedSemantics.raw456Labels line 1477
439. def OAI.MUB6.Certificate.MixedSemantics.raw456step0 line 1479
440. def OAI.MUB6.Certificate.MixedSemantics.raw456step0Labels line 1480
441. def OAI.MUB6.Certificate.MixedSemantics.raw456step1 line 1482
442. def OAI.MUB6.Certificate.MixedSemantics.raw456step1Labels line 1483
443. theorem OAI.MUB6.Certificate.MixedSemantics.canonical456 line 1485
444. def OAI.MUB6.Certificate.MixedSemantics.raw457 line 1500
445. def OAI.MUB6.Certificate.MixedSemantics.raw457Labels line 1501
446. def OAI.MUB6.Certificate.MixedSemantics.raw457step0 line 1503
447. def OAI.MUB6.Certificate.MixedSemantics.raw457step0Labels line 1504
448. theorem OAI.MUB6.Certificate.MixedSemantics.canonical457 line 1506
449. def OAI.MUB6.Certificate.MixedSemantics.raw458 line 1516
450. def OAI.MUB6.Certificate.MixedSemantics.raw458Labels line 1517
451. def OAI.MUB6.Certificate.MixedSemantics.raw458step0 line 1519
452. def OAI.MUB6.Certificate.MixedSemantics.raw458step0Labels line 1520
453. def OAI.MUB6.Certificate.MixedSemantics.raw458step1 line 1522
454. def OAI.MUB6.Certificate.MixedSemantics.raw458step1Labels line 1523
455. theorem OAI.MUB6.Certificate.MixedSemantics.canonical458 line 1525
456. def OAI.MUB6.Certificate.MixedSemantics.raw459 line 1540
457. def OAI.MUB6.Certificate.MixedSemantics.raw459Labels line 1541
458. def OAI.MUB6.Certificate.MixedSemantics.raw459step0 line 1543
459. def OAI.MUB6.Certificate.MixedSemantics.raw459step0Labels line 1544
460. theorem OAI.MUB6.Certificate.MixedSemantics.canonical459 line 1546
461. def OAI.MUB6.Certificate.MixedSemantics.raw460 line 1556
462. def OAI.MUB6.Certificate.MixedSemantics.raw460Labels line 1557
463. def OAI.MUB6.Certificate.MixedSemantics.raw460step0 line 1559
464. def OAI.MUB6.Certificate.MixedSemantics.raw460step0Labels line 1560
465. def OAI.MUB6.Certificate.MixedSemantics.raw460step1 line 1562
466. def OAI.MUB6.Certificate.MixedSemantics.raw460step1Labels line 1563
467. theorem OAI.MUB6.Certificate.MixedSemantics.canonical460 line 1565
468. def OAI.MUB6.Certificate.MixedSemantics.raw461 line 1580
469. def OAI.MUB6.Certificate.MixedSemantics.raw461Labels line 1581
470. def OAI.MUB6.Certificate.MixedSemantics.raw461step0 line 1583
471. def OAI.MUB6.Certificate.MixedSemantics.raw461step0Labels line 1584
472. theorem OAI.MUB6.Certificate.MixedSemantics.canonical461 line 1586
473. def OAI.MUB6.Certificate.MixedSemantics.raw462 line 1596
474. def OAI.MUB6.Certificate.MixedSemantics.raw462Labels line 1597
475. def OAI.MUB6.Certificate.MixedSemantics.raw462step0 line 1599
476. def OAI.MUB6.Certificate.MixedSemantics.raw462step0Labels line 1600
477. def OAI.MUB6.Certificate.MixedSemantics.raw462step1 line 1602
478. def OAI.MUB6.Certificate.MixedSemantics.raw462step1Labels line 1603
479. theorem OAI.MUB6.Certificate.MixedSemantics.canonical462 line 1605
480. def OAI.MUB6.Certificate.MixedSemantics.raw463 line 1620
481. def OAI.MUB6.Certificate.MixedSemantics.raw463Labels line 1621
482. def OAI.MUB6.Certificate.MixedSemantics.raw463step0 line 1623
483. def OAI.MUB6.Certificate.MixedSemantics.raw463step0Labels line 1624
484. theorem OAI.MUB6.Certificate.MixedSemantics.canonical463 line 1626
485. def OAI.MUB6.Certificate.MixedSemantics.raw464 line 1636
486. def OAI.MUB6.Certificate.MixedSemantics.raw464Labels line 1637
487. def OAI.MUB6.Certificate.MixedSemantics.raw464step0 line 1639
488. def OAI.MUB6.Certificate.MixedSemantics.raw464step0Labels line 1640
489. def OAI.MUB6.Certificate.MixedSemantics.raw464step1 line 1642
490. def OAI.MUB6.Certificate.MixedSemantics.raw464step1Labels line 1643
491. theorem OAI.MUB6.Certificate.MixedSemantics.canonical464 line 1645
492. def OAI.MUB6.Certificate.MixedSemantics.raw465 line 1660
493. def OAI.MUB6.Certificate.MixedSemantics.raw465Labels line 1661
494. def OAI.MUB6.Certificate.MixedSemantics.raw465step0 line 1663
495. def OAI.MUB6.Certificate.MixedSemantics.raw465step0Labels line 1664
496. theorem OAI.MUB6.Certificate.MixedSemantics.canonical465 line 1666
497. def OAI.MUB6.Certificate.MixedSemantics.raw466 line 1676
498. def OAI.MUB6.Certificate.MixedSemantics.raw466Labels line 1677
499. def OAI.MUB6.Certificate.MixedSemantics.raw466step0 line 1679
500. def OAI.MUB6.Certificate.MixedSemantics.raw466step0Labels line 1680
501. def OAI.MUB6.Certificate.MixedSemantics.raw466step1 line 1682
502. def OAI.MUB6.Certificate.MixedSemantics.raw466step1Labels line 1683
503. theorem OAI.MUB6.Certificate.MixedSemantics.canonical466 line 1685
504. def OAI.MUB6.Certificate.MixedSemantics.raw467 line 1700
505. def OAI.MUB6.Certificate.MixedSemantics.raw467Labels line 1701
506. def OAI.MUB6.Certificate.MixedSemantics.raw467step0 line 1703
507. def OAI.MUB6.Certificate.MixedSemantics.raw467step0Labels line 1704
508. def OAI.MUB6.Certificate.MixedSemantics.raw467step1 line 1706
509. def OAI.MUB6.Certificate.MixedSemantics.raw467step1Labels line 1707
510. theorem OAI.MUB6.Certificate.MixedSemantics.canonical467 line 1709
511. def OAI.MUB6.Certificate.MixedSemantics.raw468 line 1724
512. def OAI.MUB6.Certificate.MixedSemantics.raw468Labels line 1725
513. def OAI.MUB6.Certificate.MixedSemantics.raw468step0 line 1727
514. def OAI.MUB6.Certificate.MixedSemantics.raw468step0Labels line 1728
515. def OAI.MUB6.Certificate.MixedSemantics.raw468step1 line 1730
516. def OAI.MUB6.Certificate.MixedSemantics.raw468step1Labels line 1731
517. theorem OAI.MUB6.Certificate.MixedSemantics.canonical468 line 1733
518. def OAI.MUB6.Certificate.MixedSemantics.raw469 line 1748
519. def OAI.MUB6.Certificate.MixedSemantics.raw469Labels line 1749
520. def OAI.MUB6.Certificate.MixedSemantics.raw469step0 line 1751
521. def OAI.MUB6.Certificate.MixedSemantics.raw469step0Labels line 1752
522. theorem OAI.MUB6.Certificate.MixedSemantics.canonical469 line 1754
523. def OAI.MUB6.Certificate.MixedSemantics.raw470 line 1764
524. def OAI.MUB6.Certificate.MixedSemantics.raw470Labels line 1765
525. def OAI.MUB6.Certificate.MixedSemantics.raw470step0 line 1767
526. def OAI.MUB6.Certificate.MixedSemantics.raw470step0Labels line 1768
527. def OAI.MUB6.Certificate.MixedSemantics.raw470step1 line 1770
528. def OAI.MUB6.Certificate.MixedSemantics.raw470step1Labels line 1771
529. theorem OAI.MUB6.Certificate.MixedSemantics.canonical470 line 1773
530. def OAI.MUB6.Certificate.MixedSemantics.raw471 line 1788
531. def OAI.MUB6.Certificate.MixedSemantics.raw471Labels line 1789
532. def OAI.MUB6.Certificate.MixedSemantics.raw471step0 line 1791
533. def OAI.MUB6.Certificate.MixedSemantics.raw471step0Labels line 1792
534. def OAI.MUB6.Certificate.MixedSemantics.raw471step1 line 1794
535. def OAI.MUB6.Certificate.MixedSemantics.raw471step1Labels line 1795
536. theorem OAI.MUB6.Certificate.MixedSemantics.canonical471 line 1797
537. def OAI.MUB6.Certificate.MixedSemantics.raw472 line 1812
538. def OAI.MUB6.Certificate.MixedSemantics.raw472Labels line 1813
539. def OAI.MUB6.Certificate.MixedSemantics.raw472step0 line 1815
540. def OAI.MUB6.Certificate.MixedSemantics.raw472step0Labels line 1816
541. def OAI.MUB6.Certificate.MixedSemantics.raw472step1 line 1818
542. def OAI.MUB6.Certificate.MixedSemantics.raw472step1Labels line 1819
543. theorem OAI.MUB6.Certificate.MixedSemantics.canonical472 line 1821
544. def OAI.MUB6.Certificate.MixedSemantics.raw473 line 1836
545. def OAI.MUB6.Certificate.MixedSemantics.raw473Labels line 1837
546. def OAI.MUB6.Certificate.MixedSemantics.raw473step0 line 1839
547. def OAI.MUB6.Certificate.MixedSemantics.raw473step0Labels line 1840
548. theorem OAI.MUB6.Certificate.MixedSemantics.canonical473 line 1842
549. def OAI.MUB6.Certificate.MixedSemantics.raw474 line 1852
550. def OAI.MUB6.Certificate.MixedSemantics.raw474Labels line 1853
551. def OAI.MUB6.Certificate.MixedSemantics.raw474step0 line 1855
552. def OAI.MUB6.Certificate.MixedSemantics.raw474step0Labels line 1856
553. def OAI.MUB6.Certificate.MixedSemantics.raw474step1 line 1858
554. def OAI.MUB6.Certificate.MixedSemantics.raw474step1Labels line 1859
555. theorem OAI.MUB6.Certificate.MixedSemantics.canonical474 line 1861
556. def OAI.MUB6.Certificate.MixedSemantics.raw475 line 1876
557. def OAI.MUB6.Certificate.MixedSemantics.raw475Labels line 1877
558. def OAI.MUB6.Certificate.MixedSemantics.raw475step0 line 1879
559. def OAI.MUB6.Certificate.MixedSemantics.raw475step0Labels line 1880
560. def OAI.MUB6.Certificate.MixedSemantics.raw475step1 line 1882
561. def OAI.MUB6.Certificate.MixedSemantics.raw475step1Labels line 1883
562. theorem OAI.MUB6.Certificate.MixedSemantics.canonical475 line 1885
563. def OAI.MUB6.Certificate.MixedSemantics.raw476 line 1900
564. def OAI.MUB6.Certificate.MixedSemantics.raw476Labels line 1901
565. def OAI.MUB6.Certificate.MixedSemantics.raw476step0 line 1903
566. def OAI.MUB6.Certificate.MixedSemantics.raw476step0Labels line 1904
567. def OAI.MUB6.Certificate.MixedSemantics.raw476step1 line 1906
568. def OAI.MUB6.Certificate.MixedSemantics.raw476step1Labels line 1907
569. theorem OAI.MUB6.Certificate.MixedSemantics.canonical476 line 1909
570. def OAI.MUB6.Certificate.MixedSemantics.raw477 line 1924
571. def OAI.MUB6.Certificate.MixedSemantics.raw477Labels line 1925
572. def OAI.MUB6.Certificate.MixedSemantics.raw477step0 line 1927
573. def OAI.MUB6.Certificate.MixedSemantics.raw477step0Labels line 1928
574. theorem OAI.MUB6.Certificate.MixedSemantics.canonical477 line 1930
575. def OAI.MUB6.Certificate.MixedSemantics.raw478 line 1940
576. def OAI.MUB6.Certificate.MixedSemantics.raw478Labels line 1941
577. def OAI.MUB6.Certificate.MixedSemantics.raw478step0 line 1943
578. def OAI.MUB6.Certificate.MixedSemantics.raw478step0Labels line 1944
579. def OAI.MUB6.Certificate.MixedSemantics.raw478step1 line 1946
580. def OAI.MUB6.Certificate.MixedSemantics.raw478step1Labels line 1947
581. theorem OAI.MUB6.Certificate.MixedSemantics.canonical478 line 1949
582. def OAI.MUB6.Certificate.MixedSemantics.raw479 line 1964
583. def OAI.MUB6.Certificate.MixedSemantics.raw479Labels line 1965
584. def OAI.MUB6.Certificate.MixedSemantics.raw479step0 line 1967
585. def OAI.MUB6.Certificate.MixedSemantics.raw479step0Labels line 1968
586. theorem OAI.MUB6.Certificate.MixedSemantics.canonical479 line 1970
587. def OAI.MUB6.Certificate.MixedSemantics.raw480 line 1980
588. def OAI.MUB6.Certificate.MixedSemantics.raw480Labels line 1981
589. def OAI.MUB6.Certificate.MixedSemantics.raw480step0 line 1983
590. def OAI.MUB6.Certificate.MixedSemantics.raw480step0Labels line 1984
591. def OAI.MUB6.Certificate.MixedSemantics.raw480step1 line 1986
592. def OAI.MUB6.Certificate.MixedSemantics.raw480step1Labels line 1987
593. theorem OAI.MUB6.Certificate.MixedSemantics.canonical480 line 1989
594. def OAI.MUB6.Certificate.MixedSemantics.raw481 line 2004
595. def OAI.MUB6.Certificate.MixedSemantics.raw481Labels line 2005
596. def OAI.MUB6.Certificate.MixedSemantics.raw481step0 line 2007
597. def OAI.MUB6.Certificate.MixedSemantics.raw481step0Labels line 2008
598. def OAI.MUB6.Certificate.MixedSemantics.raw481step1 line 2010
599. def OAI.MUB6.Certificate.MixedSemantics.raw481step1Labels line 2011
600. theorem OAI.MUB6.Certificate.MixedSemantics.canonical481 line 2013
601. def OAI.MUB6.Certificate.MixedSemantics.raw482 line 2028
602. def OAI.MUB6.Certificate.MixedSemantics.raw482Labels line 2029
603. def OAI.MUB6.Certificate.MixedSemantics.raw482step0 line 2031
604. def OAI.MUB6.Certificate.MixedSemantics.raw482step0Labels line 2032
605. def OAI.MUB6.Certificate.MixedSemantics.raw482step1 line 2034
606. def OAI.MUB6.Certificate.MixedSemantics.raw482step1Labels line 2035
607. theorem OAI.MUB6.Certificate.MixedSemantics.canonical482 line 2037
608. def OAI.MUB6.Certificate.MixedSemantics.raw483 line 2052
609. def OAI.MUB6.Certificate.MixedSemantics.raw483Labels line 2053
610. def OAI.MUB6.Certificate.MixedSemantics.raw483step0 line 2055
611. def OAI.MUB6.Certificate.MixedSemantics.raw483step0Labels line 2056
612. theorem OAI.MUB6.Certificate.MixedSemantics.canonical483 line 2058
613. def OAI.MUB6.Certificate.MixedSemantics.raw484 line 2068
614. def OAI.MUB6.Certificate.MixedSemantics.raw484Labels line 2069
615. def OAI.MUB6.Certificate.MixedSemantics.raw484step0 line 2071
616. def OAI.MUB6.Certificate.MixedSemantics.raw484step0Labels line 2072
617. def OAI.MUB6.Certificate.MixedSemantics.raw484step1 line 2074
618. def OAI.MUB6.Certificate.MixedSemantics.raw484step1Labels line 2075
619. theorem OAI.MUB6.Certificate.MixedSemantics.canonical484 line 2077
620. def OAI.MUB6.Certificate.MixedSemantics.raw485 line 2092
621. def OAI.MUB6.Certificate.MixedSemantics.raw485Labels line 2093
622. def OAI.MUB6.Certificate.MixedSemantics.raw485step0 line 2095
623. def OAI.MUB6.Certificate.MixedSemantics.raw485step0Labels line 2096
624. theorem OAI.MUB6.Certificate.MixedSemantics.canonical485 line 2098
625. def OAI.MUB6.Certificate.MixedSemantics.raw486 line 2108
626. def OAI.MUB6.Certificate.MixedSemantics.raw486Labels line 2109
627. def OAI.MUB6.Certificate.MixedSemantics.raw486step0 line 2111
628. def OAI.MUB6.Certificate.MixedSemantics.raw486step0Labels line 2112
629. def OAI.MUB6.Certificate.MixedSemantics.raw486step1 line 2114
630. def OAI.MUB6.Certificate.MixedSemantics.raw486step1Labels line 2115
631. theorem OAI.MUB6.Certificate.MixedSemantics.canonical486 line 2117
632. def OAI.MUB6.Certificate.MixedSemantics.raw487 line 2132
633. def OAI.MUB6.Certificate.MixedSemantics.raw487Labels line 2133
634. def OAI.MUB6.Certificate.MixedSemantics.raw487step0 line 2135
635. def OAI.MUB6.Certificate.MixedSemantics.raw487step0Labels line 2136
636. def OAI.MUB6.Certificate.MixedSemantics.raw487step1 line 2138
637. def OAI.MUB6.Certificate.MixedSemantics.raw487step1Labels line 2139
638. theorem OAI.MUB6.Certificate.MixedSemantics.canonical487 line 2141
639. def OAI.MUB6.Certificate.MixedSemantics.raw488 line 2156
640. def OAI.MUB6.Certificate.MixedSemantics.raw488Labels line 2157
641. def OAI.MUB6.Certificate.MixedSemantics.raw488step0 line 2159
642. def OAI.MUB6.Certificate.MixedSemantics.raw488step0Labels line 2160
643. def OAI.MUB6.Certificate.MixedSemantics.raw488step1 line 2162
644. def OAI.MUB6.Certificate.MixedSemantics.raw488step1Labels line 2163
645. theorem OAI.MUB6.Certificate.MixedSemantics.canonical488 line 2165
646. def OAI.MUB6.Certificate.MixedSemantics.raw489 line 2180
647. def OAI.MUB6.Certificate.MixedSemantics.raw489Labels line 2181
648. def OAI.MUB6.Certificate.MixedSemantics.raw489step0 line 2183
649. def OAI.MUB6.Certificate.MixedSemantics.raw489step0Labels line 2184
650. theorem OAI.MUB6.Certificate.MixedSemantics.canonical489 line 2186
651. def OAI.MUB6.Certificate.MixedSemantics.raw490 line 2196
652. def OAI.MUB6.Certificate.MixedSemantics.raw490Labels line 2197
653. def OAI.MUB6.Certificate.MixedSemantics.raw490step0 line 2199
654. def OAI.MUB6.Certificate.MixedSemantics.raw490step0Labels line 2200
655. def OAI.MUB6.Certificate.MixedSemantics.raw490step1 line 2202
656. def OAI.MUB6.Certificate.MixedSemantics.raw490step1Labels line 2203
657. theorem OAI.MUB6.Certificate.MixedSemantics.canonical490 line 2205
658. def OAI.MUB6.Certificate.MixedSemantics.raw491 line 2220
659. def OAI.MUB6.Certificate.MixedSemantics.raw491Labels line 2221
660. def OAI.MUB6.Certificate.MixedSemantics.raw491step0 line 2223
661. def OAI.MUB6.Certificate.MixedSemantics.raw491step0Labels line 2224
662. theorem OAI.MUB6.Certificate.MixedSemantics.canonical491 line 2226
663. def OAI.MUB6.Certificate.MixedSemantics.raw492 line 2236
664. def OAI.MUB6.Certificate.MixedSemantics.raw492Labels line 2237
665. def OAI.MUB6.Certificate.MixedSemantics.raw492step0 line 2239
666. def OAI.MUB6.Certificate.MixedSemantics.raw492step0Labels line 2240
667. def OAI.MUB6.Certificate.MixedSemantics.raw492step1 line 2242
668. def OAI.MUB6.Certificate.MixedSemantics.raw492step1Labels line 2243
669. theorem OAI.MUB6.Certificate.MixedSemantics.canonical492 line 2245
670. def OAI.MUB6.Certificate.MixedSemantics.raw493 line 2260
671. def OAI.MUB6.Certificate.MixedSemantics.raw493Labels line 2261
672. def OAI.MUB6.Certificate.MixedSemantics.raw493step0 line 2263
673. def OAI.MUB6.Certificate.MixedSemantics.raw493step0Labels line 2264
674. theorem OAI.MUB6.Certificate.MixedSemantics.canonical493 line 2266
675. def OAI.MUB6.Certificate.MixedSemantics.raw494 line 2276
676. def OAI.MUB6.Certificate.MixedSemantics.raw494Labels line 2277
677. def OAI.MUB6.Certificate.MixedSemantics.raw494step0 line 2279
678. def OAI.MUB6.Certificate.MixedSemantics.raw494step0Labels line 2280
679. def OAI.MUB6.Certificate.MixedSemantics.raw494step1 line 2282
680. def OAI.MUB6.Certificate.MixedSemantics.raw494step1Labels line 2283
681. theorem OAI.MUB6.Certificate.MixedSemantics.canonical494 line 2285
682. def OAI.MUB6.Certificate.MixedSemantics.raw495 line 2300
683. def OAI.MUB6.Certificate.MixedSemantics.raw495Labels line 2301
684. def OAI.MUB6.Certificate.MixedSemantics.raw495step0 line 2303
685. def OAI.MUB6.Certificate.MixedSemantics.raw495step0Labels line 2304
686. theorem OAI.MUB6.Certificate.MixedSemantics.canonical495 line 2306
687. def OAI.MUB6.Certificate.MixedSemantics.raw496 line 2316
688. def OAI.MUB6.Certificate.MixedSemantics.raw496Labels line 2317
689. def OAI.MUB6.Certificate.MixedSemantics.raw496step0 line 2319
690. def OAI.MUB6.Certificate.MixedSemantics.raw496step0Labels line 2320
691. def OAI.MUB6.Certificate.MixedSemantics.raw496step1 line 2322
692. def OAI.MUB6.Certificate.MixedSemantics.raw496step1Labels line 2323
693. theorem OAI.MUB6.Certificate.MixedSemantics.canonical496 line 2325
694. def OAI.MUB6.Certificate.MixedSemantics.raw497 line 2340
695. def OAI.MUB6.Certificate.MixedSemantics.raw497Labels line 2341
696. def OAI.MUB6.Certificate.MixedSemantics.raw497step0 line 2343
697. def OAI.MUB6.Certificate.MixedSemantics.raw497step0Labels line 2344
698. theorem OAI.MUB6.Certificate.MixedSemantics.canonical497 line 2346
699. def OAI.MUB6.Certificate.MixedSemantics.raw498 line 2356
700. def OAI.MUB6.Certificate.MixedSemantics.raw498Labels line 2357
701. def OAI.MUB6.Certificate.MixedSemantics.raw498step0 line 2359
702. def OAI.MUB6.Certificate.MixedSemantics.raw498step0Labels line 2360
703. def OAI.MUB6.Certificate.MixedSemantics.raw498step1 line 2362
704. def OAI.MUB6.Certificate.MixedSemantics.raw498step1Labels line 2363
705. theorem OAI.MUB6.Certificate.MixedSemantics.canonical498 line 2365
706. def OAI.MUB6.Certificate.MixedSemantics.raw499 line 2380
707. def OAI.MUB6.Certificate.MixedSemantics.raw499Labels line 2381
708. def OAI.MUB6.Certificate.MixedSemantics.raw499step0 line 2383
709. def OAI.MUB6.Certificate.MixedSemantics.raw499step0Labels line 2384
710. theorem OAI.MUB6.Certificate.MixedSemantics.canonical499 line 2386
711. def OAI.MUB6.Certificate.MixedSemantics.raw500 line 2396
712. def OAI.MUB6.Certificate.MixedSemantics.raw500Labels line 2397
713. def OAI.MUB6.Certificate.MixedSemantics.raw500step0 line 2399
714. def OAI.MUB6.Certificate.MixedSemantics.raw500step0Labels line 2400
715. def OAI.MUB6.Certificate.MixedSemantics.raw500step1 line 2402
716. def OAI.MUB6.Certificate.MixedSemantics.raw500step1Labels line 2403
717. theorem OAI.MUB6.Certificate.MixedSemantics.canonical500 line 2405
718. def OAI.MUB6.Certificate.MixedSemantics.raw501 line 2420
719. def OAI.MUB6.Certificate.MixedSemantics.raw501Labels line 2421
720. def OAI.MUB6.Certificate.MixedSemantics.raw501step0 line 2423
721. def OAI.MUB6.Certificate.MixedSemantics.raw501step0Labels line 2424
722. theorem OAI.MUB6.Certificate.MixedSemantics.canonical501 line 2426
723. def OAI.MUB6.Certificate.MixedSemantics.raw502 line 2436
724. def OAI.MUB6.Certificate.MixedSemantics.raw502Labels line 2437
725. def OAI.MUB6.Certificate.MixedSemantics.raw502step0 line 2439
726. def OAI.MUB6.Certificate.MixedSemantics.raw502step0Labels line 2440
727. def OAI.MUB6.Certificate.MixedSemantics.raw502step1 line 2442
728. def OAI.MUB6.Certificate.MixedSemantics.raw502step1Labels line 2443
729. theorem OAI.MUB6.Certificate.MixedSemantics.canonical502 line 2445
730. def OAI.MUB6.Certificate.MixedSemantics.raw503 line 2460
731. def OAI.MUB6.Certificate.MixedSemantics.raw503Labels line 2461
732. def OAI.MUB6.Certificate.MixedSemantics.raw503step0 line 2463
733. def OAI.MUB6.Certificate.MixedSemantics.raw503step0Labels line 2464
734. theorem OAI.MUB6.Certificate.MixedSemantics.canonical503 line 2466
735. def OAI.MUB6.Certificate.MixedSemantics.raw504 line 2476
736. def OAI.MUB6.Certificate.MixedSemantics.raw504Labels line 2477
737. def OAI.MUB6.Certificate.MixedSemantics.raw504step0 line 2479
738. def OAI.MUB6.Certificate.MixedSemantics.raw504step0Labels line 2480
739. def OAI.MUB6.Certificate.MixedSemantics.raw504step1 line 2482
740. def OAI.MUB6.Certificate.MixedSemantics.raw504step1Labels line 2483
741. theorem OAI.MUB6.Certificate.MixedSemantics.canonical504 line 2485
742. def OAI.MUB6.Certificate.MixedSemantics.raw505 line 2500
743. def OAI.MUB6.Certificate.MixedSemantics.raw505Labels line 2501
744. def OAI.MUB6.Certificate.MixedSemantics.raw505step0 line 2503
745. def OAI.MUB6.Certificate.MixedSemantics.raw505step0Labels line 2504
746. def OAI.MUB6.Certificate.MixedSemantics.raw505step1 line 2506
747. def OAI.MUB6.Certificate.MixedSemantics.raw505step1Labels line 2507
748. theorem OAI.MUB6.Certificate.MixedSemantics.canonical505 line 2509
749. def OAI.MUB6.Certificate.MixedSemantics.raw506 line 2524
750. def OAI.MUB6.Certificate.MixedSemantics.raw506Labels line 2525
751. def OAI.MUB6.Certificate.MixedSemantics.raw506step0 line 2527
752. def OAI.MUB6.Certificate.MixedSemantics.raw506step0Labels line 2528
753. def OAI.MUB6.Certificate.MixedSemantics.raw506step1 line 2530
754. def OAI.MUB6.Certificate.MixedSemantics.raw506step1Labels line 2531
755. theorem OAI.MUB6.Certificate.MixedSemantics.canonical506 line 2533
756. def OAI.MUB6.Certificate.MixedSemantics.raw507 line 2548
757. def OAI.MUB6.Certificate.MixedSemantics.raw507Labels line 2549
758. def OAI.MUB6.Certificate.MixedSemantics.raw507step0 line 2551
759. def OAI.MUB6.Certificate.MixedSemantics.raw507step0Labels line 2552
760. theorem OAI.MUB6.Certificate.MixedSemantics.canonical507 line 2554
761. def OAI.MUB6.Certificate.MixedSemantics.raw508 line 2564
762. def OAI.MUB6.Certificate.MixedSemantics.raw508Labels line 2565
763. def OAI.MUB6.Certificate.MixedSemantics.raw508step0 line 2567
764. def OAI.MUB6.Certificate.MixedSemantics.raw508step0Labels line 2568
765. def OAI.MUB6.Certificate.MixedSemantics.raw508step1 line 2570
766. def OAI.MUB6.Certificate.MixedSemantics.raw508step1Labels line 2571
767. theorem OAI.MUB6.Certificate.MixedSemantics.canonical508 line 2573
768. def OAI.MUB6.Certificate.MixedSemantics.raw509 line 2588
769. def OAI.MUB6.Certificate.MixedSemantics.raw509Labels line 2589
770. def OAI.MUB6.Certificate.MixedSemantics.raw509step0 line 2591
771. def OAI.MUB6.Certificate.MixedSemantics.raw509step0Labels line 2592
772. theorem OAI.MUB6.Certificate.MixedSemantics.canonical509 line 2594
773. def OAI.MUB6.Certificate.MixedSemantics.raw510 line 2604
774. def OAI.MUB6.Certificate.MixedSemantics.raw510Labels line 2605
775. def OAI.MUB6.Certificate.MixedSemantics.raw510step0 line 2607
776. def OAI.MUB6.Certificate.MixedSemantics.raw510step0Labels line 2608
777. def OAI.MUB6.Certificate.MixedSemantics.raw510step1 line 2610
778. def OAI.MUB6.Certificate.MixedSemantics.raw510step1Labels line 2611
779. theorem OAI.MUB6.Certificate.MixedSemantics.canonical510 line 2613
780. def OAI.MUB6.Certificate.MixedSemantics.raw511 line 2628
781. def OAI.MUB6.Certificate.MixedSemantics.raw511Labels line 2629
782. def OAI.MUB6.Certificate.MixedSemantics.raw511step0 line 2631
783. def OAI.MUB6.Certificate.MixedSemantics.raw511step0Labels line 2632
784. def OAI.MUB6.Certificate.MixedSemantics.raw511step1 line 2634
785. def OAI.MUB6.Certificate.MixedSemantics.raw511step1Labels line 2635
786. theorem OAI.MUB6.Certificate.MixedSemantics.canonical511 line 2637