OAI/Analysis/MutuallyUnbiased/PairTargets/Assembly.lean

GitHub source file

152 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge0 line 8
  2. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck0 line 10
  3. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval0 line 13
  4. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge1 line 18
  5. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck1 line 20
  6. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval1 line 23
  7. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge2 line 30
  8. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck2 line 32
  9. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval2 line 35
  10. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge3 line 40
  11. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck3 line 42
  12. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval3 line 45
  13. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge4 line 52
  14. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck4 line 54
  15. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval4 line 57
  16. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge5 line 64
  17. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck5 line 66
  18. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval5 line 69
  19. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge6 line 74
  20. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck6 line 76
  21. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval6 line 79
  22. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge7 line 86
  23. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck7 line 88
  24. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval7 line 91
  25. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge8 line 96
  26. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck8 line 98
  27. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval8 line 101
  28. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge9 line 106
  29. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck9 line 108
  30. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval9 line 111
  31. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge10 line 118
  32. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck10 line 120
  33. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval10 line 123
  34. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge11 line 130
  35. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck11 line 132
  36. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval11 line 135
  37. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge12 line 142
  38. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck12 line 144
  39. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval12 line 147
  40. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge13 line 152
  41. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck13 line 154
  42. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval13 line 157
  43. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge14 line 164
  44. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck14 line 166
  45. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval14 line 169
  46. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge15 line 174
  47. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck15 line 176
  48. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval15 line 179
  49. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge16 line 186
  50. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck16 line 188
  51. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval16 line 191
  52. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge17 line 198
  53. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck17 line 200
  54. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval17 line 203
  55. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge18 line 208
  56. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck18 line 210
  57. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval18 line 213
  58. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge19 line 220
  59. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck19 line 222
  60. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval19 line 225
  61. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge20 line 230
  62. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck20 line 232
  63. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval20 line 235
  64. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge21 line 240
  65. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck21 line 242
  66. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval21 line 245
  67. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge22 line 252
  68. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck22 line 254
  69. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval22 line 257
  70. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge23 line 264
  71. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck23 line 266
  72. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval23 line 269
  73. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge24 line 276
  74. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck24 line 278
  75. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval24 line 281
  76. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge25 line 288
  77. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck25 line 290
  78. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval25 line 293
  79. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge26 line 298
  80. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck26 line 300
  81. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval26 line 303
  82. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge27 line 310
  83. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck27 line 312
  84. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval27 line 315
  85. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge28 line 320
  86. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck28 line 322
  87. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval28 line 325
  88. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge29 line 332
  89. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck29 line 334
  90. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval29 line 337
  91. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge30 line 344
  92. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck30 line 346
  93. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval30 line 349
  94. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge31 line 354
  95. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck31 line 356
  96. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval31 line 359
  97. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge32 line 366
  98. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck32 line 368
  99. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval32 line 371
  100. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge33 line 376
  101. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck33 line 378
  102. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval33 line 381
  103. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge34 line 386
  104. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck34 line 388
  105. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval34 line 391
  106. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge35 line 398
  107. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck35 line 400
  108. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval35 line 403
  109. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge36 line 410
  110. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck36 line 412
  111. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval36 line 415
  112. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge37 line 422
  113. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck37 line 424
  114. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval37 line 427
  115. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge38 line 432
  116. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck38 line 434
  117. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval38 line 437
  118. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge39 line 444
  119. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck39 line 446
  120. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval39 line 449
  121. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge40 line 454
  122. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck40 line 456
  123. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval40 line 459
  124. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge41 line 466
  125. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck41 line 468
  126. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval41 line 471
  127. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge42 line 478
  128. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck42 line 480
  129. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval42 line 483
  130. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge43 line 488
  131. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck43 line 490
  132. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval43 line 493
  133. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge44 line 500
  134. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck44 line 502
  135. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval44 line 505
  136. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge45 line 510
  137. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck45 line 512
  138. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval45 line 515
  139. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge46 line 520
  140. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck46 line 522
  141. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval46 line 525
  142. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge47 line 532
  143. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck47 line 534
  144. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval47 line 537
  145. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge48 line 544
  146. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck48 line 546
  147. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval48 line 549
  148. def OAI.MUB6.Certificate.PairTargetSemantics.integerMerge49 line 556
  149. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeCheck49 line 558
  150. theorem OAI.MUB6.Certificate.PairTargetSemantics.integerMergeEval49 line 561
  151. theorem OAI.MUB6.Certificate.PairTargetSemantics.finalReindex0 line 568
  152. theorem OAI.MUB6.Certificate.PairTargetSemantics.finalReindex1 line 571