OAI/Analysis/MutuallyUnbiased/GramEntries/Block4Data.lean

GitHub source file

254 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramEntries.Block4.entry0_0 line 33
2. def OAI.MUB6.Certificate.GramEntries.Block4.entry1_0 line 35
3. def OAI.MUB6.Certificate.GramEntries.Block4.entry1_1 line 37
4. def OAI.MUB6.Certificate.GramEntries.Block4.entry2_0 line 39
5. def OAI.MUB6.Certificate.GramEntries.Block4.entry2_1 line 41
6. def OAI.MUB6.Certificate.GramEntries.Block4.entry2_2 line 43
7. def OAI.MUB6.Certificate.GramEntries.Block4.entry3_0 line 45
8. def OAI.MUB6.Certificate.GramEntries.Block4.entry3_1 line 47
9. def OAI.MUB6.Certificate.GramEntries.Block4.entry3_2 line 49
10. def OAI.MUB6.Certificate.GramEntries.Block4.entry3_3 line 51
11. def OAI.MUB6.Certificate.GramEntries.Block4.entry4_0 line 53
12. def OAI.MUB6.Certificate.GramEntries.Block4.entry4_1 line 55
13. def OAI.MUB6.Certificate.GramEntries.Block4.entry4_2 line 57
14. def OAI.MUB6.Certificate.GramEntries.Block4.entry4_3 line 59
15. def OAI.MUB6.Certificate.GramEntries.Block4.entry4_4 line 61
16. def OAI.MUB6.Certificate.GramEntries.Block4.entry5_0 line 63
17. def OAI.MUB6.Certificate.GramEntries.Block4.entry5_1 line 65
18. def OAI.MUB6.Certificate.GramEntries.Block4.entry5_2 line 67
19. def OAI.MUB6.Certificate.GramEntries.Block4.entry5_3 line 69
20. def OAI.MUB6.Certificate.GramEntries.Block4.entry5_4 line 71
21. def OAI.MUB6.Certificate.GramEntries.Block4.entry5_5 line 73
22. def OAI.MUB6.Certificate.GramEntries.Block4.entry6_0 line 75
23. def OAI.MUB6.Certificate.GramEntries.Block4.entry6_1 line 77
24. def OAI.MUB6.Certificate.GramEntries.Block4.entry6_2 line 79
25. def OAI.MUB6.Certificate.GramEntries.Block4.entry6_3 line 81
26. def OAI.MUB6.Certificate.GramEntries.Block4.entry6_4 line 83
27. def OAI.MUB6.Certificate.GramEntries.Block4.entry6_5 line 85
28. def OAI.MUB6.Certificate.GramEntries.Block4.entry6_6 line 87
29. def OAI.MUB6.Certificate.GramEntries.Block4.entry7_0 line 89
30. def OAI.MUB6.Certificate.GramEntries.Block4.entry7_1 line 91
31. def OAI.MUB6.Certificate.GramEntries.Block4.entry7_2 line 93
32. def OAI.MUB6.Certificate.GramEntries.Block4.entry7_3 line 95
33. def OAI.MUB6.Certificate.GramEntries.Block4.entry7_4 line 97
34. def OAI.MUB6.Certificate.GramEntries.Block4.entry7_5 line 99
35. def OAI.MUB6.Certificate.GramEntries.Block4.entry7_6 line 101
36. def OAI.MUB6.Certificate.GramEntries.Block4.entry7_7 line 103
37. def OAI.MUB6.Certificate.GramEntries.Block4.entry8_0 line 105
38. def OAI.MUB6.Certificate.GramEntries.Block4.entry8_1 line 107
39. def OAI.MUB6.Certificate.GramEntries.Block4.entry8_2 line 109
40. def OAI.MUB6.Certificate.GramEntries.Block4.entry8_3 line 111
41. def OAI.MUB6.Certificate.GramEntries.Block4.entry8_4 line 113
42. def OAI.MUB6.Certificate.GramEntries.Block4.entry8_5 line 115
43. def OAI.MUB6.Certificate.GramEntries.Block4.entry8_6 line 117
44. def OAI.MUB6.Certificate.GramEntries.Block4.entry8_7 line 119
45. def OAI.MUB6.Certificate.GramEntries.Block4.entry8_8 line 121
46. def OAI.MUB6.Certificate.GramEntries.Block4.entry9_0 line 123
47. def OAI.MUB6.Certificate.GramEntries.Block4.entry9_1 line 125
48. def OAI.MUB6.Certificate.GramEntries.Block4.entry9_2 line 127
49. def OAI.MUB6.Certificate.GramEntries.Block4.entry9_3 line 129
50. def OAI.MUB6.Certificate.GramEntries.Block4.entry9_4 line 131
51. def OAI.MUB6.Certificate.GramEntries.Block4.entry9_5 line 133
52. def OAI.MUB6.Certificate.GramEntries.Block4.entry9_6 line 135
53. def OAI.MUB6.Certificate.GramEntries.Block4.entry9_7 line 137
54. def OAI.MUB6.Certificate.GramEntries.Block4.entry9_8 line 139
55. def OAI.MUB6.Certificate.GramEntries.Block4.entry9_9 line 141
56. def OAI.MUB6.Certificate.GramEntries.Block4.entry10_0 line 143
57. def OAI.MUB6.Certificate.GramEntries.Block4.entry10_1 line 145
58. def OAI.MUB6.Certificate.GramEntries.Block4.entry10_2 line 147
59. def OAI.MUB6.Certificate.GramEntries.Block4.entry10_3 line 149
60. def OAI.MUB6.Certificate.GramEntries.Block4.entry10_4 line 151
61. def OAI.MUB6.Certificate.GramEntries.Block4.entry10_5 line 153
62. def OAI.MUB6.Certificate.GramEntries.Block4.entry10_6 line 155
63. def OAI.MUB6.Certificate.GramEntries.Block4.entry10_7 line 157
64. def OAI.MUB6.Certificate.GramEntries.Block4.entry10_8 line 159
65. def OAI.MUB6.Certificate.GramEntries.Block4.entry10_9 line 161
66. def OAI.MUB6.Certificate.GramEntries.Block4.entry10_10 line 163
67. def OAI.MUB6.Certificate.GramEntries.Block4.entry11_0 line 165
68. def OAI.MUB6.Certificate.GramEntries.Block4.entry11_1 line 167
69. def OAI.MUB6.Certificate.GramEntries.Block4.entry11_2 line 169
70. def OAI.MUB6.Certificate.GramEntries.Block4.entry11_3 line 171
71. def OAI.MUB6.Certificate.GramEntries.Block4.entry11_4 line 173
72. def OAI.MUB6.Certificate.GramEntries.Block4.entry11_5 line 175
73. def OAI.MUB6.Certificate.GramEntries.Block4.entry11_6 line 177
74. def OAI.MUB6.Certificate.GramEntries.Block4.entry11_7 line 179
75. def OAI.MUB6.Certificate.GramEntries.Block4.entry11_8 line 181
76. def OAI.MUB6.Certificate.GramEntries.Block4.entry11_9 line 183
77. def OAI.MUB6.Certificate.GramEntries.Block4.entry11_10 line 185
78. def OAI.MUB6.Certificate.GramEntries.Block4.entry11_11 line 187
79. def OAI.MUB6.Certificate.GramEntries.Block4.entry12_0 line 189
80. def OAI.MUB6.Certificate.GramEntries.Block4.entry12_1 line 191
81. def OAI.MUB6.Certificate.GramEntries.Block4.entry12_2 line 193
82. def OAI.MUB6.Certificate.GramEntries.Block4.entry12_3 line 195
83. def OAI.MUB6.Certificate.GramEntries.Block4.entry12_4 line 197
84. def OAI.MUB6.Certificate.GramEntries.Block4.entry12_5 line 199
85. def OAI.MUB6.Certificate.GramEntries.Block4.entry12_6 line 201
86. def OAI.MUB6.Certificate.GramEntries.Block4.entry12_7 line 203
87. def OAI.MUB6.Certificate.GramEntries.Block4.entry12_8 line 205
88. def OAI.MUB6.Certificate.GramEntries.Block4.entry12_9 line 207
89. def OAI.MUB6.Certificate.GramEntries.Block4.entry12_10 line 209
90. def OAI.MUB6.Certificate.GramEntries.Block4.entry12_11 line 211
91. def OAI.MUB6.Certificate.GramEntries.Block4.entry12_12 line 213
92. def OAI.MUB6.Certificate.GramEntries.Block4.entry13_0 line 215
93. def OAI.MUB6.Certificate.GramEntries.Block4.entry13_1 line 217
94. def OAI.MUB6.Certificate.GramEntries.Block4.entry13_2 line 219
95. def OAI.MUB6.Certificate.GramEntries.Block4.entry13_3 line 221
96. def OAI.MUB6.Certificate.GramEntries.Block4.entry13_4 line 223
97. def OAI.MUB6.Certificate.GramEntries.Block4.entry13_5 line 225
98. def OAI.MUB6.Certificate.GramEntries.Block4.entry13_6 line 227
99. def OAI.MUB6.Certificate.GramEntries.Block4.entry13_7 line 229
100. def OAI.MUB6.Certificate.GramEntries.Block4.entry13_8 line 231
101. def OAI.MUB6.Certificate.GramEntries.Block4.entry13_9 line 233
102. def OAI.MUB6.Certificate.GramEntries.Block4.entry13_10 line 235
103. def OAI.MUB6.Certificate.GramEntries.Block4.entry13_11 line 237
104. def OAI.MUB6.Certificate.GramEntries.Block4.entry13_12 line 239
105. def OAI.MUB6.Certificate.GramEntries.Block4.entry13_13 line 241
106. def OAI.MUB6.Certificate.GramEntries.Block4.entry14_0 line 243
107. def OAI.MUB6.Certificate.GramEntries.Block4.entry14_1 line 245
108. def OAI.MUB6.Certificate.GramEntries.Block4.entry14_2 line 247
109. def OAI.MUB6.Certificate.GramEntries.Block4.entry14_3 line 249
110. def OAI.MUB6.Certificate.GramEntries.Block4.entry14_4 line 251
111. def OAI.MUB6.Certificate.GramEntries.Block4.entry14_5 line 253
112. def OAI.MUB6.Certificate.GramEntries.Block4.entry14_6 line 255
113. def OAI.MUB6.Certificate.GramEntries.Block4.entry14_7 line 257
114. def OAI.MUB6.Certificate.GramEntries.Block4.entry14_8 line 259
115. def OAI.MUB6.Certificate.GramEntries.Block4.entry14_9 line 261
116. def OAI.MUB6.Certificate.GramEntries.Block4.entry14_10 line 263
117. def OAI.MUB6.Certificate.GramEntries.Block4.entry14_11 line 265
118. def OAI.MUB6.Certificate.GramEntries.Block4.entry14_12 line 267
119. def OAI.MUB6.Certificate.GramEntries.Block4.entry14_13 line 269
120. def OAI.MUB6.Certificate.GramEntries.Block4.entry14_14 line 271
121. def OAI.MUB6.Certificate.GramEntries.Block4.entry15_0 line 273
122. def OAI.MUB6.Certificate.GramEntries.Block4.entry15_1 line 275
123. def OAI.MUB6.Certificate.GramEntries.Block4.entry15_2 line 277
124. def OAI.MUB6.Certificate.GramEntries.Block4.entry15_3 line 279
125. def OAI.MUB6.Certificate.GramEntries.Block4.entry15_4 line 281
126. def OAI.MUB6.Certificate.GramEntries.Block4.entry15_5 line 283
127. def OAI.MUB6.Certificate.GramEntries.Block4.entry15_6 line 285
128. def OAI.MUB6.Certificate.GramEntries.Block4.entry15_7 line 287
129. def OAI.MUB6.Certificate.GramEntries.Block4.entry15_8 line 289
130. def OAI.MUB6.Certificate.GramEntries.Block4.entry15_9 line 291
131. def OAI.MUB6.Certificate.GramEntries.Block4.entry15_10 line 293
132. def OAI.MUB6.Certificate.GramEntries.Block4.entry15_11 line 295
133. def OAI.MUB6.Certificate.GramEntries.Block4.entry15_12 line 297
134. def OAI.MUB6.Certificate.GramEntries.Block4.entry15_13 line 299
135. def OAI.MUB6.Certificate.GramEntries.Block4.entry15_14 line 301
136. def OAI.MUB6.Certificate.GramEntries.Block4.entry15_15 line 303
137. def OAI.MUB6.Certificate.GramEntries.Block4.entry16_0 line 305
138. def OAI.MUB6.Certificate.GramEntries.Block4.entry16_1 line 307
139. def OAI.MUB6.Certificate.GramEntries.Block4.entry16_2 line 309
140. def OAI.MUB6.Certificate.GramEntries.Block4.entry16_3 line 311
141. def OAI.MUB6.Certificate.GramEntries.Block4.entry16_4 line 313
142. def OAI.MUB6.Certificate.GramEntries.Block4.entry16_5 line 315
143. def OAI.MUB6.Certificate.GramEntries.Block4.entry16_6 line 317
144. def OAI.MUB6.Certificate.GramEntries.Block4.entry16_7 line 319
145. def OAI.MUB6.Certificate.GramEntries.Block4.entry16_8 line 321
146. def OAI.MUB6.Certificate.GramEntries.Block4.entry16_9 line 323
147. def OAI.MUB6.Certificate.GramEntries.Block4.entry16_10 line 325
148. def OAI.MUB6.Certificate.GramEntries.Block4.entry16_11 line 327
149. def OAI.MUB6.Certificate.GramEntries.Block4.entry16_12 line 329
150. def OAI.MUB6.Certificate.GramEntries.Block4.entry16_13 line 331
151. def OAI.MUB6.Certificate.GramEntries.Block4.entry16_14 line 333
152. def OAI.MUB6.Certificate.GramEntries.Block4.entry16_15 line 335
153. def OAI.MUB6.Certificate.GramEntries.Block4.entry16_16 line 337
154. def OAI.MUB6.Certificate.GramEntries.Block4.entry17_0 line 339
155. def OAI.MUB6.Certificate.GramEntries.Block4.entry17_1 line 341
156. def OAI.MUB6.Certificate.GramEntries.Block4.entry17_2 line 343
157. def OAI.MUB6.Certificate.GramEntries.Block4.entry17_3 line 345
158. def OAI.MUB6.Certificate.GramEntries.Block4.entry17_4 line 347
159. def OAI.MUB6.Certificate.GramEntries.Block4.entry17_5 line 349
160. def OAI.MUB6.Certificate.GramEntries.Block4.entry17_6 line 351
161. def OAI.MUB6.Certificate.GramEntries.Block4.entry17_7 line 353
162. def OAI.MUB6.Certificate.GramEntries.Block4.entry17_8 line 355
163. def OAI.MUB6.Certificate.GramEntries.Block4.entry17_9 line 357
164. def OAI.MUB6.Certificate.GramEntries.Block4.entry17_10 line 359
165. def OAI.MUB6.Certificate.GramEntries.Block4.entry17_11 line 361
166. def OAI.MUB6.Certificate.GramEntries.Block4.entry17_12 line 363
167. def OAI.MUB6.Certificate.GramEntries.Block4.entry17_13 line 365
168. def OAI.MUB6.Certificate.GramEntries.Block4.entry17_14 line 367
169. def OAI.MUB6.Certificate.GramEntries.Block4.entry17_15 line 369
170. def OAI.MUB6.Certificate.GramEntries.Block4.entry17_16 line 371
171. def OAI.MUB6.Certificate.GramEntries.Block4.entry17_17 line 373
172. def OAI.MUB6.Certificate.GramEntries.Block4.entry18_0 line 375
173. def OAI.MUB6.Certificate.GramEntries.Block4.entry18_1 line 377
174. def OAI.MUB6.Certificate.GramEntries.Block4.entry18_2 line 379
175. def OAI.MUB6.Certificate.GramEntries.Block4.entry18_3 line 381
176. def OAI.MUB6.Certificate.GramEntries.Block4.entry18_4 line 383
177. def OAI.MUB6.Certificate.GramEntries.Block4.entry18_5 line 385
178. def OAI.MUB6.Certificate.GramEntries.Block4.entry18_6 line 387
179. def OAI.MUB6.Certificate.GramEntries.Block4.entry18_7 line 389
180. def OAI.MUB6.Certificate.GramEntries.Block4.entry18_8 line 391
181. def OAI.MUB6.Certificate.GramEntries.Block4.entry18_9 line 393
182. def OAI.MUB6.Certificate.GramEntries.Block4.entry18_10 line 395
183. def OAI.MUB6.Certificate.GramEntries.Block4.entry18_11 line 397
184. def OAI.MUB6.Certificate.GramEntries.Block4.entry18_12 line 399
185. def OAI.MUB6.Certificate.GramEntries.Block4.entry18_13 line 401
186. def OAI.MUB6.Certificate.GramEntries.Block4.entry18_14 line 403
187. def OAI.MUB6.Certificate.GramEntries.Block4.entry18_15 line 405
188. def OAI.MUB6.Certificate.GramEntries.Block4.entry18_16 line 407
189. def OAI.MUB6.Certificate.GramEntries.Block4.entry18_17 line 409
190. def OAI.MUB6.Certificate.GramEntries.Block4.entry18_18 line 411
191. def OAI.MUB6.Certificate.GramEntries.Block4.entry19_0 line 413
192. def OAI.MUB6.Certificate.GramEntries.Block4.entry19_1 line 415
193. def OAI.MUB6.Certificate.GramEntries.Block4.entry19_2 line 417
194. def OAI.MUB6.Certificate.GramEntries.Block4.entry19_3 line 419
195. def OAI.MUB6.Certificate.GramEntries.Block4.entry19_4 line 421
196. def OAI.MUB6.Certificate.GramEntries.Block4.entry19_5 line 423
197. def OAI.MUB6.Certificate.GramEntries.Block4.entry19_6 line 425
198. def OAI.MUB6.Certificate.GramEntries.Block4.entry19_7 line 427
199. def OAI.MUB6.Certificate.GramEntries.Block4.entry19_8 line 429
200. def OAI.MUB6.Certificate.GramEntries.Block4.entry19_9 line 431
201. def OAI.MUB6.Certificate.GramEntries.Block4.entry19_10 line 433
202. def OAI.MUB6.Certificate.GramEntries.Block4.entry19_11 line 435
203. def OAI.MUB6.Certificate.GramEntries.Block4.entry19_12 line 437
204. def OAI.MUB6.Certificate.GramEntries.Block4.entry19_13 line 439
205. def OAI.MUB6.Certificate.GramEntries.Block4.entry19_14 line 441
206. def OAI.MUB6.Certificate.GramEntries.Block4.entry19_15 line 443
207. def OAI.MUB6.Certificate.GramEntries.Block4.entry19_16 line 445
208. def OAI.MUB6.Certificate.GramEntries.Block4.entry19_17 line 447
209. def OAI.MUB6.Certificate.GramEntries.Block4.entry19_18 line 449
210. def OAI.MUB6.Certificate.GramEntries.Block4.entry19_19 line 451
211. def OAI.MUB6.Certificate.GramEntries.Block4.entry20_0 line 453
212. def OAI.MUB6.Certificate.GramEntries.Block4.entry20_1 line 455
213. def OAI.MUB6.Certificate.GramEntries.Block4.entry20_2 line 457
214. def OAI.MUB6.Certificate.GramEntries.Block4.entry20_3 line 459
215. def OAI.MUB6.Certificate.GramEntries.Block4.entry20_4 line 461
216. def OAI.MUB6.Certificate.GramEntries.Block4.entry20_5 line 463
217. def OAI.MUB6.Certificate.GramEntries.Block4.entry20_6 line 465
218. def OAI.MUB6.Certificate.GramEntries.Block4.entry20_7 line 467
219. def OAI.MUB6.Certificate.GramEntries.Block4.entry20_8 line 469
220. def OAI.MUB6.Certificate.GramEntries.Block4.entry20_9 line 471
221. def OAI.MUB6.Certificate.GramEntries.Block4.entry20_10 line 473
222. def OAI.MUB6.Certificate.GramEntries.Block4.entry20_11 line 475
223. def OAI.MUB6.Certificate.GramEntries.Block4.entry20_12 line 477
224. def OAI.MUB6.Certificate.GramEntries.Block4.entry20_13 line 479
225. def OAI.MUB6.Certificate.GramEntries.Block4.entry20_14 line 481
226. def OAI.MUB6.Certificate.GramEntries.Block4.entry20_15 line 483
227. def OAI.MUB6.Certificate.GramEntries.Block4.entry20_16 line 485
228. def OAI.MUB6.Certificate.GramEntries.Block4.entry20_17 line 487
229. def OAI.MUB6.Certificate.GramEntries.Block4.entry20_18 line 489
230. def OAI.MUB6.Certificate.GramEntries.Block4.entry20_19 line 491
231. def OAI.MUB6.Certificate.GramEntries.Block4.entry20_20 line 493
232. def OAI.MUB6.Certificate.GramEntries.Block4.entry21_0 line 495
233. def OAI.MUB6.Certificate.GramEntries.Block4.entry21_1 line 497
234. def OAI.MUB6.Certificate.GramEntries.Block4.entry21_2 line 499
235. def OAI.MUB6.Certificate.GramEntries.Block4.entry21_3 line 501
236. def OAI.MUB6.Certificate.GramEntries.Block4.entry21_4 line 503
237. def OAI.MUB6.Certificate.GramEntries.Block4.entry21_5 line 505
238. def OAI.MUB6.Certificate.GramEntries.Block4.entry21_6 line 507
239. def OAI.MUB6.Certificate.GramEntries.Block4.entry21_7 line 509
240. def OAI.MUB6.Certificate.GramEntries.Block4.entry21_8 line 511
241. def OAI.MUB6.Certificate.GramEntries.Block4.entry21_9 line 513
242. def OAI.MUB6.Certificate.GramEntries.Block4.entry21_10 line 515
243. def OAI.MUB6.Certificate.GramEntries.Block4.entry21_11 line 517
244. def OAI.MUB6.Certificate.GramEntries.Block4.entry21_12 line 519
245. def OAI.MUB6.Certificate.GramEntries.Block4.entry21_13 line 521
246. def OAI.MUB6.Certificate.GramEntries.Block4.entry21_14 line 523
247. def OAI.MUB6.Certificate.GramEntries.Block4.entry21_15 line 525
248. def OAI.MUB6.Certificate.GramEntries.Block4.entry21_16 line 527
249. def OAI.MUB6.Certificate.GramEntries.Block4.entry21_17 line 529
250. def OAI.MUB6.Certificate.GramEntries.Block4.entry21_18 line 531
251. def OAI.MUB6.Certificate.GramEntries.Block4.entry21_19 line 533
252. def OAI.MUB6.Certificate.GramEntries.Block4.entry21_20 line 535
253. def OAI.MUB6.Certificate.GramEntries.Block4.entry21_21 line 537
254. def OAI.MUB6.Certificate.GramEntries.Block4.entries line 539