OAI/Analysis/MutuallyUnbiased/MixedSemantics/Canonical23.lean

GitHub source file

1096 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.raw2944 line 18
2. def OAI.MUB6.Certificate.MixedSemantics.raw2944Labels line 19
3. def OAI.MUB6.Certificate.MixedSemantics.raw2944step0 line 21
4. def OAI.MUB6.Certificate.MixedSemantics.raw2944step0Labels line 22
5. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2944 line 24
6. def OAI.MUB6.Certificate.MixedSemantics.raw2945 line 34
7. def OAI.MUB6.Certificate.MixedSemantics.raw2945Labels line 35
8. def OAI.MUB6.Certificate.MixedSemantics.raw2945step0 line 37
9. def OAI.MUB6.Certificate.MixedSemantics.raw2945step0Labels line 38
10. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2945 line 40
11. def OAI.MUB6.Certificate.MixedSemantics.raw2946 line 50
12. def OAI.MUB6.Certificate.MixedSemantics.raw2946Labels line 51
13. def OAI.MUB6.Certificate.MixedSemantics.raw2946step0 line 53
14. def OAI.MUB6.Certificate.MixedSemantics.raw2946step0Labels line 54
15. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2946 line 56
16. def OAI.MUB6.Certificate.MixedSemantics.raw2947 line 66
17. def OAI.MUB6.Certificate.MixedSemantics.raw2947Labels line 67
18. def OAI.MUB6.Certificate.MixedSemantics.raw2947step0 line 69
19. def OAI.MUB6.Certificate.MixedSemantics.raw2947step0Labels line 70
20. def OAI.MUB6.Certificate.MixedSemantics.raw2947step1 line 72
21. def OAI.MUB6.Certificate.MixedSemantics.raw2947step1Labels line 73
22. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2947 line 75
23. def OAI.MUB6.Certificate.MixedSemantics.raw2948 line 91
24. def OAI.MUB6.Certificate.MixedSemantics.raw2948Labels line 92
25. def OAI.MUB6.Certificate.MixedSemantics.raw2948step0 line 94
26. def OAI.MUB6.Certificate.MixedSemantics.raw2948step0Labels line 95
27. def OAI.MUB6.Certificate.MixedSemantics.raw2948step1 line 97
28. def OAI.MUB6.Certificate.MixedSemantics.raw2948step1Labels line 98
29. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2948 line 100
30. def OAI.MUB6.Certificate.MixedSemantics.raw2949 line 116
31. def OAI.MUB6.Certificate.MixedSemantics.raw2949Labels line 117
32. def OAI.MUB6.Certificate.MixedSemantics.raw2949step0 line 119
33. def OAI.MUB6.Certificate.MixedSemantics.raw2949step0Labels line 120
34. def OAI.MUB6.Certificate.MixedSemantics.raw2949step1 line 122
35. def OAI.MUB6.Certificate.MixedSemantics.raw2949step1Labels line 123
36. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2949 line 125
37. def OAI.MUB6.Certificate.MixedSemantics.raw2950 line 141
38. def OAI.MUB6.Certificate.MixedSemantics.raw2950Labels line 142
39. def OAI.MUB6.Certificate.MixedSemantics.raw2950step0 line 144
40. def OAI.MUB6.Certificate.MixedSemantics.raw2950step0Labels line 145
41. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2950 line 147
42. def OAI.MUB6.Certificate.MixedSemantics.raw2951 line 157
43. def OAI.MUB6.Certificate.MixedSemantics.raw2951Labels line 158
44. def OAI.MUB6.Certificate.MixedSemantics.raw2951step0 line 160
45. def OAI.MUB6.Certificate.MixedSemantics.raw2951step0Labels line 161
46. def OAI.MUB6.Certificate.MixedSemantics.raw2951step1 line 163
47. def OAI.MUB6.Certificate.MixedSemantics.raw2951step1Labels line 164
48. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2951 line 166
49. def OAI.MUB6.Certificate.MixedSemantics.raw2952 line 182
50. def OAI.MUB6.Certificate.MixedSemantics.raw2952Labels line 183
51. def OAI.MUB6.Certificate.MixedSemantics.raw2952step0 line 185
52. def OAI.MUB6.Certificate.MixedSemantics.raw2952step0Labels line 186
53. def OAI.MUB6.Certificate.MixedSemantics.raw2952step1 line 188
54. def OAI.MUB6.Certificate.MixedSemantics.raw2952step1Labels line 189
55. def OAI.MUB6.Certificate.MixedSemantics.raw2952step2 line 191
56. def OAI.MUB6.Certificate.MixedSemantics.raw2952step2Labels line 192
57. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2952 line 194
58. def OAI.MUB6.Certificate.MixedSemantics.raw2953 line 216
59. def OAI.MUB6.Certificate.MixedSemantics.raw2953Labels line 217
60. def OAI.MUB6.Certificate.MixedSemantics.raw2953step0 line 219
61. def OAI.MUB6.Certificate.MixedSemantics.raw2953step0Labels line 220
62. def OAI.MUB6.Certificate.MixedSemantics.raw2953step1 line 222
63. def OAI.MUB6.Certificate.MixedSemantics.raw2953step1Labels line 223
64. def OAI.MUB6.Certificate.MixedSemantics.raw2953step2 line 225
65. def OAI.MUB6.Certificate.MixedSemantics.raw2953step2Labels line 226
66. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2953 line 228
67. def OAI.MUB6.Certificate.MixedSemantics.raw2954 line 250
68. def OAI.MUB6.Certificate.MixedSemantics.raw2954Labels line 251
69. def OAI.MUB6.Certificate.MixedSemantics.raw2954step0 line 253
70. def OAI.MUB6.Certificate.MixedSemantics.raw2954step0Labels line 254
71. def OAI.MUB6.Certificate.MixedSemantics.raw2954step1 line 256
72. def OAI.MUB6.Certificate.MixedSemantics.raw2954step1Labels line 257
73. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2954 line 259
74. def OAI.MUB6.Certificate.MixedSemantics.raw2955 line 275
75. def OAI.MUB6.Certificate.MixedSemantics.raw2955Labels line 276
76. def OAI.MUB6.Certificate.MixedSemantics.raw2955step0 line 278
77. def OAI.MUB6.Certificate.MixedSemantics.raw2955step0Labels line 279
78. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2955 line 281
79. def OAI.MUB6.Certificate.MixedSemantics.raw2956 line 291
80. def OAI.MUB6.Certificate.MixedSemantics.raw2956Labels line 292
81. def OAI.MUB6.Certificate.MixedSemantics.raw2956step0 line 294
82. def OAI.MUB6.Certificate.MixedSemantics.raw2956step0Labels line 295
83. def OAI.MUB6.Certificate.MixedSemantics.raw2956step1 line 297
84. def OAI.MUB6.Certificate.MixedSemantics.raw2956step1Labels line 298
85. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2956 line 300
86. def OAI.MUB6.Certificate.MixedSemantics.raw2957 line 316
87. def OAI.MUB6.Certificate.MixedSemantics.raw2957Labels line 317
88. def OAI.MUB6.Certificate.MixedSemantics.raw2957step0 line 319
89. def OAI.MUB6.Certificate.MixedSemantics.raw2957step0Labels line 320
90. def OAI.MUB6.Certificate.MixedSemantics.raw2957step1 line 322
91. def OAI.MUB6.Certificate.MixedSemantics.raw2957step1Labels line 323
92. def OAI.MUB6.Certificate.MixedSemantics.raw2957step2 line 325
93. def OAI.MUB6.Certificate.MixedSemantics.raw2957step2Labels line 326
94. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2957 line 328
95. def OAI.MUB6.Certificate.MixedSemantics.raw2958 line 350
96. def OAI.MUB6.Certificate.MixedSemantics.raw2958Labels line 351
97. def OAI.MUB6.Certificate.MixedSemantics.raw2958step0 line 353
98. def OAI.MUB6.Certificate.MixedSemantics.raw2958step0Labels line 354
99. def OAI.MUB6.Certificate.MixedSemantics.raw2958step1 line 356
100. def OAI.MUB6.Certificate.MixedSemantics.raw2958step1Labels line 357
101. def OAI.MUB6.Certificate.MixedSemantics.raw2958step2 line 359
102. def OAI.MUB6.Certificate.MixedSemantics.raw2958step2Labels line 360
103. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2958 line 362
104. def OAI.MUB6.Certificate.MixedSemantics.raw2959 line 384
105. def OAI.MUB6.Certificate.MixedSemantics.raw2959Labels line 385
106. def OAI.MUB6.Certificate.MixedSemantics.raw2959step0 line 387
107. def OAI.MUB6.Certificate.MixedSemantics.raw2959step0Labels line 388
108. def OAI.MUB6.Certificate.MixedSemantics.raw2959step1 line 390
109. def OAI.MUB6.Certificate.MixedSemantics.raw2959step1Labels line 391
110. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2959 line 393
111. def OAI.MUB6.Certificate.MixedSemantics.raw2960 line 409
112. def OAI.MUB6.Certificate.MixedSemantics.raw2960Labels line 410
113. def OAI.MUB6.Certificate.MixedSemantics.raw2960step0 line 412
114. def OAI.MUB6.Certificate.MixedSemantics.raw2960step0Labels line 413
115. def OAI.MUB6.Certificate.MixedSemantics.raw2960step1 line 415
116. def OAI.MUB6.Certificate.MixedSemantics.raw2960step1Labels line 416
117. def OAI.MUB6.Certificate.MixedSemantics.raw2960step2 line 418
118. def OAI.MUB6.Certificate.MixedSemantics.raw2960step2Labels line 419
119. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2960 line 421
120. def OAI.MUB6.Certificate.MixedSemantics.raw2961 line 441
121. def OAI.MUB6.Certificate.MixedSemantics.raw2961Labels line 442
122. def OAI.MUB6.Certificate.MixedSemantics.raw2961step0 line 444
123. def OAI.MUB6.Certificate.MixedSemantics.raw2961step0Labels line 445
124. def OAI.MUB6.Certificate.MixedSemantics.raw2961step1 line 447
125. def OAI.MUB6.Certificate.MixedSemantics.raw2961step1Labels line 448
126. def OAI.MUB6.Certificate.MixedSemantics.raw2961step2 line 450
127. def OAI.MUB6.Certificate.MixedSemantics.raw2961step2Labels line 451
128. def OAI.MUB6.Certificate.MixedSemantics.raw2961step3 line 453
129. def OAI.MUB6.Certificate.MixedSemantics.raw2961step3Labels line 454
130. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2961 line 456
131. def OAI.MUB6.Certificate.MixedSemantics.raw2962 line 482
132. def OAI.MUB6.Certificate.MixedSemantics.raw2962Labels line 483
133. def OAI.MUB6.Certificate.MixedSemantics.raw2962step0 line 485
134. def OAI.MUB6.Certificate.MixedSemantics.raw2962step0Labels line 486
135. def OAI.MUB6.Certificate.MixedSemantics.raw2962step1 line 488
136. def OAI.MUB6.Certificate.MixedSemantics.raw2962step1Labels line 489
137. def OAI.MUB6.Certificate.MixedSemantics.raw2962step2 line 491
138. def OAI.MUB6.Certificate.MixedSemantics.raw2962step2Labels line 492
139. def OAI.MUB6.Certificate.MixedSemantics.raw2962step3 line 494
140. def OAI.MUB6.Certificate.MixedSemantics.raw2962step3Labels line 495
141. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2962 line 497
142. def OAI.MUB6.Certificate.MixedSemantics.raw2963 line 523
143. def OAI.MUB6.Certificate.MixedSemantics.raw2963Labels line 524
144. def OAI.MUB6.Certificate.MixedSemantics.raw2963step0 line 526
145. def OAI.MUB6.Certificate.MixedSemantics.raw2963step0Labels line 527
146. def OAI.MUB6.Certificate.MixedSemantics.raw2963step1 line 529
147. def OAI.MUB6.Certificate.MixedSemantics.raw2963step1Labels line 530
148. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2963 line 532
149. def OAI.MUB6.Certificate.MixedSemantics.raw2964 line 549
150. def OAI.MUB6.Certificate.MixedSemantics.raw2964Labels line 550
151. def OAI.MUB6.Certificate.MixedSemantics.raw2964step0 line 552
152. def OAI.MUB6.Certificate.MixedSemantics.raw2964step0Labels line 553
153. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2964 line 555
154. def OAI.MUB6.Certificate.MixedSemantics.raw2965 line 566
155. def OAI.MUB6.Certificate.MixedSemantics.raw2965Labels line 567
156. def OAI.MUB6.Certificate.MixedSemantics.raw2965step0 line 569
157. def OAI.MUB6.Certificate.MixedSemantics.raw2965step0Labels line 570
158. def OAI.MUB6.Certificate.MixedSemantics.raw2965step1 line 572
159. def OAI.MUB6.Certificate.MixedSemantics.raw2965step1Labels line 573
160. def OAI.MUB6.Certificate.MixedSemantics.raw2965step2 line 575
161. def OAI.MUB6.Certificate.MixedSemantics.raw2965step2Labels line 576
162. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2965 line 578
163. def OAI.MUB6.Certificate.MixedSemantics.raw2966 line 598
164. def OAI.MUB6.Certificate.MixedSemantics.raw2966Labels line 599
165. def OAI.MUB6.Certificate.MixedSemantics.raw2966step0 line 601
166. def OAI.MUB6.Certificate.MixedSemantics.raw2966step0Labels line 602
167. def OAI.MUB6.Certificate.MixedSemantics.raw2966step1 line 604
168. def OAI.MUB6.Certificate.MixedSemantics.raw2966step1Labels line 605
169. def OAI.MUB6.Certificate.MixedSemantics.raw2966step2 line 607
170. def OAI.MUB6.Certificate.MixedSemantics.raw2966step2Labels line 608
171. def OAI.MUB6.Certificate.MixedSemantics.raw2966step3 line 610
172. def OAI.MUB6.Certificate.MixedSemantics.raw2966step3Labels line 611
173. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2966 line 613
174. def OAI.MUB6.Certificate.MixedSemantics.raw2967 line 639
175. def OAI.MUB6.Certificate.MixedSemantics.raw2967Labels line 640
176. def OAI.MUB6.Certificate.MixedSemantics.raw2967step0 line 642
177. def OAI.MUB6.Certificate.MixedSemantics.raw2967step0Labels line 643
178. def OAI.MUB6.Certificate.MixedSemantics.raw2967step1 line 645
179. def OAI.MUB6.Certificate.MixedSemantics.raw2967step1Labels line 646
180. def OAI.MUB6.Certificate.MixedSemantics.raw2967step2 line 648
181. def OAI.MUB6.Certificate.MixedSemantics.raw2967step2Labels line 649
182. def OAI.MUB6.Certificate.MixedSemantics.raw2967step3 line 651
183. def OAI.MUB6.Certificate.MixedSemantics.raw2967step3Labels line 652
184. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2967 line 654
185. def OAI.MUB6.Certificate.MixedSemantics.raw2968 line 680
186. def OAI.MUB6.Certificate.MixedSemantics.raw2968Labels line 681
187. def OAI.MUB6.Certificate.MixedSemantics.raw2968step0 line 683
188. def OAI.MUB6.Certificate.MixedSemantics.raw2968step0Labels line 684
189. def OAI.MUB6.Certificate.MixedSemantics.raw2968step1 line 686
190. def OAI.MUB6.Certificate.MixedSemantics.raw2968step1Labels line 687
191. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2968 line 689
192. def OAI.MUB6.Certificate.MixedSemantics.raw2969 line 706
193. def OAI.MUB6.Certificate.MixedSemantics.raw2969Labels line 707
194. def OAI.MUB6.Certificate.MixedSemantics.raw2969step0 line 709
195. def OAI.MUB6.Certificate.MixedSemantics.raw2969step0Labels line 710
196. def OAI.MUB6.Certificate.MixedSemantics.raw2969step1 line 712
197. def OAI.MUB6.Certificate.MixedSemantics.raw2969step1Labels line 713
198. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2969 line 715
199. def OAI.MUB6.Certificate.MixedSemantics.raw2970 line 730
200. def OAI.MUB6.Certificate.MixedSemantics.raw2970Labels line 731
201. def OAI.MUB6.Certificate.MixedSemantics.raw2970step0 line 733
202. def OAI.MUB6.Certificate.MixedSemantics.raw2970step0Labels line 734
203. def OAI.MUB6.Certificate.MixedSemantics.raw2970step1 line 736
204. def OAI.MUB6.Certificate.MixedSemantics.raw2970step1Labels line 737
205. def OAI.MUB6.Certificate.MixedSemantics.raw2970step2 line 739
206. def OAI.MUB6.Certificate.MixedSemantics.raw2970step2Labels line 740
207. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2970 line 742
208. def OAI.MUB6.Certificate.MixedSemantics.raw2971 line 763
209. def OAI.MUB6.Certificate.MixedSemantics.raw2971Labels line 764
210. def OAI.MUB6.Certificate.MixedSemantics.raw2971step0 line 766
211. def OAI.MUB6.Certificate.MixedSemantics.raw2971step0Labels line 767
212. def OAI.MUB6.Certificate.MixedSemantics.raw2971step1 line 769
213. def OAI.MUB6.Certificate.MixedSemantics.raw2971step1Labels line 770
214. def OAI.MUB6.Certificate.MixedSemantics.raw2971step2 line 772
215. def OAI.MUB6.Certificate.MixedSemantics.raw2971step2Labels line 773
216. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2971 line 775
217. def OAI.MUB6.Certificate.MixedSemantics.raw2972 line 796
218. def OAI.MUB6.Certificate.MixedSemantics.raw2972Labels line 797
219. def OAI.MUB6.Certificate.MixedSemantics.raw2972step0 line 799
220. def OAI.MUB6.Certificate.MixedSemantics.raw2972step0Labels line 800
221. def OAI.MUB6.Certificate.MixedSemantics.raw2972step1 line 802
222. def OAI.MUB6.Certificate.MixedSemantics.raw2972step1Labels line 803
223. def OAI.MUB6.Certificate.MixedSemantics.raw2972step2 line 805
224. def OAI.MUB6.Certificate.MixedSemantics.raw2972step2Labels line 806
225. def OAI.MUB6.Certificate.MixedSemantics.raw2972step3 line 808
226. def OAI.MUB6.Certificate.MixedSemantics.raw2972step3Labels line 809
227. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2972 line 811
228. def OAI.MUB6.Certificate.MixedSemantics.raw2973 line 838
229. def OAI.MUB6.Certificate.MixedSemantics.raw2973Labels line 839
230. def OAI.MUB6.Certificate.MixedSemantics.raw2973step0 line 841
231. def OAI.MUB6.Certificate.MixedSemantics.raw2973step0Labels line 842
232. def OAI.MUB6.Certificate.MixedSemantics.raw2973step1 line 844
233. def OAI.MUB6.Certificate.MixedSemantics.raw2973step1Labels line 845
234. def OAI.MUB6.Certificate.MixedSemantics.raw2973step2 line 847
235. def OAI.MUB6.Certificate.MixedSemantics.raw2973step2Labels line 848
236. def OAI.MUB6.Certificate.MixedSemantics.raw2973step3 line 850
237. def OAI.MUB6.Certificate.MixedSemantics.raw2973step3Labels line 851
238. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2973 line 853
239. def OAI.MUB6.Certificate.MixedSemantics.raw2974 line 880
240. def OAI.MUB6.Certificate.MixedSemantics.raw2974Labels line 881
241. def OAI.MUB6.Certificate.MixedSemantics.raw2974step0 line 883
242. def OAI.MUB6.Certificate.MixedSemantics.raw2974step0Labels line 884
243. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2974 line 886
244. def OAI.MUB6.Certificate.MixedSemantics.raw2975 line 896
245. def OAI.MUB6.Certificate.MixedSemantics.raw2975Labels line 897
246. def OAI.MUB6.Certificate.MixedSemantics.raw2975step0 line 899
247. def OAI.MUB6.Certificate.MixedSemantics.raw2975step0Labels line 900
248. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2975 line 902
249. def OAI.MUB6.Certificate.MixedSemantics.raw2976 line 912
250. def OAI.MUB6.Certificate.MixedSemantics.raw2976Labels line 913
251. def OAI.MUB6.Certificate.MixedSemantics.raw2976step0 line 915
252. def OAI.MUB6.Certificate.MixedSemantics.raw2976step0Labels line 916
253. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2976 line 918
254. def OAI.MUB6.Certificate.MixedSemantics.raw2977 line 928
255. def OAI.MUB6.Certificate.MixedSemantics.raw2977Labels line 929
256. def OAI.MUB6.Certificate.MixedSemantics.raw2977step0 line 931
257. def OAI.MUB6.Certificate.MixedSemantics.raw2977step0Labels line 932
258. def OAI.MUB6.Certificate.MixedSemantics.raw2977step1 line 934
259. def OAI.MUB6.Certificate.MixedSemantics.raw2977step1Labels line 935
260. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2977 line 937
261. def OAI.MUB6.Certificate.MixedSemantics.raw2978 line 953
262. def OAI.MUB6.Certificate.MixedSemantics.raw2978Labels line 954
263. def OAI.MUB6.Certificate.MixedSemantics.raw2978step0 line 956
264. def OAI.MUB6.Certificate.MixedSemantics.raw2978step0Labels line 957
265. def OAI.MUB6.Certificate.MixedSemantics.raw2978step1 line 959
266. def OAI.MUB6.Certificate.MixedSemantics.raw2978step1Labels line 960
267. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2978 line 962
268. def OAI.MUB6.Certificate.MixedSemantics.raw2979 line 978
269. def OAI.MUB6.Certificate.MixedSemantics.raw2979Labels line 979
270. def OAI.MUB6.Certificate.MixedSemantics.raw2979step0 line 981
271. def OAI.MUB6.Certificate.MixedSemantics.raw2979step0Labels line 982
272. def OAI.MUB6.Certificate.MixedSemantics.raw2979step1 line 984
273. def OAI.MUB6.Certificate.MixedSemantics.raw2979step1Labels line 985
274. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2979 line 987
275. def OAI.MUB6.Certificate.MixedSemantics.raw2980 line 1003
276. def OAI.MUB6.Certificate.MixedSemantics.raw2980Labels line 1004
277. def OAI.MUB6.Certificate.MixedSemantics.raw2980step0 line 1006
278. def OAI.MUB6.Certificate.MixedSemantics.raw2980step0Labels line 1007
279. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2980 line 1009
280. def OAI.MUB6.Certificate.MixedSemantics.raw2981 line 1019
281. def OAI.MUB6.Certificate.MixedSemantics.raw2981Labels line 1020
282. def OAI.MUB6.Certificate.MixedSemantics.raw2981step0 line 1022
283. def OAI.MUB6.Certificate.MixedSemantics.raw2981step0Labels line 1023
284. def OAI.MUB6.Certificate.MixedSemantics.raw2981step1 line 1025
285. def OAI.MUB6.Certificate.MixedSemantics.raw2981step1Labels line 1026
286. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2981 line 1028
287. def OAI.MUB6.Certificate.MixedSemantics.raw2982 line 1044
288. def OAI.MUB6.Certificate.MixedSemantics.raw2982Labels line 1045
289. def OAI.MUB6.Certificate.MixedSemantics.raw2982step0 line 1047
290. def OAI.MUB6.Certificate.MixedSemantics.raw2982step0Labels line 1048
291. def OAI.MUB6.Certificate.MixedSemantics.raw2982step1 line 1050
292. def OAI.MUB6.Certificate.MixedSemantics.raw2982step1Labels line 1051
293. def OAI.MUB6.Certificate.MixedSemantics.raw2982step2 line 1053
294. def OAI.MUB6.Certificate.MixedSemantics.raw2982step2Labels line 1054
295. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2982 line 1056
296. def OAI.MUB6.Certificate.MixedSemantics.raw2983 line 1078
297. def OAI.MUB6.Certificate.MixedSemantics.raw2983Labels line 1079
298. def OAI.MUB6.Certificate.MixedSemantics.raw2983step0 line 1081
299. def OAI.MUB6.Certificate.MixedSemantics.raw2983step0Labels line 1082
300. def OAI.MUB6.Certificate.MixedSemantics.raw2983step1 line 1084
301. def OAI.MUB6.Certificate.MixedSemantics.raw2983step1Labels line 1085
302. def OAI.MUB6.Certificate.MixedSemantics.raw2983step2 line 1087
303. def OAI.MUB6.Certificate.MixedSemantics.raw2983step2Labels line 1088
304. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2983 line 1090
305. def OAI.MUB6.Certificate.MixedSemantics.raw2984 line 1112
306. def OAI.MUB6.Certificate.MixedSemantics.raw2984Labels line 1113
307. def OAI.MUB6.Certificate.MixedSemantics.raw2984step0 line 1115
308. def OAI.MUB6.Certificate.MixedSemantics.raw2984step0Labels line 1116
309. def OAI.MUB6.Certificate.MixedSemantics.raw2984step1 line 1118
310. def OAI.MUB6.Certificate.MixedSemantics.raw2984step1Labels line 1119
311. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2984 line 1121
312. def OAI.MUB6.Certificate.MixedSemantics.raw2985 line 1137
313. def OAI.MUB6.Certificate.MixedSemantics.raw2985Labels line 1138
314. def OAI.MUB6.Certificate.MixedSemantics.raw2985step0 line 1140
315. def OAI.MUB6.Certificate.MixedSemantics.raw2985step0Labels line 1141
316. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2985 line 1143
317. def OAI.MUB6.Certificate.MixedSemantics.raw2986 line 1153
318. def OAI.MUB6.Certificate.MixedSemantics.raw2986Labels line 1154
319. def OAI.MUB6.Certificate.MixedSemantics.raw2986step0 line 1156
320. def OAI.MUB6.Certificate.MixedSemantics.raw2986step0Labels line 1157
321. def OAI.MUB6.Certificate.MixedSemantics.raw2986step1 line 1159
322. def OAI.MUB6.Certificate.MixedSemantics.raw2986step1Labels line 1160
323. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2986 line 1162
324. def OAI.MUB6.Certificate.MixedSemantics.raw2987 line 1178
325. def OAI.MUB6.Certificate.MixedSemantics.raw2987Labels line 1179
326. def OAI.MUB6.Certificate.MixedSemantics.raw2987step0 line 1181
327. def OAI.MUB6.Certificate.MixedSemantics.raw2987step0Labels line 1182
328. def OAI.MUB6.Certificate.MixedSemantics.raw2987step1 line 1184
329. def OAI.MUB6.Certificate.MixedSemantics.raw2987step1Labels line 1185
330. def OAI.MUB6.Certificate.MixedSemantics.raw2987step2 line 1187
331. def OAI.MUB6.Certificate.MixedSemantics.raw2987step2Labels line 1188
332. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2987 line 1190
333. def OAI.MUB6.Certificate.MixedSemantics.raw2988 line 1212
334. def OAI.MUB6.Certificate.MixedSemantics.raw2988Labels line 1213
335. def OAI.MUB6.Certificate.MixedSemantics.raw2988step0 line 1215
336. def OAI.MUB6.Certificate.MixedSemantics.raw2988step0Labels line 1216
337. def OAI.MUB6.Certificate.MixedSemantics.raw2988step1 line 1218
338. def OAI.MUB6.Certificate.MixedSemantics.raw2988step1Labels line 1219
339. def OAI.MUB6.Certificate.MixedSemantics.raw2988step2 line 1221
340. def OAI.MUB6.Certificate.MixedSemantics.raw2988step2Labels line 1222
341. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2988 line 1224
342. def OAI.MUB6.Certificate.MixedSemantics.raw2989 line 1246
343. def OAI.MUB6.Certificate.MixedSemantics.raw2989Labels line 1247
344. def OAI.MUB6.Certificate.MixedSemantics.raw2989step0 line 1249
345. def OAI.MUB6.Certificate.MixedSemantics.raw2989step0Labels line 1250
346. def OAI.MUB6.Certificate.MixedSemantics.raw2989step1 line 1252
347. def OAI.MUB6.Certificate.MixedSemantics.raw2989step1Labels line 1253
348. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2989 line 1255
349. def OAI.MUB6.Certificate.MixedSemantics.raw2990 line 1271
350. def OAI.MUB6.Certificate.MixedSemantics.raw2990Labels line 1272
351. def OAI.MUB6.Certificate.MixedSemantics.raw2990step0 line 1274
352. def OAI.MUB6.Certificate.MixedSemantics.raw2990step0Labels line 1275
353. def OAI.MUB6.Certificate.MixedSemantics.raw2990step1 line 1277
354. def OAI.MUB6.Certificate.MixedSemantics.raw2990step1Labels line 1278
355. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2990 line 1280
356. def OAI.MUB6.Certificate.MixedSemantics.raw2991 line 1295
357. def OAI.MUB6.Certificate.MixedSemantics.raw2991Labels line 1296
358. def OAI.MUB6.Certificate.MixedSemantics.raw2991step0 line 1298
359. def OAI.MUB6.Certificate.MixedSemantics.raw2991step0Labels line 1299
360. def OAI.MUB6.Certificate.MixedSemantics.raw2991step1 line 1301
361. def OAI.MUB6.Certificate.MixedSemantics.raw2991step1Labels line 1302
362. def OAI.MUB6.Certificate.MixedSemantics.raw2991step2 line 1304
363. def OAI.MUB6.Certificate.MixedSemantics.raw2991step2Labels line 1305
364. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2991 line 1307
365. def OAI.MUB6.Certificate.MixedSemantics.raw2992 line 1328
366. def OAI.MUB6.Certificate.MixedSemantics.raw2992Labels line 1329
367. def OAI.MUB6.Certificate.MixedSemantics.raw2992step0 line 1331
368. def OAI.MUB6.Certificate.MixedSemantics.raw2992step0Labels line 1332
369. def OAI.MUB6.Certificate.MixedSemantics.raw2992step1 line 1334
370. def OAI.MUB6.Certificate.MixedSemantics.raw2992step1Labels line 1335
371. def OAI.MUB6.Certificate.MixedSemantics.raw2992step2 line 1337
372. def OAI.MUB6.Certificate.MixedSemantics.raw2992step2Labels line 1338
373. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2992 line 1340
374. def OAI.MUB6.Certificate.MixedSemantics.raw2993 line 1361
375. def OAI.MUB6.Certificate.MixedSemantics.raw2993Labels line 1362
376. def OAI.MUB6.Certificate.MixedSemantics.raw2993step0 line 1364
377. def OAI.MUB6.Certificate.MixedSemantics.raw2993step0Labels line 1365
378. def OAI.MUB6.Certificate.MixedSemantics.raw2993step1 line 1367
379. def OAI.MUB6.Certificate.MixedSemantics.raw2993step1Labels line 1368
380. def OAI.MUB6.Certificate.MixedSemantics.raw2993step2 line 1370
381. def OAI.MUB6.Certificate.MixedSemantics.raw2993step2Labels line 1371
382. def OAI.MUB6.Certificate.MixedSemantics.raw2993step3 line 1373
383. def OAI.MUB6.Certificate.MixedSemantics.raw2993step3Labels line 1374
384. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2993 line 1376
385. def OAI.MUB6.Certificate.MixedSemantics.raw2994 line 1403
386. def OAI.MUB6.Certificate.MixedSemantics.raw2994Labels line 1404
387. def OAI.MUB6.Certificate.MixedSemantics.raw2994step0 line 1406
388. def OAI.MUB6.Certificate.MixedSemantics.raw2994step0Labels line 1407
389. def OAI.MUB6.Certificate.MixedSemantics.raw2994step1 line 1409
390. def OAI.MUB6.Certificate.MixedSemantics.raw2994step1Labels line 1410
391. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2994 line 1412
392. def OAI.MUB6.Certificate.MixedSemantics.raw2995 line 1428
393. def OAI.MUB6.Certificate.MixedSemantics.raw2995Labels line 1429
394. def OAI.MUB6.Certificate.MixedSemantics.raw2995step0 line 1431
395. def OAI.MUB6.Certificate.MixedSemantics.raw2995step0Labels line 1432
396. def OAI.MUB6.Certificate.MixedSemantics.raw2995step1 line 1434
397. def OAI.MUB6.Certificate.MixedSemantics.raw2995step1Labels line 1435
398. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2995 line 1437
399. def OAI.MUB6.Certificate.MixedSemantics.raw2996 line 1452
400. def OAI.MUB6.Certificate.MixedSemantics.raw2996Labels line 1453
401. def OAI.MUB6.Certificate.MixedSemantics.raw2996step0 line 1455
402. def OAI.MUB6.Certificate.MixedSemantics.raw2996step0Labels line 1456
403. def OAI.MUB6.Certificate.MixedSemantics.raw2996step1 line 1458
404. def OAI.MUB6.Certificate.MixedSemantics.raw2996step1Labels line 1459
405. def OAI.MUB6.Certificate.MixedSemantics.raw2996step2 line 1461
406. def OAI.MUB6.Certificate.MixedSemantics.raw2996step2Labels line 1462
407. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2996 line 1464
408. def OAI.MUB6.Certificate.MixedSemantics.raw2997 line 1485
409. def OAI.MUB6.Certificate.MixedSemantics.raw2997Labels line 1486
410. def OAI.MUB6.Certificate.MixedSemantics.raw2997step0 line 1488
411. def OAI.MUB6.Certificate.MixedSemantics.raw2997step0Labels line 1489
412. def OAI.MUB6.Certificate.MixedSemantics.raw2997step1 line 1491
413. def OAI.MUB6.Certificate.MixedSemantics.raw2997step1Labels line 1492
414. def OAI.MUB6.Certificate.MixedSemantics.raw2997step2 line 1494
415. def OAI.MUB6.Certificate.MixedSemantics.raw2997step2Labels line 1495
416. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2997 line 1497
417. def OAI.MUB6.Certificate.MixedSemantics.raw2998 line 1518
418. def OAI.MUB6.Certificate.MixedSemantics.raw2998Labels line 1519
419. def OAI.MUB6.Certificate.MixedSemantics.raw2998step0 line 1521
420. def OAI.MUB6.Certificate.MixedSemantics.raw2998step0Labels line 1522
421. def OAI.MUB6.Certificate.MixedSemantics.raw2998step1 line 1524
422. def OAI.MUB6.Certificate.MixedSemantics.raw2998step1Labels line 1525
423. def OAI.MUB6.Certificate.MixedSemantics.raw2998step2 line 1527
424. def OAI.MUB6.Certificate.MixedSemantics.raw2998step2Labels line 1528
425. def OAI.MUB6.Certificate.MixedSemantics.raw2998step3 line 1530
426. def OAI.MUB6.Certificate.MixedSemantics.raw2998step3Labels line 1531
427. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2998 line 1533
428. def OAI.MUB6.Certificate.MixedSemantics.raw2999 line 1560
429. def OAI.MUB6.Certificate.MixedSemantics.raw2999Labels line 1561
430. def OAI.MUB6.Certificate.MixedSemantics.raw2999step0 line 1563
431. def OAI.MUB6.Certificate.MixedSemantics.raw2999step0Labels line 1564
432. def OAI.MUB6.Certificate.MixedSemantics.raw2999step1 line 1566
433. def OAI.MUB6.Certificate.MixedSemantics.raw2999step1Labels line 1567
434. theorem OAI.MUB6.Certificate.MixedSemantics.canonical2999 line 1569
435. def OAI.MUB6.Certificate.MixedSemantics.raw3000 line 1584
436. def OAI.MUB6.Certificate.MixedSemantics.raw3000Labels line 1585
437. def OAI.MUB6.Certificate.MixedSemantics.raw3000step0 line 1587
438. def OAI.MUB6.Certificate.MixedSemantics.raw3000step0Labels line 1588
439. def OAI.MUB6.Certificate.MixedSemantics.raw3000step1 line 1590
440. def OAI.MUB6.Certificate.MixedSemantics.raw3000step1Labels line 1591
441. def OAI.MUB6.Certificate.MixedSemantics.raw3000step2 line 1593
442. def OAI.MUB6.Certificate.MixedSemantics.raw3000step2Labels line 1594
443. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3000 line 1596
444. def OAI.MUB6.Certificate.MixedSemantics.raw3001 line 1617
445. def OAI.MUB6.Certificate.MixedSemantics.raw3001Labels line 1618
446. def OAI.MUB6.Certificate.MixedSemantics.raw3001step0 line 1620
447. def OAI.MUB6.Certificate.MixedSemantics.raw3001step0Labels line 1621
448. def OAI.MUB6.Certificate.MixedSemantics.raw3001step1 line 1623
449. def OAI.MUB6.Certificate.MixedSemantics.raw3001step1Labels line 1624
450. def OAI.MUB6.Certificate.MixedSemantics.raw3001step2 line 1626
451. def OAI.MUB6.Certificate.MixedSemantics.raw3001step2Labels line 1627
452. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3001 line 1629
453. def OAI.MUB6.Certificate.MixedSemantics.raw3002 line 1650
454. def OAI.MUB6.Certificate.MixedSemantics.raw3002Labels line 1651
455. def OAI.MUB6.Certificate.MixedSemantics.raw3002step0 line 1653
456. def OAI.MUB6.Certificate.MixedSemantics.raw3002step0Labels line 1654
457. def OAI.MUB6.Certificate.MixedSemantics.raw3002step1 line 1656
458. def OAI.MUB6.Certificate.MixedSemantics.raw3002step1Labels line 1657
459. def OAI.MUB6.Certificate.MixedSemantics.raw3002step2 line 1659
460. def OAI.MUB6.Certificate.MixedSemantics.raw3002step2Labels line 1660
461. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3002 line 1662
462. def OAI.MUB6.Certificate.MixedSemantics.raw3003 line 1683
463. def OAI.MUB6.Certificate.MixedSemantics.raw3003Labels line 1684
464. def OAI.MUB6.Certificate.MixedSemantics.raw3003step0 line 1686
465. def OAI.MUB6.Certificate.MixedSemantics.raw3003step0Labels line 1687
466. def OAI.MUB6.Certificate.MixedSemantics.raw3003step1 line 1689
467. def OAI.MUB6.Certificate.MixedSemantics.raw3003step1Labels line 1690
468. def OAI.MUB6.Certificate.MixedSemantics.raw3003step2 line 1692
469. def OAI.MUB6.Certificate.MixedSemantics.raw3003step2Labels line 1693
470. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3003 line 1695
471. def OAI.MUB6.Certificate.MixedSemantics.raw3004 line 1716
472. def OAI.MUB6.Certificate.MixedSemantics.raw3004Labels line 1717
473. def OAI.MUB6.Certificate.MixedSemantics.raw3004step0 line 1719
474. def OAI.MUB6.Certificate.MixedSemantics.raw3004step0Labels line 1720
475. def OAI.MUB6.Certificate.MixedSemantics.raw3004step1 line 1722
476. def OAI.MUB6.Certificate.MixedSemantics.raw3004step1Labels line 1723
477. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3004 line 1725
478. def OAI.MUB6.Certificate.MixedSemantics.raw3005 line 1740
479. def OAI.MUB6.Certificate.MixedSemantics.raw3005Labels line 1741
480. def OAI.MUB6.Certificate.MixedSemantics.raw3005step0 line 1743
481. def OAI.MUB6.Certificate.MixedSemantics.raw3005step0Labels line 1744
482. def OAI.MUB6.Certificate.MixedSemantics.raw3005step1 line 1746
483. def OAI.MUB6.Certificate.MixedSemantics.raw3005step1Labels line 1747
484. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3005 line 1749
485. def OAI.MUB6.Certificate.MixedSemantics.raw3006 line 1764
486. def OAI.MUB6.Certificate.MixedSemantics.raw3006Labels line 1765
487. def OAI.MUB6.Certificate.MixedSemantics.raw3006step0 line 1767
488. def OAI.MUB6.Certificate.MixedSemantics.raw3006step0Labels line 1768
489. def OAI.MUB6.Certificate.MixedSemantics.raw3006step1 line 1770
490. def OAI.MUB6.Certificate.MixedSemantics.raw3006step1Labels line 1771
491. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3006 line 1773
492. def OAI.MUB6.Certificate.MixedSemantics.raw3007 line 1788
493. def OAI.MUB6.Certificate.MixedSemantics.raw3007Labels line 1789
494. def OAI.MUB6.Certificate.MixedSemantics.raw3007step0 line 1791
495. def OAI.MUB6.Certificate.MixedSemantics.raw3007step0Labels line 1792
496. def OAI.MUB6.Certificate.MixedSemantics.raw3007step1 line 1794
497. def OAI.MUB6.Certificate.MixedSemantics.raw3007step1Labels line 1795
498. def OAI.MUB6.Certificate.MixedSemantics.raw3007step2 line 1797
499. def OAI.MUB6.Certificate.MixedSemantics.raw3007step2Labels line 1798
500. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3007 line 1800
501. def OAI.MUB6.Certificate.MixedSemantics.raw3008 line 1820
502. def OAI.MUB6.Certificate.MixedSemantics.raw3008Labels line 1821
503. def OAI.MUB6.Certificate.MixedSemantics.raw3008step0 line 1823
504. def OAI.MUB6.Certificate.MixedSemantics.raw3008step0Labels line 1824
505. def OAI.MUB6.Certificate.MixedSemantics.raw3008step1 line 1826
506. def OAI.MUB6.Certificate.MixedSemantics.raw3008step1Labels line 1827
507. def OAI.MUB6.Certificate.MixedSemantics.raw3008step2 line 1829
508. def OAI.MUB6.Certificate.MixedSemantics.raw3008step2Labels line 1830
509. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3008 line 1832
510. def OAI.MUB6.Certificate.MixedSemantics.raw3009 line 1852
511. def OAI.MUB6.Certificate.MixedSemantics.raw3009Labels line 1853
512. def OAI.MUB6.Certificate.MixedSemantics.raw3009step0 line 1855
513. def OAI.MUB6.Certificate.MixedSemantics.raw3009step0Labels line 1856
514. def OAI.MUB6.Certificate.MixedSemantics.raw3009step1 line 1858
515. def OAI.MUB6.Certificate.MixedSemantics.raw3009step1Labels line 1859
516. def OAI.MUB6.Certificate.MixedSemantics.raw3009step2 line 1861
517. def OAI.MUB6.Certificate.MixedSemantics.raw3009step2Labels line 1862
518. def OAI.MUB6.Certificate.MixedSemantics.raw3009step3 line 1864
519. def OAI.MUB6.Certificate.MixedSemantics.raw3009step3Labels line 1865
520. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3009 line 1867
521. def OAI.MUB6.Certificate.MixedSemantics.raw3010 line 1893
522. def OAI.MUB6.Certificate.MixedSemantics.raw3010Labels line 1894
523. def OAI.MUB6.Certificate.MixedSemantics.raw3010step0 line 1896
524. def OAI.MUB6.Certificate.MixedSemantics.raw3010step0Labels line 1897
525. def OAI.MUB6.Certificate.MixedSemantics.raw3010step1 line 1899
526. def OAI.MUB6.Certificate.MixedSemantics.raw3010step1Labels line 1900
527. def OAI.MUB6.Certificate.MixedSemantics.raw3010step2 line 1902
528. def OAI.MUB6.Certificate.MixedSemantics.raw3010step2Labels line 1903
529. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3010 line 1905
530. def OAI.MUB6.Certificate.MixedSemantics.raw3011 line 1925
531. def OAI.MUB6.Certificate.MixedSemantics.raw3011Labels line 1926
532. def OAI.MUB6.Certificate.MixedSemantics.raw3011step0 line 1928
533. def OAI.MUB6.Certificate.MixedSemantics.raw3011step0Labels line 1929
534. def OAI.MUB6.Certificate.MixedSemantics.raw3011step1 line 1931
535. def OAI.MUB6.Certificate.MixedSemantics.raw3011step1Labels line 1932
536. def OAI.MUB6.Certificate.MixedSemantics.raw3011step2 line 1934
537. def OAI.MUB6.Certificate.MixedSemantics.raw3011step2Labels line 1935
538. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3011 line 1937
539. def OAI.MUB6.Certificate.MixedSemantics.raw3012 line 1958
540. def OAI.MUB6.Certificate.MixedSemantics.raw3012Labels line 1959
541. def OAI.MUB6.Certificate.MixedSemantics.raw3012step0 line 1961
542. def OAI.MUB6.Certificate.MixedSemantics.raw3012step0Labels line 1962
543. def OAI.MUB6.Certificate.MixedSemantics.raw3012step1 line 1964
544. def OAI.MUB6.Certificate.MixedSemantics.raw3012step1Labels line 1965
545. def OAI.MUB6.Certificate.MixedSemantics.raw3012step2 line 1967
546. def OAI.MUB6.Certificate.MixedSemantics.raw3012step2Labels line 1968
547. def OAI.MUB6.Certificate.MixedSemantics.raw3012step3 line 1970
548. def OAI.MUB6.Certificate.MixedSemantics.raw3012step3Labels line 1971
549. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3012 line 1973
550. def OAI.MUB6.Certificate.MixedSemantics.raw3013 line 1999
551. def OAI.MUB6.Certificate.MixedSemantics.raw3013Labels line 2000
552. def OAI.MUB6.Certificate.MixedSemantics.raw3013step0 line 2002
553. def OAI.MUB6.Certificate.MixedSemantics.raw3013step0Labels line 2003
554. def OAI.MUB6.Certificate.MixedSemantics.raw3013step1 line 2005
555. def OAI.MUB6.Certificate.MixedSemantics.raw3013step1Labels line 2006
556. def OAI.MUB6.Certificate.MixedSemantics.raw3013step2 line 2008
557. def OAI.MUB6.Certificate.MixedSemantics.raw3013step2Labels line 2009
558. def OAI.MUB6.Certificate.MixedSemantics.raw3013step3 line 2011
559. def OAI.MUB6.Certificate.MixedSemantics.raw3013step3Labels line 2012
560. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3013 line 2014
561. def OAI.MUB6.Certificate.MixedSemantics.raw3014 line 2040
562. def OAI.MUB6.Certificate.MixedSemantics.raw3014Labels line 2041
563. def OAI.MUB6.Certificate.MixedSemantics.raw3014step0 line 2043
564. def OAI.MUB6.Certificate.MixedSemantics.raw3014step0Labels line 2044
565. def OAI.MUB6.Certificate.MixedSemantics.raw3014step1 line 2046
566. def OAI.MUB6.Certificate.MixedSemantics.raw3014step1Labels line 2047
567. def OAI.MUB6.Certificate.MixedSemantics.raw3014step2 line 2049
568. def OAI.MUB6.Certificate.MixedSemantics.raw3014step2Labels line 2050
569. def OAI.MUB6.Certificate.MixedSemantics.raw3014step3 line 2052
570. def OAI.MUB6.Certificate.MixedSemantics.raw3014step3Labels line 2053
571. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3014 line 2055
572. def OAI.MUB6.Certificate.MixedSemantics.raw3015 line 2081
573. def OAI.MUB6.Certificate.MixedSemantics.raw3015Labels line 2082
574. def OAI.MUB6.Certificate.MixedSemantics.raw3015step0 line 2084
575. def OAI.MUB6.Certificate.MixedSemantics.raw3015step0Labels line 2085
576. def OAI.MUB6.Certificate.MixedSemantics.raw3015step1 line 2087
577. def OAI.MUB6.Certificate.MixedSemantics.raw3015step1Labels line 2088
578. def OAI.MUB6.Certificate.MixedSemantics.raw3015step2 line 2090
579. def OAI.MUB6.Certificate.MixedSemantics.raw3015step2Labels line 2091
580. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3015 line 2093
581. def OAI.MUB6.Certificate.MixedSemantics.raw3016 line 2113
582. def OAI.MUB6.Certificate.MixedSemantics.raw3016Labels line 2114
583. def OAI.MUB6.Certificate.MixedSemantics.raw3016step0 line 2116
584. def OAI.MUB6.Certificate.MixedSemantics.raw3016step0Labels line 2117
585. def OAI.MUB6.Certificate.MixedSemantics.raw3016step1 line 2119
586. def OAI.MUB6.Certificate.MixedSemantics.raw3016step1Labels line 2120
587. def OAI.MUB6.Certificate.MixedSemantics.raw3016step2 line 2122
588. def OAI.MUB6.Certificate.MixedSemantics.raw3016step2Labels line 2123
589. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3016 line 2125
590. def OAI.MUB6.Certificate.MixedSemantics.raw3017 line 2146
591. def OAI.MUB6.Certificate.MixedSemantics.raw3017Labels line 2147
592. def OAI.MUB6.Certificate.MixedSemantics.raw3017step0 line 2149
593. def OAI.MUB6.Certificate.MixedSemantics.raw3017step0Labels line 2150
594. def OAI.MUB6.Certificate.MixedSemantics.raw3017step1 line 2152
595. def OAI.MUB6.Certificate.MixedSemantics.raw3017step1Labels line 2153
596. def OAI.MUB6.Certificate.MixedSemantics.raw3017step2 line 2155
597. def OAI.MUB6.Certificate.MixedSemantics.raw3017step2Labels line 2156
598. def OAI.MUB6.Certificate.MixedSemantics.raw3017step3 line 2158
599. def OAI.MUB6.Certificate.MixedSemantics.raw3017step3Labels line 2159
600. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3017 line 2161
601. def OAI.MUB6.Certificate.MixedSemantics.raw3018 line 2187
602. def OAI.MUB6.Certificate.MixedSemantics.raw3018Labels line 2188
603. def OAI.MUB6.Certificate.MixedSemantics.raw3018step0 line 2190
604. def OAI.MUB6.Certificate.MixedSemantics.raw3018step0Labels line 2191
605. def OAI.MUB6.Certificate.MixedSemantics.raw3018step1 line 2193
606. def OAI.MUB6.Certificate.MixedSemantics.raw3018step1Labels line 2194
607. def OAI.MUB6.Certificate.MixedSemantics.raw3018step2 line 2196
608. def OAI.MUB6.Certificate.MixedSemantics.raw3018step2Labels line 2197
609. def OAI.MUB6.Certificate.MixedSemantics.raw3018step3 line 2199
610. def OAI.MUB6.Certificate.MixedSemantics.raw3018step3Labels line 2200
611. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3018 line 2202
612. def OAI.MUB6.Certificate.MixedSemantics.raw3019 line 2228
613. def OAI.MUB6.Certificate.MixedSemantics.raw3019Labels line 2229
614. def OAI.MUB6.Certificate.MixedSemantics.raw3019step0 line 2231
615. def OAI.MUB6.Certificate.MixedSemantics.raw3019step0Labels line 2232
616. def OAI.MUB6.Certificate.MixedSemantics.raw3019step1 line 2234
617. def OAI.MUB6.Certificate.MixedSemantics.raw3019step1Labels line 2235
618. def OAI.MUB6.Certificate.MixedSemantics.raw3019step2 line 2237
619. def OAI.MUB6.Certificate.MixedSemantics.raw3019step2Labels line 2238
620. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3019 line 2240
621. def OAI.MUB6.Certificate.MixedSemantics.raw3020 line 2261
622. def OAI.MUB6.Certificate.MixedSemantics.raw3020Labels line 2262
623. def OAI.MUB6.Certificate.MixedSemantics.raw3020step0 line 2264
624. def OAI.MUB6.Certificate.MixedSemantics.raw3020step0Labels line 2265
625. def OAI.MUB6.Certificate.MixedSemantics.raw3020step1 line 2267
626. def OAI.MUB6.Certificate.MixedSemantics.raw3020step1Labels line 2268
627. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3020 line 2270
628. def OAI.MUB6.Certificate.MixedSemantics.raw3021 line 2285
629. def OAI.MUB6.Certificate.MixedSemantics.raw3021Labels line 2286
630. def OAI.MUB6.Certificate.MixedSemantics.raw3021step0 line 2288
631. def OAI.MUB6.Certificate.MixedSemantics.raw3021step0Labels line 2289
632. def OAI.MUB6.Certificate.MixedSemantics.raw3021step1 line 2291
633. def OAI.MUB6.Certificate.MixedSemantics.raw3021step1Labels line 2292
634. def OAI.MUB6.Certificate.MixedSemantics.raw3021step2 line 2294
635. def OAI.MUB6.Certificate.MixedSemantics.raw3021step2Labels line 2295
636. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3021 line 2297
637. def OAI.MUB6.Certificate.MixedSemantics.raw3022 line 2318
638. def OAI.MUB6.Certificate.MixedSemantics.raw3022Labels line 2319
639. def OAI.MUB6.Certificate.MixedSemantics.raw3022step0 line 2321
640. def OAI.MUB6.Certificate.MixedSemantics.raw3022step0Labels line 2322
641. def OAI.MUB6.Certificate.MixedSemantics.raw3022step1 line 2324
642. def OAI.MUB6.Certificate.MixedSemantics.raw3022step1Labels line 2325
643. def OAI.MUB6.Certificate.MixedSemantics.raw3022step2 line 2327
644. def OAI.MUB6.Certificate.MixedSemantics.raw3022step2Labels line 2328
645. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3022 line 2330
646. def OAI.MUB6.Certificate.MixedSemantics.raw3023 line 2351
647. def OAI.MUB6.Certificate.MixedSemantics.raw3023Labels line 2352
648. def OAI.MUB6.Certificate.MixedSemantics.raw3023step0 line 2354
649. def OAI.MUB6.Certificate.MixedSemantics.raw3023step0Labels line 2355
650. def OAI.MUB6.Certificate.MixedSemantics.raw3023step1 line 2357
651. def OAI.MUB6.Certificate.MixedSemantics.raw3023step1Labels line 2358
652. def OAI.MUB6.Certificate.MixedSemantics.raw3023step2 line 2360
653. def OAI.MUB6.Certificate.MixedSemantics.raw3023step2Labels line 2361
654. def OAI.MUB6.Certificate.MixedSemantics.raw3023step3 line 2363
655. def OAI.MUB6.Certificate.MixedSemantics.raw3023step3Labels line 2364
656. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3023 line 2366
657. def OAI.MUB6.Certificate.MixedSemantics.raw3024 line 2392
658. def OAI.MUB6.Certificate.MixedSemantics.raw3024Labels line 2393
659. def OAI.MUB6.Certificate.MixedSemantics.raw3024step0 line 2395
660. def OAI.MUB6.Certificate.MixedSemantics.raw3024step0Labels line 2396
661. def OAI.MUB6.Certificate.MixedSemantics.raw3024step1 line 2398
662. def OAI.MUB6.Certificate.MixedSemantics.raw3024step1Labels line 2399
663. def OAI.MUB6.Certificate.MixedSemantics.raw3024step2 line 2401
664. def OAI.MUB6.Certificate.MixedSemantics.raw3024step2Labels line 2402
665. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3024 line 2404
666. def OAI.MUB6.Certificate.MixedSemantics.raw3025 line 2425
667. def OAI.MUB6.Certificate.MixedSemantics.raw3025Labels line 2426
668. def OAI.MUB6.Certificate.MixedSemantics.raw3025step0 line 2428
669. def OAI.MUB6.Certificate.MixedSemantics.raw3025step0Labels line 2429
670. def OAI.MUB6.Certificate.MixedSemantics.raw3025step1 line 2431
671. def OAI.MUB6.Certificate.MixedSemantics.raw3025step1Labels line 2432
672. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3025 line 2434
673. def OAI.MUB6.Certificate.MixedSemantics.raw3026 line 2449
674. def OAI.MUB6.Certificate.MixedSemantics.raw3026Labels line 2450
675. def OAI.MUB6.Certificate.MixedSemantics.raw3026step0 line 2452
676. def OAI.MUB6.Certificate.MixedSemantics.raw3026step0Labels line 2453
677. def OAI.MUB6.Certificate.MixedSemantics.raw3026step1 line 2455
678. def OAI.MUB6.Certificate.MixedSemantics.raw3026step1Labels line 2456
679. def OAI.MUB6.Certificate.MixedSemantics.raw3026step2 line 2458
680. def OAI.MUB6.Certificate.MixedSemantics.raw3026step2Labels line 2459
681. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3026 line 2461
682. def OAI.MUB6.Certificate.MixedSemantics.raw3027 line 2482
683. def OAI.MUB6.Certificate.MixedSemantics.raw3027Labels line 2483
684. def OAI.MUB6.Certificate.MixedSemantics.raw3027step0 line 2485
685. def OAI.MUB6.Certificate.MixedSemantics.raw3027step0Labels line 2486
686. def OAI.MUB6.Certificate.MixedSemantics.raw3027step1 line 2488
687. def OAI.MUB6.Certificate.MixedSemantics.raw3027step1Labels line 2489
688. def OAI.MUB6.Certificate.MixedSemantics.raw3027step2 line 2491
689. def OAI.MUB6.Certificate.MixedSemantics.raw3027step2Labels line 2492
690. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3027 line 2494
691. def OAI.MUB6.Certificate.MixedSemantics.raw3028 line 2515
692. def OAI.MUB6.Certificate.MixedSemantics.raw3028Labels line 2516
693. def OAI.MUB6.Certificate.MixedSemantics.raw3028step0 line 2518
694. def OAI.MUB6.Certificate.MixedSemantics.raw3028step0Labels line 2519
695. def OAI.MUB6.Certificate.MixedSemantics.raw3028step1 line 2521
696. def OAI.MUB6.Certificate.MixedSemantics.raw3028step1Labels line 2522
697. def OAI.MUB6.Certificate.MixedSemantics.raw3028step2 line 2524
698. def OAI.MUB6.Certificate.MixedSemantics.raw3028step2Labels line 2525
699. def OAI.MUB6.Certificate.MixedSemantics.raw3028step3 line 2527
700. def OAI.MUB6.Certificate.MixedSemantics.raw3028step3Labels line 2528
701. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3028 line 2530
702. def OAI.MUB6.Certificate.MixedSemantics.raw3029 line 2556
703. def OAI.MUB6.Certificate.MixedSemantics.raw3029Labels line 2557
704. def OAI.MUB6.Certificate.MixedSemantics.raw3029step0 line 2559
705. def OAI.MUB6.Certificate.MixedSemantics.raw3029step0Labels line 2560
706. def OAI.MUB6.Certificate.MixedSemantics.raw3029step1 line 2562
707. def OAI.MUB6.Certificate.MixedSemantics.raw3029step1Labels line 2563
708. def OAI.MUB6.Certificate.MixedSemantics.raw3029step2 line 2565
709. def OAI.MUB6.Certificate.MixedSemantics.raw3029step2Labels line 2566
710. def OAI.MUB6.Certificate.MixedSemantics.raw3029step3 line 2568
711. def OAI.MUB6.Certificate.MixedSemantics.raw3029step3Labels line 2569
712. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3029 line 2571
713. def OAI.MUB6.Certificate.MixedSemantics.raw3030 line 2598
714. def OAI.MUB6.Certificate.MixedSemantics.raw3030Labels line 2599
715. def OAI.MUB6.Certificate.MixedSemantics.raw3030step0 line 2601
716. def OAI.MUB6.Certificate.MixedSemantics.raw3030step0Labels line 2602
717. def OAI.MUB6.Certificate.MixedSemantics.raw3030step1 line 2604
718. def OAI.MUB6.Certificate.MixedSemantics.raw3030step1Labels line 2605
719. def OAI.MUB6.Certificate.MixedSemantics.raw3030step2 line 2607
720. def OAI.MUB6.Certificate.MixedSemantics.raw3030step2Labels line 2608
721. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3030 line 2610
722. def OAI.MUB6.Certificate.MixedSemantics.raw3031 line 2631
723. def OAI.MUB6.Certificate.MixedSemantics.raw3031Labels line 2632
724. def OAI.MUB6.Certificate.MixedSemantics.raw3031step0 line 2634
725. def OAI.MUB6.Certificate.MixedSemantics.raw3031step0Labels line 2635
726. def OAI.MUB6.Certificate.MixedSemantics.raw3031step1 line 2637
727. def OAI.MUB6.Certificate.MixedSemantics.raw3031step1Labels line 2638
728. def OAI.MUB6.Certificate.MixedSemantics.raw3031step2 line 2640
729. def OAI.MUB6.Certificate.MixedSemantics.raw3031step2Labels line 2641
730. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3031 line 2643
731. def OAI.MUB6.Certificate.MixedSemantics.raw3032 line 2664
732. def OAI.MUB6.Certificate.MixedSemantics.raw3032Labels line 2665
733. def OAI.MUB6.Certificate.MixedSemantics.raw3032step0 line 2667
734. def OAI.MUB6.Certificate.MixedSemantics.raw3032step0Labels line 2668
735. def OAI.MUB6.Certificate.MixedSemantics.raw3032step1 line 2670
736. def OAI.MUB6.Certificate.MixedSemantics.raw3032step1Labels line 2671
737. def OAI.MUB6.Certificate.MixedSemantics.raw3032step2 line 2673
738. def OAI.MUB6.Certificate.MixedSemantics.raw3032step2Labels line 2674
739. def OAI.MUB6.Certificate.MixedSemantics.raw3032step3 line 2676
740. def OAI.MUB6.Certificate.MixedSemantics.raw3032step3Labels line 2677
741. def OAI.MUB6.Certificate.MixedSemantics.raw3032step4 line 2679
742. def OAI.MUB6.Certificate.MixedSemantics.raw3032step4Labels line 2680
743. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3032 line 2682
744. def OAI.MUB6.Certificate.MixedSemantics.raw3033 line 2715
745. def OAI.MUB6.Certificate.MixedSemantics.raw3033Labels line 2716
746. def OAI.MUB6.Certificate.MixedSemantics.raw3033step0 line 2718
747. def OAI.MUB6.Certificate.MixedSemantics.raw3033step0Labels line 2719
748. def OAI.MUB6.Certificate.MixedSemantics.raw3033step1 line 2721
749. def OAI.MUB6.Certificate.MixedSemantics.raw3033step1Labels line 2722
750. def OAI.MUB6.Certificate.MixedSemantics.raw3033step2 line 2724
751. def OAI.MUB6.Certificate.MixedSemantics.raw3033step2Labels line 2725
752. def OAI.MUB6.Certificate.MixedSemantics.raw3033step3 line 2727
753. def OAI.MUB6.Certificate.MixedSemantics.raw3033step3Labels line 2728
754. def OAI.MUB6.Certificate.MixedSemantics.raw3033step4 line 2730
755. def OAI.MUB6.Certificate.MixedSemantics.raw3033step4Labels line 2731
756. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3033 line 2733
757. def OAI.MUB6.Certificate.MixedSemantics.raw3034 line 2765
758. def OAI.MUB6.Certificate.MixedSemantics.raw3034Labels line 2766
759. def OAI.MUB6.Certificate.MixedSemantics.raw3034step0 line 2768
760. def OAI.MUB6.Certificate.MixedSemantics.raw3034step0Labels line 2769
761. def OAI.MUB6.Certificate.MixedSemantics.raw3034step1 line 2771
762. def OAI.MUB6.Certificate.MixedSemantics.raw3034step1Labels line 2772
763. def OAI.MUB6.Certificate.MixedSemantics.raw3034step2 line 2774
764. def OAI.MUB6.Certificate.MixedSemantics.raw3034step2Labels line 2775
765. def OAI.MUB6.Certificate.MixedSemantics.raw3034step3 line 2777
766. def OAI.MUB6.Certificate.MixedSemantics.raw3034step3Labels line 2778
767. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3034 line 2780
768. def OAI.MUB6.Certificate.MixedSemantics.raw3035 line 2807
769. def OAI.MUB6.Certificate.MixedSemantics.raw3035Labels line 2808
770. def OAI.MUB6.Certificate.MixedSemantics.raw3035step0 line 2810
771. def OAI.MUB6.Certificate.MixedSemantics.raw3035step0Labels line 2811
772. def OAI.MUB6.Certificate.MixedSemantics.raw3035step1 line 2813
773. def OAI.MUB6.Certificate.MixedSemantics.raw3035step1Labels line 2814
774. def OAI.MUB6.Certificate.MixedSemantics.raw3035step2 line 2816
775. def OAI.MUB6.Certificate.MixedSemantics.raw3035step2Labels line 2817
776. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3035 line 2819
777. def OAI.MUB6.Certificate.MixedSemantics.raw3036 line 2840
778. def OAI.MUB6.Certificate.MixedSemantics.raw3036Labels line 2841
779. def OAI.MUB6.Certificate.MixedSemantics.raw3036step0 line 2843
780. def OAI.MUB6.Certificate.MixedSemantics.raw3036step0Labels line 2844
781. def OAI.MUB6.Certificate.MixedSemantics.raw3036step1 line 2846
782. def OAI.MUB6.Certificate.MixedSemantics.raw3036step1Labels line 2847
783. def OAI.MUB6.Certificate.MixedSemantics.raw3036step2 line 2849
784. def OAI.MUB6.Certificate.MixedSemantics.raw3036step2Labels line 2850
785. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3036 line 2852
786. def OAI.MUB6.Certificate.MixedSemantics.raw3037 line 2873
787. def OAI.MUB6.Certificate.MixedSemantics.raw3037Labels line 2874
788. def OAI.MUB6.Certificate.MixedSemantics.raw3037step0 line 2876
789. def OAI.MUB6.Certificate.MixedSemantics.raw3037step0Labels line 2877
790. def OAI.MUB6.Certificate.MixedSemantics.raw3037step1 line 2879
791. def OAI.MUB6.Certificate.MixedSemantics.raw3037step1Labels line 2880
792. def OAI.MUB6.Certificate.MixedSemantics.raw3037step2 line 2882
793. def OAI.MUB6.Certificate.MixedSemantics.raw3037step2Labels line 2883
794. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3037 line 2885
795. def OAI.MUB6.Certificate.MixedSemantics.raw3038 line 2908
796. def OAI.MUB6.Certificate.MixedSemantics.raw3038Labels line 2909
797. def OAI.MUB6.Certificate.MixedSemantics.raw3038step0 line 2911
798. def OAI.MUB6.Certificate.MixedSemantics.raw3038step0Labels line 2912
799. def OAI.MUB6.Certificate.MixedSemantics.raw3038step1 line 2914
800. def OAI.MUB6.Certificate.MixedSemantics.raw3038step1Labels line 2915
801. def OAI.MUB6.Certificate.MixedSemantics.raw3038step2 line 2917
802. def OAI.MUB6.Certificate.MixedSemantics.raw3038step2Labels line 2918
803. def OAI.MUB6.Certificate.MixedSemantics.raw3038step3 line 2920
804. def OAI.MUB6.Certificate.MixedSemantics.raw3038step3Labels line 2921
805. def OAI.MUB6.Certificate.MixedSemantics.raw3038step4 line 2923
806. def OAI.MUB6.Certificate.MixedSemantics.raw3038step4Labels line 2924
807. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3038 line 2926
808. def OAI.MUB6.Certificate.MixedSemantics.raw3039 line 2958
809. def OAI.MUB6.Certificate.MixedSemantics.raw3039Labels line 2959
810. def OAI.MUB6.Certificate.MixedSemantics.raw3039step0 line 2961
811. def OAI.MUB6.Certificate.MixedSemantics.raw3039step0Labels line 2962
812. def OAI.MUB6.Certificate.MixedSemantics.raw3039step1 line 2964
813. def OAI.MUB6.Certificate.MixedSemantics.raw3039step1Labels line 2965
814. def OAI.MUB6.Certificate.MixedSemantics.raw3039step2 line 2967
815. def OAI.MUB6.Certificate.MixedSemantics.raw3039step2Labels line 2968
816. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3039 line 2970
817. def OAI.MUB6.Certificate.MixedSemantics.raw3040 line 2991
818. def OAI.MUB6.Certificate.MixedSemantics.raw3040Labels line 2992
819. def OAI.MUB6.Certificate.MixedSemantics.raw3040step0 line 2994
820. def OAI.MUB6.Certificate.MixedSemantics.raw3040step0Labels line 2995
821. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3040 line 2997
822. def OAI.MUB6.Certificate.MixedSemantics.raw3041 line 3008
823. def OAI.MUB6.Certificate.MixedSemantics.raw3041Labels line 3009
824. def OAI.MUB6.Certificate.MixedSemantics.raw3041step0 line 3011
825. def OAI.MUB6.Certificate.MixedSemantics.raw3041step0Labels line 3012
826. def OAI.MUB6.Certificate.MixedSemantics.raw3041step1 line 3014
827. def OAI.MUB6.Certificate.MixedSemantics.raw3041step1Labels line 3015
828. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3041 line 3017
829. def OAI.MUB6.Certificate.MixedSemantics.raw3042 line 3032
830. def OAI.MUB6.Certificate.MixedSemantics.raw3042Labels line 3033
831. def OAI.MUB6.Certificate.MixedSemantics.raw3042step0 line 3035
832. def OAI.MUB6.Certificate.MixedSemantics.raw3042step0Labels line 3036
833. def OAI.MUB6.Certificate.MixedSemantics.raw3042step1 line 3038
834. def OAI.MUB6.Certificate.MixedSemantics.raw3042step1Labels line 3039
835. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3042 line 3041
836. def OAI.MUB6.Certificate.MixedSemantics.raw3043 line 3058
837. def OAI.MUB6.Certificate.MixedSemantics.raw3043Labels line 3059
838. def OAI.MUB6.Certificate.MixedSemantics.raw3043step0 line 3061
839. def OAI.MUB6.Certificate.MixedSemantics.raw3043step0Labels line 3062
840. def OAI.MUB6.Certificate.MixedSemantics.raw3043step1 line 3064
841. def OAI.MUB6.Certificate.MixedSemantics.raw3043step1Labels line 3065
842. def OAI.MUB6.Certificate.MixedSemantics.raw3043step2 line 3067
843. def OAI.MUB6.Certificate.MixedSemantics.raw3043step2Labels line 3068
844. def OAI.MUB6.Certificate.MixedSemantics.raw3043step3 line 3070
845. def OAI.MUB6.Certificate.MixedSemantics.raw3043step3Labels line 3071
846. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3043 line 3073
847. def OAI.MUB6.Certificate.MixedSemantics.raw3044 line 3099
848. def OAI.MUB6.Certificate.MixedSemantics.raw3044Labels line 3100
849. def OAI.MUB6.Certificate.MixedSemantics.raw3044step0 line 3102
850. def OAI.MUB6.Certificate.MixedSemantics.raw3044step0Labels line 3103
851. def OAI.MUB6.Certificate.MixedSemantics.raw3044step1 line 3105
852. def OAI.MUB6.Certificate.MixedSemantics.raw3044step1Labels line 3106
853. def OAI.MUB6.Certificate.MixedSemantics.raw3044step2 line 3108
854. def OAI.MUB6.Certificate.MixedSemantics.raw3044step2Labels line 3109
855. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3044 line 3111
856. def OAI.MUB6.Certificate.MixedSemantics.raw3045 line 3132
857. def OAI.MUB6.Certificate.MixedSemantics.raw3045Labels line 3133
858. def OAI.MUB6.Certificate.MixedSemantics.raw3045step0 line 3135
859. def OAI.MUB6.Certificate.MixedSemantics.raw3045step0Labels line 3136
860. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3045 line 3138
861. def OAI.MUB6.Certificate.MixedSemantics.raw3046 line 3149
862. def OAI.MUB6.Certificate.MixedSemantics.raw3046Labels line 3150
863. def OAI.MUB6.Certificate.MixedSemantics.raw3046step0 line 3152
864. def OAI.MUB6.Certificate.MixedSemantics.raw3046step0Labels line 3153
865. def OAI.MUB6.Certificate.MixedSemantics.raw3046step1 line 3155
866. def OAI.MUB6.Certificate.MixedSemantics.raw3046step1Labels line 3156
867. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3046 line 3158
868. def OAI.MUB6.Certificate.MixedSemantics.raw3047 line 3173
869. def OAI.MUB6.Certificate.MixedSemantics.raw3047Labels line 3174
870. def OAI.MUB6.Certificate.MixedSemantics.raw3047step0 line 3176
871. def OAI.MUB6.Certificate.MixedSemantics.raw3047step0Labels line 3177
872. def OAI.MUB6.Certificate.MixedSemantics.raw3047step1 line 3179
873. def OAI.MUB6.Certificate.MixedSemantics.raw3047step1Labels line 3180
874. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3047 line 3182
875. def OAI.MUB6.Certificate.MixedSemantics.raw3048 line 3199
876. def OAI.MUB6.Certificate.MixedSemantics.raw3048Labels line 3200
877. def OAI.MUB6.Certificate.MixedSemantics.raw3048step0 line 3202
878. def OAI.MUB6.Certificate.MixedSemantics.raw3048step0Labels line 3203
879. def OAI.MUB6.Certificate.MixedSemantics.raw3048step1 line 3205
880. def OAI.MUB6.Certificate.MixedSemantics.raw3048step1Labels line 3206
881. def OAI.MUB6.Certificate.MixedSemantics.raw3048step2 line 3208
882. def OAI.MUB6.Certificate.MixedSemantics.raw3048step2Labels line 3209
883. def OAI.MUB6.Certificate.MixedSemantics.raw3048step3 line 3211
884. def OAI.MUB6.Certificate.MixedSemantics.raw3048step3Labels line 3212
885. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3048 line 3214
886. def OAI.MUB6.Certificate.MixedSemantics.raw3049 line 3240
887. def OAI.MUB6.Certificate.MixedSemantics.raw3049Labels line 3241
888. def OAI.MUB6.Certificate.MixedSemantics.raw3049step0 line 3243
889. def OAI.MUB6.Certificate.MixedSemantics.raw3049step0Labels line 3244
890. def OAI.MUB6.Certificate.MixedSemantics.raw3049step1 line 3246
891. def OAI.MUB6.Certificate.MixedSemantics.raw3049step1Labels line 3247
892. def OAI.MUB6.Certificate.MixedSemantics.raw3049step2 line 3249
893. def OAI.MUB6.Certificate.MixedSemantics.raw3049step2Labels line 3250
894. def OAI.MUB6.Certificate.MixedSemantics.raw3049step3 line 3252
895. def OAI.MUB6.Certificate.MixedSemantics.raw3049step3Labels line 3253
896. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3049 line 3255
897. def OAI.MUB6.Certificate.MixedSemantics.raw3050 line 3282
898. def OAI.MUB6.Certificate.MixedSemantics.raw3050Labels line 3283
899. def OAI.MUB6.Certificate.MixedSemantics.raw3050step0 line 3285
900. def OAI.MUB6.Certificate.MixedSemantics.raw3050step0Labels line 3286
901. def OAI.MUB6.Certificate.MixedSemantics.raw3050step1 line 3288
902. def OAI.MUB6.Certificate.MixedSemantics.raw3050step1Labels line 3289
903. def OAI.MUB6.Certificate.MixedSemantics.raw3050step2 line 3291
904. def OAI.MUB6.Certificate.MixedSemantics.raw3050step2Labels line 3292
905. def OAI.MUB6.Certificate.MixedSemantics.raw3050step3 line 3294
906. def OAI.MUB6.Certificate.MixedSemantics.raw3050step3Labels line 3295
907. def OAI.MUB6.Certificate.MixedSemantics.raw3050step4 line 3297
908. def OAI.MUB6.Certificate.MixedSemantics.raw3050step4Labels line 3298
909. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3050 line 3300
910. def OAI.MUB6.Certificate.MixedSemantics.raw3051 line 3332
911. def OAI.MUB6.Certificate.MixedSemantics.raw3051Labels line 3333
912. def OAI.MUB6.Certificate.MixedSemantics.raw3051step0 line 3335
913. def OAI.MUB6.Certificate.MixedSemantics.raw3051step0Labels line 3336
914. def OAI.MUB6.Certificate.MixedSemantics.raw3051step1 line 3338
915. def OAI.MUB6.Certificate.MixedSemantics.raw3051step1Labels line 3339
916. def OAI.MUB6.Certificate.MixedSemantics.raw3051step2 line 3341
917. def OAI.MUB6.Certificate.MixedSemantics.raw3051step2Labels line 3342
918. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3051 line 3344
919. def OAI.MUB6.Certificate.MixedSemantics.raw3052 line 3365
920. def OAI.MUB6.Certificate.MixedSemantics.raw3052Labels line 3366
921. def OAI.MUB6.Certificate.MixedSemantics.raw3052step0 line 3368
922. def OAI.MUB6.Certificate.MixedSemantics.raw3052step0Labels line 3369
923. def OAI.MUB6.Certificate.MixedSemantics.raw3052step1 line 3371
924. def OAI.MUB6.Certificate.MixedSemantics.raw3052step1Labels line 3372
925. def OAI.MUB6.Certificate.MixedSemantics.raw3052step2 line 3374
926. def OAI.MUB6.Certificate.MixedSemantics.raw3052step2Labels line 3375
927. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3052 line 3377
928. def OAI.MUB6.Certificate.MixedSemantics.raw3053 line 3398
929. def OAI.MUB6.Certificate.MixedSemantics.raw3053Labels line 3399
930. def OAI.MUB6.Certificate.MixedSemantics.raw3053step0 line 3401
931. def OAI.MUB6.Certificate.MixedSemantics.raw3053step0Labels line 3402
932. def OAI.MUB6.Certificate.MixedSemantics.raw3053step1 line 3404
933. def OAI.MUB6.Certificate.MixedSemantics.raw3053step1Labels line 3405
934. def OAI.MUB6.Certificate.MixedSemantics.raw3053step2 line 3407
935. def OAI.MUB6.Certificate.MixedSemantics.raw3053step2Labels line 3408
936. def OAI.MUB6.Certificate.MixedSemantics.raw3053step3 line 3410
937. def OAI.MUB6.Certificate.MixedSemantics.raw3053step3Labels line 3411
938. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3053 line 3413
939. def OAI.MUB6.Certificate.MixedSemantics.raw3054 line 3440
940. def OAI.MUB6.Certificate.MixedSemantics.raw3054Labels line 3441
941. def OAI.MUB6.Certificate.MixedSemantics.raw3054step0 line 3443
942. def OAI.MUB6.Certificate.MixedSemantics.raw3054step0Labels line 3444
943. def OAI.MUB6.Certificate.MixedSemantics.raw3054step1 line 3446
944. def OAI.MUB6.Certificate.MixedSemantics.raw3054step1Labels line 3447
945. def OAI.MUB6.Certificate.MixedSemantics.raw3054step2 line 3449
946. def OAI.MUB6.Certificate.MixedSemantics.raw3054step2Labels line 3450
947. def OAI.MUB6.Certificate.MixedSemantics.raw3054step3 line 3452
948. def OAI.MUB6.Certificate.MixedSemantics.raw3054step3Labels line 3453
949. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3054 line 3455
950. def OAI.MUB6.Certificate.MixedSemantics.raw3055 line 3482
951. def OAI.MUB6.Certificate.MixedSemantics.raw3055Labels line 3483
952. def OAI.MUB6.Certificate.MixedSemantics.raw3055step0 line 3485
953. def OAI.MUB6.Certificate.MixedSemantics.raw3055step0Labels line 3486
954. def OAI.MUB6.Certificate.MixedSemantics.raw3055step1 line 3488
955. def OAI.MUB6.Certificate.MixedSemantics.raw3055step1Labels line 3489
956. def OAI.MUB6.Certificate.MixedSemantics.raw3055step2 line 3491
957. def OAI.MUB6.Certificate.MixedSemantics.raw3055step2Labels line 3492
958. def OAI.MUB6.Certificate.MixedSemantics.raw3055step3 line 3494
959. def OAI.MUB6.Certificate.MixedSemantics.raw3055step3Labels line 3495
960. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3055 line 3497
961. def OAI.MUB6.Certificate.MixedSemantics.raw3056 line 3524
962. def OAI.MUB6.Certificate.MixedSemantics.raw3056Labels line 3525
963. def OAI.MUB6.Certificate.MixedSemantics.raw3056step0 line 3527
964. def OAI.MUB6.Certificate.MixedSemantics.raw3056step0Labels line 3528
965. def OAI.MUB6.Certificate.MixedSemantics.raw3056step1 line 3530
966. def OAI.MUB6.Certificate.MixedSemantics.raw3056step1Labels line 3531
967. def OAI.MUB6.Certificate.MixedSemantics.raw3056step2 line 3533
968. def OAI.MUB6.Certificate.MixedSemantics.raw3056step2Labels line 3534
969. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3056 line 3536
970. def OAI.MUB6.Certificate.MixedSemantics.raw3057 line 3557
971. def OAI.MUB6.Certificate.MixedSemantics.raw3057Labels line 3558
972. def OAI.MUB6.Certificate.MixedSemantics.raw3057step0 line 3560
973. def OAI.MUB6.Certificate.MixedSemantics.raw3057step0Labels line 3561
974. def OAI.MUB6.Certificate.MixedSemantics.raw3057step1 line 3563
975. def OAI.MUB6.Certificate.MixedSemantics.raw3057step1Labels line 3564
976. def OAI.MUB6.Certificate.MixedSemantics.raw3057step2 line 3566
977. def OAI.MUB6.Certificate.MixedSemantics.raw3057step2Labels line 3567
978. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3057 line 3569
979. def OAI.MUB6.Certificate.MixedSemantics.raw3058 line 3590
980. def OAI.MUB6.Certificate.MixedSemantics.raw3058Labels line 3591
981. def OAI.MUB6.Certificate.MixedSemantics.raw3058step0 line 3593
982. def OAI.MUB6.Certificate.MixedSemantics.raw3058step0Labels line 3594
983. def OAI.MUB6.Certificate.MixedSemantics.raw3058step1 line 3596
984. def OAI.MUB6.Certificate.MixedSemantics.raw3058step1Labels line 3597
985. def OAI.MUB6.Certificate.MixedSemantics.raw3058step2 line 3599
986. def OAI.MUB6.Certificate.MixedSemantics.raw3058step2Labels line 3600
987. def OAI.MUB6.Certificate.MixedSemantics.raw3058step3 line 3602
988. def OAI.MUB6.Certificate.MixedSemantics.raw3058step3Labels line 3603
989. def OAI.MUB6.Certificate.MixedSemantics.raw3058step4 line 3605
990. def OAI.MUB6.Certificate.MixedSemantics.raw3058step4Labels line 3606
991. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3058 line 3608
992. def OAI.MUB6.Certificate.MixedSemantics.raw3059 line 3641
993. def OAI.MUB6.Certificate.MixedSemantics.raw3059Labels line 3642
994. def OAI.MUB6.Certificate.MixedSemantics.raw3059step0 line 3644
995. def OAI.MUB6.Certificate.MixedSemantics.raw3059step0Labels line 3645
996. def OAI.MUB6.Certificate.MixedSemantics.raw3059step1 line 3647
997. def OAI.MUB6.Certificate.MixedSemantics.raw3059step1Labels line 3648
998. def OAI.MUB6.Certificate.MixedSemantics.raw3059step2 line 3650
999. def OAI.MUB6.Certificate.MixedSemantics.raw3059step2Labels line 3651
1000. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3059 line 3653
1001. def OAI.MUB6.Certificate.MixedSemantics.raw3060 line 3675
1002. def OAI.MUB6.Certificate.MixedSemantics.raw3060Labels line 3676
1003. def OAI.MUB6.Certificate.MixedSemantics.raw3060step0 line 3678
1004. def OAI.MUB6.Certificate.MixedSemantics.raw3060step0Labels line 3679
1005. def OAI.MUB6.Certificate.MixedSemantics.raw3060step1 line 3681
1006. def OAI.MUB6.Certificate.MixedSemantics.raw3060step1Labels line 3682
1007. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3060 line 3684
1008. def OAI.MUB6.Certificate.MixedSemantics.raw3061 line 3700
1009. def OAI.MUB6.Certificate.MixedSemantics.raw3061Labels line 3701
1010. def OAI.MUB6.Certificate.MixedSemantics.raw3061step0 line 3703
1011. def OAI.MUB6.Certificate.MixedSemantics.raw3061step0Labels line 3704
1012. def OAI.MUB6.Certificate.MixedSemantics.raw3061step1 line 3706
1013. def OAI.MUB6.Certificate.MixedSemantics.raw3061step1Labels line 3707
1014. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3061 line 3709
1015. def OAI.MUB6.Certificate.MixedSemantics.raw3062 line 3725
1016. def OAI.MUB6.Certificate.MixedSemantics.raw3062Labels line 3726
1017. def OAI.MUB6.Certificate.MixedSemantics.raw3062step0 line 3728
1018. def OAI.MUB6.Certificate.MixedSemantics.raw3062step0Labels line 3729
1019. def OAI.MUB6.Certificate.MixedSemantics.raw3062step1 line 3731
1020. def OAI.MUB6.Certificate.MixedSemantics.raw3062step1Labels line 3732
1021. def OAI.MUB6.Certificate.MixedSemantics.raw3062step2 line 3734
1022. def OAI.MUB6.Certificate.MixedSemantics.raw3062step2Labels line 3735
1023. def OAI.MUB6.Certificate.MixedSemantics.raw3062step3 line 3737
1024. def OAI.MUB6.Certificate.MixedSemantics.raw3062step3Labels line 3738
1025. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3062 line 3740
1026. def OAI.MUB6.Certificate.MixedSemantics.raw3063 line 3768
1027. def OAI.MUB6.Certificate.MixedSemantics.raw3063Labels line 3769
1028. def OAI.MUB6.Certificate.MixedSemantics.raw3063step0 line 3771
1029. def OAI.MUB6.Certificate.MixedSemantics.raw3063step0Labels line 3772
1030. def OAI.MUB6.Certificate.MixedSemantics.raw3063step1 line 3774
1031. def OAI.MUB6.Certificate.MixedSemantics.raw3063step1Labels line 3775
1032. def OAI.MUB6.Certificate.MixedSemantics.raw3063step2 line 3777
1033. def OAI.MUB6.Certificate.MixedSemantics.raw3063step2Labels line 3778
1034. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3063 line 3780
1035. def OAI.MUB6.Certificate.MixedSemantics.raw3064 line 3802
1036. def OAI.MUB6.Certificate.MixedSemantics.raw3064Labels line 3803
1037. def OAI.MUB6.Certificate.MixedSemantics.raw3064step0 line 3805
1038. def OAI.MUB6.Certificate.MixedSemantics.raw3064step0Labels line 3806
1039. def OAI.MUB6.Certificate.MixedSemantics.raw3064step1 line 3808
1040. def OAI.MUB6.Certificate.MixedSemantics.raw3064step1Labels line 3809
1041. def OAI.MUB6.Certificate.MixedSemantics.raw3064step2 line 3811
1042. def OAI.MUB6.Certificate.MixedSemantics.raw3064step2Labels line 3812
1043. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3064 line 3814
1044. def OAI.MUB6.Certificate.MixedSemantics.raw3065 line 3836
1045. def OAI.MUB6.Certificate.MixedSemantics.raw3065Labels line 3837
1046. def OAI.MUB6.Certificate.MixedSemantics.raw3065step0 line 3839
1047. def OAI.MUB6.Certificate.MixedSemantics.raw3065step0Labels line 3840
1048. def OAI.MUB6.Certificate.MixedSemantics.raw3065step1 line 3842
1049. def OAI.MUB6.Certificate.MixedSemantics.raw3065step1Labels line 3843
1050. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3065 line 3845
1051. def OAI.MUB6.Certificate.MixedSemantics.raw3066 line 3861
1052. def OAI.MUB6.Certificate.MixedSemantics.raw3066Labels line 3862
1053. def OAI.MUB6.Certificate.MixedSemantics.raw3066step0 line 3864
1054. def OAI.MUB6.Certificate.MixedSemantics.raw3066step0Labels line 3865
1055. def OAI.MUB6.Certificate.MixedSemantics.raw3066step1 line 3867
1056. def OAI.MUB6.Certificate.MixedSemantics.raw3066step1Labels line 3868
1057. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3066 line 3870
1058. def OAI.MUB6.Certificate.MixedSemantics.raw3067 line 3886
1059. def OAI.MUB6.Certificate.MixedSemantics.raw3067Labels line 3887
1060. def OAI.MUB6.Certificate.MixedSemantics.raw3067step0 line 3889
1061. def OAI.MUB6.Certificate.MixedSemantics.raw3067step0Labels line 3890
1062. def OAI.MUB6.Certificate.MixedSemantics.raw3067step1 line 3892
1063. def OAI.MUB6.Certificate.MixedSemantics.raw3067step1Labels line 3893
1064. def OAI.MUB6.Certificate.MixedSemantics.raw3067step2 line 3895
1065. def OAI.MUB6.Certificate.MixedSemantics.raw3067step2Labels line 3896
1066. def OAI.MUB6.Certificate.MixedSemantics.raw3067step3 line 3898
1067. def OAI.MUB6.Certificate.MixedSemantics.raw3067step3Labels line 3899
1068. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3067 line 3901
1069. def OAI.MUB6.Certificate.MixedSemantics.raw3068 line 3929
1070. def OAI.MUB6.Certificate.MixedSemantics.raw3068Labels line 3930
1071. def OAI.MUB6.Certificate.MixedSemantics.raw3068step0 line 3932
1072. def OAI.MUB6.Certificate.MixedSemantics.raw3068step0Labels line 3933
1073. def OAI.MUB6.Certificate.MixedSemantics.raw3068step1 line 3935
1074. def OAI.MUB6.Certificate.MixedSemantics.raw3068step1Labels line 3936
1075. def OAI.MUB6.Certificate.MixedSemantics.raw3068step2 line 3938
1076. def OAI.MUB6.Certificate.MixedSemantics.raw3068step2Labels line 3939
1077. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3068 line 3941
1078. def OAI.MUB6.Certificate.MixedSemantics.raw3069 line 3963
1079. def OAI.MUB6.Certificate.MixedSemantics.raw3069Labels line 3964
1080. def OAI.MUB6.Certificate.MixedSemantics.raw3069step0 line 3966
1081. def OAI.MUB6.Certificate.MixedSemantics.raw3069step0Labels line 3967
1082. def OAI.MUB6.Certificate.MixedSemantics.raw3069step1 line 3969
1083. def OAI.MUB6.Certificate.MixedSemantics.raw3069step1Labels line 3970
1084. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3069 line 3972
1085. def OAI.MUB6.Certificate.MixedSemantics.raw3070 line 3988
1086. def OAI.MUB6.Certificate.MixedSemantics.raw3070Labels line 3989
1087. def OAI.MUB6.Certificate.MixedSemantics.raw3070step0 line 3991
1088. def OAI.MUB6.Certificate.MixedSemantics.raw3070step0Labels line 3992
1089. def OAI.MUB6.Certificate.MixedSemantics.raw3070step1 line 3994
1090. def OAI.MUB6.Certificate.MixedSemantics.raw3070step1Labels line 3995
1091. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3070 line 3997
1092. def OAI.MUB6.Certificate.MixedSemantics.raw3071 line 4013
1093. def OAI.MUB6.Certificate.MixedSemantics.raw3071Labels line 4014
1094. def OAI.MUB6.Certificate.MixedSemantics.raw3071step0 line 4016
1095. def OAI.MUB6.Certificate.MixedSemantics.raw3071step0Labels line 4017
1096. theorem OAI.MUB6.Certificate.MixedSemantics.canonical3071 line 4019