OAI/Analysis/MutuallyUnbiased/MixedSemantics/Canonical0.lean

GitHub source file

776 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.raw0 line 17
2. def OAI.MUB6.Certificate.MixedSemantics.raw0Labels line 18
3. def OAI.MUB6.Certificate.MixedSemantics.raw0step0 line 20
4. def OAI.MUB6.Certificate.MixedSemantics.raw0step0Labels line 21
5. def OAI.MUB6.Certificate.MixedSemantics.raw0step1 line 23
6. def OAI.MUB6.Certificate.MixedSemantics.raw0step1Labels line 24
7. theorem OAI.MUB6.Certificate.MixedSemantics.canonical0 line 26
8. def OAI.MUB6.Certificate.MixedSemantics.raw1 line 41
9. def OAI.MUB6.Certificate.MixedSemantics.raw1Labels line 42
10. def OAI.MUB6.Certificate.MixedSemantics.raw1step0 line 44
11. def OAI.MUB6.Certificate.MixedSemantics.raw1step0Labels line 45
12. theorem OAI.MUB6.Certificate.MixedSemantics.canonical1 line 47
13. def OAI.MUB6.Certificate.MixedSemantics.raw2 line 57
14. def OAI.MUB6.Certificate.MixedSemantics.raw2Labels line 58
15. def OAI.MUB6.Certificate.MixedSemantics.raw2step0 line 60
16. def OAI.MUB6.Certificate.MixedSemantics.raw2step0Labels line 61
17. def OAI.MUB6.Certificate.MixedSemantics.raw2step1 line 63
18. def OAI.MUB6.Certificate.MixedSemantics.raw2step1Labels line 64
19. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2 line 66
20. def OAI.MUB6.Certificate.MixedSemantics.raw3 line 81
21. def OAI.MUB6.Certificate.MixedSemantics.raw3Labels line 82
22. def OAI.MUB6.Certificate.MixedSemantics.raw3step0 line 84
23. def OAI.MUB6.Certificate.MixedSemantics.raw3step0Labels line 85
24. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3 line 87
25. def OAI.MUB6.Certificate.MixedSemantics.raw4 line 97
26. def OAI.MUB6.Certificate.MixedSemantics.raw4Labels line 98
27. def OAI.MUB6.Certificate.MixedSemantics.raw4step0 line 100
28. def OAI.MUB6.Certificate.MixedSemantics.raw4step0Labels line 101
29. def OAI.MUB6.Certificate.MixedSemantics.raw4step1 line 103
30. def OAI.MUB6.Certificate.MixedSemantics.raw4step1Labels line 104
31. theorem OAI.MUB6.Certificate.MixedSemantics.canonical4 line 106
32. def OAI.MUB6.Certificate.MixedSemantics.raw5 line 121
33. def OAI.MUB6.Certificate.MixedSemantics.raw5Labels line 122
34. def OAI.MUB6.Certificate.MixedSemantics.raw5step0 line 124
35. def OAI.MUB6.Certificate.MixedSemantics.raw5step0Labels line 125
36. theorem OAI.MUB6.Certificate.MixedSemantics.canonical5 line 127
37. def OAI.MUB6.Certificate.MixedSemantics.raw6 line 137
38. def OAI.MUB6.Certificate.MixedSemantics.raw6Labels line 138
39. def OAI.MUB6.Certificate.MixedSemantics.raw6step0 line 140
40. def OAI.MUB6.Certificate.MixedSemantics.raw6step0Labels line 141
41. def OAI.MUB6.Certificate.MixedSemantics.raw6step1 line 143
42. def OAI.MUB6.Certificate.MixedSemantics.raw6step1Labels line 144
43. theorem OAI.MUB6.Certificate.MixedSemantics.canonical6 line 146
44. def OAI.MUB6.Certificate.MixedSemantics.raw7 line 161
45. def OAI.MUB6.Certificate.MixedSemantics.raw7Labels line 162
46. def OAI.MUB6.Certificate.MixedSemantics.raw7step0 line 164
47. def OAI.MUB6.Certificate.MixedSemantics.raw7step0Labels line 165
48. theorem OAI.MUB6.Certificate.MixedSemantics.canonical7 line 167
49. def OAI.MUB6.Certificate.MixedSemantics.raw8 line 177
50. def OAI.MUB6.Certificate.MixedSemantics.raw8Labels line 178
51. def OAI.MUB6.Certificate.MixedSemantics.raw8step0 line 180
52. def OAI.MUB6.Certificate.MixedSemantics.raw8step0Labels line 181
53. def OAI.MUB6.Certificate.MixedSemantics.raw8step1 line 183
54. def OAI.MUB6.Certificate.MixedSemantics.raw8step1Labels line 184
55. theorem OAI.MUB6.Certificate.MixedSemantics.canonical8 line 186
56. def OAI.MUB6.Certificate.MixedSemantics.raw9 line 201
57. def OAI.MUB6.Certificate.MixedSemantics.raw9Labels line 202
58. def OAI.MUB6.Certificate.MixedSemantics.raw9step0 line 204
59. def OAI.MUB6.Certificate.MixedSemantics.raw9step0Labels line 205
60. theorem OAI.MUB6.Certificate.MixedSemantics.canonical9 line 207
61. def OAI.MUB6.Certificate.MixedSemantics.raw10 line 217
62. def OAI.MUB6.Certificate.MixedSemantics.raw10Labels line 218
63. def OAI.MUB6.Certificate.MixedSemantics.raw10step0 line 220
64. def OAI.MUB6.Certificate.MixedSemantics.raw10step0Labels line 221
65. def OAI.MUB6.Certificate.MixedSemantics.raw10step1 line 223
66. def OAI.MUB6.Certificate.MixedSemantics.raw10step1Labels line 224
67. theorem OAI.MUB6.Certificate.MixedSemantics.canonical10 line 226
68. def OAI.MUB6.Certificate.MixedSemantics.raw11 line 241
69. def OAI.MUB6.Certificate.MixedSemantics.raw11Labels line 242
70. def OAI.MUB6.Certificate.MixedSemantics.raw11step0 line 244
71. def OAI.MUB6.Certificate.MixedSemantics.raw11step0Labels line 245
72. theorem OAI.MUB6.Certificate.MixedSemantics.canonical11 line 247
73. def OAI.MUB6.Certificate.MixedSemantics.raw12 line 257
74. def OAI.MUB6.Certificate.MixedSemantics.raw12Labels line 258
75. def OAI.MUB6.Certificate.MixedSemantics.raw12step0 line 260
76. def OAI.MUB6.Certificate.MixedSemantics.raw12step0Labels line 261
77. def OAI.MUB6.Certificate.MixedSemantics.raw12step1 line 263
78. def OAI.MUB6.Certificate.MixedSemantics.raw12step1Labels line 264
79. theorem OAI.MUB6.Certificate.MixedSemantics.canonical12 line 266
80. def OAI.MUB6.Certificate.MixedSemantics.raw13 line 281
81. def OAI.MUB6.Certificate.MixedSemantics.raw13Labels line 282
82. def OAI.MUB6.Certificate.MixedSemantics.raw13step0 line 284
83. def OAI.MUB6.Certificate.MixedSemantics.raw13step0Labels line 285
84. theorem OAI.MUB6.Certificate.MixedSemantics.canonical13 line 287
85. def OAI.MUB6.Certificate.MixedSemantics.raw14 line 297
86. def OAI.MUB6.Certificate.MixedSemantics.raw14Labels line 298
87. def OAI.MUB6.Certificate.MixedSemantics.raw14step0 line 300
88. def OAI.MUB6.Certificate.MixedSemantics.raw14step0Labels line 301
89. def OAI.MUB6.Certificate.MixedSemantics.raw14step1 line 303
90. def OAI.MUB6.Certificate.MixedSemantics.raw14step1Labels line 304
91. theorem OAI.MUB6.Certificate.MixedSemantics.canonical14 line 306
92. def OAI.MUB6.Certificate.MixedSemantics.raw15 line 321
93. def OAI.MUB6.Certificate.MixedSemantics.raw15Labels line 322
94. def OAI.MUB6.Certificate.MixedSemantics.raw15step0 line 324
95. def OAI.MUB6.Certificate.MixedSemantics.raw15step0Labels line 325
96. theorem OAI.MUB6.Certificate.MixedSemantics.canonical15 line 327
97. def OAI.MUB6.Certificate.MixedSemantics.raw16 line 337
98. def OAI.MUB6.Certificate.MixedSemantics.raw16Labels line 338
99. def OAI.MUB6.Certificate.MixedSemantics.raw16step0 line 340
100. def OAI.MUB6.Certificate.MixedSemantics.raw16step0Labels line 341
101. def OAI.MUB6.Certificate.MixedSemantics.raw16step1 line 343
102. def OAI.MUB6.Certificate.MixedSemantics.raw16step1Labels line 344
103. theorem OAI.MUB6.Certificate.MixedSemantics.canonical16 line 346
104. def OAI.MUB6.Certificate.MixedSemantics.raw17 line 361
105. def OAI.MUB6.Certificate.MixedSemantics.raw17Labels line 362
106. def OAI.MUB6.Certificate.MixedSemantics.raw17step0 line 364
107. def OAI.MUB6.Certificate.MixedSemantics.raw17step0Labels line 365
108. theorem OAI.MUB6.Certificate.MixedSemantics.canonical17 line 367
109. def OAI.MUB6.Certificate.MixedSemantics.raw18 line 377
110. def OAI.MUB6.Certificate.MixedSemantics.raw18Labels line 378
111. def OAI.MUB6.Certificate.MixedSemantics.raw18step0 line 380
112. def OAI.MUB6.Certificate.MixedSemantics.raw18step0Labels line 381
113. def OAI.MUB6.Certificate.MixedSemantics.raw18step1 line 383
114. def OAI.MUB6.Certificate.MixedSemantics.raw18step1Labels line 384
115. theorem OAI.MUB6.Certificate.MixedSemantics.canonical18 line 386
116. def OAI.MUB6.Certificate.MixedSemantics.raw19 line 401
117. def OAI.MUB6.Certificate.MixedSemantics.raw19Labels line 402
118. def OAI.MUB6.Certificate.MixedSemantics.raw19step0 line 404
119. def OAI.MUB6.Certificate.MixedSemantics.raw19step0Labels line 405
120. theorem OAI.MUB6.Certificate.MixedSemantics.canonical19 line 407
121. def OAI.MUB6.Certificate.MixedSemantics.raw20 line 417
122. def OAI.MUB6.Certificate.MixedSemantics.raw20Labels line 418
123. def OAI.MUB6.Certificate.MixedSemantics.raw20step0 line 420
124. def OAI.MUB6.Certificate.MixedSemantics.raw20step0Labels line 421
125. def OAI.MUB6.Certificate.MixedSemantics.raw20step1 line 423
126. def OAI.MUB6.Certificate.MixedSemantics.raw20step1Labels line 424
127. theorem OAI.MUB6.Certificate.MixedSemantics.canonical20 line 426
128. def OAI.MUB6.Certificate.MixedSemantics.raw21 line 441
129. def OAI.MUB6.Certificate.MixedSemantics.raw21Labels line 442
130. def OAI.MUB6.Certificate.MixedSemantics.raw21step0 line 444
131. def OAI.MUB6.Certificate.MixedSemantics.raw21step0Labels line 445
132. theorem OAI.MUB6.Certificate.MixedSemantics.canonical21 line 447
133. def OAI.MUB6.Certificate.MixedSemantics.raw22 line 457
134. def OAI.MUB6.Certificate.MixedSemantics.raw22Labels line 458
135. def OAI.MUB6.Certificate.MixedSemantics.raw22step0 line 460
136. def OAI.MUB6.Certificate.MixedSemantics.raw22step0Labels line 461
137. def OAI.MUB6.Certificate.MixedSemantics.raw22step1 line 463
138. def OAI.MUB6.Certificate.MixedSemantics.raw22step1Labels line 464
139. theorem OAI.MUB6.Certificate.MixedSemantics.canonical22 line 466
140. def OAI.MUB6.Certificate.MixedSemantics.raw23 line 481
141. def OAI.MUB6.Certificate.MixedSemantics.raw23Labels line 482
142. def OAI.MUB6.Certificate.MixedSemantics.raw23step0 line 484
143. def OAI.MUB6.Certificate.MixedSemantics.raw23step0Labels line 485
144. theorem OAI.MUB6.Certificate.MixedSemantics.canonical23 line 487
145. def OAI.MUB6.Certificate.MixedSemantics.raw24 line 497
146. def OAI.MUB6.Certificate.MixedSemantics.raw24Labels line 498
147. def OAI.MUB6.Certificate.MixedSemantics.raw24step0 line 500
148. def OAI.MUB6.Certificate.MixedSemantics.raw24step0Labels line 501
149. def OAI.MUB6.Certificate.MixedSemantics.raw24step1 line 503
150. def OAI.MUB6.Certificate.MixedSemantics.raw24step1Labels line 504
151. theorem OAI.MUB6.Certificate.MixedSemantics.canonical24 line 506
152. def OAI.MUB6.Certificate.MixedSemantics.raw25 line 521
153. def OAI.MUB6.Certificate.MixedSemantics.raw25Labels line 522
154. def OAI.MUB6.Certificate.MixedSemantics.raw25step0 line 524
155. def OAI.MUB6.Certificate.MixedSemantics.raw25step0Labels line 525
156. theorem OAI.MUB6.Certificate.MixedSemantics.canonical25 line 527
157. def OAI.MUB6.Certificate.MixedSemantics.raw26 line 537
158. def OAI.MUB6.Certificate.MixedSemantics.raw26Labels line 538
159. def OAI.MUB6.Certificate.MixedSemantics.raw26step0 line 540
160. def OAI.MUB6.Certificate.MixedSemantics.raw26step0Labels line 541
161. def OAI.MUB6.Certificate.MixedSemantics.raw26step1 line 543
162. def OAI.MUB6.Certificate.MixedSemantics.raw26step1Labels line 544
163. theorem OAI.MUB6.Certificate.MixedSemantics.canonical26 line 546
164. def OAI.MUB6.Certificate.MixedSemantics.raw27 line 561
165. def OAI.MUB6.Certificate.MixedSemantics.raw27Labels line 562
166. def OAI.MUB6.Certificate.MixedSemantics.raw27step0 line 564
167. def OAI.MUB6.Certificate.MixedSemantics.raw27step0Labels line 565
168. theorem OAI.MUB6.Certificate.MixedSemantics.canonical27 line 567
169. def OAI.MUB6.Certificate.MixedSemantics.raw28 line 577
170. def OAI.MUB6.Certificate.MixedSemantics.raw28Labels line 578
171. def OAI.MUB6.Certificate.MixedSemantics.raw28step0 line 580
172. def OAI.MUB6.Certificate.MixedSemantics.raw28step0Labels line 581
173. def OAI.MUB6.Certificate.MixedSemantics.raw28step1 line 583
174. def OAI.MUB6.Certificate.MixedSemantics.raw28step1Labels line 584
175. theorem OAI.MUB6.Certificate.MixedSemantics.canonical28 line 586
176. def OAI.MUB6.Certificate.MixedSemantics.raw29 line 601
177. def OAI.MUB6.Certificate.MixedSemantics.raw29Labels line 602
178. def OAI.MUB6.Certificate.MixedSemantics.raw29step0 line 604
179. def OAI.MUB6.Certificate.MixedSemantics.raw29step0Labels line 605
180. theorem OAI.MUB6.Certificate.MixedSemantics.canonical29 line 607
181. def OAI.MUB6.Certificate.MixedSemantics.raw30 line 617
182. def OAI.MUB6.Certificate.MixedSemantics.raw30Labels line 618
183. def OAI.MUB6.Certificate.MixedSemantics.raw30step0 line 620
184. def OAI.MUB6.Certificate.MixedSemantics.raw30step0Labels line 621
185. def OAI.MUB6.Certificate.MixedSemantics.raw30step1 line 623
186. def OAI.MUB6.Certificate.MixedSemantics.raw30step1Labels line 624
187. theorem OAI.MUB6.Certificate.MixedSemantics.canonical30 line 626
188. def OAI.MUB6.Certificate.MixedSemantics.raw31 line 641
189. def OAI.MUB6.Certificate.MixedSemantics.raw31Labels line 642
190. def OAI.MUB6.Certificate.MixedSemantics.raw31step0 line 644
191. def OAI.MUB6.Certificate.MixedSemantics.raw31step0Labels line 645
192. theorem OAI.MUB6.Certificate.MixedSemantics.canonical31 line 647
193. def OAI.MUB6.Certificate.MixedSemantics.raw32 line 657
194. def OAI.MUB6.Certificate.MixedSemantics.raw32Labels line 658
195. def OAI.MUB6.Certificate.MixedSemantics.raw32step0 line 660
196. def OAI.MUB6.Certificate.MixedSemantics.raw32step0Labels line 661
197. def OAI.MUB6.Certificate.MixedSemantics.raw32step1 line 663
198. def OAI.MUB6.Certificate.MixedSemantics.raw32step1Labels line 664
199. theorem OAI.MUB6.Certificate.MixedSemantics.canonical32 line 666
200. def OAI.MUB6.Certificate.MixedSemantics.raw33 line 681
201. def OAI.MUB6.Certificate.MixedSemantics.raw33Labels line 682
202. def OAI.MUB6.Certificate.MixedSemantics.raw33step0 line 684
203. def OAI.MUB6.Certificate.MixedSemantics.raw33step0Labels line 685
204. theorem OAI.MUB6.Certificate.MixedSemantics.canonical33 line 687
205. def OAI.MUB6.Certificate.MixedSemantics.raw34 line 697
206. def OAI.MUB6.Certificate.MixedSemantics.raw34Labels line 698
207. def OAI.MUB6.Certificate.MixedSemantics.raw34step0 line 700
208. def OAI.MUB6.Certificate.MixedSemantics.raw34step0Labels line 701
209. def OAI.MUB6.Certificate.MixedSemantics.raw34step1 line 703
210. def OAI.MUB6.Certificate.MixedSemantics.raw34step1Labels line 704
211. theorem OAI.MUB6.Certificate.MixedSemantics.canonical34 line 706
212. def OAI.MUB6.Certificate.MixedSemantics.raw35 line 721
213. def OAI.MUB6.Certificate.MixedSemantics.raw35Labels line 722
214. def OAI.MUB6.Certificate.MixedSemantics.raw35step0 line 724
215. def OAI.MUB6.Certificate.MixedSemantics.raw35step0Labels line 725
216. theorem OAI.MUB6.Certificate.MixedSemantics.canonical35 line 727
217. def OAI.MUB6.Certificate.MixedSemantics.raw36 line 737
218. def OAI.MUB6.Certificate.MixedSemantics.raw36Labels line 738
219. def OAI.MUB6.Certificate.MixedSemantics.raw36step0 line 740
220. def OAI.MUB6.Certificate.MixedSemantics.raw36step0Labels line 741
221. def OAI.MUB6.Certificate.MixedSemantics.raw36step1 line 743
222. def OAI.MUB6.Certificate.MixedSemantics.raw36step1Labels line 744
223. theorem OAI.MUB6.Certificate.MixedSemantics.canonical36 line 746
224. def OAI.MUB6.Certificate.MixedSemantics.raw37 line 761
225. def OAI.MUB6.Certificate.MixedSemantics.raw37Labels line 762
226. def OAI.MUB6.Certificate.MixedSemantics.raw37step0 line 764
227. def OAI.MUB6.Certificate.MixedSemantics.raw37step0Labels line 765
228. theorem OAI.MUB6.Certificate.MixedSemantics.canonical37 line 767
229. def OAI.MUB6.Certificate.MixedSemantics.raw38 line 777
230. def OAI.MUB6.Certificate.MixedSemantics.raw38Labels line 778
231. def OAI.MUB6.Certificate.MixedSemantics.raw38step0 line 780
232. def OAI.MUB6.Certificate.MixedSemantics.raw38step0Labels line 781
233. def OAI.MUB6.Certificate.MixedSemantics.raw38step1 line 783
234. def OAI.MUB6.Certificate.MixedSemantics.raw38step1Labels line 784
235. theorem OAI.MUB6.Certificate.MixedSemantics.canonical38 line 786
236. def OAI.MUB6.Certificate.MixedSemantics.raw39 line 801
237. def OAI.MUB6.Certificate.MixedSemantics.raw39Labels line 802
238. def OAI.MUB6.Certificate.MixedSemantics.raw39step0 line 804
239. def OAI.MUB6.Certificate.MixedSemantics.raw39step0Labels line 805
240. def OAI.MUB6.Certificate.MixedSemantics.raw39step1 line 807
241. def OAI.MUB6.Certificate.MixedSemantics.raw39step1Labels line 808
242. theorem OAI.MUB6.Certificate.MixedSemantics.canonical39 line 810
243. def OAI.MUB6.Certificate.MixedSemantics.raw40 line 825
244. def OAI.MUB6.Certificate.MixedSemantics.raw40Labels line 826
245. def OAI.MUB6.Certificate.MixedSemantics.raw40step0 line 828
246. def OAI.MUB6.Certificate.MixedSemantics.raw40step0Labels line 829
247. def OAI.MUB6.Certificate.MixedSemantics.raw40step1 line 831
248. def OAI.MUB6.Certificate.MixedSemantics.raw40step1Labels line 832
249. theorem OAI.MUB6.Certificate.MixedSemantics.canonical40 line 834
250. def OAI.MUB6.Certificate.MixedSemantics.raw41 line 849
251. def OAI.MUB6.Certificate.MixedSemantics.raw41Labels line 850
252. def OAI.MUB6.Certificate.MixedSemantics.raw41step0 line 852
253. def OAI.MUB6.Certificate.MixedSemantics.raw41step0Labels line 853
254. theorem OAI.MUB6.Certificate.MixedSemantics.canonical41 line 855
255. def OAI.MUB6.Certificate.MixedSemantics.raw42 line 865
256. def OAI.MUB6.Certificate.MixedSemantics.raw42Labels line 866
257. def OAI.MUB6.Certificate.MixedSemantics.raw42step0 line 868
258. def OAI.MUB6.Certificate.MixedSemantics.raw42step0Labels line 869
259. def OAI.MUB6.Certificate.MixedSemantics.raw42step1 line 871
260. def OAI.MUB6.Certificate.MixedSemantics.raw42step1Labels line 872
261. theorem OAI.MUB6.Certificate.MixedSemantics.canonical42 line 874
262. def OAI.MUB6.Certificate.MixedSemantics.raw43 line 889
263. def OAI.MUB6.Certificate.MixedSemantics.raw43Labels line 890
264. def OAI.MUB6.Certificate.MixedSemantics.raw43step0 line 892
265. def OAI.MUB6.Certificate.MixedSemantics.raw43step0Labels line 893
266. theorem OAI.MUB6.Certificate.MixedSemantics.canonical43 line 895
267. def OAI.MUB6.Certificate.MixedSemantics.raw44 line 905
268. def OAI.MUB6.Certificate.MixedSemantics.raw44Labels line 906
269. def OAI.MUB6.Certificate.MixedSemantics.raw44step0 line 908
270. def OAI.MUB6.Certificate.MixedSemantics.raw44step0Labels line 909
271. def OAI.MUB6.Certificate.MixedSemantics.raw44step1 line 911
272. def OAI.MUB6.Certificate.MixedSemantics.raw44step1Labels line 912
273. theorem OAI.MUB6.Certificate.MixedSemantics.canonical44 line 914
274. def OAI.MUB6.Certificate.MixedSemantics.raw45 line 929
275. def OAI.MUB6.Certificate.MixedSemantics.raw45Labels line 930
276. def OAI.MUB6.Certificate.MixedSemantics.raw45step0 line 932
277. def OAI.MUB6.Certificate.MixedSemantics.raw45step0Labels line 933
278. theorem OAI.MUB6.Certificate.MixedSemantics.canonical45 line 935
279. def OAI.MUB6.Certificate.MixedSemantics.raw46 line 945
280. def OAI.MUB6.Certificate.MixedSemantics.raw46Labels line 946
281. def OAI.MUB6.Certificate.MixedSemantics.raw46step0 line 948
282. def OAI.MUB6.Certificate.MixedSemantics.raw46step0Labels line 949
283. def OAI.MUB6.Certificate.MixedSemantics.raw46step1 line 951
284. def OAI.MUB6.Certificate.MixedSemantics.raw46step1Labels line 952
285. theorem OAI.MUB6.Certificate.MixedSemantics.canonical46 line 954
286. def OAI.MUB6.Certificate.MixedSemantics.raw47 line 969
287. def OAI.MUB6.Certificate.MixedSemantics.raw47Labels line 970
288. def OAI.MUB6.Certificate.MixedSemantics.raw47step0 line 972
289. def OAI.MUB6.Certificate.MixedSemantics.raw47step0Labels line 973
290. theorem OAI.MUB6.Certificate.MixedSemantics.canonical47 line 975
291. def OAI.MUB6.Certificate.MixedSemantics.raw48 line 985
292. def OAI.MUB6.Certificate.MixedSemantics.raw48Labels line 986
293. def OAI.MUB6.Certificate.MixedSemantics.raw48step0 line 988
294. def OAI.MUB6.Certificate.MixedSemantics.raw48step0Labels line 989
295. def OAI.MUB6.Certificate.MixedSemantics.raw48step1 line 991
296. def OAI.MUB6.Certificate.MixedSemantics.raw48step1Labels line 992
297. theorem OAI.MUB6.Certificate.MixedSemantics.canonical48 line 994
298. def OAI.MUB6.Certificate.MixedSemantics.raw49 line 1009
299. def OAI.MUB6.Certificate.MixedSemantics.raw49Labels line 1010
300. def OAI.MUB6.Certificate.MixedSemantics.raw49step0 line 1012
301. def OAI.MUB6.Certificate.MixedSemantics.raw49step0Labels line 1013
302. theorem OAI.MUB6.Certificate.MixedSemantics.canonical49 line 1015
303. def OAI.MUB6.Certificate.MixedSemantics.raw50 line 1025
304. def OAI.MUB6.Certificate.MixedSemantics.raw50Labels line 1026
305. def OAI.MUB6.Certificate.MixedSemantics.raw50step0 line 1028
306. def OAI.MUB6.Certificate.MixedSemantics.raw50step0Labels line 1029
307. def OAI.MUB6.Certificate.MixedSemantics.raw50step1 line 1031
308. def OAI.MUB6.Certificate.MixedSemantics.raw50step1Labels line 1032
309. theorem OAI.MUB6.Certificate.MixedSemantics.canonical50 line 1034
310. def OAI.MUB6.Certificate.MixedSemantics.raw51 line 1049
311. def OAI.MUB6.Certificate.MixedSemantics.raw51Labels line 1050
312. def OAI.MUB6.Certificate.MixedSemantics.raw51step0 line 1052
313. def OAI.MUB6.Certificate.MixedSemantics.raw51step0Labels line 1053
314. def OAI.MUB6.Certificate.MixedSemantics.raw51step1 line 1055
315. def OAI.MUB6.Certificate.MixedSemantics.raw51step1Labels line 1056
316. theorem OAI.MUB6.Certificate.MixedSemantics.canonical51 line 1058
317. def OAI.MUB6.Certificate.MixedSemantics.raw52 line 1073
318. def OAI.MUB6.Certificate.MixedSemantics.raw52Labels line 1074
319. def OAI.MUB6.Certificate.MixedSemantics.raw52step0 line 1076
320. def OAI.MUB6.Certificate.MixedSemantics.raw52step0Labels line 1077
321. def OAI.MUB6.Certificate.MixedSemantics.raw52step1 line 1079
322. def OAI.MUB6.Certificate.MixedSemantics.raw52step1Labels line 1080
323. theorem OAI.MUB6.Certificate.MixedSemantics.canonical52 line 1082
324. def OAI.MUB6.Certificate.MixedSemantics.raw53 line 1097
325. def OAI.MUB6.Certificate.MixedSemantics.raw53Labels line 1098
326. def OAI.MUB6.Certificate.MixedSemantics.raw53step0 line 1100
327. def OAI.MUB6.Certificate.MixedSemantics.raw53step0Labels line 1101
328. theorem OAI.MUB6.Certificate.MixedSemantics.canonical53 line 1103
329. def OAI.MUB6.Certificate.MixedSemantics.raw54 line 1113
330. def OAI.MUB6.Certificate.MixedSemantics.raw54Labels line 1114
331. def OAI.MUB6.Certificate.MixedSemantics.raw54step0 line 1116
332. def OAI.MUB6.Certificate.MixedSemantics.raw54step0Labels line 1117
333. def OAI.MUB6.Certificate.MixedSemantics.raw54step1 line 1119
334. def OAI.MUB6.Certificate.MixedSemantics.raw54step1Labels line 1120
335. theorem OAI.MUB6.Certificate.MixedSemantics.canonical54 line 1122
336. def OAI.MUB6.Certificate.MixedSemantics.raw55 line 1137
337. def OAI.MUB6.Certificate.MixedSemantics.raw55Labels line 1138
338. def OAI.MUB6.Certificate.MixedSemantics.raw55step0 line 1140
339. def OAI.MUB6.Certificate.MixedSemantics.raw55step0Labels line 1141
340. theorem OAI.MUB6.Certificate.MixedSemantics.canonical55 line 1143
341. def OAI.MUB6.Certificate.MixedSemantics.raw56 line 1153
342. def OAI.MUB6.Certificate.MixedSemantics.raw56Labels line 1154
343. def OAI.MUB6.Certificate.MixedSemantics.raw56step0 line 1156
344. def OAI.MUB6.Certificate.MixedSemantics.raw56step0Labels line 1157
345. def OAI.MUB6.Certificate.MixedSemantics.raw56step1 line 1159
346. def OAI.MUB6.Certificate.MixedSemantics.raw56step1Labels line 1160
347. theorem OAI.MUB6.Certificate.MixedSemantics.canonical56 line 1162
348. def OAI.MUB6.Certificate.MixedSemantics.raw57 line 1177
349. def OAI.MUB6.Certificate.MixedSemantics.raw57Labels line 1178
350. def OAI.MUB6.Certificate.MixedSemantics.raw57step0 line 1180
351. def OAI.MUB6.Certificate.MixedSemantics.raw57step0Labels line 1181
352. theorem OAI.MUB6.Certificate.MixedSemantics.canonical57 line 1183
353. def OAI.MUB6.Certificate.MixedSemantics.raw58 line 1193
354. def OAI.MUB6.Certificate.MixedSemantics.raw58Labels line 1194
355. def OAI.MUB6.Certificate.MixedSemantics.raw58step0 line 1196
356. def OAI.MUB6.Certificate.MixedSemantics.raw58step0Labels line 1197
357. def OAI.MUB6.Certificate.MixedSemantics.raw58step1 line 1199
358. def OAI.MUB6.Certificate.MixedSemantics.raw58step1Labels line 1200
359. theorem OAI.MUB6.Certificate.MixedSemantics.canonical58 line 1202
360. def OAI.MUB6.Certificate.MixedSemantics.raw59 line 1217
361. def OAI.MUB6.Certificate.MixedSemantics.raw59Labels line 1218
362. def OAI.MUB6.Certificate.MixedSemantics.raw59step0 line 1220
363. def OAI.MUB6.Certificate.MixedSemantics.raw59step0Labels line 1221
364. theorem OAI.MUB6.Certificate.MixedSemantics.canonical59 line 1223
365. def OAI.MUB6.Certificate.MixedSemantics.raw60 line 1233
366. def OAI.MUB6.Certificate.MixedSemantics.raw60Labels line 1234
367. def OAI.MUB6.Certificate.MixedSemantics.raw60step0 line 1236
368. def OAI.MUB6.Certificate.MixedSemantics.raw60step0Labels line 1237
369. def OAI.MUB6.Certificate.MixedSemantics.raw60step1 line 1239
370. def OAI.MUB6.Certificate.MixedSemantics.raw60step1Labels line 1240
371. theorem OAI.MUB6.Certificate.MixedSemantics.canonical60 line 1242
372. def OAI.MUB6.Certificate.MixedSemantics.raw61 line 1257
373. def OAI.MUB6.Certificate.MixedSemantics.raw61Labels line 1258
374. def OAI.MUB6.Certificate.MixedSemantics.raw61step0 line 1260
375. def OAI.MUB6.Certificate.MixedSemantics.raw61step0Labels line 1261
376. theorem OAI.MUB6.Certificate.MixedSemantics.canonical61 line 1263
377. def OAI.MUB6.Certificate.MixedSemantics.raw62 line 1273
378. def OAI.MUB6.Certificate.MixedSemantics.raw62Labels line 1274
379. def OAI.MUB6.Certificate.MixedSemantics.raw62step0 line 1276
380. def OAI.MUB6.Certificate.MixedSemantics.raw62step0Labels line 1277
381. def OAI.MUB6.Certificate.MixedSemantics.raw62step1 line 1279
382. def OAI.MUB6.Certificate.MixedSemantics.raw62step1Labels line 1280
383. theorem OAI.MUB6.Certificate.MixedSemantics.canonical62 line 1282
384. def OAI.MUB6.Certificate.MixedSemantics.raw63 line 1297
385. def OAI.MUB6.Certificate.MixedSemantics.raw63Labels line 1298
386. def OAI.MUB6.Certificate.MixedSemantics.raw63step0 line 1300
387. def OAI.MUB6.Certificate.MixedSemantics.raw63step0Labels line 1301
388. theorem OAI.MUB6.Certificate.MixedSemantics.canonical63 line 1303
389. def OAI.MUB6.Certificate.MixedSemantics.raw64 line 1313
390. def OAI.MUB6.Certificate.MixedSemantics.raw64Labels line 1314
391. def OAI.MUB6.Certificate.MixedSemantics.raw64step0 line 1316
392. def OAI.MUB6.Certificate.MixedSemantics.raw64step0Labels line 1317
393. def OAI.MUB6.Certificate.MixedSemantics.raw64step1 line 1319
394. def OAI.MUB6.Certificate.MixedSemantics.raw64step1Labels line 1320
395. theorem OAI.MUB6.Certificate.MixedSemantics.canonical64 line 1322
396. def OAI.MUB6.Certificate.MixedSemantics.raw65 line 1337
397. def OAI.MUB6.Certificate.MixedSemantics.raw65Labels line 1338
398. def OAI.MUB6.Certificate.MixedSemantics.raw65step0 line 1340
399. def OAI.MUB6.Certificate.MixedSemantics.raw65step0Labels line 1341
400. def OAI.MUB6.Certificate.MixedSemantics.raw65step1 line 1343
401. def OAI.MUB6.Certificate.MixedSemantics.raw65step1Labels line 1344
402. theorem OAI.MUB6.Certificate.MixedSemantics.canonical65 line 1346
403. def OAI.MUB6.Certificate.MixedSemantics.raw66 line 1361
404. def OAI.MUB6.Certificate.MixedSemantics.raw66Labels line 1362
405. def OAI.MUB6.Certificate.MixedSemantics.raw66step0 line 1364
406. def OAI.MUB6.Certificate.MixedSemantics.raw66step0Labels line 1365
407. def OAI.MUB6.Certificate.MixedSemantics.raw66step1 line 1367
408. def OAI.MUB6.Certificate.MixedSemantics.raw66step1Labels line 1368
409. theorem OAI.MUB6.Certificate.MixedSemantics.canonical66 line 1370
410. def OAI.MUB6.Certificate.MixedSemantics.raw67 line 1385
411. def OAI.MUB6.Certificate.MixedSemantics.raw67Labels line 1386
412. def OAI.MUB6.Certificate.MixedSemantics.raw67step0 line 1388
413. def OAI.MUB6.Certificate.MixedSemantics.raw67step0Labels line 1389
414. theorem OAI.MUB6.Certificate.MixedSemantics.canonical67 line 1391
415. def OAI.MUB6.Certificate.MixedSemantics.raw68 line 1401
416. def OAI.MUB6.Certificate.MixedSemantics.raw68Labels line 1402
417. def OAI.MUB6.Certificate.MixedSemantics.raw68step0 line 1404
418. def OAI.MUB6.Certificate.MixedSemantics.raw68step0Labels line 1405
419. def OAI.MUB6.Certificate.MixedSemantics.raw68step1 line 1407
420. def OAI.MUB6.Certificate.MixedSemantics.raw68step1Labels line 1408
421. theorem OAI.MUB6.Certificate.MixedSemantics.canonical68 line 1410
422. def OAI.MUB6.Certificate.MixedSemantics.raw69 line 1425
423. def OAI.MUB6.Certificate.MixedSemantics.raw69Labels line 1426
424. def OAI.MUB6.Certificate.MixedSemantics.raw69step0 line 1428
425. def OAI.MUB6.Certificate.MixedSemantics.raw69step0Labels line 1429
426. theorem OAI.MUB6.Certificate.MixedSemantics.canonical69 line 1431
427. def OAI.MUB6.Certificate.MixedSemantics.raw70 line 1441
428. def OAI.MUB6.Certificate.MixedSemantics.raw70Labels line 1442
429. def OAI.MUB6.Certificate.MixedSemantics.raw70step0 line 1444
430. def OAI.MUB6.Certificate.MixedSemantics.raw70step0Labels line 1445
431. def OAI.MUB6.Certificate.MixedSemantics.raw70step1 line 1447
432. def OAI.MUB6.Certificate.MixedSemantics.raw70step1Labels line 1448
433. theorem OAI.MUB6.Certificate.MixedSemantics.canonical70 line 1450
434. def OAI.MUB6.Certificate.MixedSemantics.raw71 line 1465
435. def OAI.MUB6.Certificate.MixedSemantics.raw71Labels line 1466
436. def OAI.MUB6.Certificate.MixedSemantics.raw71step0 line 1468
437. def OAI.MUB6.Certificate.MixedSemantics.raw71step0Labels line 1469
438. def OAI.MUB6.Certificate.MixedSemantics.raw71step1 line 1471
439. def OAI.MUB6.Certificate.MixedSemantics.raw71step1Labels line 1472
440. theorem OAI.MUB6.Certificate.MixedSemantics.canonical71 line 1474
441. def OAI.MUB6.Certificate.MixedSemantics.raw72 line 1489
442. def OAI.MUB6.Certificate.MixedSemantics.raw72Labels line 1490
443. def OAI.MUB6.Certificate.MixedSemantics.raw72step0 line 1492
444. def OAI.MUB6.Certificate.MixedSemantics.raw72step0Labels line 1493
445. def OAI.MUB6.Certificate.MixedSemantics.raw72step1 line 1495
446. def OAI.MUB6.Certificate.MixedSemantics.raw72step1Labels line 1496
447. theorem OAI.MUB6.Certificate.MixedSemantics.canonical72 line 1498
448. def OAI.MUB6.Certificate.MixedSemantics.raw73 line 1513
449. def OAI.MUB6.Certificate.MixedSemantics.raw73Labels line 1514
450. def OAI.MUB6.Certificate.MixedSemantics.raw73step0 line 1516
451. def OAI.MUB6.Certificate.MixedSemantics.raw73step0Labels line 1517
452. theorem OAI.MUB6.Certificate.MixedSemantics.canonical73 line 1519
453. def OAI.MUB6.Certificate.MixedSemantics.raw74 line 1529
454. def OAI.MUB6.Certificate.MixedSemantics.raw74Labels line 1530
455. def OAI.MUB6.Certificate.MixedSemantics.raw74step0 line 1532
456. def OAI.MUB6.Certificate.MixedSemantics.raw74step0Labels line 1533
457. def OAI.MUB6.Certificate.MixedSemantics.raw74step1 line 1535
458. def OAI.MUB6.Certificate.MixedSemantics.raw74step1Labels line 1536
459. theorem OAI.MUB6.Certificate.MixedSemantics.canonical74 line 1538
460. def OAI.MUB6.Certificate.MixedSemantics.raw75 line 1553
461. def OAI.MUB6.Certificate.MixedSemantics.raw75Labels line 1554
462. def OAI.MUB6.Certificate.MixedSemantics.raw75step0 line 1556
463. def OAI.MUB6.Certificate.MixedSemantics.raw75step0Labels line 1557
464. theorem OAI.MUB6.Certificate.MixedSemantics.canonical75 line 1559
465. def OAI.MUB6.Certificate.MixedSemantics.raw76 line 1569
466. def OAI.MUB6.Certificate.MixedSemantics.raw76Labels line 1570
467. def OAI.MUB6.Certificate.MixedSemantics.raw76step0 line 1572
468. def OAI.MUB6.Certificate.MixedSemantics.raw76step0Labels line 1573
469. def OAI.MUB6.Certificate.MixedSemantics.raw76step1 line 1575
470. def OAI.MUB6.Certificate.MixedSemantics.raw76step1Labels line 1576
471. theorem OAI.MUB6.Certificate.MixedSemantics.canonical76 line 1578
472. def OAI.MUB6.Certificate.MixedSemantics.raw77 line 1593
473. def OAI.MUB6.Certificate.MixedSemantics.raw77Labels line 1594
474. def OAI.MUB6.Certificate.MixedSemantics.raw77step0 line 1596
475. def OAI.MUB6.Certificate.MixedSemantics.raw77step0Labels line 1597
476. theorem OAI.MUB6.Certificate.MixedSemantics.canonical77 line 1599
477. def OAI.MUB6.Certificate.MixedSemantics.raw78 line 1609
478. def OAI.MUB6.Certificate.MixedSemantics.raw78Labels line 1610
479. def OAI.MUB6.Certificate.MixedSemantics.raw78step0 line 1612
480. def OAI.MUB6.Certificate.MixedSemantics.raw78step0Labels line 1613
481. def OAI.MUB6.Certificate.MixedSemantics.raw78step1 line 1615
482. def OAI.MUB6.Certificate.MixedSemantics.raw78step1Labels line 1616
483. theorem OAI.MUB6.Certificate.MixedSemantics.canonical78 line 1618
484. def OAI.MUB6.Certificate.MixedSemantics.raw79 line 1633
485. def OAI.MUB6.Certificate.MixedSemantics.raw79Labels line 1634
486. def OAI.MUB6.Certificate.MixedSemantics.raw79step0 line 1636
487. def OAI.MUB6.Certificate.MixedSemantics.raw79step0Labels line 1637
488. theorem OAI.MUB6.Certificate.MixedSemantics.canonical79 line 1639
489. def OAI.MUB6.Certificate.MixedSemantics.raw80 line 1649
490. def OAI.MUB6.Certificate.MixedSemantics.raw80Labels line 1650
491. def OAI.MUB6.Certificate.MixedSemantics.raw80step0 line 1652
492. def OAI.MUB6.Certificate.MixedSemantics.raw80step0Labels line 1653
493. def OAI.MUB6.Certificate.MixedSemantics.raw80step1 line 1655
494. def OAI.MUB6.Certificate.MixedSemantics.raw80step1Labels line 1656
495. theorem OAI.MUB6.Certificate.MixedSemantics.canonical80 line 1658
496. def OAI.MUB6.Certificate.MixedSemantics.raw81 line 1673
497. def OAI.MUB6.Certificate.MixedSemantics.raw81Labels line 1674
498. def OAI.MUB6.Certificate.MixedSemantics.raw81step0 line 1676
499. def OAI.MUB6.Certificate.MixedSemantics.raw81step0Labels line 1677
500. theorem OAI.MUB6.Certificate.MixedSemantics.canonical81 line 1679
501. def OAI.MUB6.Certificate.MixedSemantics.raw82 line 1689
502. def OAI.MUB6.Certificate.MixedSemantics.raw82Labels line 1690
503. def OAI.MUB6.Certificate.MixedSemantics.raw82step0 line 1692
504. def OAI.MUB6.Certificate.MixedSemantics.raw82step0Labels line 1693
505. def OAI.MUB6.Certificate.MixedSemantics.raw82step1 line 1695
506. def OAI.MUB6.Certificate.MixedSemantics.raw82step1Labels line 1696
507. theorem OAI.MUB6.Certificate.MixedSemantics.canonical82 line 1698
508. def OAI.MUB6.Certificate.MixedSemantics.raw83 line 1713
509. def OAI.MUB6.Certificate.MixedSemantics.raw83Labels line 1714
510. def OAI.MUB6.Certificate.MixedSemantics.raw83step0 line 1716
511. def OAI.MUB6.Certificate.MixedSemantics.raw83step0Labels line 1717
512. theorem OAI.MUB6.Certificate.MixedSemantics.canonical83 line 1719
513. def OAI.MUB6.Certificate.MixedSemantics.raw84 line 1729
514. def OAI.MUB6.Certificate.MixedSemantics.raw84Labels line 1730
515. def OAI.MUB6.Certificate.MixedSemantics.raw84step0 line 1732
516. def OAI.MUB6.Certificate.MixedSemantics.raw84step0Labels line 1733
517. def OAI.MUB6.Certificate.MixedSemantics.raw84step1 line 1735
518. def OAI.MUB6.Certificate.MixedSemantics.raw84step1Labels line 1736
519. theorem OAI.MUB6.Certificate.MixedSemantics.canonical84 line 1738
520. def OAI.MUB6.Certificate.MixedSemantics.raw85 line 1753
521. def OAI.MUB6.Certificate.MixedSemantics.raw85Labels line 1754
522. def OAI.MUB6.Certificate.MixedSemantics.raw85step0 line 1756
523. def OAI.MUB6.Certificate.MixedSemantics.raw85step0Labels line 1757
524. theorem OAI.MUB6.Certificate.MixedSemantics.canonical85 line 1759
525. def OAI.MUB6.Certificate.MixedSemantics.raw86 line 1769
526. def OAI.MUB6.Certificate.MixedSemantics.raw86Labels line 1770
527. def OAI.MUB6.Certificate.MixedSemantics.raw86step0 line 1772
528. def OAI.MUB6.Certificate.MixedSemantics.raw86step0Labels line 1773
529. def OAI.MUB6.Certificate.MixedSemantics.raw86step1 line 1775
530. def OAI.MUB6.Certificate.MixedSemantics.raw86step1Labels line 1776
531. theorem OAI.MUB6.Certificate.MixedSemantics.canonical86 line 1778
532. def OAI.MUB6.Certificate.MixedSemantics.raw87 line 1793
533. def OAI.MUB6.Certificate.MixedSemantics.raw87Labels line 1794
534. def OAI.MUB6.Certificate.MixedSemantics.raw87step0 line 1796
535. def OAI.MUB6.Certificate.MixedSemantics.raw87step0Labels line 1797
536. theorem OAI.MUB6.Certificate.MixedSemantics.canonical87 line 1799
537. def OAI.MUB6.Certificate.MixedSemantics.raw88 line 1809
538. def OAI.MUB6.Certificate.MixedSemantics.raw88Labels line 1810
539. def OAI.MUB6.Certificate.MixedSemantics.raw88step0 line 1812
540. def OAI.MUB6.Certificate.MixedSemantics.raw88step0Labels line 1813
541. def OAI.MUB6.Certificate.MixedSemantics.raw88step1 line 1815
542. def OAI.MUB6.Certificate.MixedSemantics.raw88step1Labels line 1816
543. theorem OAI.MUB6.Certificate.MixedSemantics.canonical88 line 1818
544. def OAI.MUB6.Certificate.MixedSemantics.raw89 line 1833
545. def OAI.MUB6.Certificate.MixedSemantics.raw89Labels line 1834
546. def OAI.MUB6.Certificate.MixedSemantics.raw89step0 line 1836
547. def OAI.MUB6.Certificate.MixedSemantics.raw89step0Labels line 1837
548. theorem OAI.MUB6.Certificate.MixedSemantics.canonical89 line 1839
549. def OAI.MUB6.Certificate.MixedSemantics.raw90 line 1849
550. def OAI.MUB6.Certificate.MixedSemantics.raw90Labels line 1850
551. def OAI.MUB6.Certificate.MixedSemantics.raw90step0 line 1852
552. def OAI.MUB6.Certificate.MixedSemantics.raw90step0Labels line 1853
553. def OAI.MUB6.Certificate.MixedSemantics.raw90step1 line 1855
554. def OAI.MUB6.Certificate.MixedSemantics.raw90step1Labels line 1856
555. theorem OAI.MUB6.Certificate.MixedSemantics.canonical90 line 1858
556. def OAI.MUB6.Certificate.MixedSemantics.raw91 line 1873
557. def OAI.MUB6.Certificate.MixedSemantics.raw91Labels line 1874
558. def OAI.MUB6.Certificate.MixedSemantics.raw91step0 line 1876
559. def OAI.MUB6.Certificate.MixedSemantics.raw91step0Labels line 1877
560. theorem OAI.MUB6.Certificate.MixedSemantics.canonical91 line 1879
561. def OAI.MUB6.Certificate.MixedSemantics.raw92 line 1889
562. def OAI.MUB6.Certificate.MixedSemantics.raw92Labels line 1890
563. def OAI.MUB6.Certificate.MixedSemantics.raw92step0 line 1892
564. def OAI.MUB6.Certificate.MixedSemantics.raw92step0Labels line 1893
565. def OAI.MUB6.Certificate.MixedSemantics.raw92step1 line 1895
566. def OAI.MUB6.Certificate.MixedSemantics.raw92step1Labels line 1896
567. theorem OAI.MUB6.Certificate.MixedSemantics.canonical92 line 1898
568. def OAI.MUB6.Certificate.MixedSemantics.raw93 line 1913
569. def OAI.MUB6.Certificate.MixedSemantics.raw93Labels line 1914
570. def OAI.MUB6.Certificate.MixedSemantics.raw93step0 line 1916
571. def OAI.MUB6.Certificate.MixedSemantics.raw93step0Labels line 1917
572. theorem OAI.MUB6.Certificate.MixedSemantics.canonical93 line 1919
573. def OAI.MUB6.Certificate.MixedSemantics.raw94 line 1929
574. def OAI.MUB6.Certificate.MixedSemantics.raw94Labels line 1930
575. def OAI.MUB6.Certificate.MixedSemantics.raw94step0 line 1932
576. def OAI.MUB6.Certificate.MixedSemantics.raw94step0Labels line 1933
577. def OAI.MUB6.Certificate.MixedSemantics.raw94step1 line 1935
578. def OAI.MUB6.Certificate.MixedSemantics.raw94step1Labels line 1936
579. theorem OAI.MUB6.Certificate.MixedSemantics.canonical94 line 1938
580. def OAI.MUB6.Certificate.MixedSemantics.raw95 line 1953
581. def OAI.MUB6.Certificate.MixedSemantics.raw95Labels line 1954
582. def OAI.MUB6.Certificate.MixedSemantics.raw95step0 line 1956
583. def OAI.MUB6.Certificate.MixedSemantics.raw95step0Labels line 1957
584. theorem OAI.MUB6.Certificate.MixedSemantics.canonical95 line 1959
585. def OAI.MUB6.Certificate.MixedSemantics.raw96 line 1969
586. def OAI.MUB6.Certificate.MixedSemantics.raw96Labels line 1970
587. def OAI.MUB6.Certificate.MixedSemantics.raw96step0 line 1972
588. def OAI.MUB6.Certificate.MixedSemantics.raw96step0Labels line 1973
589. def OAI.MUB6.Certificate.MixedSemantics.raw96step1 line 1975
590. def OAI.MUB6.Certificate.MixedSemantics.raw96step1Labels line 1976
591. theorem OAI.MUB6.Certificate.MixedSemantics.canonical96 line 1978
592. def OAI.MUB6.Certificate.MixedSemantics.raw97 line 1993
593. def OAI.MUB6.Certificate.MixedSemantics.raw97Labels line 1994
594. def OAI.MUB6.Certificate.MixedSemantics.raw97step0 line 1996
595. def OAI.MUB6.Certificate.MixedSemantics.raw97step0Labels line 1997
596. theorem OAI.MUB6.Certificate.MixedSemantics.canonical97 line 1999
597. def OAI.MUB6.Certificate.MixedSemantics.raw98 line 2009
598. def OAI.MUB6.Certificate.MixedSemantics.raw98Labels line 2010
599. def OAI.MUB6.Certificate.MixedSemantics.raw98step0 line 2012
600. def OAI.MUB6.Certificate.MixedSemantics.raw98step0Labels line 2013
601. def OAI.MUB6.Certificate.MixedSemantics.raw98step1 line 2015
602. def OAI.MUB6.Certificate.MixedSemantics.raw98step1Labels line 2016
603. theorem OAI.MUB6.Certificate.MixedSemantics.canonical98 line 2018
604. def OAI.MUB6.Certificate.MixedSemantics.raw99 line 2033
605. def OAI.MUB6.Certificate.MixedSemantics.raw99Labels line 2034
606. def OAI.MUB6.Certificate.MixedSemantics.raw99step0 line 2036
607. def OAI.MUB6.Certificate.MixedSemantics.raw99step0Labels line 2037
608. theorem OAI.MUB6.Certificate.MixedSemantics.canonical99 line 2039
609. def OAI.MUB6.Certificate.MixedSemantics.raw100 line 2049
610. def OAI.MUB6.Certificate.MixedSemantics.raw100Labels line 2050
611. def OAI.MUB6.Certificate.MixedSemantics.raw100step0 line 2052
612. def OAI.MUB6.Certificate.MixedSemantics.raw100step0Labels line 2053
613. def OAI.MUB6.Certificate.MixedSemantics.raw100step1 line 2055
614. def OAI.MUB6.Certificate.MixedSemantics.raw100step1Labels line 2056
615. theorem OAI.MUB6.Certificate.MixedSemantics.canonical100 line 2058
616. def OAI.MUB6.Certificate.MixedSemantics.raw101 line 2073
617. def OAI.MUB6.Certificate.MixedSemantics.raw101Labels line 2074
618. def OAI.MUB6.Certificate.MixedSemantics.raw101step0 line 2076
619. def OAI.MUB6.Certificate.MixedSemantics.raw101step0Labels line 2077
620. theorem OAI.MUB6.Certificate.MixedSemantics.canonical101 line 2079
621. def OAI.MUB6.Certificate.MixedSemantics.raw102 line 2089
622. def OAI.MUB6.Certificate.MixedSemantics.raw102Labels line 2090
623. def OAI.MUB6.Certificate.MixedSemantics.raw102step0 line 2092
624. def OAI.MUB6.Certificate.MixedSemantics.raw102step0Labels line 2093
625. def OAI.MUB6.Certificate.MixedSemantics.raw102step1 line 2095
626. def OAI.MUB6.Certificate.MixedSemantics.raw102step1Labels line 2096
627. theorem OAI.MUB6.Certificate.MixedSemantics.canonical102 line 2098
628. def OAI.MUB6.Certificate.MixedSemantics.raw103 line 2113
629. def OAI.MUB6.Certificate.MixedSemantics.raw103Labels line 2114
630. def OAI.MUB6.Certificate.MixedSemantics.raw103step0 line 2116
631. def OAI.MUB6.Certificate.MixedSemantics.raw103step0Labels line 2117
632. theorem OAI.MUB6.Certificate.MixedSemantics.canonical103 line 2119
633. def OAI.MUB6.Certificate.MixedSemantics.raw104 line 2129
634. def OAI.MUB6.Certificate.MixedSemantics.raw104Labels line 2130
635. def OAI.MUB6.Certificate.MixedSemantics.raw104step0 line 2132
636. def OAI.MUB6.Certificate.MixedSemantics.raw104step0Labels line 2133
637. def OAI.MUB6.Certificate.MixedSemantics.raw104step1 line 2135
638. def OAI.MUB6.Certificate.MixedSemantics.raw104step1Labels line 2136
639. theorem OAI.MUB6.Certificate.MixedSemantics.canonical104 line 2138
640. def OAI.MUB6.Certificate.MixedSemantics.raw105 line 2153
641. def OAI.MUB6.Certificate.MixedSemantics.raw105Labels line 2154
642. def OAI.MUB6.Certificate.MixedSemantics.raw105step0 line 2156
643. def OAI.MUB6.Certificate.MixedSemantics.raw105step0Labels line 2157
644. theorem OAI.MUB6.Certificate.MixedSemantics.canonical105 line 2159
645. def OAI.MUB6.Certificate.MixedSemantics.raw106 line 2169
646. def OAI.MUB6.Certificate.MixedSemantics.raw106Labels line 2170
647. def OAI.MUB6.Certificate.MixedSemantics.raw106step0 line 2172
648. def OAI.MUB6.Certificate.MixedSemantics.raw106step0Labels line 2173
649. def OAI.MUB6.Certificate.MixedSemantics.raw106step1 line 2175
650. def OAI.MUB6.Certificate.MixedSemantics.raw106step1Labels line 2176
651. theorem OAI.MUB6.Certificate.MixedSemantics.canonical106 line 2178
652. def OAI.MUB6.Certificate.MixedSemantics.raw107 line 2193
653. def OAI.MUB6.Certificate.MixedSemantics.raw107Labels line 2194
654. def OAI.MUB6.Certificate.MixedSemantics.raw107step0 line 2196
655. def OAI.MUB6.Certificate.MixedSemantics.raw107step0Labels line 2197
656. theorem OAI.MUB6.Certificate.MixedSemantics.canonical107 line 2199
657. def OAI.MUB6.Certificate.MixedSemantics.raw108 line 2209
658. def OAI.MUB6.Certificate.MixedSemantics.raw108Labels line 2210
659. def OAI.MUB6.Certificate.MixedSemantics.raw108step0 line 2212
660. def OAI.MUB6.Certificate.MixedSemantics.raw108step0Labels line 2213
661. def OAI.MUB6.Certificate.MixedSemantics.raw108step1 line 2215
662. def OAI.MUB6.Certificate.MixedSemantics.raw108step1Labels line 2216
663. theorem OAI.MUB6.Certificate.MixedSemantics.canonical108 line 2218
664. def OAI.MUB6.Certificate.MixedSemantics.raw109 line 2233
665. def OAI.MUB6.Certificate.MixedSemantics.raw109Labels line 2234
666. def OAI.MUB6.Certificate.MixedSemantics.raw109step0 line 2236
667. def OAI.MUB6.Certificate.MixedSemantics.raw109step0Labels line 2237
668. theorem OAI.MUB6.Certificate.MixedSemantics.canonical109 line 2239
669. def OAI.MUB6.Certificate.MixedSemantics.raw110 line 2249
670. def OAI.MUB6.Certificate.MixedSemantics.raw110Labels line 2250
671. def OAI.MUB6.Certificate.MixedSemantics.raw110step0 line 2252
672. def OAI.MUB6.Certificate.MixedSemantics.raw110step0Labels line 2253
673. def OAI.MUB6.Certificate.MixedSemantics.raw110step1 line 2255
674. def OAI.MUB6.Certificate.MixedSemantics.raw110step1Labels line 2256
675. theorem OAI.MUB6.Certificate.MixedSemantics.canonical110 line 2258
676. def OAI.MUB6.Certificate.MixedSemantics.raw111 line 2273
677. def OAI.MUB6.Certificate.MixedSemantics.raw111Labels line 2274
678. def OAI.MUB6.Certificate.MixedSemantics.raw111step0 line 2276
679. def OAI.MUB6.Certificate.MixedSemantics.raw111step0Labels line 2277
680. theorem OAI.MUB6.Certificate.MixedSemantics.canonical111 line 2279
681. def OAI.MUB6.Certificate.MixedSemantics.raw112 line 2289
682. def OAI.MUB6.Certificate.MixedSemantics.raw112Labels line 2290
683. def OAI.MUB6.Certificate.MixedSemantics.raw112step0 line 2292
684. def OAI.MUB6.Certificate.MixedSemantics.raw112step0Labels line 2293
685. def OAI.MUB6.Certificate.MixedSemantics.raw112step1 line 2295
686. def OAI.MUB6.Certificate.MixedSemantics.raw112step1Labels line 2296
687. theorem OAI.MUB6.Certificate.MixedSemantics.canonical112 line 2298
688. def OAI.MUB6.Certificate.MixedSemantics.raw113 line 2313
689. def OAI.MUB6.Certificate.MixedSemantics.raw113Labels line 2314
690. def OAI.MUB6.Certificate.MixedSemantics.raw113step0 line 2316
691. def OAI.MUB6.Certificate.MixedSemantics.raw113step0Labels line 2317
692. theorem OAI.MUB6.Certificate.MixedSemantics.canonical113 line 2319
693. def OAI.MUB6.Certificate.MixedSemantics.raw114 line 2329
694. def OAI.MUB6.Certificate.MixedSemantics.raw114Labels line 2330
695. def OAI.MUB6.Certificate.MixedSemantics.raw114step0 line 2332
696. def OAI.MUB6.Certificate.MixedSemantics.raw114step0Labels line 2333
697. def OAI.MUB6.Certificate.MixedSemantics.raw114step1 line 2335
698. def OAI.MUB6.Certificate.MixedSemantics.raw114step1Labels line 2336
699. theorem OAI.MUB6.Certificate.MixedSemantics.canonical114 line 2338
700. def OAI.MUB6.Certificate.MixedSemantics.raw115 line 2353
701. def OAI.MUB6.Certificate.MixedSemantics.raw115Labels line 2354
702. def OAI.MUB6.Certificate.MixedSemantics.raw115step0 line 2356
703. def OAI.MUB6.Certificate.MixedSemantics.raw115step0Labels line 2357
704. theorem OAI.MUB6.Certificate.MixedSemantics.canonical115 line 2359
705. def OAI.MUB6.Certificate.MixedSemantics.raw116 line 2369
706. def OAI.MUB6.Certificate.MixedSemantics.raw116Labels line 2370
707. def OAI.MUB6.Certificate.MixedSemantics.raw116step0 line 2372
708. def OAI.MUB6.Certificate.MixedSemantics.raw116step0Labels line 2373
709. def OAI.MUB6.Certificate.MixedSemantics.raw116step1 line 2375
710. def OAI.MUB6.Certificate.MixedSemantics.raw116step1Labels line 2376
711. theorem OAI.MUB6.Certificate.MixedSemantics.canonical116 line 2378
712. def OAI.MUB6.Certificate.MixedSemantics.raw117 line 2393
713. def OAI.MUB6.Certificate.MixedSemantics.raw117Labels line 2394
714. def OAI.MUB6.Certificate.MixedSemantics.raw117step0 line 2396
715. def OAI.MUB6.Certificate.MixedSemantics.raw117step0Labels line 2397
716. theorem OAI.MUB6.Certificate.MixedSemantics.canonical117 line 2399
717. def OAI.MUB6.Certificate.MixedSemantics.raw118 line 2409
718. def OAI.MUB6.Certificate.MixedSemantics.raw118Labels line 2410
719. def OAI.MUB6.Certificate.MixedSemantics.raw118step0 line 2412
720. def OAI.MUB6.Certificate.MixedSemantics.raw118step0Labels line 2413
721. def OAI.MUB6.Certificate.MixedSemantics.raw118step1 line 2415
722. def OAI.MUB6.Certificate.MixedSemantics.raw118step1Labels line 2416
723. theorem OAI.MUB6.Certificate.MixedSemantics.canonical118 line 2418
724. def OAI.MUB6.Certificate.MixedSemantics.raw119 line 2433
725. def OAI.MUB6.Certificate.MixedSemantics.raw119Labels line 2434
726. def OAI.MUB6.Certificate.MixedSemantics.raw119step0 line 2436
727. def OAI.MUB6.Certificate.MixedSemantics.raw119step0Labels line 2437
728. theorem OAI.MUB6.Certificate.MixedSemantics.canonical119 line 2439
729. def OAI.MUB6.Certificate.MixedSemantics.raw120 line 2449
730. def OAI.MUB6.Certificate.MixedSemantics.raw120Labels line 2450
731. def OAI.MUB6.Certificate.MixedSemantics.raw120step0 line 2452
732. def OAI.MUB6.Certificate.MixedSemantics.raw120step0Labels line 2453
733. def OAI.MUB6.Certificate.MixedSemantics.raw120step1 line 2455
734. def OAI.MUB6.Certificate.MixedSemantics.raw120step1Labels line 2456
735. theorem OAI.MUB6.Certificate.MixedSemantics.canonical120 line 2458
736. def OAI.MUB6.Certificate.MixedSemantics.raw121 line 2473
737. def OAI.MUB6.Certificate.MixedSemantics.raw121Labels line 2474
738. def OAI.MUB6.Certificate.MixedSemantics.raw121step0 line 2476
739. def OAI.MUB6.Certificate.MixedSemantics.raw121step0Labels line 2477
740. theorem OAI.MUB6.Certificate.MixedSemantics.canonical121 line 2479
741. def OAI.MUB6.Certificate.MixedSemantics.raw122 line 2489
742. def OAI.MUB6.Certificate.MixedSemantics.raw122Labels line 2490
743. def OAI.MUB6.Certificate.MixedSemantics.raw122step0 line 2492
744. def OAI.MUB6.Certificate.MixedSemantics.raw122step0Labels line 2493
745. def OAI.MUB6.Certificate.MixedSemantics.raw122step1 line 2495
746. def OAI.MUB6.Certificate.MixedSemantics.raw122step1Labels line 2496
747. theorem OAI.MUB6.Certificate.MixedSemantics.canonical122 line 2498
748. def OAI.MUB6.Certificate.MixedSemantics.raw123 line 2513
749. def OAI.MUB6.Certificate.MixedSemantics.raw123Labels line 2514
750. def OAI.MUB6.Certificate.MixedSemantics.raw123step0 line 2516
751. def OAI.MUB6.Certificate.MixedSemantics.raw123step0Labels line 2517
752. theorem OAI.MUB6.Certificate.MixedSemantics.canonical123 line 2519
753. def OAI.MUB6.Certificate.MixedSemantics.raw124 line 2529
754. def OAI.MUB6.Certificate.MixedSemantics.raw124Labels line 2530
755. def OAI.MUB6.Certificate.MixedSemantics.raw124step0 line 2532
756. def OAI.MUB6.Certificate.MixedSemantics.raw124step0Labels line 2533
757. def OAI.MUB6.Certificate.MixedSemantics.raw124step1 line 2535
758. def OAI.MUB6.Certificate.MixedSemantics.raw124step1Labels line 2536
759. theorem OAI.MUB6.Certificate.MixedSemantics.canonical124 line 2538
760. def OAI.MUB6.Certificate.MixedSemantics.raw125 line 2553
761. def OAI.MUB6.Certificate.MixedSemantics.raw125Labels line 2554
762. def OAI.MUB6.Certificate.MixedSemantics.raw125step0 line 2556
763. def OAI.MUB6.Certificate.MixedSemantics.raw125step0Labels line 2557
764. theorem OAI.MUB6.Certificate.MixedSemantics.canonical125 line 2559
765. def OAI.MUB6.Certificate.MixedSemantics.raw126 line 2569
766. def OAI.MUB6.Certificate.MixedSemantics.raw126Labels line 2570
767. def OAI.MUB6.Certificate.MixedSemantics.raw126step0 line 2572
768. def OAI.MUB6.Certificate.MixedSemantics.raw126step0Labels line 2573
769. def OAI.MUB6.Certificate.MixedSemantics.raw126step1 line 2575
770. def OAI.MUB6.Certificate.MixedSemantics.raw126step1Labels line 2576
771. theorem OAI.MUB6.Certificate.MixedSemantics.canonical126 line 2578
772. def OAI.MUB6.Certificate.MixedSemantics.raw127 line 2593
773. def OAI.MUB6.Certificate.MixedSemantics.raw127Labels line 2594
774. def OAI.MUB6.Certificate.MixedSemantics.raw127step0 line 2596
775. def OAI.MUB6.Certificate.MixedSemantics.raw127step0Labels line 2597
776. theorem OAI.MUB6.Certificate.MixedSemantics.canonical127 line 2599