OAI/Analysis/MutuallyUnbiased/MixedSemantics/Canonical1.lean

GitHub source file

798 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.raw128 line 20
2. def OAI.MUB6.Certificate.MixedSemantics.raw128Labels line 21
3. def OAI.MUB6.Certificate.MixedSemantics.raw128step0 line 23
4. def OAI.MUB6.Certificate.MixedSemantics.raw128step0Labels line 24
5. def OAI.MUB6.Certificate.MixedSemantics.raw128step1 line 26
6. def OAI.MUB6.Certificate.MixedSemantics.raw128step1Labels line 27
7. theorem OAI.MUB6.Certificate.MixedSemantics.canonical128 line 29
8. def OAI.MUB6.Certificate.MixedSemantics.raw129 line 44
9. def OAI.MUB6.Certificate.MixedSemantics.raw129Labels line 45
10. def OAI.MUB6.Certificate.MixedSemantics.raw129step0 line 47
11. def OAI.MUB6.Certificate.MixedSemantics.raw129step0Labels line 48
12. theorem OAI.MUB6.Certificate.MixedSemantics.canonical129 line 50
13. def OAI.MUB6.Certificate.MixedSemantics.raw130 line 60
14. def OAI.MUB6.Certificate.MixedSemantics.raw130Labels line 61
15. def OAI.MUB6.Certificate.MixedSemantics.raw130step0 line 63
16. def OAI.MUB6.Certificate.MixedSemantics.raw130step0Labels line 64
17. def OAI.MUB6.Certificate.MixedSemantics.raw130step1 line 66
18. def OAI.MUB6.Certificate.MixedSemantics.raw130step1Labels line 67
19. theorem OAI.MUB6.Certificate.MixedSemantics.canonical130 line 69
20. def OAI.MUB6.Certificate.MixedSemantics.raw131 line 84
21. def OAI.MUB6.Certificate.MixedSemantics.raw131Labels line 85
22. def OAI.MUB6.Certificate.MixedSemantics.raw131step0 line 87
23. def OAI.MUB6.Certificate.MixedSemantics.raw131step0Labels line 88
24. theorem OAI.MUB6.Certificate.MixedSemantics.canonical131 line 90
25. def OAI.MUB6.Certificate.MixedSemantics.raw132 line 100
26. def OAI.MUB6.Certificate.MixedSemantics.raw132Labels line 101
27. def OAI.MUB6.Certificate.MixedSemantics.raw132step0 line 103
28. def OAI.MUB6.Certificate.MixedSemantics.raw132step0Labels line 104
29. def OAI.MUB6.Certificate.MixedSemantics.raw132step1 line 106
30. def OAI.MUB6.Certificate.MixedSemantics.raw132step1Labels line 107
31. theorem OAI.MUB6.Certificate.MixedSemantics.canonical132 line 109
32. def OAI.MUB6.Certificate.MixedSemantics.raw133 line 124
33. def OAI.MUB6.Certificate.MixedSemantics.raw133Labels line 125
34. def OAI.MUB6.Certificate.MixedSemantics.raw133step0 line 127
35. def OAI.MUB6.Certificate.MixedSemantics.raw133step0Labels line 128
36. theorem OAI.MUB6.Certificate.MixedSemantics.canonical133 line 130
37. def OAI.MUB6.Certificate.MixedSemantics.raw134 line 140
38. def OAI.MUB6.Certificate.MixedSemantics.raw134Labels line 141
39. def OAI.MUB6.Certificate.MixedSemantics.raw134step0 line 143
40. def OAI.MUB6.Certificate.MixedSemantics.raw134step0Labels line 144
41. def OAI.MUB6.Certificate.MixedSemantics.raw134step1 line 146
42. def OAI.MUB6.Certificate.MixedSemantics.raw134step1Labels line 147
43. theorem OAI.MUB6.Certificate.MixedSemantics.canonical134 line 149
44. def OAI.MUB6.Certificate.MixedSemantics.raw135 line 164
45. def OAI.MUB6.Certificate.MixedSemantics.raw135Labels line 165
46. def OAI.MUB6.Certificate.MixedSemantics.raw135step0 line 167
47. def OAI.MUB6.Certificate.MixedSemantics.raw135step0Labels line 168
48. theorem OAI.MUB6.Certificate.MixedSemantics.canonical135 line 170
49. def OAI.MUB6.Certificate.MixedSemantics.raw136 line 180
50. def OAI.MUB6.Certificate.MixedSemantics.raw136Labels line 181
51. def OAI.MUB6.Certificate.MixedSemantics.raw136step0 line 183
52. def OAI.MUB6.Certificate.MixedSemantics.raw136step0Labels line 184
53. def OAI.MUB6.Certificate.MixedSemantics.raw136step1 line 186
54. def OAI.MUB6.Certificate.MixedSemantics.raw136step1Labels line 187
55. theorem OAI.MUB6.Certificate.MixedSemantics.canonical136 line 189
56. def OAI.MUB6.Certificate.MixedSemantics.raw137 line 204
57. def OAI.MUB6.Certificate.MixedSemantics.raw137Labels line 205
58. def OAI.MUB6.Certificate.MixedSemantics.raw137step0 line 207
59. def OAI.MUB6.Certificate.MixedSemantics.raw137step0Labels line 208
60. theorem OAI.MUB6.Certificate.MixedSemantics.canonical137 line 210
61. def OAI.MUB6.Certificate.MixedSemantics.raw138 line 220
62. def OAI.MUB6.Certificate.MixedSemantics.raw138Labels line 221
63. def OAI.MUB6.Certificate.MixedSemantics.raw138step0 line 223
64. def OAI.MUB6.Certificate.MixedSemantics.raw138step0Labels line 224
65. def OAI.MUB6.Certificate.MixedSemantics.raw138step1 line 226
66. def OAI.MUB6.Certificate.MixedSemantics.raw138step1Labels line 227
67. theorem OAI.MUB6.Certificate.MixedSemantics.canonical138 line 229
68. def OAI.MUB6.Certificate.MixedSemantics.raw139 line 244
69. def OAI.MUB6.Certificate.MixedSemantics.raw139Labels line 245
70. def OAI.MUB6.Certificate.MixedSemantics.raw139step0 line 247
71. def OAI.MUB6.Certificate.MixedSemantics.raw139step0Labels line 248
72. theorem OAI.MUB6.Certificate.MixedSemantics.canonical139 line 250
73. def OAI.MUB6.Certificate.MixedSemantics.raw140 line 260
74. def OAI.MUB6.Certificate.MixedSemantics.raw140Labels line 261
75. def OAI.MUB6.Certificate.MixedSemantics.raw140step0 line 263
76. def OAI.MUB6.Certificate.MixedSemantics.raw140step0Labels line 264
77. def OAI.MUB6.Certificate.MixedSemantics.raw140step1 line 266
78. def OAI.MUB6.Certificate.MixedSemantics.raw140step1Labels line 267
79. theorem OAI.MUB6.Certificate.MixedSemantics.canonical140 line 269
80. def OAI.MUB6.Certificate.MixedSemantics.raw141 line 284
81. def OAI.MUB6.Certificate.MixedSemantics.raw141Labels line 285
82. def OAI.MUB6.Certificate.MixedSemantics.raw141step0 line 287
83. def OAI.MUB6.Certificate.MixedSemantics.raw141step0Labels line 288
84. theorem OAI.MUB6.Certificate.MixedSemantics.canonical141 line 290
85. def OAI.MUB6.Certificate.MixedSemantics.raw142 line 300
86. def OAI.MUB6.Certificate.MixedSemantics.raw142Labels line 301
87. def OAI.MUB6.Certificate.MixedSemantics.raw142step0 line 303
88. def OAI.MUB6.Certificate.MixedSemantics.raw142step0Labels line 304
89. def OAI.MUB6.Certificate.MixedSemantics.raw142step1 line 306
90. def OAI.MUB6.Certificate.MixedSemantics.raw142step1Labels line 307
91. theorem OAI.MUB6.Certificate.MixedSemantics.canonical142 line 309
92. def OAI.MUB6.Certificate.MixedSemantics.raw143 line 324
93. def OAI.MUB6.Certificate.MixedSemantics.raw143Labels line 325
94. def OAI.MUB6.Certificate.MixedSemantics.raw143step0 line 327
95. def OAI.MUB6.Certificate.MixedSemantics.raw143step0Labels line 328
96. theorem OAI.MUB6.Certificate.MixedSemantics.canonical143 line 330
97. def OAI.MUB6.Certificate.MixedSemantics.raw144 line 340
98. def OAI.MUB6.Certificate.MixedSemantics.raw144Labels line 341
99. def OAI.MUB6.Certificate.MixedSemantics.raw144step0 line 343
100. def OAI.MUB6.Certificate.MixedSemantics.raw144step0Labels line 344
101. def OAI.MUB6.Certificate.MixedSemantics.raw144step1 line 346
102. def OAI.MUB6.Certificate.MixedSemantics.raw144step1Labels line 347
103. theorem OAI.MUB6.Certificate.MixedSemantics.canonical144 line 349
104. def OAI.MUB6.Certificate.MixedSemantics.raw145 line 364
105. def OAI.MUB6.Certificate.MixedSemantics.raw145Labels line 365
106. def OAI.MUB6.Certificate.MixedSemantics.raw145step0 line 367
107. def OAI.MUB6.Certificate.MixedSemantics.raw145step0Labels line 368
108. theorem OAI.MUB6.Certificate.MixedSemantics.canonical145 line 370
109. def OAI.MUB6.Certificate.MixedSemantics.raw146 line 380
110. def OAI.MUB6.Certificate.MixedSemantics.raw146Labels line 381
111. def OAI.MUB6.Certificate.MixedSemantics.raw146step0 line 383
112. def OAI.MUB6.Certificate.MixedSemantics.raw146step0Labels line 384
113. def OAI.MUB6.Certificate.MixedSemantics.raw146step1 line 386
114. def OAI.MUB6.Certificate.MixedSemantics.raw146step1Labels line 387
115. theorem OAI.MUB6.Certificate.MixedSemantics.canonical146 line 389
116. def OAI.MUB6.Certificate.MixedSemantics.raw147 line 404
117. def OAI.MUB6.Certificate.MixedSemantics.raw147Labels line 405
118. def OAI.MUB6.Certificate.MixedSemantics.raw147step0 line 407
119. def OAI.MUB6.Certificate.MixedSemantics.raw147step0Labels line 408
120. theorem OAI.MUB6.Certificate.MixedSemantics.canonical147 line 410
121. def OAI.MUB6.Certificate.MixedSemantics.raw148 line 420
122. def OAI.MUB6.Certificate.MixedSemantics.raw148Labels line 421
123. def OAI.MUB6.Certificate.MixedSemantics.raw148step0 line 423
124. def OAI.MUB6.Certificate.MixedSemantics.raw148step0Labels line 424
125. def OAI.MUB6.Certificate.MixedSemantics.raw148step1 line 426
126. def OAI.MUB6.Certificate.MixedSemantics.raw148step1Labels line 427
127. theorem OAI.MUB6.Certificate.MixedSemantics.canonical148 line 429
128. def OAI.MUB6.Certificate.MixedSemantics.raw149 line 444
129. def OAI.MUB6.Certificate.MixedSemantics.raw149Labels line 445
130. def OAI.MUB6.Certificate.MixedSemantics.raw149step0 line 447
131. def OAI.MUB6.Certificate.MixedSemantics.raw149step0Labels line 448
132. theorem OAI.MUB6.Certificate.MixedSemantics.canonical149 line 450
133. def OAI.MUB6.Certificate.MixedSemantics.raw150 line 460
134. def OAI.MUB6.Certificate.MixedSemantics.raw150Labels line 461
135. def OAI.MUB6.Certificate.MixedSemantics.raw150step0 line 463
136. def OAI.MUB6.Certificate.MixedSemantics.raw150step0Labels line 464
137. def OAI.MUB6.Certificate.MixedSemantics.raw150step1 line 466
138. def OAI.MUB6.Certificate.MixedSemantics.raw150step1Labels line 467
139. theorem OAI.MUB6.Certificate.MixedSemantics.canonical150 line 469
140. def OAI.MUB6.Certificate.MixedSemantics.raw151 line 484
141. def OAI.MUB6.Certificate.MixedSemantics.raw151Labels line 485
142. def OAI.MUB6.Certificate.MixedSemantics.raw151step0 line 487
143. def OAI.MUB6.Certificate.MixedSemantics.raw151step0Labels line 488
144. theorem OAI.MUB6.Certificate.MixedSemantics.canonical151 line 490
145. def OAI.MUB6.Certificate.MixedSemantics.raw152 line 500
146. def OAI.MUB6.Certificate.MixedSemantics.raw152Labels line 501
147. def OAI.MUB6.Certificate.MixedSemantics.raw152step0 line 503
148. def OAI.MUB6.Certificate.MixedSemantics.raw152step0Labels line 504
149. def OAI.MUB6.Certificate.MixedSemantics.raw152step1 line 506
150. def OAI.MUB6.Certificate.MixedSemantics.raw152step1Labels line 507
151. theorem OAI.MUB6.Certificate.MixedSemantics.canonical152 line 509
152. def OAI.MUB6.Certificate.MixedSemantics.raw153 line 524
153. def OAI.MUB6.Certificate.MixedSemantics.raw153Labels line 525
154. def OAI.MUB6.Certificate.MixedSemantics.raw153step0 line 527
155. def OAI.MUB6.Certificate.MixedSemantics.raw153step0Labels line 528
156. theorem OAI.MUB6.Certificate.MixedSemantics.canonical153 line 530
157. def OAI.MUB6.Certificate.MixedSemantics.raw154 line 540
158. def OAI.MUB6.Certificate.MixedSemantics.raw154Labels line 541
159. def OAI.MUB6.Certificate.MixedSemantics.raw154step0 line 543
160. def OAI.MUB6.Certificate.MixedSemantics.raw154step0Labels line 544
161. def OAI.MUB6.Certificate.MixedSemantics.raw154step1 line 546
162. def OAI.MUB6.Certificate.MixedSemantics.raw154step1Labels line 547
163. theorem OAI.MUB6.Certificate.MixedSemantics.canonical154 line 549
164. def OAI.MUB6.Certificate.MixedSemantics.raw155 line 564
165. def OAI.MUB6.Certificate.MixedSemantics.raw155Labels line 565
166. def OAI.MUB6.Certificate.MixedSemantics.raw155step0 line 567
167. def OAI.MUB6.Certificate.MixedSemantics.raw155step0Labels line 568
168. theorem OAI.MUB6.Certificate.MixedSemantics.canonical155 line 570
169. def OAI.MUB6.Certificate.MixedSemantics.raw156 line 580
170. def OAI.MUB6.Certificate.MixedSemantics.raw156Labels line 581
171. def OAI.MUB6.Certificate.MixedSemantics.raw156step0 line 583
172. def OAI.MUB6.Certificate.MixedSemantics.raw156step0Labels line 584
173. def OAI.MUB6.Certificate.MixedSemantics.raw156step1 line 586
174. def OAI.MUB6.Certificate.MixedSemantics.raw156step1Labels line 587
175. theorem OAI.MUB6.Certificate.MixedSemantics.canonical156 line 589
176. def OAI.MUB6.Certificate.MixedSemantics.raw157 line 604
177. def OAI.MUB6.Certificate.MixedSemantics.raw157Labels line 605
178. def OAI.MUB6.Certificate.MixedSemantics.raw157step0 line 607
179. def OAI.MUB6.Certificate.MixedSemantics.raw157step0Labels line 608
180. theorem OAI.MUB6.Certificate.MixedSemantics.canonical157 line 610
181. def OAI.MUB6.Certificate.MixedSemantics.raw158 line 620
182. def OAI.MUB6.Certificate.MixedSemantics.raw158Labels line 621
183. def OAI.MUB6.Certificate.MixedSemantics.raw158step0 line 623
184. def OAI.MUB6.Certificate.MixedSemantics.raw158step0Labels line 624
185. def OAI.MUB6.Certificate.MixedSemantics.raw158step1 line 626
186. def OAI.MUB6.Certificate.MixedSemantics.raw158step1Labels line 627
187. theorem OAI.MUB6.Certificate.MixedSemantics.canonical158 line 629
188. def OAI.MUB6.Certificate.MixedSemantics.raw159 line 644
189. def OAI.MUB6.Certificate.MixedSemantics.raw159Labels line 645
190. def OAI.MUB6.Certificate.MixedSemantics.raw159step0 line 647
191. def OAI.MUB6.Certificate.MixedSemantics.raw159step0Labels line 648
192. theorem OAI.MUB6.Certificate.MixedSemantics.canonical159 line 650
193. def OAI.MUB6.Certificate.MixedSemantics.raw160 line 660
194. def OAI.MUB6.Certificate.MixedSemantics.raw160Labels line 661
195. def OAI.MUB6.Certificate.MixedSemantics.raw160step0 line 663
196. def OAI.MUB6.Certificate.MixedSemantics.raw160step0Labels line 664
197. def OAI.MUB6.Certificate.MixedSemantics.raw160step1 line 666
198. def OAI.MUB6.Certificate.MixedSemantics.raw160step1Labels line 667
199. theorem OAI.MUB6.Certificate.MixedSemantics.canonical160 line 669
200. def OAI.MUB6.Certificate.MixedSemantics.raw161 line 684
201. def OAI.MUB6.Certificate.MixedSemantics.raw161Labels line 685
202. def OAI.MUB6.Certificate.MixedSemantics.raw161step0 line 687
203. def OAI.MUB6.Certificate.MixedSemantics.raw161step0Labels line 688
204. theorem OAI.MUB6.Certificate.MixedSemantics.canonical161 line 690
205. def OAI.MUB6.Certificate.MixedSemantics.raw162 line 700
206. def OAI.MUB6.Certificate.MixedSemantics.raw162Labels line 701
207. def OAI.MUB6.Certificate.MixedSemantics.raw162step0 line 703
208. def OAI.MUB6.Certificate.MixedSemantics.raw162step0Labels line 704
209. def OAI.MUB6.Certificate.MixedSemantics.raw162step1 line 706
210. def OAI.MUB6.Certificate.MixedSemantics.raw162step1Labels line 707
211. theorem OAI.MUB6.Certificate.MixedSemantics.canonical162 line 709
212. def OAI.MUB6.Certificate.MixedSemantics.raw163 line 724
213. def OAI.MUB6.Certificate.MixedSemantics.raw163Labels line 725
214. def OAI.MUB6.Certificate.MixedSemantics.raw163step0 line 727
215. def OAI.MUB6.Certificate.MixedSemantics.raw163step0Labels line 728
216. theorem OAI.MUB6.Certificate.MixedSemantics.canonical163 line 730
217. def OAI.MUB6.Certificate.MixedSemantics.raw164 line 740
218. def OAI.MUB6.Certificate.MixedSemantics.raw164Labels line 741
219. def OAI.MUB6.Certificate.MixedSemantics.raw164step0 line 743
220. def OAI.MUB6.Certificate.MixedSemantics.raw164step0Labels line 744
221. def OAI.MUB6.Certificate.MixedSemantics.raw164step1 line 746
222. def OAI.MUB6.Certificate.MixedSemantics.raw164step1Labels line 747
223. theorem OAI.MUB6.Certificate.MixedSemantics.canonical164 line 749
224. def OAI.MUB6.Certificate.MixedSemantics.raw165 line 764
225. def OAI.MUB6.Certificate.MixedSemantics.raw165Labels line 765
226. def OAI.MUB6.Certificate.MixedSemantics.raw165step0 line 767
227. def OAI.MUB6.Certificate.MixedSemantics.raw165step0Labels line 768
228. theorem OAI.MUB6.Certificate.MixedSemantics.canonical165 line 770
229. def OAI.MUB6.Certificate.MixedSemantics.raw166 line 780
230. def OAI.MUB6.Certificate.MixedSemantics.raw166Labels line 781
231. def OAI.MUB6.Certificate.MixedSemantics.raw166step0 line 783
232. def OAI.MUB6.Certificate.MixedSemantics.raw166step0Labels line 784
233. def OAI.MUB6.Certificate.MixedSemantics.raw166step1 line 786
234. def OAI.MUB6.Certificate.MixedSemantics.raw166step1Labels line 787
235. theorem OAI.MUB6.Certificate.MixedSemantics.canonical166 line 789
236. def OAI.MUB6.Certificate.MixedSemantics.raw167 line 804
237. def OAI.MUB6.Certificate.MixedSemantics.raw167Labels line 805
238. def OAI.MUB6.Certificate.MixedSemantics.raw167step0 line 807
239. def OAI.MUB6.Certificate.MixedSemantics.raw167step0Labels line 808
240. theorem OAI.MUB6.Certificate.MixedSemantics.canonical167 line 810
241. def OAI.MUB6.Certificate.MixedSemantics.raw168 line 820
242. def OAI.MUB6.Certificate.MixedSemantics.raw168Labels line 821
243. def OAI.MUB6.Certificate.MixedSemantics.raw168step0 line 823
244. def OAI.MUB6.Certificate.MixedSemantics.raw168step0Labels line 824
245. def OAI.MUB6.Certificate.MixedSemantics.raw168step1 line 826
246. def OAI.MUB6.Certificate.MixedSemantics.raw168step1Labels line 827
247. theorem OAI.MUB6.Certificate.MixedSemantics.canonical168 line 829
248. def OAI.MUB6.Certificate.MixedSemantics.raw169 line 844
249. def OAI.MUB6.Certificate.MixedSemantics.raw169Labels line 845
250. def OAI.MUB6.Certificate.MixedSemantics.raw169step0 line 847
251. def OAI.MUB6.Certificate.MixedSemantics.raw169step0Labels line 848
252. theorem OAI.MUB6.Certificate.MixedSemantics.canonical169 line 850
253. def OAI.MUB6.Certificate.MixedSemantics.raw170 line 860
254. def OAI.MUB6.Certificate.MixedSemantics.raw170Labels line 861
255. def OAI.MUB6.Certificate.MixedSemantics.raw170step0 line 863
256. def OAI.MUB6.Certificate.MixedSemantics.raw170step0Labels line 864
257. def OAI.MUB6.Certificate.MixedSemantics.raw170step1 line 866
258. def OAI.MUB6.Certificate.MixedSemantics.raw170step1Labels line 867
259. theorem OAI.MUB6.Certificate.MixedSemantics.canonical170 line 869
260. def OAI.MUB6.Certificate.MixedSemantics.raw171 line 884
261. def OAI.MUB6.Certificate.MixedSemantics.raw171Labels line 885
262. def OAI.MUB6.Certificate.MixedSemantics.raw171step0 line 887
263. def OAI.MUB6.Certificate.MixedSemantics.raw171step0Labels line 888
264. def OAI.MUB6.Certificate.MixedSemantics.raw171step1 line 890
265. def OAI.MUB6.Certificate.MixedSemantics.raw171step1Labels line 891
266. theorem OAI.MUB6.Certificate.MixedSemantics.canonical171 line 893
267. def OAI.MUB6.Certificate.MixedSemantics.raw172 line 908
268. def OAI.MUB6.Certificate.MixedSemantics.raw172Labels line 909
269. def OAI.MUB6.Certificate.MixedSemantics.raw172step0 line 911
270. def OAI.MUB6.Certificate.MixedSemantics.raw172step0Labels line 912
271. def OAI.MUB6.Certificate.MixedSemantics.raw172step1 line 914
272. def OAI.MUB6.Certificate.MixedSemantics.raw172step1Labels line 915
273. theorem OAI.MUB6.Certificate.MixedSemantics.canonical172 line 917
274. def OAI.MUB6.Certificate.MixedSemantics.raw173 line 932
275. def OAI.MUB6.Certificate.MixedSemantics.raw173Labels line 933
276. def OAI.MUB6.Certificate.MixedSemantics.raw173step0 line 935
277. def OAI.MUB6.Certificate.MixedSemantics.raw173step0Labels line 936
278. theorem OAI.MUB6.Certificate.MixedSemantics.canonical173 line 938
279. def OAI.MUB6.Certificate.MixedSemantics.raw174 line 948
280. def OAI.MUB6.Certificate.MixedSemantics.raw174Labels line 949
281. def OAI.MUB6.Certificate.MixedSemantics.raw174step0 line 951
282. def OAI.MUB6.Certificate.MixedSemantics.raw174step0Labels line 952
283. def OAI.MUB6.Certificate.MixedSemantics.raw174step1 line 954
284. def OAI.MUB6.Certificate.MixedSemantics.raw174step1Labels line 955
285. theorem OAI.MUB6.Certificate.MixedSemantics.canonical174 line 957
286. def OAI.MUB6.Certificate.MixedSemantics.raw175 line 972
287. def OAI.MUB6.Certificate.MixedSemantics.raw175Labels line 973
288. def OAI.MUB6.Certificate.MixedSemantics.raw175step0 line 975
289. def OAI.MUB6.Certificate.MixedSemantics.raw175step0Labels line 976
290. def OAI.MUB6.Certificate.MixedSemantics.raw175step1 line 978
291. def OAI.MUB6.Certificate.MixedSemantics.raw175step1Labels line 979
292. theorem OAI.MUB6.Certificate.MixedSemantics.canonical175 line 981
293. def OAI.MUB6.Certificate.MixedSemantics.raw176 line 996
294. def OAI.MUB6.Certificate.MixedSemantics.raw176Labels line 997
295. def OAI.MUB6.Certificate.MixedSemantics.raw176step0 line 999
296. def OAI.MUB6.Certificate.MixedSemantics.raw176step0Labels line 1000
297. def OAI.MUB6.Certificate.MixedSemantics.raw176step1 line 1002
298. def OAI.MUB6.Certificate.MixedSemantics.raw176step1Labels line 1003
299. theorem OAI.MUB6.Certificate.MixedSemantics.canonical176 line 1005
300. def OAI.MUB6.Certificate.MixedSemantics.raw177 line 1020
301. def OAI.MUB6.Certificate.MixedSemantics.raw177Labels line 1021
302. def OAI.MUB6.Certificate.MixedSemantics.raw177step0 line 1023
303. def OAI.MUB6.Certificate.MixedSemantics.raw177step0Labels line 1024
304. def OAI.MUB6.Certificate.MixedSemantics.raw177step1 line 1026
305. def OAI.MUB6.Certificate.MixedSemantics.raw177step1Labels line 1027
306. theorem OAI.MUB6.Certificate.MixedSemantics.canonical177 line 1029
307. def OAI.MUB6.Certificate.MixedSemantics.raw178 line 1044
308. def OAI.MUB6.Certificate.MixedSemantics.raw178Labels line 1045
309. def OAI.MUB6.Certificate.MixedSemantics.raw178step0 line 1047
310. def OAI.MUB6.Certificate.MixedSemantics.raw178step0Labels line 1048
311. def OAI.MUB6.Certificate.MixedSemantics.raw178step1 line 1050
312. def OAI.MUB6.Certificate.MixedSemantics.raw178step1Labels line 1051
313. theorem OAI.MUB6.Certificate.MixedSemantics.canonical178 line 1053
314. def OAI.MUB6.Certificate.MixedSemantics.raw179 line 1068
315. def OAI.MUB6.Certificate.MixedSemantics.raw179Labels line 1069
316. def OAI.MUB6.Certificate.MixedSemantics.raw179step0 line 1071
317. def OAI.MUB6.Certificate.MixedSemantics.raw179step0Labels line 1072
318. theorem OAI.MUB6.Certificate.MixedSemantics.canonical179 line 1074
319. def OAI.MUB6.Certificate.MixedSemantics.raw180 line 1084
320. def OAI.MUB6.Certificate.MixedSemantics.raw180Labels line 1085
321. def OAI.MUB6.Certificate.MixedSemantics.raw180step0 line 1087
322. def OAI.MUB6.Certificate.MixedSemantics.raw180step0Labels line 1088
323. def OAI.MUB6.Certificate.MixedSemantics.raw180step1 line 1090
324. def OAI.MUB6.Certificate.MixedSemantics.raw180step1Labels line 1091
325. theorem OAI.MUB6.Certificate.MixedSemantics.canonical180 line 1093
326. def OAI.MUB6.Certificate.MixedSemantics.raw181 line 1108
327. def OAI.MUB6.Certificate.MixedSemantics.raw181Labels line 1109
328. def OAI.MUB6.Certificate.MixedSemantics.raw181step0 line 1111
329. def OAI.MUB6.Certificate.MixedSemantics.raw181step0Labels line 1112
330. theorem OAI.MUB6.Certificate.MixedSemantics.canonical181 line 1114
331. def OAI.MUB6.Certificate.MixedSemantics.raw182 line 1124
332. def OAI.MUB6.Certificate.MixedSemantics.raw182Labels line 1125
333. def OAI.MUB6.Certificate.MixedSemantics.raw182step0 line 1127
334. def OAI.MUB6.Certificate.MixedSemantics.raw182step0Labels line 1128
335. def OAI.MUB6.Certificate.MixedSemantics.raw182step1 line 1130
336. def OAI.MUB6.Certificate.MixedSemantics.raw182step1Labels line 1131
337. theorem OAI.MUB6.Certificate.MixedSemantics.canonical182 line 1133
338. def OAI.MUB6.Certificate.MixedSemantics.raw183 line 1148
339. def OAI.MUB6.Certificate.MixedSemantics.raw183Labels line 1149
340. def OAI.MUB6.Certificate.MixedSemantics.raw183step0 line 1151
341. def OAI.MUB6.Certificate.MixedSemantics.raw183step0Labels line 1152
342. theorem OAI.MUB6.Certificate.MixedSemantics.canonical183 line 1154
343. def OAI.MUB6.Certificate.MixedSemantics.raw184 line 1164
344. def OAI.MUB6.Certificate.MixedSemantics.raw184Labels line 1165
345. def OAI.MUB6.Certificate.MixedSemantics.raw184step0 line 1167
346. def OAI.MUB6.Certificate.MixedSemantics.raw184step0Labels line 1168
347. def OAI.MUB6.Certificate.MixedSemantics.raw184step1 line 1170
348. def OAI.MUB6.Certificate.MixedSemantics.raw184step1Labels line 1171
349. theorem OAI.MUB6.Certificate.MixedSemantics.canonical184 line 1173
350. def OAI.MUB6.Certificate.MixedSemantics.raw185 line 1188
351. def OAI.MUB6.Certificate.MixedSemantics.raw185Labels line 1189
352. def OAI.MUB6.Certificate.MixedSemantics.raw185step0 line 1191
353. def OAI.MUB6.Certificate.MixedSemantics.raw185step0Labels line 1192
354. theorem OAI.MUB6.Certificate.MixedSemantics.canonical185 line 1194
355. def OAI.MUB6.Certificate.MixedSemantics.raw186 line 1204
356. def OAI.MUB6.Certificate.MixedSemantics.raw186Labels line 1205
357. def OAI.MUB6.Certificate.MixedSemantics.raw186step0 line 1207
358. def OAI.MUB6.Certificate.MixedSemantics.raw186step0Labels line 1208
359. def OAI.MUB6.Certificate.MixedSemantics.raw186step1 line 1210
360. def OAI.MUB6.Certificate.MixedSemantics.raw186step1Labels line 1211
361. theorem OAI.MUB6.Certificate.MixedSemantics.canonical186 line 1213
362. def OAI.MUB6.Certificate.MixedSemantics.raw187 line 1228
363. def OAI.MUB6.Certificate.MixedSemantics.raw187Labels line 1229
364. def OAI.MUB6.Certificate.MixedSemantics.raw187step0 line 1231
365. def OAI.MUB6.Certificate.MixedSemantics.raw187step0Labels line 1232
366. theorem OAI.MUB6.Certificate.MixedSemantics.canonical187 line 1234
367. def OAI.MUB6.Certificate.MixedSemantics.raw188 line 1244
368. def OAI.MUB6.Certificate.MixedSemantics.raw188Labels line 1245
369. def OAI.MUB6.Certificate.MixedSemantics.raw188step0 line 1247
370. def OAI.MUB6.Certificate.MixedSemantics.raw188step0Labels line 1248
371. def OAI.MUB6.Certificate.MixedSemantics.raw188step1 line 1250
372. def OAI.MUB6.Certificate.MixedSemantics.raw188step1Labels line 1251
373. theorem OAI.MUB6.Certificate.MixedSemantics.canonical188 line 1253
374. def OAI.MUB6.Certificate.MixedSemantics.raw189 line 1268
375. def OAI.MUB6.Certificate.MixedSemantics.raw189Labels line 1269
376. def OAI.MUB6.Certificate.MixedSemantics.raw189step0 line 1271
377. def OAI.MUB6.Certificate.MixedSemantics.raw189step0Labels line 1272
378. theorem OAI.MUB6.Certificate.MixedSemantics.canonical189 line 1274
379. def OAI.MUB6.Certificate.MixedSemantics.raw190 line 1284
380. def OAI.MUB6.Certificate.MixedSemantics.raw190Labels line 1285
381. def OAI.MUB6.Certificate.MixedSemantics.raw190step0 line 1287
382. def OAI.MUB6.Certificate.MixedSemantics.raw190step0Labels line 1288
383. def OAI.MUB6.Certificate.MixedSemantics.raw190step1 line 1290
384. def OAI.MUB6.Certificate.MixedSemantics.raw190step1Labels line 1291
385. theorem OAI.MUB6.Certificate.MixedSemantics.canonical190 line 1293
386. def OAI.MUB6.Certificate.MixedSemantics.raw191 line 1308
387. def OAI.MUB6.Certificate.MixedSemantics.raw191Labels line 1309
388. def OAI.MUB6.Certificate.MixedSemantics.raw191step0 line 1311
389. def OAI.MUB6.Certificate.MixedSemantics.raw191step0Labels line 1312
390. theorem OAI.MUB6.Certificate.MixedSemantics.canonical191 line 1314
391. def OAI.MUB6.Certificate.MixedSemantics.raw192 line 1324
392. def OAI.MUB6.Certificate.MixedSemantics.raw192Labels line 1325
393. def OAI.MUB6.Certificate.MixedSemantics.raw192step0 line 1327
394. def OAI.MUB6.Certificate.MixedSemantics.raw192step0Labels line 1328
395. def OAI.MUB6.Certificate.MixedSemantics.raw192step1 line 1330
396. def OAI.MUB6.Certificate.MixedSemantics.raw192step1Labels line 1331
397. theorem OAI.MUB6.Certificate.MixedSemantics.canonical192 line 1333
398. def OAI.MUB6.Certificate.MixedSemantics.raw193 line 1348
399. def OAI.MUB6.Certificate.MixedSemantics.raw193Labels line 1349
400. def OAI.MUB6.Certificate.MixedSemantics.raw193step0 line 1351
401. def OAI.MUB6.Certificate.MixedSemantics.raw193step0Labels line 1352
402. theorem OAI.MUB6.Certificate.MixedSemantics.canonical193 line 1354
403. def OAI.MUB6.Certificate.MixedSemantics.raw194 line 1364
404. def OAI.MUB6.Certificate.MixedSemantics.raw194Labels line 1365
405. def OAI.MUB6.Certificate.MixedSemantics.raw194step0 line 1367
406. def OAI.MUB6.Certificate.MixedSemantics.raw194step0Labels line 1368
407. def OAI.MUB6.Certificate.MixedSemantics.raw194step1 line 1370
408. def OAI.MUB6.Certificate.MixedSemantics.raw194step1Labels line 1371
409. theorem OAI.MUB6.Certificate.MixedSemantics.canonical194 line 1373
410. def OAI.MUB6.Certificate.MixedSemantics.raw195 line 1388
411. def OAI.MUB6.Certificate.MixedSemantics.raw195Labels line 1389
412. def OAI.MUB6.Certificate.MixedSemantics.raw195step0 line 1391
413. def OAI.MUB6.Certificate.MixedSemantics.raw195step0Labels line 1392
414. theorem OAI.MUB6.Certificate.MixedSemantics.canonical195 line 1394
415. def OAI.MUB6.Certificate.MixedSemantics.raw196 line 1404
416. def OAI.MUB6.Certificate.MixedSemantics.raw196Labels line 1405
417. def OAI.MUB6.Certificate.MixedSemantics.raw196step0 line 1407
418. def OAI.MUB6.Certificate.MixedSemantics.raw196step0Labels line 1408
419. def OAI.MUB6.Certificate.MixedSemantics.raw196step1 line 1410
420. def OAI.MUB6.Certificate.MixedSemantics.raw196step1Labels line 1411
421. theorem OAI.MUB6.Certificate.MixedSemantics.canonical196 line 1413
422. def OAI.MUB6.Certificate.MixedSemantics.raw197 line 1428
423. def OAI.MUB6.Certificate.MixedSemantics.raw197Labels line 1429
424. def OAI.MUB6.Certificate.MixedSemantics.raw197step0 line 1431
425. def OAI.MUB6.Certificate.MixedSemantics.raw197step0Labels line 1432
426. theorem OAI.MUB6.Certificate.MixedSemantics.canonical197 line 1434
427. def OAI.MUB6.Certificate.MixedSemantics.raw198 line 1444
428. def OAI.MUB6.Certificate.MixedSemantics.raw198Labels line 1445
429. def OAI.MUB6.Certificate.MixedSemantics.raw198step0 line 1447
430. def OAI.MUB6.Certificate.MixedSemantics.raw198step0Labels line 1448
431. def OAI.MUB6.Certificate.MixedSemantics.raw198step1 line 1450
432. def OAI.MUB6.Certificate.MixedSemantics.raw198step1Labels line 1451
433. theorem OAI.MUB6.Certificate.MixedSemantics.canonical198 line 1453
434. def OAI.MUB6.Certificate.MixedSemantics.raw199 line 1468
435. def OAI.MUB6.Certificate.MixedSemantics.raw199Labels line 1469
436. def OAI.MUB6.Certificate.MixedSemantics.raw199step0 line 1471
437. def OAI.MUB6.Certificate.MixedSemantics.raw199step0Labels line 1472
438. theorem OAI.MUB6.Certificate.MixedSemantics.canonical199 line 1474
439. def OAI.MUB6.Certificate.MixedSemantics.raw200 line 1484
440. def OAI.MUB6.Certificate.MixedSemantics.raw200Labels line 1485
441. def OAI.MUB6.Certificate.MixedSemantics.raw200step0 line 1487
442. def OAI.MUB6.Certificate.MixedSemantics.raw200step0Labels line 1488
443. def OAI.MUB6.Certificate.MixedSemantics.raw200step1 line 1490
444. def OAI.MUB6.Certificate.MixedSemantics.raw200step1Labels line 1491
445. theorem OAI.MUB6.Certificate.MixedSemantics.canonical200 line 1493
446. def OAI.MUB6.Certificate.MixedSemantics.raw201 line 1508
447. def OAI.MUB6.Certificate.MixedSemantics.raw201Labels line 1509
448. def OAI.MUB6.Certificate.MixedSemantics.raw201step0 line 1511
449. def OAI.MUB6.Certificate.MixedSemantics.raw201step0Labels line 1512
450. theorem OAI.MUB6.Certificate.MixedSemantics.canonical201 line 1514
451. def OAI.MUB6.Certificate.MixedSemantics.raw202 line 1524
452. def OAI.MUB6.Certificate.MixedSemantics.raw202Labels line 1525
453. def OAI.MUB6.Certificate.MixedSemantics.raw202step0 line 1527
454. def OAI.MUB6.Certificate.MixedSemantics.raw202step0Labels line 1528
455. def OAI.MUB6.Certificate.MixedSemantics.raw202step1 line 1530
456. def OAI.MUB6.Certificate.MixedSemantics.raw202step1Labels line 1531
457. theorem OAI.MUB6.Certificate.MixedSemantics.canonical202 line 1533
458. def OAI.MUB6.Certificate.MixedSemantics.raw203 line 1548
459. def OAI.MUB6.Certificate.MixedSemantics.raw203Labels line 1549
460. def OAI.MUB6.Certificate.MixedSemantics.raw203step0 line 1551
461. def OAI.MUB6.Certificate.MixedSemantics.raw203step0Labels line 1552
462. theorem OAI.MUB6.Certificate.MixedSemantics.canonical203 line 1554
463. def OAI.MUB6.Certificate.MixedSemantics.raw204 line 1564
464. def OAI.MUB6.Certificate.MixedSemantics.raw204Labels line 1565
465. def OAI.MUB6.Certificate.MixedSemantics.raw204step0 line 1567
466. def OAI.MUB6.Certificate.MixedSemantics.raw204step0Labels line 1568
467. def OAI.MUB6.Certificate.MixedSemantics.raw204step1 line 1570
468. def OAI.MUB6.Certificate.MixedSemantics.raw204step1Labels line 1571
469. theorem OAI.MUB6.Certificate.MixedSemantics.canonical204 line 1573
470. def OAI.MUB6.Certificate.MixedSemantics.raw205 line 1588
471. def OAI.MUB6.Certificate.MixedSemantics.raw205Labels line 1589
472. def OAI.MUB6.Certificate.MixedSemantics.raw205step0 line 1591
473. def OAI.MUB6.Certificate.MixedSemantics.raw205step0Labels line 1592
474. def OAI.MUB6.Certificate.MixedSemantics.raw205step1 line 1594
475. def OAI.MUB6.Certificate.MixedSemantics.raw205step1Labels line 1595
476. theorem OAI.MUB6.Certificate.MixedSemantics.canonical205 line 1597
477. def OAI.MUB6.Certificate.MixedSemantics.raw206 line 1612
478. def OAI.MUB6.Certificate.MixedSemantics.raw206Labels line 1613
479. def OAI.MUB6.Certificate.MixedSemantics.raw206step0 line 1615
480. def OAI.MUB6.Certificate.MixedSemantics.raw206step0Labels line 1616
481. def OAI.MUB6.Certificate.MixedSemantics.raw206step1 line 1618
482. def OAI.MUB6.Certificate.MixedSemantics.raw206step1Labels line 1619
483. theorem OAI.MUB6.Certificate.MixedSemantics.canonical206 line 1621
484. def OAI.MUB6.Certificate.MixedSemantics.raw207 line 1636
485. def OAI.MUB6.Certificate.MixedSemantics.raw207Labels line 1637
486. def OAI.MUB6.Certificate.MixedSemantics.raw207step0 line 1639
487. def OAI.MUB6.Certificate.MixedSemantics.raw207step0Labels line 1640
488. def OAI.MUB6.Certificate.MixedSemantics.raw207step1 line 1642
489. def OAI.MUB6.Certificate.MixedSemantics.raw207step1Labels line 1643
490. theorem OAI.MUB6.Certificate.MixedSemantics.canonical207 line 1645
491. def OAI.MUB6.Certificate.MixedSemantics.raw208 line 1660
492. def OAI.MUB6.Certificate.MixedSemantics.raw208Labels line 1661
493. def OAI.MUB6.Certificate.MixedSemantics.raw208step0 line 1663
494. def OAI.MUB6.Certificate.MixedSemantics.raw208step0Labels line 1664
495. def OAI.MUB6.Certificate.MixedSemantics.raw208step1 line 1666
496. def OAI.MUB6.Certificate.MixedSemantics.raw208step1Labels line 1667
497. theorem OAI.MUB6.Certificate.MixedSemantics.canonical208 line 1669
498. def OAI.MUB6.Certificate.MixedSemantics.raw209 line 1684
499. def OAI.MUB6.Certificate.MixedSemantics.raw209Labels line 1685
500. def OAI.MUB6.Certificate.MixedSemantics.raw209step0 line 1687
501. def OAI.MUB6.Certificate.MixedSemantics.raw209step0Labels line 1688
502. theorem OAI.MUB6.Certificate.MixedSemantics.canonical209 line 1690
503. def OAI.MUB6.Certificate.MixedSemantics.raw210 line 1700
504. def OAI.MUB6.Certificate.MixedSemantics.raw210Labels line 1701
505. def OAI.MUB6.Certificate.MixedSemantics.raw210step0 line 1703
506. def OAI.MUB6.Certificate.MixedSemantics.raw210step0Labels line 1704
507. def OAI.MUB6.Certificate.MixedSemantics.raw210step1 line 1706
508. def OAI.MUB6.Certificate.MixedSemantics.raw210step1Labels line 1707
509. theorem OAI.MUB6.Certificate.MixedSemantics.canonical210 line 1709
510. def OAI.MUB6.Certificate.MixedSemantics.raw211 line 1724
511. def OAI.MUB6.Certificate.MixedSemantics.raw211Labels line 1725
512. def OAI.MUB6.Certificate.MixedSemantics.raw211step0 line 1727
513. def OAI.MUB6.Certificate.MixedSemantics.raw211step0Labels line 1728
514. def OAI.MUB6.Certificate.MixedSemantics.raw211step1 line 1730
515. def OAI.MUB6.Certificate.MixedSemantics.raw211step1Labels line 1731
516. theorem OAI.MUB6.Certificate.MixedSemantics.canonical211 line 1733
517. def OAI.MUB6.Certificate.MixedSemantics.raw212 line 1748
518. def OAI.MUB6.Certificate.MixedSemantics.raw212Labels line 1749
519. def OAI.MUB6.Certificate.MixedSemantics.raw212step0 line 1751
520. def OAI.MUB6.Certificate.MixedSemantics.raw212step0Labels line 1752
521. def OAI.MUB6.Certificate.MixedSemantics.raw212step1 line 1754
522. def OAI.MUB6.Certificate.MixedSemantics.raw212step1Labels line 1755
523. theorem OAI.MUB6.Certificate.MixedSemantics.canonical212 line 1757
524. def OAI.MUB6.Certificate.MixedSemantics.raw213 line 1772
525. def OAI.MUB6.Certificate.MixedSemantics.raw213Labels line 1773
526. def OAI.MUB6.Certificate.MixedSemantics.raw213step0 line 1775
527. def OAI.MUB6.Certificate.MixedSemantics.raw213step0Labels line 1776
528. theorem OAI.MUB6.Certificate.MixedSemantics.canonical213 line 1778
529. def OAI.MUB6.Certificate.MixedSemantics.raw214 line 1788
530. def OAI.MUB6.Certificate.MixedSemantics.raw214Labels line 1789
531. def OAI.MUB6.Certificate.MixedSemantics.raw214step0 line 1791
532. def OAI.MUB6.Certificate.MixedSemantics.raw214step0Labels line 1792
533. def OAI.MUB6.Certificate.MixedSemantics.raw214step1 line 1794
534. def OAI.MUB6.Certificate.MixedSemantics.raw214step1Labels line 1795
535. theorem OAI.MUB6.Certificate.MixedSemantics.canonical214 line 1797
536. def OAI.MUB6.Certificate.MixedSemantics.raw215 line 1812
537. def OAI.MUB6.Certificate.MixedSemantics.raw215Labels line 1813
538. def OAI.MUB6.Certificate.MixedSemantics.raw215step0 line 1815
539. def OAI.MUB6.Certificate.MixedSemantics.raw215step0Labels line 1816
540. def OAI.MUB6.Certificate.MixedSemantics.raw215step1 line 1818
541. def OAI.MUB6.Certificate.MixedSemantics.raw215step1Labels line 1819
542. theorem OAI.MUB6.Certificate.MixedSemantics.canonical215 line 1821
543. def OAI.MUB6.Certificate.MixedSemantics.raw216 line 1836
544. def OAI.MUB6.Certificate.MixedSemantics.raw216Labels line 1837
545. def OAI.MUB6.Certificate.MixedSemantics.raw216step0 line 1839
546. def OAI.MUB6.Certificate.MixedSemantics.raw216step0Labels line 1840
547. def OAI.MUB6.Certificate.MixedSemantics.raw216step1 line 1842
548. def OAI.MUB6.Certificate.MixedSemantics.raw216step1Labels line 1843
549. theorem OAI.MUB6.Certificate.MixedSemantics.canonical216 line 1845
550. def OAI.MUB6.Certificate.MixedSemantics.raw217 line 1860
551. def OAI.MUB6.Certificate.MixedSemantics.raw217Labels line 1861
552. def OAI.MUB6.Certificate.MixedSemantics.raw217step0 line 1863
553. def OAI.MUB6.Certificate.MixedSemantics.raw217step0Labels line 1864
554. def OAI.MUB6.Certificate.MixedSemantics.raw217step1 line 1866
555. def OAI.MUB6.Certificate.MixedSemantics.raw217step1Labels line 1867
556. theorem OAI.MUB6.Certificate.MixedSemantics.canonical217 line 1869
557. def OAI.MUB6.Certificate.MixedSemantics.raw218 line 1884
558. def OAI.MUB6.Certificate.MixedSemantics.raw218Labels line 1885
559. def OAI.MUB6.Certificate.MixedSemantics.raw218step0 line 1887
560. def OAI.MUB6.Certificate.MixedSemantics.raw218step0Labels line 1888
561. def OAI.MUB6.Certificate.MixedSemantics.raw218step1 line 1890
562. def OAI.MUB6.Certificate.MixedSemantics.raw218step1Labels line 1891
563. theorem OAI.MUB6.Certificate.MixedSemantics.canonical218 line 1893
564. def OAI.MUB6.Certificate.MixedSemantics.raw219 line 1908
565. def OAI.MUB6.Certificate.MixedSemantics.raw219Labels line 1909
566. def OAI.MUB6.Certificate.MixedSemantics.raw219step0 line 1911
567. def OAI.MUB6.Certificate.MixedSemantics.raw219step0Labels line 1912
568. def OAI.MUB6.Certificate.MixedSemantics.raw219step1 line 1914
569. def OAI.MUB6.Certificate.MixedSemantics.raw219step1Labels line 1915
570. theorem OAI.MUB6.Certificate.MixedSemantics.canonical219 line 1917
571. def OAI.MUB6.Certificate.MixedSemantics.raw220 line 1932
572. def OAI.MUB6.Certificate.MixedSemantics.raw220Labels line 1933
573. def OAI.MUB6.Certificate.MixedSemantics.raw220step0 line 1935
574. def OAI.MUB6.Certificate.MixedSemantics.raw220step0Labels line 1936
575. def OAI.MUB6.Certificate.MixedSemantics.raw220step1 line 1938
576. def OAI.MUB6.Certificate.MixedSemantics.raw220step1Labels line 1939
577. theorem OAI.MUB6.Certificate.MixedSemantics.canonical220 line 1941
578. def OAI.MUB6.Certificate.MixedSemantics.raw221 line 1956
579. def OAI.MUB6.Certificate.MixedSemantics.raw221Labels line 1957
580. def OAI.MUB6.Certificate.MixedSemantics.raw221step0 line 1959
581. def OAI.MUB6.Certificate.MixedSemantics.raw221step0Labels line 1960
582. theorem OAI.MUB6.Certificate.MixedSemantics.canonical221 line 1962
583. def OAI.MUB6.Certificate.MixedSemantics.raw222 line 1972
584. def OAI.MUB6.Certificate.MixedSemantics.raw222Labels line 1973
585. def OAI.MUB6.Certificate.MixedSemantics.raw222step0 line 1975
586. def OAI.MUB6.Certificate.MixedSemantics.raw222step0Labels line 1976
587. def OAI.MUB6.Certificate.MixedSemantics.raw222step1 line 1978
588. def OAI.MUB6.Certificate.MixedSemantics.raw222step1Labels line 1979
589. theorem OAI.MUB6.Certificate.MixedSemantics.canonical222 line 1981
590. def OAI.MUB6.Certificate.MixedSemantics.raw223 line 1996
591. def OAI.MUB6.Certificate.MixedSemantics.raw223Labels line 1997
592. def OAI.MUB6.Certificate.MixedSemantics.raw223step0 line 1999
593. def OAI.MUB6.Certificate.MixedSemantics.raw223step0Labels line 2000
594. def OAI.MUB6.Certificate.MixedSemantics.raw223step1 line 2002
595. def OAI.MUB6.Certificate.MixedSemantics.raw223step1Labels line 2003
596. theorem OAI.MUB6.Certificate.MixedSemantics.canonical223 line 2005
597. def OAI.MUB6.Certificate.MixedSemantics.raw224 line 2020
598. def OAI.MUB6.Certificate.MixedSemantics.raw224Labels line 2021
599. def OAI.MUB6.Certificate.MixedSemantics.raw224step0 line 2023
600. def OAI.MUB6.Certificate.MixedSemantics.raw224step0Labels line 2024
601. def OAI.MUB6.Certificate.MixedSemantics.raw224step1 line 2026
602. def OAI.MUB6.Certificate.MixedSemantics.raw224step1Labels line 2027
603. theorem OAI.MUB6.Certificate.MixedSemantics.canonical224 line 2029
604. def OAI.MUB6.Certificate.MixedSemantics.raw225 line 2044
605. def OAI.MUB6.Certificate.MixedSemantics.raw225Labels line 2045
606. def OAI.MUB6.Certificate.MixedSemantics.raw225step0 line 2047
607. def OAI.MUB6.Certificate.MixedSemantics.raw225step0Labels line 2048
608. def OAI.MUB6.Certificate.MixedSemantics.raw225step1 line 2050
609. def OAI.MUB6.Certificate.MixedSemantics.raw225step1Labels line 2051
610. theorem OAI.MUB6.Certificate.MixedSemantics.canonical225 line 2053
611. def OAI.MUB6.Certificate.MixedSemantics.raw226 line 2068
612. def OAI.MUB6.Certificate.MixedSemantics.raw226Labels line 2069
613. def OAI.MUB6.Certificate.MixedSemantics.raw226step0 line 2071
614. def OAI.MUB6.Certificate.MixedSemantics.raw226step0Labels line 2072
615. def OAI.MUB6.Certificate.MixedSemantics.raw226step1 line 2074
616. def OAI.MUB6.Certificate.MixedSemantics.raw226step1Labels line 2075
617. theorem OAI.MUB6.Certificate.MixedSemantics.canonical226 line 2077
618. def OAI.MUB6.Certificate.MixedSemantics.raw227 line 2092
619. def OAI.MUB6.Certificate.MixedSemantics.raw227Labels line 2093
620. def OAI.MUB6.Certificate.MixedSemantics.raw227step0 line 2095
621. def OAI.MUB6.Certificate.MixedSemantics.raw227step0Labels line 2096
622. theorem OAI.MUB6.Certificate.MixedSemantics.canonical227 line 2098
623. def OAI.MUB6.Certificate.MixedSemantics.raw228 line 2108
624. def OAI.MUB6.Certificate.MixedSemantics.raw228Labels line 2109
625. def OAI.MUB6.Certificate.MixedSemantics.raw228step0 line 2111
626. def OAI.MUB6.Certificate.MixedSemantics.raw228step0Labels line 2112
627. def OAI.MUB6.Certificate.MixedSemantics.raw228step1 line 2114
628. def OAI.MUB6.Certificate.MixedSemantics.raw228step1Labels line 2115
629. theorem OAI.MUB6.Certificate.MixedSemantics.canonical228 line 2117
630. def OAI.MUB6.Certificate.MixedSemantics.raw229 line 2132
631. def OAI.MUB6.Certificate.MixedSemantics.raw229Labels line 2133
632. def OAI.MUB6.Certificate.MixedSemantics.raw229step0 line 2135
633. def OAI.MUB6.Certificate.MixedSemantics.raw229step0Labels line 2136
634. def OAI.MUB6.Certificate.MixedSemantics.raw229step1 line 2138
635. def OAI.MUB6.Certificate.MixedSemantics.raw229step1Labels line 2139
636. theorem OAI.MUB6.Certificate.MixedSemantics.canonical229 line 2141
637. def OAI.MUB6.Certificate.MixedSemantics.raw230 line 2156
638. def OAI.MUB6.Certificate.MixedSemantics.raw230Labels line 2157
639. def OAI.MUB6.Certificate.MixedSemantics.raw230step0 line 2159
640. def OAI.MUB6.Certificate.MixedSemantics.raw230step0Labels line 2160
641. def OAI.MUB6.Certificate.MixedSemantics.raw230step1 line 2162
642. def OAI.MUB6.Certificate.MixedSemantics.raw230step1Labels line 2163
643. theorem OAI.MUB6.Certificate.MixedSemantics.canonical230 line 2165
644. def OAI.MUB6.Certificate.MixedSemantics.raw231 line 2180
645. def OAI.MUB6.Certificate.MixedSemantics.raw231Labels line 2181
646. def OAI.MUB6.Certificate.MixedSemantics.raw231step0 line 2183
647. def OAI.MUB6.Certificate.MixedSemantics.raw231step0Labels line 2184
648. theorem OAI.MUB6.Certificate.MixedSemantics.canonical231 line 2186
649. def OAI.MUB6.Certificate.MixedSemantics.raw232 line 2196
650. def OAI.MUB6.Certificate.MixedSemantics.raw232Labels line 2197
651. def OAI.MUB6.Certificate.MixedSemantics.raw232step0 line 2199
652. def OAI.MUB6.Certificate.MixedSemantics.raw232step0Labels line 2200
653. def OAI.MUB6.Certificate.MixedSemantics.raw232step1 line 2202
654. def OAI.MUB6.Certificate.MixedSemantics.raw232step1Labels line 2203
655. theorem OAI.MUB6.Certificate.MixedSemantics.canonical232 line 2205
656. def OAI.MUB6.Certificate.MixedSemantics.raw233 line 2220
657. def OAI.MUB6.Certificate.MixedSemantics.raw233Labels line 2221
658. def OAI.MUB6.Certificate.MixedSemantics.raw233step0 line 2223
659. def OAI.MUB6.Certificate.MixedSemantics.raw233step0Labels line 2224
660. theorem OAI.MUB6.Certificate.MixedSemantics.canonical233 line 2226
661. def OAI.MUB6.Certificate.MixedSemantics.raw234 line 2236
662. def OAI.MUB6.Certificate.MixedSemantics.raw234Labels line 2237
663. def OAI.MUB6.Certificate.MixedSemantics.raw234step0 line 2239
664. def OAI.MUB6.Certificate.MixedSemantics.raw234step0Labels line 2240
665. def OAI.MUB6.Certificate.MixedSemantics.raw234step1 line 2242
666. def OAI.MUB6.Certificate.MixedSemantics.raw234step1Labels line 2243
667. theorem OAI.MUB6.Certificate.MixedSemantics.canonical234 line 2245
668. def OAI.MUB6.Certificate.MixedSemantics.raw235 line 2260
669. def OAI.MUB6.Certificate.MixedSemantics.raw235Labels line 2261
670. def OAI.MUB6.Certificate.MixedSemantics.raw235step0 line 2263
671. def OAI.MUB6.Certificate.MixedSemantics.raw235step0Labels line 2264
672. theorem OAI.MUB6.Certificate.MixedSemantics.canonical235 line 2266
673. def OAI.MUB6.Certificate.MixedSemantics.raw236 line 2276
674. def OAI.MUB6.Certificate.MixedSemantics.raw236Labels line 2277
675. def OAI.MUB6.Certificate.MixedSemantics.raw236step0 line 2279
676. def OAI.MUB6.Certificate.MixedSemantics.raw236step0Labels line 2280
677. def OAI.MUB6.Certificate.MixedSemantics.raw236step1 line 2282
678. def OAI.MUB6.Certificate.MixedSemantics.raw236step1Labels line 2283
679. theorem OAI.MUB6.Certificate.MixedSemantics.canonical236 line 2285
680. def OAI.MUB6.Certificate.MixedSemantics.raw237 line 2300
681. def OAI.MUB6.Certificate.MixedSemantics.raw237Labels line 2301
682. def OAI.MUB6.Certificate.MixedSemantics.raw237step0 line 2303
683. def OAI.MUB6.Certificate.MixedSemantics.raw237step0Labels line 2304
684. theorem OAI.MUB6.Certificate.MixedSemantics.canonical237 line 2306
685. def OAI.MUB6.Certificate.MixedSemantics.raw238 line 2316
686. def OAI.MUB6.Certificate.MixedSemantics.raw238Labels line 2317
687. def OAI.MUB6.Certificate.MixedSemantics.raw238step0 line 2319
688. def OAI.MUB6.Certificate.MixedSemantics.raw238step0Labels line 2320
689. def OAI.MUB6.Certificate.MixedSemantics.raw238step1 line 2322
690. def OAI.MUB6.Certificate.MixedSemantics.raw238step1Labels line 2323
691. theorem OAI.MUB6.Certificate.MixedSemantics.canonical238 line 2325
692. def OAI.MUB6.Certificate.MixedSemantics.raw239 line 2340
693. def OAI.MUB6.Certificate.MixedSemantics.raw239Labels line 2341
694. def OAI.MUB6.Certificate.MixedSemantics.raw239step0 line 2343
695. def OAI.MUB6.Certificate.MixedSemantics.raw239step0Labels line 2344
696. theorem OAI.MUB6.Certificate.MixedSemantics.canonical239 line 2346
697. def OAI.MUB6.Certificate.MixedSemantics.raw240 line 2356
698. def OAI.MUB6.Certificate.MixedSemantics.raw240Labels line 2357
699. def OAI.MUB6.Certificate.MixedSemantics.raw240step0 line 2359
700. def OAI.MUB6.Certificate.MixedSemantics.raw240step0Labels line 2360
701. def OAI.MUB6.Certificate.MixedSemantics.raw240step1 line 2362
702. def OAI.MUB6.Certificate.MixedSemantics.raw240step1Labels line 2363
703. theorem OAI.MUB6.Certificate.MixedSemantics.canonical240 line 2365
704. def OAI.MUB6.Certificate.MixedSemantics.raw241 line 2380
705. def OAI.MUB6.Certificate.MixedSemantics.raw241Labels line 2381
706. def OAI.MUB6.Certificate.MixedSemantics.raw241step0 line 2383
707. def OAI.MUB6.Certificate.MixedSemantics.raw241step0Labels line 2384
708. theorem OAI.MUB6.Certificate.MixedSemantics.canonical241 line 2386
709. def OAI.MUB6.Certificate.MixedSemantics.raw242 line 2396
710. def OAI.MUB6.Certificate.MixedSemantics.raw242Labels line 2397
711. def OAI.MUB6.Certificate.MixedSemantics.raw242step0 line 2399
712. def OAI.MUB6.Certificate.MixedSemantics.raw242step0Labels line 2400
713. def OAI.MUB6.Certificate.MixedSemantics.raw242step1 line 2402
714. def OAI.MUB6.Certificate.MixedSemantics.raw242step1Labels line 2403
715. theorem OAI.MUB6.Certificate.MixedSemantics.canonical242 line 2405
716. def OAI.MUB6.Certificate.MixedSemantics.raw243 line 2420
717. def OAI.MUB6.Certificate.MixedSemantics.raw243Labels line 2421
718. def OAI.MUB6.Certificate.MixedSemantics.raw243step0 line 2423
719. def OAI.MUB6.Certificate.MixedSemantics.raw243step0Labels line 2424
720. def OAI.MUB6.Certificate.MixedSemantics.raw243step1 line 2426
721. def OAI.MUB6.Certificate.MixedSemantics.raw243step1Labels line 2427
722. theorem OAI.MUB6.Certificate.MixedSemantics.canonical243 line 2429
723. def OAI.MUB6.Certificate.MixedSemantics.raw244 line 2444
724. def OAI.MUB6.Certificate.MixedSemantics.raw244Labels line 2445
725. def OAI.MUB6.Certificate.MixedSemantics.raw244step0 line 2447
726. def OAI.MUB6.Certificate.MixedSemantics.raw244step0Labels line 2448
727. def OAI.MUB6.Certificate.MixedSemantics.raw244step1 line 2450
728. def OAI.MUB6.Certificate.MixedSemantics.raw244step1Labels line 2451
729. theorem OAI.MUB6.Certificate.MixedSemantics.canonical244 line 2453
730. def OAI.MUB6.Certificate.MixedSemantics.raw245 line 2468
731. def OAI.MUB6.Certificate.MixedSemantics.raw245Labels line 2469
732. def OAI.MUB6.Certificate.MixedSemantics.raw245step0 line 2471
733. def OAI.MUB6.Certificate.MixedSemantics.raw245step0Labels line 2472
734. def OAI.MUB6.Certificate.MixedSemantics.raw245step1 line 2474
735. def OAI.MUB6.Certificate.MixedSemantics.raw245step1Labels line 2475
736. theorem OAI.MUB6.Certificate.MixedSemantics.canonical245 line 2477
737. def OAI.MUB6.Certificate.MixedSemantics.raw246 line 2492
738. def OAI.MUB6.Certificate.MixedSemantics.raw246Labels line 2493
739. def OAI.MUB6.Certificate.MixedSemantics.raw246step0 line 2495
740. def OAI.MUB6.Certificate.MixedSemantics.raw246step0Labels line 2496
741. def OAI.MUB6.Certificate.MixedSemantics.raw246step1 line 2498
742. def OAI.MUB6.Certificate.MixedSemantics.raw246step1Labels line 2499
743. theorem OAI.MUB6.Certificate.MixedSemantics.canonical246 line 2501
744. def OAI.MUB6.Certificate.MixedSemantics.raw247 line 2516
745. def OAI.MUB6.Certificate.MixedSemantics.raw247Labels line 2517
746. def OAI.MUB6.Certificate.MixedSemantics.raw247step0 line 2519
747. def OAI.MUB6.Certificate.MixedSemantics.raw247step0Labels line 2520
748. theorem OAI.MUB6.Certificate.MixedSemantics.canonical247 line 2522
749. def OAI.MUB6.Certificate.MixedSemantics.raw248 line 2532
750. def OAI.MUB6.Certificate.MixedSemantics.raw248Labels line 2533
751. def OAI.MUB6.Certificate.MixedSemantics.raw248step0 line 2535
752. def OAI.MUB6.Certificate.MixedSemantics.raw248step0Labels line 2536
753. def OAI.MUB6.Certificate.MixedSemantics.raw248step1 line 2538
754. def OAI.MUB6.Certificate.MixedSemantics.raw248step1Labels line 2539
755. theorem OAI.MUB6.Certificate.MixedSemantics.canonical248 line 2541
756. def OAI.MUB6.Certificate.MixedSemantics.raw249 line 2556
757. def OAI.MUB6.Certificate.MixedSemantics.raw249Labels line 2557
758. def OAI.MUB6.Certificate.MixedSemantics.raw249step0 line 2559
759. def OAI.MUB6.Certificate.MixedSemantics.raw249step0Labels line 2560
760. theorem OAI.MUB6.Certificate.MixedSemantics.canonical249 line 2562
761. def OAI.MUB6.Certificate.MixedSemantics.raw250 line 2572
762. def OAI.MUB6.Certificate.MixedSemantics.raw250Labels line 2573
763. def OAI.MUB6.Certificate.MixedSemantics.raw250step0 line 2575
764. def OAI.MUB6.Certificate.MixedSemantics.raw250step0Labels line 2576
765. def OAI.MUB6.Certificate.MixedSemantics.raw250step1 line 2578
766. def OAI.MUB6.Certificate.MixedSemantics.raw250step1Labels line 2579
767. theorem OAI.MUB6.Certificate.MixedSemantics.canonical250 line 2581
768. def OAI.MUB6.Certificate.MixedSemantics.raw251 line 2596
769. def OAI.MUB6.Certificate.MixedSemantics.raw251Labels line 2597
770. def OAI.MUB6.Certificate.MixedSemantics.raw251step0 line 2599
771. def OAI.MUB6.Certificate.MixedSemantics.raw251step0Labels line 2600
772. def OAI.MUB6.Certificate.MixedSemantics.raw251step1 line 2602
773. def OAI.MUB6.Certificate.MixedSemantics.raw251step1Labels line 2603
774. theorem OAI.MUB6.Certificate.MixedSemantics.canonical251 line 2605
775. def OAI.MUB6.Certificate.MixedSemantics.raw252 line 2620
776. def OAI.MUB6.Certificate.MixedSemantics.raw252Labels line 2621
777. def OAI.MUB6.Certificate.MixedSemantics.raw252step0 line 2623
778. def OAI.MUB6.Certificate.MixedSemantics.raw252step0Labels line 2624
779. def OAI.MUB6.Certificate.MixedSemantics.raw252step1 line 2626
780. def OAI.MUB6.Certificate.MixedSemantics.raw252step1Labels line 2627
781. theorem OAI.MUB6.Certificate.MixedSemantics.canonical252 line 2629
782. def OAI.MUB6.Certificate.MixedSemantics.raw253 line 2644
783. def OAI.MUB6.Certificate.MixedSemantics.raw253Labels line 2645
784. def OAI.MUB6.Certificate.MixedSemantics.raw253step0 line 2647
785. def OAI.MUB6.Certificate.MixedSemantics.raw253step0Labels line 2648
786. theorem OAI.MUB6.Certificate.MixedSemantics.canonical253 line 2650
787. def OAI.MUB6.Certificate.MixedSemantics.raw254 line 2660
788. def OAI.MUB6.Certificate.MixedSemantics.raw254Labels line 2661
789. def OAI.MUB6.Certificate.MixedSemantics.raw254step0 line 2663
790. def OAI.MUB6.Certificate.MixedSemantics.raw254step0Labels line 2664
791. def OAI.MUB6.Certificate.MixedSemantics.raw254step1 line 2666
792. def OAI.MUB6.Certificate.MixedSemantics.raw254step1Labels line 2667
793. theorem OAI.MUB6.Certificate.MixedSemantics.canonical254 line 2669
794. def OAI.MUB6.Certificate.MixedSemantics.raw255 line 2684
795. def OAI.MUB6.Certificate.MixedSemantics.raw255Labels line 2685
796. def OAI.MUB6.Certificate.MixedSemantics.raw255step0 line 2687
797. def OAI.MUB6.Certificate.MixedSemantics.raw255step0Labels line 2688
798. theorem OAI.MUB6.Certificate.MixedSemantics.canonical255 line 2690