OAI/Analysis/MutuallyUnbiased/GramData/Block1.lean

GitHub source file

468 declarations, 0 contain sorry, 0 declared as axioms

Exact integer matrix for λ = (1, 1, 3), m = 21, exponent = 13.

  1. def OAI.MUB6.Certificate.GramData.Block1.Z line 14
  2. def OAI.MUB6.Certificate.GramData.Block1.entries line 38
  3. def OAI.MUB6.Certificate.GramData.Block1.D line 62
  4. theorem OAI.MUB6.Certificate.GramData.Block1.pivot_0 line 64
  5. theorem OAI.MUB6.Certificate.GramData.Block1.pivot_1 line 66
  6. theorem OAI.MUB6.Certificate.GramData.Block1.pivot_2 line 68
  7. theorem OAI.MUB6.Certificate.GramData.Block1.pivot_3 line 70
  8. theorem OAI.MUB6.Certificate.GramData.Block1.pivot_4 line 72
  9. theorem OAI.MUB6.Certificate.GramData.Block1.pivot_5 line 74
  10. theorem OAI.MUB6.Certificate.GramData.Block1.pivot_6 line 76
  11. theorem OAI.MUB6.Certificate.GramData.Block1.pivot_7 line 78
  12. theorem OAI.MUB6.Certificate.GramData.Block1.pivot_8 line 80
  13. theorem OAI.MUB6.Certificate.GramData.Block1.pivot_9 line 82
  14. theorem OAI.MUB6.Certificate.GramData.Block1.pivot_10 line 84
  15. theorem OAI.MUB6.Certificate.GramData.Block1.pivot_11 line 86
  16. theorem OAI.MUB6.Certificate.GramData.Block1.pivot_12 line 88
  17. theorem OAI.MUB6.Certificate.GramData.Block1.pivot_13 line 90
  18. theorem OAI.MUB6.Certificate.GramData.Block1.pivot_14 line 92
  19. theorem OAI.MUB6.Certificate.GramData.Block1.pivot_15 line 94
  20. theorem OAI.MUB6.Certificate.GramData.Block1.pivot_16 line 96
  21. theorem OAI.MUB6.Certificate.GramData.Block1.pivot_17 line 98
  22. theorem OAI.MUB6.Certificate.GramData.Block1.pivot_18 line 100
  23. theorem OAI.MUB6.Certificate.GramData.Block1.pivot_19 line 102
  24. theorem OAI.MUB6.Certificate.GramData.Block1.pivot_20 line 104
  25. theorem OAI.MUB6.Certificate.GramData.Block1.entry_0_0 line 106
  26. theorem OAI.MUB6.Certificate.GramData.Block1.entry_0_1 line 110
  27. theorem OAI.MUB6.Certificate.GramData.Block1.entry_0_2 line 114
  28. theorem OAI.MUB6.Certificate.GramData.Block1.entry_0_3 line 118
  29. theorem OAI.MUB6.Certificate.GramData.Block1.entry_0_4 line 122
  30. theorem OAI.MUB6.Certificate.GramData.Block1.entry_0_5 line 126
  31. theorem OAI.MUB6.Certificate.GramData.Block1.entry_0_6 line 130
  32. theorem OAI.MUB6.Certificate.GramData.Block1.entry_0_7 line 134
  33. theorem OAI.MUB6.Certificate.GramData.Block1.entry_0_8 line 138
  34. theorem OAI.MUB6.Certificate.GramData.Block1.entry_0_9 line 142
  35. theorem OAI.MUB6.Certificate.GramData.Block1.entry_0_10 line 146
  36. theorem OAI.MUB6.Certificate.GramData.Block1.entry_0_11 line 150
  37. theorem OAI.MUB6.Certificate.GramData.Block1.entry_0_12 line 154
  38. theorem OAI.MUB6.Certificate.GramData.Block1.entry_0_13 line 158
  39. theorem OAI.MUB6.Certificate.GramData.Block1.entry_0_14 line 162
  40. theorem OAI.MUB6.Certificate.GramData.Block1.entry_0_15 line 166
  41. theorem OAI.MUB6.Certificate.GramData.Block1.entry_0_16 line 170
  42. theorem OAI.MUB6.Certificate.GramData.Block1.entry_0_17 line 174
  43. theorem OAI.MUB6.Certificate.GramData.Block1.entry_0_18 line 178
  44. theorem OAI.MUB6.Certificate.GramData.Block1.entry_0_19 line 182
  45. theorem OAI.MUB6.Certificate.GramData.Block1.entry_0_20 line 186
  46. theorem OAI.MUB6.Certificate.GramData.Block1.entry_1_0 line 190
  47. theorem OAI.MUB6.Certificate.GramData.Block1.entry_1_1 line 194
  48. theorem OAI.MUB6.Certificate.GramData.Block1.entry_1_2 line 198
  49. theorem OAI.MUB6.Certificate.GramData.Block1.entry_1_3 line 202
  50. theorem OAI.MUB6.Certificate.GramData.Block1.entry_1_4 line 206
  51. theorem OAI.MUB6.Certificate.GramData.Block1.entry_1_5 line 210
  52. theorem OAI.MUB6.Certificate.GramData.Block1.entry_1_6 line 214
  53. theorem OAI.MUB6.Certificate.GramData.Block1.entry_1_7 line 218
  54. theorem OAI.MUB6.Certificate.GramData.Block1.entry_1_8 line 222
  55. theorem OAI.MUB6.Certificate.GramData.Block1.entry_1_9 line 226
  56. theorem OAI.MUB6.Certificate.GramData.Block1.entry_1_10 line 230
  57. theorem OAI.MUB6.Certificate.GramData.Block1.entry_1_11 line 234
  58. theorem OAI.MUB6.Certificate.GramData.Block1.entry_1_12 line 238
  59. theorem OAI.MUB6.Certificate.GramData.Block1.entry_1_13 line 242
  60. theorem OAI.MUB6.Certificate.GramData.Block1.entry_1_14 line 246
  61. theorem OAI.MUB6.Certificate.GramData.Block1.entry_1_15 line 250
  62. theorem OAI.MUB6.Certificate.GramData.Block1.entry_1_16 line 254
  63. theorem OAI.MUB6.Certificate.GramData.Block1.entry_1_17 line 258
  64. theorem OAI.MUB6.Certificate.GramData.Block1.entry_1_18 line 262
  65. theorem OAI.MUB6.Certificate.GramData.Block1.entry_1_19 line 266
  66. theorem OAI.MUB6.Certificate.GramData.Block1.entry_1_20 line 270
  67. theorem OAI.MUB6.Certificate.GramData.Block1.entry_2_0 line 274
  68. theorem OAI.MUB6.Certificate.GramData.Block1.entry_2_1 line 278
  69. theorem OAI.MUB6.Certificate.GramData.Block1.entry_2_2 line 282
  70. theorem OAI.MUB6.Certificate.GramData.Block1.entry_2_3 line 286
  71. theorem OAI.MUB6.Certificate.GramData.Block1.entry_2_4 line 290
  72. theorem OAI.MUB6.Certificate.GramData.Block1.entry_2_5 line 294
  73. theorem OAI.MUB6.Certificate.GramData.Block1.entry_2_6 line 298
  74. theorem OAI.MUB6.Certificate.GramData.Block1.entry_2_7 line 302
  75. theorem OAI.MUB6.Certificate.GramData.Block1.entry_2_8 line 306
  76. theorem OAI.MUB6.Certificate.GramData.Block1.entry_2_9 line 310
  77. theorem OAI.MUB6.Certificate.GramData.Block1.entry_2_10 line 314
  78. theorem OAI.MUB6.Certificate.GramData.Block1.entry_2_11 line 318
  79. theorem OAI.MUB6.Certificate.GramData.Block1.entry_2_12 line 322
  80. theorem OAI.MUB6.Certificate.GramData.Block1.entry_2_13 line 326
  81. theorem OAI.MUB6.Certificate.GramData.Block1.entry_2_14 line 330
  82. theorem OAI.MUB6.Certificate.GramData.Block1.entry_2_15 line 334
  83. theorem OAI.MUB6.Certificate.GramData.Block1.entry_2_16 line 338
  84. theorem OAI.MUB6.Certificate.GramData.Block1.entry_2_17 line 342
  85. theorem OAI.MUB6.Certificate.GramData.Block1.entry_2_18 line 346
  86. theorem OAI.MUB6.Certificate.GramData.Block1.entry_2_19 line 350
  87. theorem OAI.MUB6.Certificate.GramData.Block1.entry_2_20 line 354
  88. theorem OAI.MUB6.Certificate.GramData.Block1.entry_3_0 line 358
  89. theorem OAI.MUB6.Certificate.GramData.Block1.entry_3_1 line 362
  90. theorem OAI.MUB6.Certificate.GramData.Block1.entry_3_2 line 366
  91. theorem OAI.MUB6.Certificate.GramData.Block1.entry_3_3 line 370
  92. theorem OAI.MUB6.Certificate.GramData.Block1.entry_3_4 line 374
  93. theorem OAI.MUB6.Certificate.GramData.Block1.entry_3_5 line 378
  94. theorem OAI.MUB6.Certificate.GramData.Block1.entry_3_6 line 382
  95. theorem OAI.MUB6.Certificate.GramData.Block1.entry_3_7 line 386
  96. theorem OAI.MUB6.Certificate.GramData.Block1.entry_3_8 line 390
  97. theorem OAI.MUB6.Certificate.GramData.Block1.entry_3_9 line 394
  98. theorem OAI.MUB6.Certificate.GramData.Block1.entry_3_10 line 398
  99. theorem OAI.MUB6.Certificate.GramData.Block1.entry_3_11 line 402
  100. theorem OAI.MUB6.Certificate.GramData.Block1.entry_3_12 line 406
  101. theorem OAI.MUB6.Certificate.GramData.Block1.entry_3_13 line 410
  102. theorem OAI.MUB6.Certificate.GramData.Block1.entry_3_14 line 414
  103. theorem OAI.MUB6.Certificate.GramData.Block1.entry_3_15 line 418
  104. theorem OAI.MUB6.Certificate.GramData.Block1.entry_3_16 line 422
  105. theorem OAI.MUB6.Certificate.GramData.Block1.entry_3_17 line 426
  106. theorem OAI.MUB6.Certificate.GramData.Block1.entry_3_18 line 430
  107. theorem OAI.MUB6.Certificate.GramData.Block1.entry_3_19 line 434
  108. theorem OAI.MUB6.Certificate.GramData.Block1.entry_3_20 line 438
  109. theorem OAI.MUB6.Certificate.GramData.Block1.entry_4_0 line 442
  110. theorem OAI.MUB6.Certificate.GramData.Block1.entry_4_1 line 446
  111. theorem OAI.MUB6.Certificate.GramData.Block1.entry_4_2 line 450
  112. theorem OAI.MUB6.Certificate.GramData.Block1.entry_4_3 line 454
  113. theorem OAI.MUB6.Certificate.GramData.Block1.entry_4_4 line 458
  114. theorem OAI.MUB6.Certificate.GramData.Block1.entry_4_5 line 462
  115. theorem OAI.MUB6.Certificate.GramData.Block1.entry_4_6 line 466
  116. theorem OAI.MUB6.Certificate.GramData.Block1.entry_4_7 line 470
  117. theorem OAI.MUB6.Certificate.GramData.Block1.entry_4_8 line 474
  118. theorem OAI.MUB6.Certificate.GramData.Block1.entry_4_9 line 478
  119. theorem OAI.MUB6.Certificate.GramData.Block1.entry_4_10 line 482
  120. theorem OAI.MUB6.Certificate.GramData.Block1.entry_4_11 line 486
  121. theorem OAI.MUB6.Certificate.GramData.Block1.entry_4_12 line 490
  122. theorem OAI.MUB6.Certificate.GramData.Block1.entry_4_13 line 494
  123. theorem OAI.MUB6.Certificate.GramData.Block1.entry_4_14 line 498
  124. theorem OAI.MUB6.Certificate.GramData.Block1.entry_4_15 line 502
  125. theorem OAI.MUB6.Certificate.GramData.Block1.entry_4_16 line 506
  126. theorem OAI.MUB6.Certificate.GramData.Block1.entry_4_17 line 510
  127. theorem OAI.MUB6.Certificate.GramData.Block1.entry_4_18 line 514
  128. theorem OAI.MUB6.Certificate.GramData.Block1.entry_4_19 line 518
  129. theorem OAI.MUB6.Certificate.GramData.Block1.entry_4_20 line 522
  130. theorem OAI.MUB6.Certificate.GramData.Block1.entry_5_0 line 526
  131. theorem OAI.MUB6.Certificate.GramData.Block1.entry_5_1 line 530
  132. theorem OAI.MUB6.Certificate.GramData.Block1.entry_5_2 line 534
  133. theorem OAI.MUB6.Certificate.GramData.Block1.entry_5_3 line 538
  134. theorem OAI.MUB6.Certificate.GramData.Block1.entry_5_4 line 542
  135. theorem OAI.MUB6.Certificate.GramData.Block1.entry_5_5 line 546
  136. theorem OAI.MUB6.Certificate.GramData.Block1.entry_5_6 line 550
  137. theorem OAI.MUB6.Certificate.GramData.Block1.entry_5_7 line 554
  138. theorem OAI.MUB6.Certificate.GramData.Block1.entry_5_8 line 558
  139. theorem OAI.MUB6.Certificate.GramData.Block1.entry_5_9 line 562
  140. theorem OAI.MUB6.Certificate.GramData.Block1.entry_5_10 line 566
  141. theorem OAI.MUB6.Certificate.GramData.Block1.entry_5_11 line 570
  142. theorem OAI.MUB6.Certificate.GramData.Block1.entry_5_12 line 574
  143. theorem OAI.MUB6.Certificate.GramData.Block1.entry_5_13 line 578
  144. theorem OAI.MUB6.Certificate.GramData.Block1.entry_5_14 line 582
  145. theorem OAI.MUB6.Certificate.GramData.Block1.entry_5_15 line 586
  146. theorem OAI.MUB6.Certificate.GramData.Block1.entry_5_16 line 590
  147. theorem OAI.MUB6.Certificate.GramData.Block1.entry_5_17 line 594
  148. theorem OAI.MUB6.Certificate.GramData.Block1.entry_5_18 line 598
  149. theorem OAI.MUB6.Certificate.GramData.Block1.entry_5_19 line 602
  150. theorem OAI.MUB6.Certificate.GramData.Block1.entry_5_20 line 606
  151. theorem OAI.MUB6.Certificate.GramData.Block1.entry_6_0 line 610
  152. theorem OAI.MUB6.Certificate.GramData.Block1.entry_6_1 line 614
  153. theorem OAI.MUB6.Certificate.GramData.Block1.entry_6_2 line 618
  154. theorem OAI.MUB6.Certificate.GramData.Block1.entry_6_3 line 622
  155. theorem OAI.MUB6.Certificate.GramData.Block1.entry_6_4 line 626
  156. theorem OAI.MUB6.Certificate.GramData.Block1.entry_6_5 line 630
  157. theorem OAI.MUB6.Certificate.GramData.Block1.entry_6_6 line 634
  158. theorem OAI.MUB6.Certificate.GramData.Block1.entry_6_7 line 638
  159. theorem OAI.MUB6.Certificate.GramData.Block1.entry_6_8 line 642
  160. theorem OAI.MUB6.Certificate.GramData.Block1.entry_6_9 line 646
  161. theorem OAI.MUB6.Certificate.GramData.Block1.entry_6_10 line 650
  162. theorem OAI.MUB6.Certificate.GramData.Block1.entry_6_11 line 654
  163. theorem OAI.MUB6.Certificate.GramData.Block1.entry_6_12 line 658
  164. theorem OAI.MUB6.Certificate.GramData.Block1.entry_6_13 line 662
  165. theorem OAI.MUB6.Certificate.GramData.Block1.entry_6_14 line 666
  166. theorem OAI.MUB6.Certificate.GramData.Block1.entry_6_15 line 670
  167. theorem OAI.MUB6.Certificate.GramData.Block1.entry_6_16 line 674
  168. theorem OAI.MUB6.Certificate.GramData.Block1.entry_6_17 line 678
  169. theorem OAI.MUB6.Certificate.GramData.Block1.entry_6_18 line 682
  170. theorem OAI.MUB6.Certificate.GramData.Block1.entry_6_19 line 686
  171. theorem OAI.MUB6.Certificate.GramData.Block1.entry_6_20 line 690
  172. theorem OAI.MUB6.Certificate.GramData.Block1.entry_7_0 line 694
  173. theorem OAI.MUB6.Certificate.GramData.Block1.entry_7_1 line 698
  174. theorem OAI.MUB6.Certificate.GramData.Block1.entry_7_2 line 702
  175. theorem OAI.MUB6.Certificate.GramData.Block1.entry_7_3 line 706
  176. theorem OAI.MUB6.Certificate.GramData.Block1.entry_7_4 line 710
  177. theorem OAI.MUB6.Certificate.GramData.Block1.entry_7_5 line 714
  178. theorem OAI.MUB6.Certificate.GramData.Block1.entry_7_6 line 718
  179. theorem OAI.MUB6.Certificate.GramData.Block1.entry_7_7 line 722
  180. theorem OAI.MUB6.Certificate.GramData.Block1.entry_7_8 line 726
  181. theorem OAI.MUB6.Certificate.GramData.Block1.entry_7_9 line 730
  182. theorem OAI.MUB6.Certificate.GramData.Block1.entry_7_10 line 734
  183. theorem OAI.MUB6.Certificate.GramData.Block1.entry_7_11 line 738
  184. theorem OAI.MUB6.Certificate.GramData.Block1.entry_7_12 line 742
  185. theorem OAI.MUB6.Certificate.GramData.Block1.entry_7_13 line 746
  186. theorem OAI.MUB6.Certificate.GramData.Block1.entry_7_14 line 750
  187. theorem OAI.MUB6.Certificate.GramData.Block1.entry_7_15 line 754
  188. theorem OAI.MUB6.Certificate.GramData.Block1.entry_7_16 line 758
  189. theorem OAI.MUB6.Certificate.GramData.Block1.entry_7_17 line 762
  190. theorem OAI.MUB6.Certificate.GramData.Block1.entry_7_18 line 766
  191. theorem OAI.MUB6.Certificate.GramData.Block1.entry_7_19 line 770
  192. theorem OAI.MUB6.Certificate.GramData.Block1.entry_7_20 line 774
  193. theorem OAI.MUB6.Certificate.GramData.Block1.entry_8_0 line 778
  194. theorem OAI.MUB6.Certificate.GramData.Block1.entry_8_1 line 782
  195. theorem OAI.MUB6.Certificate.GramData.Block1.entry_8_2 line 786
  196. theorem OAI.MUB6.Certificate.GramData.Block1.entry_8_3 line 790
  197. theorem OAI.MUB6.Certificate.GramData.Block1.entry_8_4 line 794
  198. theorem OAI.MUB6.Certificate.GramData.Block1.entry_8_5 line 798
  199. theorem OAI.MUB6.Certificate.GramData.Block1.entry_8_6 line 802
  200. theorem OAI.MUB6.Certificate.GramData.Block1.entry_8_7 line 806
  201. theorem OAI.MUB6.Certificate.GramData.Block1.entry_8_8 line 810
  202. theorem OAI.MUB6.Certificate.GramData.Block1.entry_8_9 line 814
  203. theorem OAI.MUB6.Certificate.GramData.Block1.entry_8_10 line 818
  204. theorem OAI.MUB6.Certificate.GramData.Block1.entry_8_11 line 822
  205. theorem OAI.MUB6.Certificate.GramData.Block1.entry_8_12 line 826
  206. theorem OAI.MUB6.Certificate.GramData.Block1.entry_8_13 line 830
  207. theorem OAI.MUB6.Certificate.GramData.Block1.entry_8_14 line 834
  208. theorem OAI.MUB6.Certificate.GramData.Block1.entry_8_15 line 838
  209. theorem OAI.MUB6.Certificate.GramData.Block1.entry_8_16 line 842
  210. theorem OAI.MUB6.Certificate.GramData.Block1.entry_8_17 line 846
  211. theorem OAI.MUB6.Certificate.GramData.Block1.entry_8_18 line 850
  212. theorem OAI.MUB6.Certificate.GramData.Block1.entry_8_19 line 854
  213. theorem OAI.MUB6.Certificate.GramData.Block1.entry_8_20 line 858
  214. theorem OAI.MUB6.Certificate.GramData.Block1.entry_9_0 line 862
  215. theorem OAI.MUB6.Certificate.GramData.Block1.entry_9_1 line 866
  216. theorem OAI.MUB6.Certificate.GramData.Block1.entry_9_2 line 870
  217. theorem OAI.MUB6.Certificate.GramData.Block1.entry_9_3 line 874
  218. theorem OAI.MUB6.Certificate.GramData.Block1.entry_9_4 line 878
  219. theorem OAI.MUB6.Certificate.GramData.Block1.entry_9_5 line 882
  220. theorem OAI.MUB6.Certificate.GramData.Block1.entry_9_6 line 886
  221. theorem OAI.MUB6.Certificate.GramData.Block1.entry_9_7 line 890
  222. theorem OAI.MUB6.Certificate.GramData.Block1.entry_9_8 line 894
  223. theorem OAI.MUB6.Certificate.GramData.Block1.entry_9_9 line 898
  224. theorem OAI.MUB6.Certificate.GramData.Block1.entry_9_10 line 902
  225. theorem OAI.MUB6.Certificate.GramData.Block1.entry_9_11 line 906
  226. theorem OAI.MUB6.Certificate.GramData.Block1.entry_9_12 line 910
  227. theorem OAI.MUB6.Certificate.GramData.Block1.entry_9_13 line 914
  228. theorem OAI.MUB6.Certificate.GramData.Block1.entry_9_14 line 918
  229. theorem OAI.MUB6.Certificate.GramData.Block1.entry_9_15 line 922
  230. theorem OAI.MUB6.Certificate.GramData.Block1.entry_9_16 line 926
  231. theorem OAI.MUB6.Certificate.GramData.Block1.entry_9_17 line 930
  232. theorem OAI.MUB6.Certificate.GramData.Block1.entry_9_18 line 934
  233. theorem OAI.MUB6.Certificate.GramData.Block1.entry_9_19 line 938
  234. theorem OAI.MUB6.Certificate.GramData.Block1.entry_9_20 line 942
  235. theorem OAI.MUB6.Certificate.GramData.Block1.entry_10_0 line 946
  236. theorem OAI.MUB6.Certificate.GramData.Block1.entry_10_1 line 950
  237. theorem OAI.MUB6.Certificate.GramData.Block1.entry_10_2 line 954
  238. theorem OAI.MUB6.Certificate.GramData.Block1.entry_10_3 line 958
  239. theorem OAI.MUB6.Certificate.GramData.Block1.entry_10_4 line 962
  240. theorem OAI.MUB6.Certificate.GramData.Block1.entry_10_5 line 966
  241. theorem OAI.MUB6.Certificate.GramData.Block1.entry_10_6 line 970
  242. theorem OAI.MUB6.Certificate.GramData.Block1.entry_10_7 line 974
  243. theorem OAI.MUB6.Certificate.GramData.Block1.entry_10_8 line 978
  244. theorem OAI.MUB6.Certificate.GramData.Block1.entry_10_9 line 982
  245. theorem OAI.MUB6.Certificate.GramData.Block1.entry_10_10 line 986
  246. theorem OAI.MUB6.Certificate.GramData.Block1.entry_10_11 line 990
  247. theorem OAI.MUB6.Certificate.GramData.Block1.entry_10_12 line 994
  248. theorem OAI.MUB6.Certificate.GramData.Block1.entry_10_13 line 998
  249. theorem OAI.MUB6.Certificate.GramData.Block1.entry_10_14 line 1002
  250. theorem OAI.MUB6.Certificate.GramData.Block1.entry_10_15 line 1006
  251. theorem OAI.MUB6.Certificate.GramData.Block1.entry_10_16 line 1010
  252. theorem OAI.MUB6.Certificate.GramData.Block1.entry_10_17 line 1014
  253. theorem OAI.MUB6.Certificate.GramData.Block1.entry_10_18 line 1018
  254. theorem OAI.MUB6.Certificate.GramData.Block1.entry_10_19 line 1022
  255. theorem OAI.MUB6.Certificate.GramData.Block1.entry_10_20 line 1026
  256. theorem OAI.MUB6.Certificate.GramData.Block1.entry_11_0 line 1030
  257. theorem OAI.MUB6.Certificate.GramData.Block1.entry_11_1 line 1034
  258. theorem OAI.MUB6.Certificate.GramData.Block1.entry_11_2 line 1038
  259. theorem OAI.MUB6.Certificate.GramData.Block1.entry_11_3 line 1042
  260. theorem OAI.MUB6.Certificate.GramData.Block1.entry_11_4 line 1046
  261. theorem OAI.MUB6.Certificate.GramData.Block1.entry_11_5 line 1050
  262. theorem OAI.MUB6.Certificate.GramData.Block1.entry_11_6 line 1054
  263. theorem OAI.MUB6.Certificate.GramData.Block1.entry_11_7 line 1058
  264. theorem OAI.MUB6.Certificate.GramData.Block1.entry_11_8 line 1062
  265. theorem OAI.MUB6.Certificate.GramData.Block1.entry_11_9 line 1066
  266. theorem OAI.MUB6.Certificate.GramData.Block1.entry_11_10 line 1070
  267. theorem OAI.MUB6.Certificate.GramData.Block1.entry_11_11 line 1074
  268. theorem OAI.MUB6.Certificate.GramData.Block1.entry_11_12 line 1078
  269. theorem OAI.MUB6.Certificate.GramData.Block1.entry_11_13 line 1082
  270. theorem OAI.MUB6.Certificate.GramData.Block1.entry_11_14 line 1086
  271. theorem OAI.MUB6.Certificate.GramData.Block1.entry_11_15 line 1090
  272. theorem OAI.MUB6.Certificate.GramData.Block1.entry_11_16 line 1094
  273. theorem OAI.MUB6.Certificate.GramData.Block1.entry_11_17 line 1098
  274. theorem OAI.MUB6.Certificate.GramData.Block1.entry_11_18 line 1102
  275. theorem OAI.MUB6.Certificate.GramData.Block1.entry_11_19 line 1106
  276. theorem OAI.MUB6.Certificate.GramData.Block1.entry_11_20 line 1110
  277. theorem OAI.MUB6.Certificate.GramData.Block1.entry_12_0 line 1114
  278. theorem OAI.MUB6.Certificate.GramData.Block1.entry_12_1 line 1118
  279. theorem OAI.MUB6.Certificate.GramData.Block1.entry_12_2 line 1122
  280. theorem OAI.MUB6.Certificate.GramData.Block1.entry_12_3 line 1126
  281. theorem OAI.MUB6.Certificate.GramData.Block1.entry_12_4 line 1130
  282. theorem OAI.MUB6.Certificate.GramData.Block1.entry_12_5 line 1134
  283. theorem OAI.MUB6.Certificate.GramData.Block1.entry_12_6 line 1138
  284. theorem OAI.MUB6.Certificate.GramData.Block1.entry_12_7 line 1142
  285. theorem OAI.MUB6.Certificate.GramData.Block1.entry_12_8 line 1146
  286. theorem OAI.MUB6.Certificate.GramData.Block1.entry_12_9 line 1150
  287. theorem OAI.MUB6.Certificate.GramData.Block1.entry_12_10 line 1154
  288. theorem OAI.MUB6.Certificate.GramData.Block1.entry_12_11 line 1158
  289. theorem OAI.MUB6.Certificate.GramData.Block1.entry_12_12 line 1162
  290. theorem OAI.MUB6.Certificate.GramData.Block1.entry_12_13 line 1166
  291. theorem OAI.MUB6.Certificate.GramData.Block1.entry_12_14 line 1170
  292. theorem OAI.MUB6.Certificate.GramData.Block1.entry_12_15 line 1174
  293. theorem OAI.MUB6.Certificate.GramData.Block1.entry_12_16 line 1178
  294. theorem OAI.MUB6.Certificate.GramData.Block1.entry_12_17 line 1182
  295. theorem OAI.MUB6.Certificate.GramData.Block1.entry_12_18 line 1186
  296. theorem OAI.MUB6.Certificate.GramData.Block1.entry_12_19 line 1190
  297. theorem OAI.MUB6.Certificate.GramData.Block1.entry_12_20 line 1194
  298. theorem OAI.MUB6.Certificate.GramData.Block1.entry_13_0 line 1198
  299. theorem OAI.MUB6.Certificate.GramData.Block1.entry_13_1 line 1202
  300. theorem OAI.MUB6.Certificate.GramData.Block1.entry_13_2 line 1206
  301. theorem OAI.MUB6.Certificate.GramData.Block1.entry_13_3 line 1210
  302. theorem OAI.MUB6.Certificate.GramData.Block1.entry_13_4 line 1214
  303. theorem OAI.MUB6.Certificate.GramData.Block1.entry_13_5 line 1218
  304. theorem OAI.MUB6.Certificate.GramData.Block1.entry_13_6 line 1222
  305. theorem OAI.MUB6.Certificate.GramData.Block1.entry_13_7 line 1226
  306. theorem OAI.MUB6.Certificate.GramData.Block1.entry_13_8 line 1230
  307. theorem OAI.MUB6.Certificate.GramData.Block1.entry_13_9 line 1234
  308. theorem OAI.MUB6.Certificate.GramData.Block1.entry_13_10 line 1238
  309. theorem OAI.MUB6.Certificate.GramData.Block1.entry_13_11 line 1242
  310. theorem OAI.MUB6.Certificate.GramData.Block1.entry_13_12 line 1246
  311. theorem OAI.MUB6.Certificate.GramData.Block1.entry_13_13 line 1250
  312. theorem OAI.MUB6.Certificate.GramData.Block1.entry_13_14 line 1254
  313. theorem OAI.MUB6.Certificate.GramData.Block1.entry_13_15 line 1258
  314. theorem OAI.MUB6.Certificate.GramData.Block1.entry_13_16 line 1262
  315. theorem OAI.MUB6.Certificate.GramData.Block1.entry_13_17 line 1266
  316. theorem OAI.MUB6.Certificate.GramData.Block1.entry_13_18 line 1270
  317. theorem OAI.MUB6.Certificate.GramData.Block1.entry_13_19 line 1274
  318. theorem OAI.MUB6.Certificate.GramData.Block1.entry_13_20 line 1278
  319. theorem OAI.MUB6.Certificate.GramData.Block1.entry_14_0 line 1282
  320. theorem OAI.MUB6.Certificate.GramData.Block1.entry_14_1 line 1286
  321. theorem OAI.MUB6.Certificate.GramData.Block1.entry_14_2 line 1290
  322. theorem OAI.MUB6.Certificate.GramData.Block1.entry_14_3 line 1294
  323. theorem OAI.MUB6.Certificate.GramData.Block1.entry_14_4 line 1298
  324. theorem OAI.MUB6.Certificate.GramData.Block1.entry_14_5 line 1302
  325. theorem OAI.MUB6.Certificate.GramData.Block1.entry_14_6 line 1306
  326. theorem OAI.MUB6.Certificate.GramData.Block1.entry_14_7 line 1310
  327. theorem OAI.MUB6.Certificate.GramData.Block1.entry_14_8 line 1314
  328. theorem OAI.MUB6.Certificate.GramData.Block1.entry_14_9 line 1318
  329. theorem OAI.MUB6.Certificate.GramData.Block1.entry_14_10 line 1322
  330. theorem OAI.MUB6.Certificate.GramData.Block1.entry_14_11 line 1326
  331. theorem OAI.MUB6.Certificate.GramData.Block1.entry_14_12 line 1330
  332. theorem OAI.MUB6.Certificate.GramData.Block1.entry_14_13 line 1334
  333. theorem OAI.MUB6.Certificate.GramData.Block1.entry_14_14 line 1338
  334. theorem OAI.MUB6.Certificate.GramData.Block1.entry_14_15 line 1342
  335. theorem OAI.MUB6.Certificate.GramData.Block1.entry_14_16 line 1346
  336. theorem OAI.MUB6.Certificate.GramData.Block1.entry_14_17 line 1350
  337. theorem OAI.MUB6.Certificate.GramData.Block1.entry_14_18 line 1354
  338. theorem OAI.MUB6.Certificate.GramData.Block1.entry_14_19 line 1358
  339. theorem OAI.MUB6.Certificate.GramData.Block1.entry_14_20 line 1362
  340. theorem OAI.MUB6.Certificate.GramData.Block1.entry_15_0 line 1366
  341. theorem OAI.MUB6.Certificate.GramData.Block1.entry_15_1 line 1370
  342. theorem OAI.MUB6.Certificate.GramData.Block1.entry_15_2 line 1374
  343. theorem OAI.MUB6.Certificate.GramData.Block1.entry_15_3 line 1378
  344. theorem OAI.MUB6.Certificate.GramData.Block1.entry_15_4 line 1382
  345. theorem OAI.MUB6.Certificate.GramData.Block1.entry_15_5 line 1386
  346. theorem OAI.MUB6.Certificate.GramData.Block1.entry_15_6 line 1390
  347. theorem OAI.MUB6.Certificate.GramData.Block1.entry_15_7 line 1394
  348. theorem OAI.MUB6.Certificate.GramData.Block1.entry_15_8 line 1398
  349. theorem OAI.MUB6.Certificate.GramData.Block1.entry_15_9 line 1402
  350. theorem OAI.MUB6.Certificate.GramData.Block1.entry_15_10 line 1406
  351. theorem OAI.MUB6.Certificate.GramData.Block1.entry_15_11 line 1410
  352. theorem OAI.MUB6.Certificate.GramData.Block1.entry_15_12 line 1414
  353. theorem OAI.MUB6.Certificate.GramData.Block1.entry_15_13 line 1418
  354. theorem OAI.MUB6.Certificate.GramData.Block1.entry_15_14 line 1422
  355. theorem OAI.MUB6.Certificate.GramData.Block1.entry_15_15 line 1426
  356. theorem OAI.MUB6.Certificate.GramData.Block1.entry_15_16 line 1430
  357. theorem OAI.MUB6.Certificate.GramData.Block1.entry_15_17 line 1434
  358. theorem OAI.MUB6.Certificate.GramData.Block1.entry_15_18 line 1438
  359. theorem OAI.MUB6.Certificate.GramData.Block1.entry_15_19 line 1442
  360. theorem OAI.MUB6.Certificate.GramData.Block1.entry_15_20 line 1446
  361. theorem OAI.MUB6.Certificate.GramData.Block1.entry_16_0 line 1450
  362. theorem OAI.MUB6.Certificate.GramData.Block1.entry_16_1 line 1454
  363. theorem OAI.MUB6.Certificate.GramData.Block1.entry_16_2 line 1458
  364. theorem OAI.MUB6.Certificate.GramData.Block1.entry_16_3 line 1462
  365. theorem OAI.MUB6.Certificate.GramData.Block1.entry_16_4 line 1466
  366. theorem OAI.MUB6.Certificate.GramData.Block1.entry_16_5 line 1470
  367. theorem OAI.MUB6.Certificate.GramData.Block1.entry_16_6 line 1474
  368. theorem OAI.MUB6.Certificate.GramData.Block1.entry_16_7 line 1478
  369. theorem OAI.MUB6.Certificate.GramData.Block1.entry_16_8 line 1482
  370. theorem OAI.MUB6.Certificate.GramData.Block1.entry_16_9 line 1486
  371. theorem OAI.MUB6.Certificate.GramData.Block1.entry_16_10 line 1490
  372. theorem OAI.MUB6.Certificate.GramData.Block1.entry_16_11 line 1494
  373. theorem OAI.MUB6.Certificate.GramData.Block1.entry_16_12 line 1498
  374. theorem OAI.MUB6.Certificate.GramData.Block1.entry_16_13 line 1502
  375. theorem OAI.MUB6.Certificate.GramData.Block1.entry_16_14 line 1506
  376. theorem OAI.MUB6.Certificate.GramData.Block1.entry_16_15 line 1510
  377. theorem OAI.MUB6.Certificate.GramData.Block1.entry_16_16 line 1514
  378. theorem OAI.MUB6.Certificate.GramData.Block1.entry_16_17 line 1518
  379. theorem OAI.MUB6.Certificate.GramData.Block1.entry_16_18 line 1522
  380. theorem OAI.MUB6.Certificate.GramData.Block1.entry_16_19 line 1526
  381. theorem OAI.MUB6.Certificate.GramData.Block1.entry_16_20 line 1530
  382. theorem OAI.MUB6.Certificate.GramData.Block1.entry_17_0 line 1534
  383. theorem OAI.MUB6.Certificate.GramData.Block1.entry_17_1 line 1538
  384. theorem OAI.MUB6.Certificate.GramData.Block1.entry_17_2 line 1542
  385. theorem OAI.MUB6.Certificate.GramData.Block1.entry_17_3 line 1546
  386. theorem OAI.MUB6.Certificate.GramData.Block1.entry_17_4 line 1550
  387. theorem OAI.MUB6.Certificate.GramData.Block1.entry_17_5 line 1554
  388. theorem OAI.MUB6.Certificate.GramData.Block1.entry_17_6 line 1558
  389. theorem OAI.MUB6.Certificate.GramData.Block1.entry_17_7 line 1562
  390. theorem OAI.MUB6.Certificate.GramData.Block1.entry_17_8 line 1566
  391. theorem OAI.MUB6.Certificate.GramData.Block1.entry_17_9 line 1570
  392. theorem OAI.MUB6.Certificate.GramData.Block1.entry_17_10 line 1574
  393. theorem OAI.MUB6.Certificate.GramData.Block1.entry_17_11 line 1578
  394. theorem OAI.MUB6.Certificate.GramData.Block1.entry_17_12 line 1582
  395. theorem OAI.MUB6.Certificate.GramData.Block1.entry_17_13 line 1586
  396. theorem OAI.MUB6.Certificate.GramData.Block1.entry_17_14 line 1590
  397. theorem OAI.MUB6.Certificate.GramData.Block1.entry_17_15 line 1594
  398. theorem OAI.MUB6.Certificate.GramData.Block1.entry_17_16 line 1598
  399. theorem OAI.MUB6.Certificate.GramData.Block1.entry_17_17 line 1602
  400. theorem OAI.MUB6.Certificate.GramData.Block1.entry_17_18 line 1606
  401. theorem OAI.MUB6.Certificate.GramData.Block1.entry_17_19 line 1610
  402. theorem OAI.MUB6.Certificate.GramData.Block1.entry_17_20 line 1614
  403. theorem OAI.MUB6.Certificate.GramData.Block1.entry_18_0 line 1618
  404. theorem OAI.MUB6.Certificate.GramData.Block1.entry_18_1 line 1622
  405. theorem OAI.MUB6.Certificate.GramData.Block1.entry_18_2 line 1626
  406. theorem OAI.MUB6.Certificate.GramData.Block1.entry_18_3 line 1630
  407. theorem OAI.MUB6.Certificate.GramData.Block1.entry_18_4 line 1634
  408. theorem OAI.MUB6.Certificate.GramData.Block1.entry_18_5 line 1638
  409. theorem OAI.MUB6.Certificate.GramData.Block1.entry_18_6 line 1642
  410. theorem OAI.MUB6.Certificate.GramData.Block1.entry_18_7 line 1646
  411. theorem OAI.MUB6.Certificate.GramData.Block1.entry_18_8 line 1650
  412. theorem OAI.MUB6.Certificate.GramData.Block1.entry_18_9 line 1654
  413. theorem OAI.MUB6.Certificate.GramData.Block1.entry_18_10 line 1658
  414. theorem OAI.MUB6.Certificate.GramData.Block1.entry_18_11 line 1662
  415. theorem OAI.MUB6.Certificate.GramData.Block1.entry_18_12 line 1666
  416. theorem OAI.MUB6.Certificate.GramData.Block1.entry_18_13 line 1670
  417. theorem OAI.MUB6.Certificate.GramData.Block1.entry_18_14 line 1674
  418. theorem OAI.MUB6.Certificate.GramData.Block1.entry_18_15 line 1678
  419. theorem OAI.MUB6.Certificate.GramData.Block1.entry_18_16 line 1682
  420. theorem OAI.MUB6.Certificate.GramData.Block1.entry_18_17 line 1686
  421. theorem OAI.MUB6.Certificate.GramData.Block1.entry_18_18 line 1690
  422. theorem OAI.MUB6.Certificate.GramData.Block1.entry_18_19 line 1694
  423. theorem OAI.MUB6.Certificate.GramData.Block1.entry_18_20 line 1698
  424. theorem OAI.MUB6.Certificate.GramData.Block1.entry_19_0 line 1702
  425. theorem OAI.MUB6.Certificate.GramData.Block1.entry_19_1 line 1706
  426. theorem OAI.MUB6.Certificate.GramData.Block1.entry_19_2 line 1710
  427. theorem OAI.MUB6.Certificate.GramData.Block1.entry_19_3 line 1714
  428. theorem OAI.MUB6.Certificate.GramData.Block1.entry_19_4 line 1718
  429. theorem OAI.MUB6.Certificate.GramData.Block1.entry_19_5 line 1722
  430. theorem OAI.MUB6.Certificate.GramData.Block1.entry_19_6 line 1726
  431. theorem OAI.MUB6.Certificate.GramData.Block1.entry_19_7 line 1730
  432. theorem OAI.MUB6.Certificate.GramData.Block1.entry_19_8 line 1734
  433. theorem OAI.MUB6.Certificate.GramData.Block1.entry_19_9 line 1738
  434. theorem OAI.MUB6.Certificate.GramData.Block1.entry_19_10 line 1742
  435. theorem OAI.MUB6.Certificate.GramData.Block1.entry_19_11 line 1746
  436. theorem OAI.MUB6.Certificate.GramData.Block1.entry_19_12 line 1750
  437. theorem OAI.MUB6.Certificate.GramData.Block1.entry_19_13 line 1754
  438. theorem OAI.MUB6.Certificate.GramData.Block1.entry_19_14 line 1758
  439. theorem OAI.MUB6.Certificate.GramData.Block1.entry_19_15 line 1762
  440. theorem OAI.MUB6.Certificate.GramData.Block1.entry_19_16 line 1766
  441. theorem OAI.MUB6.Certificate.GramData.Block1.entry_19_17 line 1770
  442. theorem OAI.MUB6.Certificate.GramData.Block1.entry_19_18 line 1774
  443. theorem OAI.MUB6.Certificate.GramData.Block1.entry_19_19 line 1778
  444. theorem OAI.MUB6.Certificate.GramData.Block1.entry_19_20 line 1782
  445. theorem OAI.MUB6.Certificate.GramData.Block1.entry_20_0 line 1786
  446. theorem OAI.MUB6.Certificate.GramData.Block1.entry_20_1 line 1790
  447. theorem OAI.MUB6.Certificate.GramData.Block1.entry_20_2 line 1794
  448. theorem OAI.MUB6.Certificate.GramData.Block1.entry_20_3 line 1798
  449. theorem OAI.MUB6.Certificate.GramData.Block1.entry_20_4 line 1802
  450. theorem OAI.MUB6.Certificate.GramData.Block1.entry_20_5 line 1806
  451. theorem OAI.MUB6.Certificate.GramData.Block1.entry_20_6 line 1810
  452. theorem OAI.MUB6.Certificate.GramData.Block1.entry_20_7 line 1814
  453. theorem OAI.MUB6.Certificate.GramData.Block1.entry_20_8 line 1818
  454. theorem OAI.MUB6.Certificate.GramData.Block1.entry_20_9 line 1822
  455. theorem OAI.MUB6.Certificate.GramData.Block1.entry_20_10 line 1826
  456. theorem OAI.MUB6.Certificate.GramData.Block1.entry_20_11 line 1830
  457. theorem OAI.MUB6.Certificate.GramData.Block1.entry_20_12 line 1834
  458. theorem OAI.MUB6.Certificate.GramData.Block1.entry_20_13 line 1838
  459. theorem OAI.MUB6.Certificate.GramData.Block1.entry_20_14 line 1842
  460. theorem OAI.MUB6.Certificate.GramData.Block1.entry_20_15 line 1846
  461. theorem OAI.MUB6.Certificate.GramData.Block1.entry_20_16 line 1850
  462. theorem OAI.MUB6.Certificate.GramData.Block1.entry_20_17 line 1854
  463. theorem OAI.MUB6.Certificate.GramData.Block1.entry_20_18 line 1858
  464. theorem OAI.MUB6.Certificate.GramData.Block1.entry_20_19 line 1862
  465. theorem OAI.MUB6.Certificate.GramData.Block1.entry_20_20 line 1866
  466. theorem OAI.MUB6.Certificate.GramData.Block1.pivots_pos line 1870
  467. theorem OAI.MUB6.Certificate.GramData.Block1.gram line 1895
  468. theorem OAI.MUB6.Certificate.GramData.Block1.positiveDefinite line 2341