OAI/Analysis/MutuallyUnbiased/MixedSemantics/Canonical5.lean

GitHub source file

852 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.raw640 line 17
2. def OAI.MUB6.Certificate.MixedSemantics.raw640Labels line 18
3. def OAI.MUB6.Certificate.MixedSemantics.raw640step0 line 20
4. def OAI.MUB6.Certificate.MixedSemantics.raw640step0Labels line 21
5. def OAI.MUB6.Certificate.MixedSemantics.raw640step1 line 23
6. def OAI.MUB6.Certificate.MixedSemantics.raw640step1Labels line 24
7. theorem OAI.MUB6.Certificate.MixedSemantics.canonical640 line 26
8. def OAI.MUB6.Certificate.MixedSemantics.raw641 line 41
9. def OAI.MUB6.Certificate.MixedSemantics.raw641Labels line 42
10. def OAI.MUB6.Certificate.MixedSemantics.raw641step0 line 44
11. def OAI.MUB6.Certificate.MixedSemantics.raw641step0Labels line 45
12. theorem OAI.MUB6.Certificate.MixedSemantics.canonical641 line 47
13. def OAI.MUB6.Certificate.MixedSemantics.raw642 line 57
14. def OAI.MUB6.Certificate.MixedSemantics.raw642Labels line 58
15. def OAI.MUB6.Certificate.MixedSemantics.raw642step0 line 60
16. def OAI.MUB6.Certificate.MixedSemantics.raw642step0Labels line 61
17. def OAI.MUB6.Certificate.MixedSemantics.raw642step1 line 63
18. def OAI.MUB6.Certificate.MixedSemantics.raw642step1Labels line 64
19. theorem OAI.MUB6.Certificate.MixedSemantics.canonical642 line 66
20. def OAI.MUB6.Certificate.MixedSemantics.raw643 line 81
21. def OAI.MUB6.Certificate.MixedSemantics.raw643Labels line 82
22. def OAI.MUB6.Certificate.MixedSemantics.raw643step0 line 84
23. def OAI.MUB6.Certificate.MixedSemantics.raw643step0Labels line 85
24. theorem OAI.MUB6.Certificate.MixedSemantics.canonical643 line 87
25. def OAI.MUB6.Certificate.MixedSemantics.raw644 line 97
26. def OAI.MUB6.Certificate.MixedSemantics.raw644Labels line 98
27. def OAI.MUB6.Certificate.MixedSemantics.raw644step0 line 100
28. def OAI.MUB6.Certificate.MixedSemantics.raw644step0Labels line 101
29. def OAI.MUB6.Certificate.MixedSemantics.raw644step1 line 103
30. def OAI.MUB6.Certificate.MixedSemantics.raw644step1Labels line 104
31. theorem OAI.MUB6.Certificate.MixedSemantics.canonical644 line 106
32. def OAI.MUB6.Certificate.MixedSemantics.raw645 line 121
33. def OAI.MUB6.Certificate.MixedSemantics.raw645Labels line 122
34. def OAI.MUB6.Certificate.MixedSemantics.raw645step0 line 124
35. def OAI.MUB6.Certificate.MixedSemantics.raw645step0Labels line 125
36. theorem OAI.MUB6.Certificate.MixedSemantics.canonical645 line 127
37. def OAI.MUB6.Certificate.MixedSemantics.raw646 line 137
38. def OAI.MUB6.Certificate.MixedSemantics.raw646Labels line 138
39. def OAI.MUB6.Certificate.MixedSemantics.raw646step0 line 140
40. def OAI.MUB6.Certificate.MixedSemantics.raw646step0Labels line 141
41. def OAI.MUB6.Certificate.MixedSemantics.raw646step1 line 143
42. def OAI.MUB6.Certificate.MixedSemantics.raw646step1Labels line 144
43. theorem OAI.MUB6.Certificate.MixedSemantics.canonical646 line 146
44. def OAI.MUB6.Certificate.MixedSemantics.raw647 line 161
45. def OAI.MUB6.Certificate.MixedSemantics.raw647Labels line 162
46. def OAI.MUB6.Certificate.MixedSemantics.raw647step0 line 164
47. def OAI.MUB6.Certificate.MixedSemantics.raw647step0Labels line 165
48. theorem OAI.MUB6.Certificate.MixedSemantics.canonical647 line 167
49. def OAI.MUB6.Certificate.MixedSemantics.raw648 line 177
50. def OAI.MUB6.Certificate.MixedSemantics.raw648Labels line 178
51. def OAI.MUB6.Certificate.MixedSemantics.raw648step0 line 180
52. def OAI.MUB6.Certificate.MixedSemantics.raw648step0Labels line 181
53. def OAI.MUB6.Certificate.MixedSemantics.raw648step1 line 183
54. def OAI.MUB6.Certificate.MixedSemantics.raw648step1Labels line 184
55. theorem OAI.MUB6.Certificate.MixedSemantics.canonical648 line 186
56. def OAI.MUB6.Certificate.MixedSemantics.raw649 line 201
57. def OAI.MUB6.Certificate.MixedSemantics.raw649Labels line 202
58. def OAI.MUB6.Certificate.MixedSemantics.raw649step0 line 204
59. def OAI.MUB6.Certificate.MixedSemantics.raw649step0Labels line 205
60. theorem OAI.MUB6.Certificate.MixedSemantics.canonical649 line 207
61. def OAI.MUB6.Certificate.MixedSemantics.raw650 line 217
62. def OAI.MUB6.Certificate.MixedSemantics.raw650Labels line 218
63. def OAI.MUB6.Certificate.MixedSemantics.raw650step0 line 220
64. def OAI.MUB6.Certificate.MixedSemantics.raw650step0Labels line 221
65. def OAI.MUB6.Certificate.MixedSemantics.raw650step1 line 223
66. def OAI.MUB6.Certificate.MixedSemantics.raw650step1Labels line 224
67. theorem OAI.MUB6.Certificate.MixedSemantics.canonical650 line 226
68. def OAI.MUB6.Certificate.MixedSemantics.raw651 line 241
69. def OAI.MUB6.Certificate.MixedSemantics.raw651Labels line 242
70. def OAI.MUB6.Certificate.MixedSemantics.raw651step0 line 244
71. def OAI.MUB6.Certificate.MixedSemantics.raw651step0Labels line 245
72. theorem OAI.MUB6.Certificate.MixedSemantics.canonical651 line 247
73. def OAI.MUB6.Certificate.MixedSemantics.raw652 line 257
74. def OAI.MUB6.Certificate.MixedSemantics.raw652Labels line 258
75. def OAI.MUB6.Certificate.MixedSemantics.raw652step0 line 260
76. def OAI.MUB6.Certificate.MixedSemantics.raw652step0Labels line 261
77. def OAI.MUB6.Certificate.MixedSemantics.raw652step1 line 263
78. def OAI.MUB6.Certificate.MixedSemantics.raw652step1Labels line 264
79. theorem OAI.MUB6.Certificate.MixedSemantics.canonical652 line 266
80. def OAI.MUB6.Certificate.MixedSemantics.raw653 line 281
81. def OAI.MUB6.Certificate.MixedSemantics.raw653Labels line 282
82. def OAI.MUB6.Certificate.MixedSemantics.raw653step0 line 284
83. def OAI.MUB6.Certificate.MixedSemantics.raw653step0Labels line 285
84. theorem OAI.MUB6.Certificate.MixedSemantics.canonical653 line 287
85. def OAI.MUB6.Certificate.MixedSemantics.raw654 line 297
86. def OAI.MUB6.Certificate.MixedSemantics.raw654Labels line 298
87. def OAI.MUB6.Certificate.MixedSemantics.raw654step0 line 300
88. def OAI.MUB6.Certificate.MixedSemantics.raw654step0Labels line 301
89. def OAI.MUB6.Certificate.MixedSemantics.raw654step1 line 303
90. def OAI.MUB6.Certificate.MixedSemantics.raw654step1Labels line 304
91. theorem OAI.MUB6.Certificate.MixedSemantics.canonical654 line 306
92. def OAI.MUB6.Certificate.MixedSemantics.raw655 line 321
93. def OAI.MUB6.Certificate.MixedSemantics.raw655Labels line 322
94. def OAI.MUB6.Certificate.MixedSemantics.raw655step0 line 324
95. def OAI.MUB6.Certificate.MixedSemantics.raw655step0Labels line 325
96. def OAI.MUB6.Certificate.MixedSemantics.raw655step1 line 327
97. def OAI.MUB6.Certificate.MixedSemantics.raw655step1Labels line 328
98. theorem OAI.MUB6.Certificate.MixedSemantics.canonical655 line 330
99. def OAI.MUB6.Certificate.MixedSemantics.raw656 line 345
100. def OAI.MUB6.Certificate.MixedSemantics.raw656Labels line 346
101. def OAI.MUB6.Certificate.MixedSemantics.raw656step0 line 348
102. def OAI.MUB6.Certificate.MixedSemantics.raw656step0Labels line 349
103. def OAI.MUB6.Certificate.MixedSemantics.raw656step1 line 351
104. def OAI.MUB6.Certificate.MixedSemantics.raw656step1Labels line 352
105. theorem OAI.MUB6.Certificate.MixedSemantics.canonical656 line 354
106. def OAI.MUB6.Certificate.MixedSemantics.raw657 line 369
107. def OAI.MUB6.Certificate.MixedSemantics.raw657Labels line 370
108. def OAI.MUB6.Certificate.MixedSemantics.raw657step0 line 372
109. def OAI.MUB6.Certificate.MixedSemantics.raw657step0Labels line 373
110. theorem OAI.MUB6.Certificate.MixedSemantics.canonical657 line 375
111. def OAI.MUB6.Certificate.MixedSemantics.raw658 line 385
112. def OAI.MUB6.Certificate.MixedSemantics.raw658Labels line 386
113. def OAI.MUB6.Certificate.MixedSemantics.raw658step0 line 388
114. def OAI.MUB6.Certificate.MixedSemantics.raw658step0Labels line 389
115. def OAI.MUB6.Certificate.MixedSemantics.raw658step1 line 391
116. def OAI.MUB6.Certificate.MixedSemantics.raw658step1Labels line 392
117. theorem OAI.MUB6.Certificate.MixedSemantics.canonical658 line 394
118. def OAI.MUB6.Certificate.MixedSemantics.raw659 line 409
119. def OAI.MUB6.Certificate.MixedSemantics.raw659Labels line 410
120. def OAI.MUB6.Certificate.MixedSemantics.raw659step0 line 412
121. def OAI.MUB6.Certificate.MixedSemantics.raw659step0Labels line 413
122. theorem OAI.MUB6.Certificate.MixedSemantics.canonical659 line 415
123. def OAI.MUB6.Certificate.MixedSemantics.raw660 line 425
124. def OAI.MUB6.Certificate.MixedSemantics.raw660Labels line 426
125. theorem OAI.MUB6.Certificate.MixedSemantics.canonical660 line 428
126. def OAI.MUB6.Certificate.MixedSemantics.raw661 line 433
127. def OAI.MUB6.Certificate.MixedSemantics.raw661Labels line 434
128. theorem OAI.MUB6.Certificate.MixedSemantics.canonical661 line 436
129. def OAI.MUB6.Certificate.MixedSemantics.raw662 line 441
130. def OAI.MUB6.Certificate.MixedSemantics.raw662Labels line 442
131. theorem OAI.MUB6.Certificate.MixedSemantics.canonical662 line 444
132. def OAI.MUB6.Certificate.MixedSemantics.raw663 line 449
133. def OAI.MUB6.Certificate.MixedSemantics.raw663Labels line 450
134. theorem OAI.MUB6.Certificate.MixedSemantics.canonical663 line 452
135. def OAI.MUB6.Certificate.MixedSemantics.raw664 line 457
136. def OAI.MUB6.Certificate.MixedSemantics.raw664Labels line 458
137. theorem OAI.MUB6.Certificate.MixedSemantics.canonical664 line 460
138. def OAI.MUB6.Certificate.MixedSemantics.raw665 line 465
139. def OAI.MUB6.Certificate.MixedSemantics.raw665Labels line 466
140. theorem OAI.MUB6.Certificate.MixedSemantics.canonical665 line 468
141. def OAI.MUB6.Certificate.MixedSemantics.raw666 line 473
142. def OAI.MUB6.Certificate.MixedSemantics.raw666Labels line 474
143. def OAI.MUB6.Certificate.MixedSemantics.raw666step0 line 476
144. def OAI.MUB6.Certificate.MixedSemantics.raw666step0Labels line 477
145. def OAI.MUB6.Certificate.MixedSemantics.raw666step1 line 479
146. def OAI.MUB6.Certificate.MixedSemantics.raw666step1Labels line 480
147. theorem OAI.MUB6.Certificate.MixedSemantics.canonical666 line 482
148. def OAI.MUB6.Certificate.MixedSemantics.raw667 line 497
149. def OAI.MUB6.Certificate.MixedSemantics.raw667Labels line 498
150. def OAI.MUB6.Certificate.MixedSemantics.raw667step0 line 500
151. def OAI.MUB6.Certificate.MixedSemantics.raw667step0Labels line 501
152. theorem OAI.MUB6.Certificate.MixedSemantics.canonical667 line 503
153. def OAI.MUB6.Certificate.MixedSemantics.raw668 line 513
154. def OAI.MUB6.Certificate.MixedSemantics.raw668Labels line 514
155. def OAI.MUB6.Certificate.MixedSemantics.raw668step0 line 516
156. def OAI.MUB6.Certificate.MixedSemantics.raw668step0Labels line 517
157. def OAI.MUB6.Certificate.MixedSemantics.raw668step1 line 519
158. def OAI.MUB6.Certificate.MixedSemantics.raw668step1Labels line 520
159. def OAI.MUB6.Certificate.MixedSemantics.raw668step2 line 522
160. def OAI.MUB6.Certificate.MixedSemantics.raw668step2Labels line 523
161. theorem OAI.MUB6.Certificate.MixedSemantics.canonical668 line 525
162. def OAI.MUB6.Certificate.MixedSemantics.raw669 line 545
163. def OAI.MUB6.Certificate.MixedSemantics.raw669Labels line 546
164. def OAI.MUB6.Certificate.MixedSemantics.raw669step0 line 548
165. def OAI.MUB6.Certificate.MixedSemantics.raw669step0Labels line 549
166. def OAI.MUB6.Certificate.MixedSemantics.raw669step1 line 551
167. def OAI.MUB6.Certificate.MixedSemantics.raw669step1Labels line 552
168. theorem OAI.MUB6.Certificate.MixedSemantics.canonical669 line 554
169. def OAI.MUB6.Certificate.MixedSemantics.raw670 line 569
170. def OAI.MUB6.Certificate.MixedSemantics.raw670Labels line 570
171. def OAI.MUB6.Certificate.MixedSemantics.raw670step0 line 572
172. def OAI.MUB6.Certificate.MixedSemantics.raw670step0Labels line 573
173. theorem OAI.MUB6.Certificate.MixedSemantics.canonical670 line 575
174. def OAI.MUB6.Certificate.MixedSemantics.raw671 line 585
175. def OAI.MUB6.Certificate.MixedSemantics.raw671Labels line 586
176. def OAI.MUB6.Certificate.MixedSemantics.raw671step0 line 588
177. def OAI.MUB6.Certificate.MixedSemantics.raw671step0Labels line 589
178. def OAI.MUB6.Certificate.MixedSemantics.raw671step1 line 591
179. def OAI.MUB6.Certificate.MixedSemantics.raw671step1Labels line 592
180. def OAI.MUB6.Certificate.MixedSemantics.raw671step2 line 594
181. def OAI.MUB6.Certificate.MixedSemantics.raw671step2Labels line 595
182. theorem OAI.MUB6.Certificate.MixedSemantics.canonical671 line 597
183. def OAI.MUB6.Certificate.MixedSemantics.raw672 line 617
184. def OAI.MUB6.Certificate.MixedSemantics.raw672Labels line 618
185. def OAI.MUB6.Certificate.MixedSemantics.raw672step0 line 620
186. def OAI.MUB6.Certificate.MixedSemantics.raw672step0Labels line 621
187. def OAI.MUB6.Certificate.MixedSemantics.raw672step1 line 623
188. def OAI.MUB6.Certificate.MixedSemantics.raw672step1Labels line 624
189. theorem OAI.MUB6.Certificate.MixedSemantics.canonical672 line 626
190. def OAI.MUB6.Certificate.MixedSemantics.raw673 line 641
191. def OAI.MUB6.Certificate.MixedSemantics.raw673Labels line 642
192. def OAI.MUB6.Certificate.MixedSemantics.raw673step0 line 644
193. def OAI.MUB6.Certificate.MixedSemantics.raw673step0Labels line 645
194. theorem OAI.MUB6.Certificate.MixedSemantics.canonical673 line 647
195. def OAI.MUB6.Certificate.MixedSemantics.raw674 line 657
196. def OAI.MUB6.Certificate.MixedSemantics.raw674Labels line 658
197. def OAI.MUB6.Certificate.MixedSemantics.raw674step0 line 660
198. def OAI.MUB6.Certificate.MixedSemantics.raw674step0Labels line 661
199. def OAI.MUB6.Certificate.MixedSemantics.raw674step1 line 663
200. def OAI.MUB6.Certificate.MixedSemantics.raw674step1Labels line 664
201. def OAI.MUB6.Certificate.MixedSemantics.raw674step2 line 666
202. def OAI.MUB6.Certificate.MixedSemantics.raw674step2Labels line 667
203. theorem OAI.MUB6.Certificate.MixedSemantics.canonical674 line 669
204. def OAI.MUB6.Certificate.MixedSemantics.raw675 line 689
205. def OAI.MUB6.Certificate.MixedSemantics.raw675Labels line 690
206. def OAI.MUB6.Certificate.MixedSemantics.raw675step0 line 692
207. def OAI.MUB6.Certificate.MixedSemantics.raw675step0Labels line 693
208. def OAI.MUB6.Certificate.MixedSemantics.raw675step1 line 695
209. def OAI.MUB6.Certificate.MixedSemantics.raw675step1Labels line 696
210. theorem OAI.MUB6.Certificate.MixedSemantics.canonical675 line 698
211. def OAI.MUB6.Certificate.MixedSemantics.raw676 line 713
212. def OAI.MUB6.Certificate.MixedSemantics.raw676Labels line 714
213. def OAI.MUB6.Certificate.MixedSemantics.raw676step0 line 716
214. def OAI.MUB6.Certificate.MixedSemantics.raw676step0Labels line 717
215. theorem OAI.MUB6.Certificate.MixedSemantics.canonical676 line 719
216. def OAI.MUB6.Certificate.MixedSemantics.raw677 line 729
217. def OAI.MUB6.Certificate.MixedSemantics.raw677Labels line 730
218. def OAI.MUB6.Certificate.MixedSemantics.raw677step0 line 732
219. def OAI.MUB6.Certificate.MixedSemantics.raw677step0Labels line 733
220. def OAI.MUB6.Certificate.MixedSemantics.raw677step1 line 735
221. def OAI.MUB6.Certificate.MixedSemantics.raw677step1Labels line 736
222. def OAI.MUB6.Certificate.MixedSemantics.raw677step2 line 738
223. def OAI.MUB6.Certificate.MixedSemantics.raw677step2Labels line 739
224. theorem OAI.MUB6.Certificate.MixedSemantics.canonical677 line 741
225. def OAI.MUB6.Certificate.MixedSemantics.raw678 line 761
226. def OAI.MUB6.Certificate.MixedSemantics.raw678Labels line 762
227. def OAI.MUB6.Certificate.MixedSemantics.raw678step0 line 764
228. def OAI.MUB6.Certificate.MixedSemantics.raw678step0Labels line 765
229. def OAI.MUB6.Certificate.MixedSemantics.raw678step1 line 767
230. def OAI.MUB6.Certificate.MixedSemantics.raw678step1Labels line 768
231. theorem OAI.MUB6.Certificate.MixedSemantics.canonical678 line 770
232. def OAI.MUB6.Certificate.MixedSemantics.raw679 line 785
233. def OAI.MUB6.Certificate.MixedSemantics.raw679Labels line 786
234. def OAI.MUB6.Certificate.MixedSemantics.raw679step0 line 788
235. def OAI.MUB6.Certificate.MixedSemantics.raw679step0Labels line 789
236. theorem OAI.MUB6.Certificate.MixedSemantics.canonical679 line 791
237. def OAI.MUB6.Certificate.MixedSemantics.raw680 line 801
238. def OAI.MUB6.Certificate.MixedSemantics.raw680Labels line 802
239. def OAI.MUB6.Certificate.MixedSemantics.raw680step0 line 804
240. def OAI.MUB6.Certificate.MixedSemantics.raw680step0Labels line 805
241. def OAI.MUB6.Certificate.MixedSemantics.raw680step1 line 807
242. def OAI.MUB6.Certificate.MixedSemantics.raw680step1Labels line 808
243. def OAI.MUB6.Certificate.MixedSemantics.raw680step2 line 810
244. def OAI.MUB6.Certificate.MixedSemantics.raw680step2Labels line 811
245. theorem OAI.MUB6.Certificate.MixedSemantics.canonical680 line 813
246. def OAI.MUB6.Certificate.MixedSemantics.raw681 line 833
247. def OAI.MUB6.Certificate.MixedSemantics.raw681Labels line 834
248. def OAI.MUB6.Certificate.MixedSemantics.raw681step0 line 836
249. def OAI.MUB6.Certificate.MixedSemantics.raw681step0Labels line 837
250. def OAI.MUB6.Certificate.MixedSemantics.raw681step1 line 839
251. def OAI.MUB6.Certificate.MixedSemantics.raw681step1Labels line 840
252. theorem OAI.MUB6.Certificate.MixedSemantics.canonical681 line 842
253. def OAI.MUB6.Certificate.MixedSemantics.raw682 line 857
254. def OAI.MUB6.Certificate.MixedSemantics.raw682Labels line 858
255. def OAI.MUB6.Certificate.MixedSemantics.raw682step0 line 860
256. def OAI.MUB6.Certificate.MixedSemantics.raw682step0Labels line 861
257. theorem OAI.MUB6.Certificate.MixedSemantics.canonical682 line 863
258. def OAI.MUB6.Certificate.MixedSemantics.raw683 line 873
259. def OAI.MUB6.Certificate.MixedSemantics.raw683Labels line 874
260. def OAI.MUB6.Certificate.MixedSemantics.raw683step0 line 876
261. def OAI.MUB6.Certificate.MixedSemantics.raw683step0Labels line 877
262. def OAI.MUB6.Certificate.MixedSemantics.raw683step1 line 879
263. def OAI.MUB6.Certificate.MixedSemantics.raw683step1Labels line 880
264. def OAI.MUB6.Certificate.MixedSemantics.raw683step2 line 882
265. def OAI.MUB6.Certificate.MixedSemantics.raw683step2Labels line 883
266. theorem OAI.MUB6.Certificate.MixedSemantics.canonical683 line 885
267. def OAI.MUB6.Certificate.MixedSemantics.raw684 line 905
268. def OAI.MUB6.Certificate.MixedSemantics.raw684Labels line 906
269. def OAI.MUB6.Certificate.MixedSemantics.raw684step0 line 908
270. def OAI.MUB6.Certificate.MixedSemantics.raw684step0Labels line 909
271. def OAI.MUB6.Certificate.MixedSemantics.raw684step1 line 911
272. def OAI.MUB6.Certificate.MixedSemantics.raw684step1Labels line 912
273. theorem OAI.MUB6.Certificate.MixedSemantics.canonical684 line 914
274. def OAI.MUB6.Certificate.MixedSemantics.raw685 line 929
275. def OAI.MUB6.Certificate.MixedSemantics.raw685Labels line 930
276. def OAI.MUB6.Certificate.MixedSemantics.raw685step0 line 932
277. def OAI.MUB6.Certificate.MixedSemantics.raw685step0Labels line 933
278. theorem OAI.MUB6.Certificate.MixedSemantics.canonical685 line 935
279. def OAI.MUB6.Certificate.MixedSemantics.raw686 line 945
280. def OAI.MUB6.Certificate.MixedSemantics.raw686Labels line 946
281. def OAI.MUB6.Certificate.MixedSemantics.raw686step0 line 948
282. def OAI.MUB6.Certificate.MixedSemantics.raw686step0Labels line 949
283. def OAI.MUB6.Certificate.MixedSemantics.raw686step1 line 951
284. def OAI.MUB6.Certificate.MixedSemantics.raw686step1Labels line 952
285. def OAI.MUB6.Certificate.MixedSemantics.raw686step2 line 954
286. def OAI.MUB6.Certificate.MixedSemantics.raw686step2Labels line 955
287. theorem OAI.MUB6.Certificate.MixedSemantics.canonical686 line 957
288. def OAI.MUB6.Certificate.MixedSemantics.raw687 line 977
289. def OAI.MUB6.Certificate.MixedSemantics.raw687Labels line 978
290. def OAI.MUB6.Certificate.MixedSemantics.raw687step0 line 980
291. def OAI.MUB6.Certificate.MixedSemantics.raw687step0Labels line 981
292. def OAI.MUB6.Certificate.MixedSemantics.raw687step1 line 983
293. def OAI.MUB6.Certificate.MixedSemantics.raw687step1Labels line 984
294. theorem OAI.MUB6.Certificate.MixedSemantics.canonical687 line 986
295. def OAI.MUB6.Certificate.MixedSemantics.raw688 line 1001
296. def OAI.MUB6.Certificate.MixedSemantics.raw688Labels line 1002
297. def OAI.MUB6.Certificate.MixedSemantics.raw688step0 line 1004
298. def OAI.MUB6.Certificate.MixedSemantics.raw688step0Labels line 1005
299. theorem OAI.MUB6.Certificate.MixedSemantics.canonical688 line 1007
300. def OAI.MUB6.Certificate.MixedSemantics.raw689 line 1017
301. def OAI.MUB6.Certificate.MixedSemantics.raw689Labels line 1018
302. def OAI.MUB6.Certificate.MixedSemantics.raw689step0 line 1020
303. def OAI.MUB6.Certificate.MixedSemantics.raw689step0Labels line 1021
304. def OAI.MUB6.Certificate.MixedSemantics.raw689step1 line 1023
305. def OAI.MUB6.Certificate.MixedSemantics.raw689step1Labels line 1024
306. def OAI.MUB6.Certificate.MixedSemantics.raw689step2 line 1026
307. def OAI.MUB6.Certificate.MixedSemantics.raw689step2Labels line 1027
308. theorem OAI.MUB6.Certificate.MixedSemantics.canonical689 line 1029
309. def OAI.MUB6.Certificate.MixedSemantics.raw690 line 1049
310. def OAI.MUB6.Certificate.MixedSemantics.raw690Labels line 1050
311. def OAI.MUB6.Certificate.MixedSemantics.raw690step0 line 1052
312. def OAI.MUB6.Certificate.MixedSemantics.raw690step0Labels line 1053
313. def OAI.MUB6.Certificate.MixedSemantics.raw690step1 line 1055
314. def OAI.MUB6.Certificate.MixedSemantics.raw690step1Labels line 1056
315. theorem OAI.MUB6.Certificate.MixedSemantics.canonical690 line 1058
316. def OAI.MUB6.Certificate.MixedSemantics.raw691 line 1073
317. def OAI.MUB6.Certificate.MixedSemantics.raw691Labels line 1074
318. def OAI.MUB6.Certificate.MixedSemantics.raw691step0 line 1076
319. def OAI.MUB6.Certificate.MixedSemantics.raw691step0Labels line 1077
320. theorem OAI.MUB6.Certificate.MixedSemantics.canonical691 line 1079
321. def OAI.MUB6.Certificate.MixedSemantics.raw692 line 1089
322. def OAI.MUB6.Certificate.MixedSemantics.raw692Labels line 1090
323. def OAI.MUB6.Certificate.MixedSemantics.raw692step0 line 1092
324. def OAI.MUB6.Certificate.MixedSemantics.raw692step0Labels line 1093
325. def OAI.MUB6.Certificate.MixedSemantics.raw692step1 line 1095
326. def OAI.MUB6.Certificate.MixedSemantics.raw692step1Labels line 1096
327. def OAI.MUB6.Certificate.MixedSemantics.raw692step2 line 1098
328. def OAI.MUB6.Certificate.MixedSemantics.raw692step2Labels line 1099
329. theorem OAI.MUB6.Certificate.MixedSemantics.canonical692 line 1101
330. def OAI.MUB6.Certificate.MixedSemantics.raw693 line 1121
331. def OAI.MUB6.Certificate.MixedSemantics.raw693Labels line 1122
332. def OAI.MUB6.Certificate.MixedSemantics.raw693step0 line 1124
333. def OAI.MUB6.Certificate.MixedSemantics.raw693step0Labels line 1125
334. def OAI.MUB6.Certificate.MixedSemantics.raw693step1 line 1127
335. def OAI.MUB6.Certificate.MixedSemantics.raw693step1Labels line 1128
336. theorem OAI.MUB6.Certificate.MixedSemantics.canonical693 line 1130
337. def OAI.MUB6.Certificate.MixedSemantics.raw694 line 1145
338. def OAI.MUB6.Certificate.MixedSemantics.raw694Labels line 1146
339. def OAI.MUB6.Certificate.MixedSemantics.raw694step0 line 1148
340. def OAI.MUB6.Certificate.MixedSemantics.raw694step0Labels line 1149
341. theorem OAI.MUB6.Certificate.MixedSemantics.canonical694 line 1151
342. def OAI.MUB6.Certificate.MixedSemantics.raw695 line 1161
343. def OAI.MUB6.Certificate.MixedSemantics.raw695Labels line 1162
344. def OAI.MUB6.Certificate.MixedSemantics.raw695step0 line 1164
345. def OAI.MUB6.Certificate.MixedSemantics.raw695step0Labels line 1165
346. def OAI.MUB6.Certificate.MixedSemantics.raw695step1 line 1167
347. def OAI.MUB6.Certificate.MixedSemantics.raw695step1Labels line 1168
348. def OAI.MUB6.Certificate.MixedSemantics.raw695step2 line 1170
349. def OAI.MUB6.Certificate.MixedSemantics.raw695step2Labels line 1171
350. theorem OAI.MUB6.Certificate.MixedSemantics.canonical695 line 1173
351. def OAI.MUB6.Certificate.MixedSemantics.raw696 line 1193
352. def OAI.MUB6.Certificate.MixedSemantics.raw696Labels line 1194
353. def OAI.MUB6.Certificate.MixedSemantics.raw696step0 line 1196
354. def OAI.MUB6.Certificate.MixedSemantics.raw696step0Labels line 1197
355. def OAI.MUB6.Certificate.MixedSemantics.raw696step1 line 1199
356. def OAI.MUB6.Certificate.MixedSemantics.raw696step1Labels line 1200
357. theorem OAI.MUB6.Certificate.MixedSemantics.canonical696 line 1202
358. def OAI.MUB6.Certificate.MixedSemantics.raw697 line 1217
359. def OAI.MUB6.Certificate.MixedSemantics.raw697Labels line 1218
360. def OAI.MUB6.Certificate.MixedSemantics.raw697step0 line 1220
361. def OAI.MUB6.Certificate.MixedSemantics.raw697step0Labels line 1221
362. theorem OAI.MUB6.Certificate.MixedSemantics.canonical697 line 1223
363. def OAI.MUB6.Certificate.MixedSemantics.raw698 line 1233
364. def OAI.MUB6.Certificate.MixedSemantics.raw698Labels line 1234
365. def OAI.MUB6.Certificate.MixedSemantics.raw698step0 line 1236
366. def OAI.MUB6.Certificate.MixedSemantics.raw698step0Labels line 1237
367. def OAI.MUB6.Certificate.MixedSemantics.raw698step1 line 1239
368. def OAI.MUB6.Certificate.MixedSemantics.raw698step1Labels line 1240
369. def OAI.MUB6.Certificate.MixedSemantics.raw698step2 line 1242
370. def OAI.MUB6.Certificate.MixedSemantics.raw698step2Labels line 1243
371. theorem OAI.MUB6.Certificate.MixedSemantics.canonical698 line 1245
372. def OAI.MUB6.Certificate.MixedSemantics.raw699 line 1265
373. def OAI.MUB6.Certificate.MixedSemantics.raw699Labels line 1266
374. def OAI.MUB6.Certificate.MixedSemantics.raw699step0 line 1268
375. def OAI.MUB6.Certificate.MixedSemantics.raw699step0Labels line 1269
376. def OAI.MUB6.Certificate.MixedSemantics.raw699step1 line 1271
377. def OAI.MUB6.Certificate.MixedSemantics.raw699step1Labels line 1272
378. theorem OAI.MUB6.Certificate.MixedSemantics.canonical699 line 1274
379. def OAI.MUB6.Certificate.MixedSemantics.raw700 line 1289
380. def OAI.MUB6.Certificate.MixedSemantics.raw700Labels line 1290
381. def OAI.MUB6.Certificate.MixedSemantics.raw700step0 line 1292
382. def OAI.MUB6.Certificate.MixedSemantics.raw700step0Labels line 1293
383. theorem OAI.MUB6.Certificate.MixedSemantics.canonical700 line 1295
384. def OAI.MUB6.Certificate.MixedSemantics.raw701 line 1305
385. def OAI.MUB6.Certificate.MixedSemantics.raw701Labels line 1306
386. def OAI.MUB6.Certificate.MixedSemantics.raw701step0 line 1308
387. def OAI.MUB6.Certificate.MixedSemantics.raw701step0Labels line 1309
388. def OAI.MUB6.Certificate.MixedSemantics.raw701step1 line 1311
389. def OAI.MUB6.Certificate.MixedSemantics.raw701step1Labels line 1312
390. def OAI.MUB6.Certificate.MixedSemantics.raw701step2 line 1314
391. def OAI.MUB6.Certificate.MixedSemantics.raw701step2Labels line 1315
392. theorem OAI.MUB6.Certificate.MixedSemantics.canonical701 line 1317
393. def OAI.MUB6.Certificate.MixedSemantics.raw702 line 1337
394. def OAI.MUB6.Certificate.MixedSemantics.raw702Labels line 1338
395. def OAI.MUB6.Certificate.MixedSemantics.raw702step0 line 1340
396. def OAI.MUB6.Certificate.MixedSemantics.raw702step0Labels line 1341
397. def OAI.MUB6.Certificate.MixedSemantics.raw702step1 line 1343
398. def OAI.MUB6.Certificate.MixedSemantics.raw702step1Labels line 1344
399. theorem OAI.MUB6.Certificate.MixedSemantics.canonical702 line 1346
400. def OAI.MUB6.Certificate.MixedSemantics.raw703 line 1361
401. def OAI.MUB6.Certificate.MixedSemantics.raw703Labels line 1362
402. def OAI.MUB6.Certificate.MixedSemantics.raw703step0 line 1364
403. def OAI.MUB6.Certificate.MixedSemantics.raw703step0Labels line 1365
404. theorem OAI.MUB6.Certificate.MixedSemantics.canonical703 line 1367
405. def OAI.MUB6.Certificate.MixedSemantics.raw704 line 1377
406. def OAI.MUB6.Certificate.MixedSemantics.raw704Labels line 1378
407. def OAI.MUB6.Certificate.MixedSemantics.raw704step0 line 1380
408. def OAI.MUB6.Certificate.MixedSemantics.raw704step0Labels line 1381
409. def OAI.MUB6.Certificate.MixedSemantics.raw704step1 line 1383
410. def OAI.MUB6.Certificate.MixedSemantics.raw704step1Labels line 1384
411. def OAI.MUB6.Certificate.MixedSemantics.raw704step2 line 1386
412. def OAI.MUB6.Certificate.MixedSemantics.raw704step2Labels line 1387
413. theorem OAI.MUB6.Certificate.MixedSemantics.canonical704 line 1389
414. def OAI.MUB6.Certificate.MixedSemantics.raw705 line 1409
415. def OAI.MUB6.Certificate.MixedSemantics.raw705Labels line 1410
416. def OAI.MUB6.Certificate.MixedSemantics.raw705step0 line 1412
417. def OAI.MUB6.Certificate.MixedSemantics.raw705step0Labels line 1413
418. def OAI.MUB6.Certificate.MixedSemantics.raw705step1 line 1415
419. def OAI.MUB6.Certificate.MixedSemantics.raw705step1Labels line 1416
420. theorem OAI.MUB6.Certificate.MixedSemantics.canonical705 line 1418
421. def OAI.MUB6.Certificate.MixedSemantics.raw706 line 1433
422. def OAI.MUB6.Certificate.MixedSemantics.raw706Labels line 1434
423. def OAI.MUB6.Certificate.MixedSemantics.raw706step0 line 1436
424. def OAI.MUB6.Certificate.MixedSemantics.raw706step0Labels line 1437
425. theorem OAI.MUB6.Certificate.MixedSemantics.canonical706 line 1439
426. def OAI.MUB6.Certificate.MixedSemantics.raw707 line 1449
427. def OAI.MUB6.Certificate.MixedSemantics.raw707Labels line 1450
428. def OAI.MUB6.Certificate.MixedSemantics.raw707step0 line 1452
429. def OAI.MUB6.Certificate.MixedSemantics.raw707step0Labels line 1453
430. def OAI.MUB6.Certificate.MixedSemantics.raw707step1 line 1455
431. def OAI.MUB6.Certificate.MixedSemantics.raw707step1Labels line 1456
432. def OAI.MUB6.Certificate.MixedSemantics.raw707step2 line 1458
433. def OAI.MUB6.Certificate.MixedSemantics.raw707step2Labels line 1459
434. theorem OAI.MUB6.Certificate.MixedSemantics.canonical707 line 1461
435. def OAI.MUB6.Certificate.MixedSemantics.raw708 line 1481
436. def OAI.MUB6.Certificate.MixedSemantics.raw708Labels line 1482
437. def OAI.MUB6.Certificate.MixedSemantics.raw708step0 line 1484
438. def OAI.MUB6.Certificate.MixedSemantics.raw708step0Labels line 1485
439. def OAI.MUB6.Certificate.MixedSemantics.raw708step1 line 1487
440. def OAI.MUB6.Certificate.MixedSemantics.raw708step1Labels line 1488
441. theorem OAI.MUB6.Certificate.MixedSemantics.canonical708 line 1490
442. def OAI.MUB6.Certificate.MixedSemantics.raw709 line 1505
443. def OAI.MUB6.Certificate.MixedSemantics.raw709Labels line 1506
444. def OAI.MUB6.Certificate.MixedSemantics.raw709step0 line 1508
445. def OAI.MUB6.Certificate.MixedSemantics.raw709step0Labels line 1509
446. theorem OAI.MUB6.Certificate.MixedSemantics.canonical709 line 1511
447. def OAI.MUB6.Certificate.MixedSemantics.raw710 line 1521
448. def OAI.MUB6.Certificate.MixedSemantics.raw710Labels line 1522
449. def OAI.MUB6.Certificate.MixedSemantics.raw710step0 line 1524
450. def OAI.MUB6.Certificate.MixedSemantics.raw710step0Labels line 1525
451. def OAI.MUB6.Certificate.MixedSemantics.raw710step1 line 1527
452. def OAI.MUB6.Certificate.MixedSemantics.raw710step1Labels line 1528
453. def OAI.MUB6.Certificate.MixedSemantics.raw710step2 line 1530
454. def OAI.MUB6.Certificate.MixedSemantics.raw710step2Labels line 1531
455. theorem OAI.MUB6.Certificate.MixedSemantics.canonical710 line 1533
456. def OAI.MUB6.Certificate.MixedSemantics.raw711 line 1553
457. def OAI.MUB6.Certificate.MixedSemantics.raw711Labels line 1554
458. def OAI.MUB6.Certificate.MixedSemantics.raw711step0 line 1556
459. def OAI.MUB6.Certificate.MixedSemantics.raw711step0Labels line 1557
460. def OAI.MUB6.Certificate.MixedSemantics.raw711step1 line 1559
461. def OAI.MUB6.Certificate.MixedSemantics.raw711step1Labels line 1560
462. theorem OAI.MUB6.Certificate.MixedSemantics.canonical711 line 1562
463. def OAI.MUB6.Certificate.MixedSemantics.raw712 line 1577
464. def OAI.MUB6.Certificate.MixedSemantics.raw712Labels line 1578
465. def OAI.MUB6.Certificate.MixedSemantics.raw712step0 line 1580
466. def OAI.MUB6.Certificate.MixedSemantics.raw712step0Labels line 1581
467. theorem OAI.MUB6.Certificate.MixedSemantics.canonical712 line 1583
468. def OAI.MUB6.Certificate.MixedSemantics.raw713 line 1593
469. def OAI.MUB6.Certificate.MixedSemantics.raw713Labels line 1594
470. def OAI.MUB6.Certificate.MixedSemantics.raw713step0 line 1596
471. def OAI.MUB6.Certificate.MixedSemantics.raw713step0Labels line 1597
472. def OAI.MUB6.Certificate.MixedSemantics.raw713step1 line 1599
473. def OAI.MUB6.Certificate.MixedSemantics.raw713step1Labels line 1600
474. def OAI.MUB6.Certificate.MixedSemantics.raw713step2 line 1602
475. def OAI.MUB6.Certificate.MixedSemantics.raw713step2Labels line 1603
476. theorem OAI.MUB6.Certificate.MixedSemantics.canonical713 line 1605
477. def OAI.MUB6.Certificate.MixedSemantics.raw714 line 1625
478. def OAI.MUB6.Certificate.MixedSemantics.raw714Labels line 1626
479. def OAI.MUB6.Certificate.MixedSemantics.raw714step0 line 1628
480. def OAI.MUB6.Certificate.MixedSemantics.raw714step0Labels line 1629
481. def OAI.MUB6.Certificate.MixedSemantics.raw714step1 line 1631
482. def OAI.MUB6.Certificate.MixedSemantics.raw714step1Labels line 1632
483. theorem OAI.MUB6.Certificate.MixedSemantics.canonical714 line 1634
484. def OAI.MUB6.Certificate.MixedSemantics.raw715 line 1649
485. def OAI.MUB6.Certificate.MixedSemantics.raw715Labels line 1650
486. def OAI.MUB6.Certificate.MixedSemantics.raw715step0 line 1652
487. def OAI.MUB6.Certificate.MixedSemantics.raw715step0Labels line 1653
488. theorem OAI.MUB6.Certificate.MixedSemantics.canonical715 line 1655
489. def OAI.MUB6.Certificate.MixedSemantics.raw716 line 1665
490. def OAI.MUB6.Certificate.MixedSemantics.raw716Labels line 1666
491. def OAI.MUB6.Certificate.MixedSemantics.raw716step0 line 1668
492. def OAI.MUB6.Certificate.MixedSemantics.raw716step0Labels line 1669
493. def OAI.MUB6.Certificate.MixedSemantics.raw716step1 line 1671
494. def OAI.MUB6.Certificate.MixedSemantics.raw716step1Labels line 1672
495. def OAI.MUB6.Certificate.MixedSemantics.raw716step2 line 1674
496. def OAI.MUB6.Certificate.MixedSemantics.raw716step2Labels line 1675
497. theorem OAI.MUB6.Certificate.MixedSemantics.canonical716 line 1677
498. def OAI.MUB6.Certificate.MixedSemantics.raw717 line 1697
499. def OAI.MUB6.Certificate.MixedSemantics.raw717Labels line 1698
500. def OAI.MUB6.Certificate.MixedSemantics.raw717step0 line 1700
501. def OAI.MUB6.Certificate.MixedSemantics.raw717step0Labels line 1701
502. def OAI.MUB6.Certificate.MixedSemantics.raw717step1 line 1703
503. def OAI.MUB6.Certificate.MixedSemantics.raw717step1Labels line 1704
504. theorem OAI.MUB6.Certificate.MixedSemantics.canonical717 line 1706
505. def OAI.MUB6.Certificate.MixedSemantics.raw718 line 1721
506. def OAI.MUB6.Certificate.MixedSemantics.raw718Labels line 1722
507. def OAI.MUB6.Certificate.MixedSemantics.raw718step0 line 1724
508. def OAI.MUB6.Certificate.MixedSemantics.raw718step0Labels line 1725
509. theorem OAI.MUB6.Certificate.MixedSemantics.canonical718 line 1727
510. def OAI.MUB6.Certificate.MixedSemantics.raw719 line 1737
511. def OAI.MUB6.Certificate.MixedSemantics.raw719Labels line 1738
512. def OAI.MUB6.Certificate.MixedSemantics.raw719step0 line 1740
513. def OAI.MUB6.Certificate.MixedSemantics.raw719step0Labels line 1741
514. def OAI.MUB6.Certificate.MixedSemantics.raw719step1 line 1743
515. def OAI.MUB6.Certificate.MixedSemantics.raw719step1Labels line 1744
516. def OAI.MUB6.Certificate.MixedSemantics.raw719step2 line 1746
517. def OAI.MUB6.Certificate.MixedSemantics.raw719step2Labels line 1747
518. theorem OAI.MUB6.Certificate.MixedSemantics.canonical719 line 1749
519. def OAI.MUB6.Certificate.MixedSemantics.raw720 line 1769
520. def OAI.MUB6.Certificate.MixedSemantics.raw720Labels line 1770
521. def OAI.MUB6.Certificate.MixedSemantics.raw720step0 line 1772
522. def OAI.MUB6.Certificate.MixedSemantics.raw720step0Labels line 1773
523. def OAI.MUB6.Certificate.MixedSemantics.raw720step1 line 1775
524. def OAI.MUB6.Certificate.MixedSemantics.raw720step1Labels line 1776
525. theorem OAI.MUB6.Certificate.MixedSemantics.canonical720 line 1778
526. def OAI.MUB6.Certificate.MixedSemantics.raw721 line 1793
527. def OAI.MUB6.Certificate.MixedSemantics.raw721Labels line 1794
528. def OAI.MUB6.Certificate.MixedSemantics.raw721step0 line 1796
529. def OAI.MUB6.Certificate.MixedSemantics.raw721step0Labels line 1797
530. theorem OAI.MUB6.Certificate.MixedSemantics.canonical721 line 1799
531. def OAI.MUB6.Certificate.MixedSemantics.raw722 line 1809
532. def OAI.MUB6.Certificate.MixedSemantics.raw722Labels line 1810
533. def OAI.MUB6.Certificate.MixedSemantics.raw722step0 line 1812
534. def OAI.MUB6.Certificate.MixedSemantics.raw722step0Labels line 1813
535. def OAI.MUB6.Certificate.MixedSemantics.raw722step1 line 1815
536. def OAI.MUB6.Certificate.MixedSemantics.raw722step1Labels line 1816
537. def OAI.MUB6.Certificate.MixedSemantics.raw722step2 line 1818
538. def OAI.MUB6.Certificate.MixedSemantics.raw722step2Labels line 1819
539. theorem OAI.MUB6.Certificate.MixedSemantics.canonical722 line 1821
540. def OAI.MUB6.Certificate.MixedSemantics.raw723 line 1841
541. def OAI.MUB6.Certificate.MixedSemantics.raw723Labels line 1842
542. def OAI.MUB6.Certificate.MixedSemantics.raw723step0 line 1844
543. def OAI.MUB6.Certificate.MixedSemantics.raw723step0Labels line 1845
544. def OAI.MUB6.Certificate.MixedSemantics.raw723step1 line 1847
545. def OAI.MUB6.Certificate.MixedSemantics.raw723step1Labels line 1848
546. theorem OAI.MUB6.Certificate.MixedSemantics.canonical723 line 1850
547. def OAI.MUB6.Certificate.MixedSemantics.raw724 line 1865
548. def OAI.MUB6.Certificate.MixedSemantics.raw724Labels line 1866
549. def OAI.MUB6.Certificate.MixedSemantics.raw724step0 line 1868
550. def OAI.MUB6.Certificate.MixedSemantics.raw724step0Labels line 1869
551. theorem OAI.MUB6.Certificate.MixedSemantics.canonical724 line 1871
552. def OAI.MUB6.Certificate.MixedSemantics.raw725 line 1881
553. def OAI.MUB6.Certificate.MixedSemantics.raw725Labels line 1882
554. def OAI.MUB6.Certificate.MixedSemantics.raw725step0 line 1884
555. def OAI.MUB6.Certificate.MixedSemantics.raw725step0Labels line 1885
556. def OAI.MUB6.Certificate.MixedSemantics.raw725step1 line 1887
557. def OAI.MUB6.Certificate.MixedSemantics.raw725step1Labels line 1888
558. def OAI.MUB6.Certificate.MixedSemantics.raw725step2 line 1890
559. def OAI.MUB6.Certificate.MixedSemantics.raw725step2Labels line 1891
560. theorem OAI.MUB6.Certificate.MixedSemantics.canonical725 line 1893
561. def OAI.MUB6.Certificate.MixedSemantics.raw726 line 1913
562. def OAI.MUB6.Certificate.MixedSemantics.raw726Labels line 1914
563. def OAI.MUB6.Certificate.MixedSemantics.raw726step0 line 1916
564. def OAI.MUB6.Certificate.MixedSemantics.raw726step0Labels line 1917
565. def OAI.MUB6.Certificate.MixedSemantics.raw726step1 line 1919
566. def OAI.MUB6.Certificate.MixedSemantics.raw726step1Labels line 1920
567. theorem OAI.MUB6.Certificate.MixedSemantics.canonical726 line 1922
568. def OAI.MUB6.Certificate.MixedSemantics.raw727 line 1937
569. def OAI.MUB6.Certificate.MixedSemantics.raw727Labels line 1938
570. def OAI.MUB6.Certificate.MixedSemantics.raw727step0 line 1940
571. def OAI.MUB6.Certificate.MixedSemantics.raw727step0Labels line 1941
572. theorem OAI.MUB6.Certificate.MixedSemantics.canonical727 line 1943
573. def OAI.MUB6.Certificate.MixedSemantics.raw728 line 1953
574. def OAI.MUB6.Certificate.MixedSemantics.raw728Labels line 1954
575. def OAI.MUB6.Certificate.MixedSemantics.raw728step0 line 1956
576. def OAI.MUB6.Certificate.MixedSemantics.raw728step0Labels line 1957
577. def OAI.MUB6.Certificate.MixedSemantics.raw728step1 line 1959
578. def OAI.MUB6.Certificate.MixedSemantics.raw728step1Labels line 1960
579. def OAI.MUB6.Certificate.MixedSemantics.raw728step2 line 1962
580. def OAI.MUB6.Certificate.MixedSemantics.raw728step2Labels line 1963
581. theorem OAI.MUB6.Certificate.MixedSemantics.canonical728 line 1965
582. def OAI.MUB6.Certificate.MixedSemantics.raw729 line 1985
583. def OAI.MUB6.Certificate.MixedSemantics.raw729Labels line 1986
584. def OAI.MUB6.Certificate.MixedSemantics.raw729step0 line 1988
585. def OAI.MUB6.Certificate.MixedSemantics.raw729step0Labels line 1989
586. def OAI.MUB6.Certificate.MixedSemantics.raw729step1 line 1991
587. def OAI.MUB6.Certificate.MixedSemantics.raw729step1Labels line 1992
588. theorem OAI.MUB6.Certificate.MixedSemantics.canonical729 line 1994
589. def OAI.MUB6.Certificate.MixedSemantics.raw730 line 2009
590. def OAI.MUB6.Certificate.MixedSemantics.raw730Labels line 2010
591. def OAI.MUB6.Certificate.MixedSemantics.raw730step0 line 2012
592. def OAI.MUB6.Certificate.MixedSemantics.raw730step0Labels line 2013
593. theorem OAI.MUB6.Certificate.MixedSemantics.canonical730 line 2015
594. def OAI.MUB6.Certificate.MixedSemantics.raw731 line 2025
595. def OAI.MUB6.Certificate.MixedSemantics.raw731Labels line 2026
596. def OAI.MUB6.Certificate.MixedSemantics.raw731step0 line 2028
597. def OAI.MUB6.Certificate.MixedSemantics.raw731step0Labels line 2029
598. def OAI.MUB6.Certificate.MixedSemantics.raw731step1 line 2031
599. def OAI.MUB6.Certificate.MixedSemantics.raw731step1Labels line 2032
600. def OAI.MUB6.Certificate.MixedSemantics.raw731step2 line 2034
601. def OAI.MUB6.Certificate.MixedSemantics.raw731step2Labels line 2035
602. theorem OAI.MUB6.Certificate.MixedSemantics.canonical731 line 2037
603. def OAI.MUB6.Certificate.MixedSemantics.raw732 line 2057
604. def OAI.MUB6.Certificate.MixedSemantics.raw732Labels line 2058
605. def OAI.MUB6.Certificate.MixedSemantics.raw732step0 line 2060
606. def OAI.MUB6.Certificate.MixedSemantics.raw732step0Labels line 2061
607. def OAI.MUB6.Certificate.MixedSemantics.raw732step1 line 2063
608. def OAI.MUB6.Certificate.MixedSemantics.raw732step1Labels line 2064
609. theorem OAI.MUB6.Certificate.MixedSemantics.canonical732 line 2066
610. def OAI.MUB6.Certificate.MixedSemantics.raw733 line 2081
611. def OAI.MUB6.Certificate.MixedSemantics.raw733Labels line 2082
612. def OAI.MUB6.Certificate.MixedSemantics.raw733step0 line 2084
613. def OAI.MUB6.Certificate.MixedSemantics.raw733step0Labels line 2085
614. theorem OAI.MUB6.Certificate.MixedSemantics.canonical733 line 2087
615. def OAI.MUB6.Certificate.MixedSemantics.raw734 line 2097
616. def OAI.MUB6.Certificate.MixedSemantics.raw734Labels line 2098
617. def OAI.MUB6.Certificate.MixedSemantics.raw734step0 line 2100
618. def OAI.MUB6.Certificate.MixedSemantics.raw734step0Labels line 2101
619. def OAI.MUB6.Certificate.MixedSemantics.raw734step1 line 2103
620. def OAI.MUB6.Certificate.MixedSemantics.raw734step1Labels line 2104
621. def OAI.MUB6.Certificate.MixedSemantics.raw734step2 line 2106
622. def OAI.MUB6.Certificate.MixedSemantics.raw734step2Labels line 2107
623. theorem OAI.MUB6.Certificate.MixedSemantics.canonical734 line 2109
624. def OAI.MUB6.Certificate.MixedSemantics.raw735 line 2129
625. def OAI.MUB6.Certificate.MixedSemantics.raw735Labels line 2130
626. def OAI.MUB6.Certificate.MixedSemantics.raw735step0 line 2132
627. def OAI.MUB6.Certificate.MixedSemantics.raw735step0Labels line 2133
628. def OAI.MUB6.Certificate.MixedSemantics.raw735step1 line 2135
629. def OAI.MUB6.Certificate.MixedSemantics.raw735step1Labels line 2136
630. theorem OAI.MUB6.Certificate.MixedSemantics.canonical735 line 2138
631. def OAI.MUB6.Certificate.MixedSemantics.raw736 line 2153
632. def OAI.MUB6.Certificate.MixedSemantics.raw736Labels line 2154
633. def OAI.MUB6.Certificate.MixedSemantics.raw736step0 line 2156
634. def OAI.MUB6.Certificate.MixedSemantics.raw736step0Labels line 2157
635. theorem OAI.MUB6.Certificate.MixedSemantics.canonical736 line 2159
636. def OAI.MUB6.Certificate.MixedSemantics.raw737 line 2169
637. def OAI.MUB6.Certificate.MixedSemantics.raw737Labels line 2170
638. def OAI.MUB6.Certificate.MixedSemantics.raw737step0 line 2172
639. def OAI.MUB6.Certificate.MixedSemantics.raw737step0Labels line 2173
640. def OAI.MUB6.Certificate.MixedSemantics.raw737step1 line 2175
641. def OAI.MUB6.Certificate.MixedSemantics.raw737step1Labels line 2176
642. def OAI.MUB6.Certificate.MixedSemantics.raw737step2 line 2178
643. def OAI.MUB6.Certificate.MixedSemantics.raw737step2Labels line 2179
644. theorem OAI.MUB6.Certificate.MixedSemantics.canonical737 line 2181
645. def OAI.MUB6.Certificate.MixedSemantics.raw738 line 2201
646. def OAI.MUB6.Certificate.MixedSemantics.raw738Labels line 2202
647. def OAI.MUB6.Certificate.MixedSemantics.raw738step0 line 2204
648. def OAI.MUB6.Certificate.MixedSemantics.raw738step0Labels line 2205
649. def OAI.MUB6.Certificate.MixedSemantics.raw738step1 line 2207
650. def OAI.MUB6.Certificate.MixedSemantics.raw738step1Labels line 2208
651. theorem OAI.MUB6.Certificate.MixedSemantics.canonical738 line 2210
652. def OAI.MUB6.Certificate.MixedSemantics.raw739 line 2225
653. def OAI.MUB6.Certificate.MixedSemantics.raw739Labels line 2226
654. def OAI.MUB6.Certificate.MixedSemantics.raw739step0 line 2228
655. def OAI.MUB6.Certificate.MixedSemantics.raw739step0Labels line 2229
656. theorem OAI.MUB6.Certificate.MixedSemantics.canonical739 line 2231
657. def OAI.MUB6.Certificate.MixedSemantics.raw740 line 2241
658. def OAI.MUB6.Certificate.MixedSemantics.raw740Labels line 2242
659. def OAI.MUB6.Certificate.MixedSemantics.raw740step0 line 2244
660. def OAI.MUB6.Certificate.MixedSemantics.raw740step0Labels line 2245
661. def OAI.MUB6.Certificate.MixedSemantics.raw740step1 line 2247
662. def OAI.MUB6.Certificate.MixedSemantics.raw740step1Labels line 2248
663. def OAI.MUB6.Certificate.MixedSemantics.raw740step2 line 2250
664. def OAI.MUB6.Certificate.MixedSemantics.raw740step2Labels line 2251
665. theorem OAI.MUB6.Certificate.MixedSemantics.canonical740 line 2253
666. def OAI.MUB6.Certificate.MixedSemantics.raw741 line 2273
667. def OAI.MUB6.Certificate.MixedSemantics.raw741Labels line 2274
668. def OAI.MUB6.Certificate.MixedSemantics.raw741step0 line 2276
669. def OAI.MUB6.Certificate.MixedSemantics.raw741step0Labels line 2277
670. def OAI.MUB6.Certificate.MixedSemantics.raw741step1 line 2279
671. def OAI.MUB6.Certificate.MixedSemantics.raw741step1Labels line 2280
672. theorem OAI.MUB6.Certificate.MixedSemantics.canonical741 line 2282
673. def OAI.MUB6.Certificate.MixedSemantics.raw742 line 2297
674. def OAI.MUB6.Certificate.MixedSemantics.raw742Labels line 2298
675. def OAI.MUB6.Certificate.MixedSemantics.raw742step0 line 2300
676. def OAI.MUB6.Certificate.MixedSemantics.raw742step0Labels line 2301
677. theorem OAI.MUB6.Certificate.MixedSemantics.canonical742 line 2303
678. def OAI.MUB6.Certificate.MixedSemantics.raw743 line 2313
679. def OAI.MUB6.Certificate.MixedSemantics.raw743Labels line 2314
680. def OAI.MUB6.Certificate.MixedSemantics.raw743step0 line 2316
681. def OAI.MUB6.Certificate.MixedSemantics.raw743step0Labels line 2317
682. def OAI.MUB6.Certificate.MixedSemantics.raw743step1 line 2319
683. def OAI.MUB6.Certificate.MixedSemantics.raw743step1Labels line 2320
684. def OAI.MUB6.Certificate.MixedSemantics.raw743step2 line 2322
685. def OAI.MUB6.Certificate.MixedSemantics.raw743step2Labels line 2323
686. theorem OAI.MUB6.Certificate.MixedSemantics.canonical743 line 2325
687. def OAI.MUB6.Certificate.MixedSemantics.raw744 line 2345
688. def OAI.MUB6.Certificate.MixedSemantics.raw744Labels line 2346
689. def OAI.MUB6.Certificate.MixedSemantics.raw744step0 line 2348
690. def OAI.MUB6.Certificate.MixedSemantics.raw744step0Labels line 2349
691. def OAI.MUB6.Certificate.MixedSemantics.raw744step1 line 2351
692. def OAI.MUB6.Certificate.MixedSemantics.raw744step1Labels line 2352
693. theorem OAI.MUB6.Certificate.MixedSemantics.canonical744 line 2354
694. def OAI.MUB6.Certificate.MixedSemantics.raw745 line 2369
695. def OAI.MUB6.Certificate.MixedSemantics.raw745Labels line 2370
696. def OAI.MUB6.Certificate.MixedSemantics.raw745step0 line 2372
697. def OAI.MUB6.Certificate.MixedSemantics.raw745step0Labels line 2373
698. theorem OAI.MUB6.Certificate.MixedSemantics.canonical745 line 2375
699. def OAI.MUB6.Certificate.MixedSemantics.raw746 line 2385
700. def OAI.MUB6.Certificate.MixedSemantics.raw746Labels line 2386
701. def OAI.MUB6.Certificate.MixedSemantics.raw746step0 line 2388
702. def OAI.MUB6.Certificate.MixedSemantics.raw746step0Labels line 2389
703. def OAI.MUB6.Certificate.MixedSemantics.raw746step1 line 2391
704. def OAI.MUB6.Certificate.MixedSemantics.raw746step1Labels line 2392
705. def OAI.MUB6.Certificate.MixedSemantics.raw746step2 line 2394
706. def OAI.MUB6.Certificate.MixedSemantics.raw746step2Labels line 2395
707. theorem OAI.MUB6.Certificate.MixedSemantics.canonical746 line 2397
708. def OAI.MUB6.Certificate.MixedSemantics.raw747 line 2417
709. def OAI.MUB6.Certificate.MixedSemantics.raw747Labels line 2418
710. def OAI.MUB6.Certificate.MixedSemantics.raw747step0 line 2420
711. def OAI.MUB6.Certificate.MixedSemantics.raw747step0Labels line 2421
712. def OAI.MUB6.Certificate.MixedSemantics.raw747step1 line 2423
713. def OAI.MUB6.Certificate.MixedSemantics.raw747step1Labels line 2424
714. theorem OAI.MUB6.Certificate.MixedSemantics.canonical747 line 2426
715. def OAI.MUB6.Certificate.MixedSemantics.raw748 line 2441
716. def OAI.MUB6.Certificate.MixedSemantics.raw748Labels line 2442
717. def OAI.MUB6.Certificate.MixedSemantics.raw748step0 line 2444
718. def OAI.MUB6.Certificate.MixedSemantics.raw748step0Labels line 2445
719. theorem OAI.MUB6.Certificate.MixedSemantics.canonical748 line 2447
720. def OAI.MUB6.Certificate.MixedSemantics.raw749 line 2457
721. def OAI.MUB6.Certificate.MixedSemantics.raw749Labels line 2458
722. def OAI.MUB6.Certificate.MixedSemantics.raw749step0 line 2460
723. def OAI.MUB6.Certificate.MixedSemantics.raw749step0Labels line 2461
724. def OAI.MUB6.Certificate.MixedSemantics.raw749step1 line 2463
725. def OAI.MUB6.Certificate.MixedSemantics.raw749step1Labels line 2464
726. def OAI.MUB6.Certificate.MixedSemantics.raw749step2 line 2466
727. def OAI.MUB6.Certificate.MixedSemantics.raw749step2Labels line 2467
728. theorem OAI.MUB6.Certificate.MixedSemantics.canonical749 line 2469
729. def OAI.MUB6.Certificate.MixedSemantics.raw750 line 2489
730. def OAI.MUB6.Certificate.MixedSemantics.raw750Labels line 2490
731. def OAI.MUB6.Certificate.MixedSemantics.raw750step0 line 2492
732. def OAI.MUB6.Certificate.MixedSemantics.raw750step0Labels line 2493
733. def OAI.MUB6.Certificate.MixedSemantics.raw750step1 line 2495
734. def OAI.MUB6.Certificate.MixedSemantics.raw750step1Labels line 2496
735. theorem OAI.MUB6.Certificate.MixedSemantics.canonical750 line 2498
736. def OAI.MUB6.Certificate.MixedSemantics.raw751 line 2513
737. def OAI.MUB6.Certificate.MixedSemantics.raw751Labels line 2514
738. def OAI.MUB6.Certificate.MixedSemantics.raw751step0 line 2516
739. def OAI.MUB6.Certificate.MixedSemantics.raw751step0Labels line 2517
740. theorem OAI.MUB6.Certificate.MixedSemantics.canonical751 line 2519
741. def OAI.MUB6.Certificate.MixedSemantics.raw752 line 2529
742. def OAI.MUB6.Certificate.MixedSemantics.raw752Labels line 2530
743. def OAI.MUB6.Certificate.MixedSemantics.raw752step0 line 2532
744. def OAI.MUB6.Certificate.MixedSemantics.raw752step0Labels line 2533
745. def OAI.MUB6.Certificate.MixedSemantics.raw752step1 line 2535
746. def OAI.MUB6.Certificate.MixedSemantics.raw752step1Labels line 2536
747. def OAI.MUB6.Certificate.MixedSemantics.raw752step2 line 2538
748. def OAI.MUB6.Certificate.MixedSemantics.raw752step2Labels line 2539
749. theorem OAI.MUB6.Certificate.MixedSemantics.canonical752 line 2541
750. def OAI.MUB6.Certificate.MixedSemantics.raw753 line 2561
751. def OAI.MUB6.Certificate.MixedSemantics.raw753Labels line 2562
752. def OAI.MUB6.Certificate.MixedSemantics.raw753step0 line 2564
753. def OAI.MUB6.Certificate.MixedSemantics.raw753step0Labels line 2565
754. def OAI.MUB6.Certificate.MixedSemantics.raw753step1 line 2567
755. def OAI.MUB6.Certificate.MixedSemantics.raw753step1Labels line 2568
756. theorem OAI.MUB6.Certificate.MixedSemantics.canonical753 line 2570
757. def OAI.MUB6.Certificate.MixedSemantics.raw754 line 2585
758. def OAI.MUB6.Certificate.MixedSemantics.raw754Labels line 2586
759. def OAI.MUB6.Certificate.MixedSemantics.raw754step0 line 2588
760. def OAI.MUB6.Certificate.MixedSemantics.raw754step0Labels line 2589
761. theorem OAI.MUB6.Certificate.MixedSemantics.canonical754 line 2591
762. def OAI.MUB6.Certificate.MixedSemantics.raw755 line 2601
763. def OAI.MUB6.Certificate.MixedSemantics.raw755Labels line 2602
764. def OAI.MUB6.Certificate.MixedSemantics.raw755step0 line 2604
765. def OAI.MUB6.Certificate.MixedSemantics.raw755step0Labels line 2605
766. def OAI.MUB6.Certificate.MixedSemantics.raw755step1 line 2607
767. def OAI.MUB6.Certificate.MixedSemantics.raw755step1Labels line 2608
768. def OAI.MUB6.Certificate.MixedSemantics.raw755step2 line 2610
769. def OAI.MUB6.Certificate.MixedSemantics.raw755step2Labels line 2611
770. theorem OAI.MUB6.Certificate.MixedSemantics.canonical755 line 2613
771. def OAI.MUB6.Certificate.MixedSemantics.raw756 line 2633
772. def OAI.MUB6.Certificate.MixedSemantics.raw756Labels line 2634
773. def OAI.MUB6.Certificate.MixedSemantics.raw756step0 line 2636
774. def OAI.MUB6.Certificate.MixedSemantics.raw756step0Labels line 2637
775. def OAI.MUB6.Certificate.MixedSemantics.raw756step1 line 2639
776. def OAI.MUB6.Certificate.MixedSemantics.raw756step1Labels line 2640
777. theorem OAI.MUB6.Certificate.MixedSemantics.canonical756 line 2642
778. def OAI.MUB6.Certificate.MixedSemantics.raw757 line 2657
779. def OAI.MUB6.Certificate.MixedSemantics.raw757Labels line 2658
780. def OAI.MUB6.Certificate.MixedSemantics.raw757step0 line 2660
781. def OAI.MUB6.Certificate.MixedSemantics.raw757step0Labels line 2661
782. theorem OAI.MUB6.Certificate.MixedSemantics.canonical757 line 2663
783. def OAI.MUB6.Certificate.MixedSemantics.raw758 line 2673
784. def OAI.MUB6.Certificate.MixedSemantics.raw758Labels line 2674
785. def OAI.MUB6.Certificate.MixedSemantics.raw758step0 line 2676
786. def OAI.MUB6.Certificate.MixedSemantics.raw758step0Labels line 2677
787. def OAI.MUB6.Certificate.MixedSemantics.raw758step1 line 2679
788. def OAI.MUB6.Certificate.MixedSemantics.raw758step1Labels line 2680
789. def OAI.MUB6.Certificate.MixedSemantics.raw758step2 line 2682
790. def OAI.MUB6.Certificate.MixedSemantics.raw758step2Labels line 2683
791. theorem OAI.MUB6.Certificate.MixedSemantics.canonical758 line 2685
792. def OAI.MUB6.Certificate.MixedSemantics.raw759 line 2705
793. def OAI.MUB6.Certificate.MixedSemantics.raw759Labels line 2706
794. def OAI.MUB6.Certificate.MixedSemantics.raw759step0 line 2708
795. def OAI.MUB6.Certificate.MixedSemantics.raw759step0Labels line 2709
796. def OAI.MUB6.Certificate.MixedSemantics.raw759step1 line 2711
797. def OAI.MUB6.Certificate.MixedSemantics.raw759step1Labels line 2712
798. theorem OAI.MUB6.Certificate.MixedSemantics.canonical759 line 2714
799. def OAI.MUB6.Certificate.MixedSemantics.raw760 line 2729
800. def OAI.MUB6.Certificate.MixedSemantics.raw760Labels line 2730
801. def OAI.MUB6.Certificate.MixedSemantics.raw760step0 line 2732
802. def OAI.MUB6.Certificate.MixedSemantics.raw760step0Labels line 2733
803. theorem OAI.MUB6.Certificate.MixedSemantics.canonical760 line 2735
804. def OAI.MUB6.Certificate.MixedSemantics.raw761 line 2745
805. def OAI.MUB6.Certificate.MixedSemantics.raw761Labels line 2746
806. def OAI.MUB6.Certificate.MixedSemantics.raw761step0 line 2748
807. def OAI.MUB6.Certificate.MixedSemantics.raw761step0Labels line 2749
808. def OAI.MUB6.Certificate.MixedSemantics.raw761step1 line 2751
809. def OAI.MUB6.Certificate.MixedSemantics.raw761step1Labels line 2752
810. def OAI.MUB6.Certificate.MixedSemantics.raw761step2 line 2754
811. def OAI.MUB6.Certificate.MixedSemantics.raw761step2Labels line 2755
812. theorem OAI.MUB6.Certificate.MixedSemantics.canonical761 line 2757
813. def OAI.MUB6.Certificate.MixedSemantics.raw762 line 2777
814. def OAI.MUB6.Certificate.MixedSemantics.raw762Labels line 2778
815. def OAI.MUB6.Certificate.MixedSemantics.raw762step0 line 2780
816. def OAI.MUB6.Certificate.MixedSemantics.raw762step0Labels line 2781
817. def OAI.MUB6.Certificate.MixedSemantics.raw762step1 line 2783
818. def OAI.MUB6.Certificate.MixedSemantics.raw762step1Labels line 2784
819. theorem OAI.MUB6.Certificate.MixedSemantics.canonical762 line 2786
820. def OAI.MUB6.Certificate.MixedSemantics.raw763 line 2801
821. def OAI.MUB6.Certificate.MixedSemantics.raw763Labels line 2802
822. def OAI.MUB6.Certificate.MixedSemantics.raw763step0 line 2804
823. def OAI.MUB6.Certificate.MixedSemantics.raw763step0Labels line 2805
824. theorem OAI.MUB6.Certificate.MixedSemantics.canonical763 line 2807
825. def OAI.MUB6.Certificate.MixedSemantics.raw764 line 2817
826. def OAI.MUB6.Certificate.MixedSemantics.raw764Labels line 2818
827. def OAI.MUB6.Certificate.MixedSemantics.raw764step0 line 2820
828. def OAI.MUB6.Certificate.MixedSemantics.raw764step0Labels line 2821
829. def OAI.MUB6.Certificate.MixedSemantics.raw764step1 line 2823
830. def OAI.MUB6.Certificate.MixedSemantics.raw764step1Labels line 2824
831. def OAI.MUB6.Certificate.MixedSemantics.raw764step2 line 2826
832. def OAI.MUB6.Certificate.MixedSemantics.raw764step2Labels line 2827
833. theorem OAI.MUB6.Certificate.MixedSemantics.canonical764 line 2829
834. def OAI.MUB6.Certificate.MixedSemantics.raw765 line 2849
835. def OAI.MUB6.Certificate.MixedSemantics.raw765Labels line 2850
836. def OAI.MUB6.Certificate.MixedSemantics.raw765step0 line 2852
837. def OAI.MUB6.Certificate.MixedSemantics.raw765step0Labels line 2853
838. def OAI.MUB6.Certificate.MixedSemantics.raw765step1 line 2855
839. def OAI.MUB6.Certificate.MixedSemantics.raw765step1Labels line 2856
840. theorem OAI.MUB6.Certificate.MixedSemantics.canonical765 line 2858
841. def OAI.MUB6.Certificate.MixedSemantics.raw766 line 2873
842. def OAI.MUB6.Certificate.MixedSemantics.raw766Labels line 2874
843. def OAI.MUB6.Certificate.MixedSemantics.raw766step0 line 2876
844. def OAI.MUB6.Certificate.MixedSemantics.raw766step0Labels line 2877
845. theorem OAI.MUB6.Certificate.MixedSemantics.canonical766 line 2879
846. def OAI.MUB6.Certificate.MixedSemantics.raw767 line 2889
847. def OAI.MUB6.Certificate.MixedSemantics.raw767Labels line 2890
848. def OAI.MUB6.Certificate.MixedSemantics.raw767step0 line 2892
849. def OAI.MUB6.Certificate.MixedSemantics.raw767step0Labels line 2893
850. def OAI.MUB6.Certificate.MixedSemantics.raw767step1 line 2895
851. def OAI.MUB6.Certificate.MixedSemantics.raw767step1Labels line 2896
852. theorem OAI.MUB6.Certificate.MixedSemantics.canonical767 line 2898