OAI/Analysis/PlanarPacking/Certificate/AtomKernels.lean

GitHub source file

328 declarations, 0 contain sorry, 0 declared as axioms

Finite interval certificates for the planar Fourier construction

These rational enclosures certify the numerical bounds in the sharp planar Fourier construction of OpenAI. All interval endpoints are exact integers.

  1. def OAI.SharpPlanar.CachedData.atomPoint0 line 15
  2. lemma OAI.SharpPlanar.CachedData.atomPoint0_contains line 16
  3. def OAI.SharpPlanar.CachedData.atomPoint1 line 23
  4. lemma OAI.SharpPlanar.CachedData.atomPoint1_contains line 24
  5. def OAI.SharpPlanar.CachedData.atomPoint2 line 31
  6. lemma OAI.SharpPlanar.CachedData.atomPoint2_contains line 32
  7. def OAI.SharpPlanar.CachedData.atomPoint3 line 40
  8. lemma OAI.SharpPlanar.CachedData.atomPoint3_contains line 41
  9. def OAI.SharpPlanar.CachedData.atomPoint4 line 49
  10. lemma OAI.SharpPlanar.CachedData.atomPoint4_contains line 50
  11. def OAI.SharpPlanar.CachedData.atomPoint5 line 58
  12. lemma OAI.SharpPlanar.CachedData.atomPoint5_contains line 59
  13. def OAI.SharpPlanar.CachedData.atomPoint6 line 67
  14. lemma OAI.SharpPlanar.CachedData.atomPoint6_contains line 68
  15. def OAI.SharpPlanar.CachedData.atomPoints line 76
  16. lemma OAI.SharpPlanar.CachedData.atomPoints_contains line 77
  17. def OAI.SharpPlanar.CachedData.atomKernel0_0 line 86
  18. lemma OAI.SharpPlanar.CachedData.atomKernel0_0_eq line 87
  19. lemma OAI.SharpPlanar.CachedData.atomKernel0_0_contains line 89
  20. def OAI.SharpPlanar.CachedData.atomKernel0_1 line 95
  21. lemma OAI.SharpPlanar.CachedData.atomKernel0_1_eq line 96
  22. lemma OAI.SharpPlanar.CachedData.atomKernel0_1_contains line 98
  23. def OAI.SharpPlanar.CachedData.atomKernel1_0 line 111
  24. lemma OAI.SharpPlanar.CachedData.atomKernel1_0_eq line 112
  25. lemma OAI.SharpPlanar.CachedData.atomKernel1_0_contains line 114
  26. def OAI.SharpPlanar.CachedData.atomKernel1_1 line 120
  27. lemma OAI.SharpPlanar.CachedData.atomKernel1_1_eq line 121
  28. lemma OAI.SharpPlanar.CachedData.atomKernel1_1_contains line 123
  29. def OAI.SharpPlanar.CachedData.atomKernel3_0 line 136
  30. lemma OAI.SharpPlanar.CachedData.atomKernel3_0_eq line 137
  31. lemma OAI.SharpPlanar.CachedData.atomKernel3_0_contains line 139
  32. def OAI.SharpPlanar.CachedData.atomKernel3_1 line 145
  33. lemma OAI.SharpPlanar.CachedData.atomKernel3_1_eq line 146
  34. lemma OAI.SharpPlanar.CachedData.atomKernel3_1_contains line 148
  35. def OAI.SharpPlanar.CachedData.atomKernel4_0 line 161
  36. lemma OAI.SharpPlanar.CachedData.atomKernel4_0_eq line 162
  37. lemma OAI.SharpPlanar.CachedData.atomKernel4_0_contains line 164
  38. def OAI.SharpPlanar.CachedData.atomKernel4_1 line 170
  39. lemma OAI.SharpPlanar.CachedData.atomKernel4_1_eq line 171
  40. lemma OAI.SharpPlanar.CachedData.atomKernel4_1_contains line 173
  41. def OAI.SharpPlanar.CachedData.atomKernel7_0 line 186
  42. lemma OAI.SharpPlanar.CachedData.atomKernel7_0_eq line 187
  43. lemma OAI.SharpPlanar.CachedData.atomKernel7_0_contains line 189
  44. def OAI.SharpPlanar.CachedData.atomKernel7_1 line 195
  45. lemma OAI.SharpPlanar.CachedData.atomKernel7_1_eq line 196
  46. lemma OAI.SharpPlanar.CachedData.atomKernel7_1_contains line 198
  47. def OAI.SharpPlanar.CachedData.atomKernel9_0 line 211
  48. lemma OAI.SharpPlanar.CachedData.atomKernel9_0_eq line 212
  49. lemma OAI.SharpPlanar.CachedData.atomKernel9_0_contains line 214
  50. def OAI.SharpPlanar.CachedData.atomKernel9_1 line 220
  51. lemma OAI.SharpPlanar.CachedData.atomKernel9_1_eq line 221
  52. lemma OAI.SharpPlanar.CachedData.atomKernel9_1_contains line 223
  53. def OAI.SharpPlanar.CachedData.atomKernel12_0 line 236
  54. lemma OAI.SharpPlanar.CachedData.atomKernel12_0_eq line 237
  55. lemma OAI.SharpPlanar.CachedData.atomKernel12_0_contains line 239
  56. def OAI.SharpPlanar.CachedData.atomKernel12_1 line 245
  57. lemma OAI.SharpPlanar.CachedData.atomKernel12_1_eq line 246
  58. lemma OAI.SharpPlanar.CachedData.atomKernel12_1_contains line 248
  59. def OAI.SharpPlanar.CachedData.atomKernel13_0 line 261
  60. lemma OAI.SharpPlanar.CachedData.atomKernel13_0_eq line 262
  61. lemma OAI.SharpPlanar.CachedData.atomKernel13_0_contains line 264
  62. def OAI.SharpPlanar.CachedData.atomKernel13_1 line 270
  63. lemma OAI.SharpPlanar.CachedData.atomKernel13_1_eq line 271
  64. lemma OAI.SharpPlanar.CachedData.atomKernel13_1_contains line 273
  65. def OAI.SharpPlanar.CachedData.atomKernel15_0 line 286
  66. lemma OAI.SharpPlanar.CachedData.atomKernel15_0_eq line 287
  67. lemma OAI.SharpPlanar.CachedData.atomKernel15_0_contains line 289
  68. def OAI.SharpPlanar.CachedData.atomKernel15_1 line 295
  69. lemma OAI.SharpPlanar.CachedData.atomKernel15_1_eq line 296
  70. lemma OAI.SharpPlanar.CachedData.atomKernel15_1_contains line 298
  71. def OAI.SharpPlanar.CachedData.atomKernel16_0 line 311
  72. lemma OAI.SharpPlanar.CachedData.atomKernel16_0_eq line 312
  73. lemma OAI.SharpPlanar.CachedData.atomKernel16_0_contains line 314
  74. def OAI.SharpPlanar.CachedData.atomKernel16_1 line 320
  75. lemma OAI.SharpPlanar.CachedData.atomKernel16_1_eq line 321
  76. lemma OAI.SharpPlanar.CachedData.atomKernel16_1_contains line 323
  77. def OAI.SharpPlanar.CachedData.atomKernel19_0 line 336
  78. lemma OAI.SharpPlanar.CachedData.atomKernel19_0_eq line 337
  79. lemma OAI.SharpPlanar.CachedData.atomKernel19_0_contains line 339
  80. def OAI.SharpPlanar.CachedData.atomKernel19_1 line 345
  81. lemma OAI.SharpPlanar.CachedData.atomKernel19_1_eq line 346
  82. lemma OAI.SharpPlanar.CachedData.atomKernel19_1_contains line 348
  83. def OAI.SharpPlanar.CachedData.atomKernel21_0 line 361
  84. lemma OAI.SharpPlanar.CachedData.atomKernel21_0_eq line 362
  85. lemma OAI.SharpPlanar.CachedData.atomKernel21_0_contains line 364
  86. def OAI.SharpPlanar.CachedData.atomKernel21_1 line 370
  87. lemma OAI.SharpPlanar.CachedData.atomKernel21_1_eq line 371
  88. lemma OAI.SharpPlanar.CachedData.atomKernel21_1_contains line 373
  89. def OAI.SharpPlanar.CachedData.atomKernel24_0 line 386
  90. lemma OAI.SharpPlanar.CachedData.atomKernel24_0_eq line 387
  91. lemma OAI.SharpPlanar.CachedData.atomKernel24_0_contains line 389
  92. def OAI.SharpPlanar.CachedData.atomKernel24_1 line 395
  93. lemma OAI.SharpPlanar.CachedData.atomKernel24_1_eq line 396
  94. lemma OAI.SharpPlanar.CachedData.atomKernel24_1_contains line 398
  95. def OAI.SharpPlanar.CachedData.atomKernel25_0 line 411
  96. lemma OAI.SharpPlanar.CachedData.atomKernel25_0_eq line 412
  97. lemma OAI.SharpPlanar.CachedData.atomKernel25_0_contains line 414
  98. def OAI.SharpPlanar.CachedData.atomKernel25_1 line 420
  99. lemma OAI.SharpPlanar.CachedData.atomKernel25_1_eq line 421
  100. lemma OAI.SharpPlanar.CachedData.atomKernel25_1_contains line 423
  101. def OAI.SharpPlanar.CachedData.atomKernel27_0 line 436
  102. lemma OAI.SharpPlanar.CachedData.atomKernel27_0_eq line 437
  103. lemma OAI.SharpPlanar.CachedData.atomKernel27_0_contains line 439
  104. def OAI.SharpPlanar.CachedData.atomKernel27_1 line 445
  105. lemma OAI.SharpPlanar.CachedData.atomKernel27_1_eq line 446
  106. lemma OAI.SharpPlanar.CachedData.atomKernel27_1_contains line 448
  107. def OAI.SharpPlanar.CachedData.atomKernel28_0 line 461
  108. lemma OAI.SharpPlanar.CachedData.atomKernel28_0_eq line 462
  109. lemma OAI.SharpPlanar.CachedData.atomKernel28_0_contains line 464
  110. def OAI.SharpPlanar.CachedData.atomKernel28_1 line 470
  111. lemma OAI.SharpPlanar.CachedData.atomKernel28_1_eq line 471
  112. lemma OAI.SharpPlanar.CachedData.atomKernel28_1_contains line 473
  113. def OAI.SharpPlanar.CachedData.atomKernel31_0 line 486
  114. lemma OAI.SharpPlanar.CachedData.atomKernel31_0_eq line 487
  115. lemma OAI.SharpPlanar.CachedData.atomKernel31_0_contains line 489
  116. def OAI.SharpPlanar.CachedData.atomKernel31_1 line 495
  117. lemma OAI.SharpPlanar.CachedData.atomKernel31_1_eq line 496
  118. lemma OAI.SharpPlanar.CachedData.atomKernel31_1_contains line 498
  119. def OAI.SharpPlanar.CachedData.atomKernel33_0 line 511
  120. lemma OAI.SharpPlanar.CachedData.atomKernel33_0_eq line 512
  121. lemma OAI.SharpPlanar.CachedData.atomKernel33_0_contains line 514
  122. def OAI.SharpPlanar.CachedData.atomKernel33_1 line 520
  123. lemma OAI.SharpPlanar.CachedData.atomKernel33_1_eq line 521
  124. lemma OAI.SharpPlanar.CachedData.atomKernel33_1_contains line 523
  125. def OAI.SharpPlanar.CachedData.atomKernel36_0 line 536
  126. lemma OAI.SharpPlanar.CachedData.atomKernel36_0_eq line 537
  127. lemma OAI.SharpPlanar.CachedData.atomKernel36_0_contains line 539
  128. def OAI.SharpPlanar.CachedData.atomKernel36_1 line 545
  129. lemma OAI.SharpPlanar.CachedData.atomKernel36_1_eq line 546
  130. lemma OAI.SharpPlanar.CachedData.atomKernel36_1_contains line 548
  131. def OAI.SharpPlanar.CachedData.atomKernel37_0 line 561
  132. lemma OAI.SharpPlanar.CachedData.atomKernel37_0_eq line 562
  133. lemma OAI.SharpPlanar.CachedData.atomKernel37_0_contains line 564
  134. def OAI.SharpPlanar.CachedData.atomKernel37_1 line 570
  135. lemma OAI.SharpPlanar.CachedData.atomKernel37_1_eq line 571
  136. lemma OAI.SharpPlanar.CachedData.atomKernel37_1_contains line 573
  137. def OAI.SharpPlanar.CachedData.atomKernel39_0 line 586
  138. lemma OAI.SharpPlanar.CachedData.atomKernel39_0_eq line 587
  139. lemma OAI.SharpPlanar.CachedData.atomKernel39_0_contains line 589
  140. def OAI.SharpPlanar.CachedData.atomKernel39_1 line 595
  141. lemma OAI.SharpPlanar.CachedData.atomKernel39_1_eq line 596
  142. lemma OAI.SharpPlanar.CachedData.atomKernel39_1_contains line 598
  143. def OAI.SharpPlanar.CachedData.atomKernel40_0 line 611
  144. lemma OAI.SharpPlanar.CachedData.atomKernel40_0_eq line 612
  145. lemma OAI.SharpPlanar.CachedData.atomKernel40_0_contains line 614
  146. def OAI.SharpPlanar.CachedData.atomKernel40_1 line 620
  147. lemma OAI.SharpPlanar.CachedData.atomKernel40_1_eq line 621
  148. lemma OAI.SharpPlanar.CachedData.atomKernel40_1_contains line 623
  149. def OAI.SharpPlanar.CachedData.atomKernel43_0 line 636
  150. lemma OAI.SharpPlanar.CachedData.atomKernel43_0_eq line 637
  151. lemma OAI.SharpPlanar.CachedData.atomKernel43_0_contains line 639
  152. def OAI.SharpPlanar.CachedData.atomKernel43_1 line 645
  153. lemma OAI.SharpPlanar.CachedData.atomKernel43_1_eq line 646
  154. lemma OAI.SharpPlanar.CachedData.atomKernel43_1_contains line 648
  155. def OAI.SharpPlanar.CachedData.atomKernel45_0 line 661
  156. lemma OAI.SharpPlanar.CachedData.atomKernel45_0_eq line 662
  157. lemma OAI.SharpPlanar.CachedData.atomKernel45_0_contains line 664
  158. def OAI.SharpPlanar.CachedData.atomKernel45_1 line 670
  159. lemma OAI.SharpPlanar.CachedData.atomKernel45_1_eq line 671
  160. lemma OAI.SharpPlanar.CachedData.atomKernel45_1_contains line 673
  161. def OAI.SharpPlanar.CachedData.atomKernel48_0 line 686
  162. lemma OAI.SharpPlanar.CachedData.atomKernel48_0_eq line 687
  163. lemma OAI.SharpPlanar.CachedData.atomKernel48_0_contains line 689
  164. def OAI.SharpPlanar.CachedData.atomKernel48_1 line 695
  165. lemma OAI.SharpPlanar.CachedData.atomKernel48_1_eq line 696
  166. lemma OAI.SharpPlanar.CachedData.atomKernel48_1_contains line 698
  167. def OAI.SharpPlanar.CachedData.atomKernel49_0 line 711
  168. lemma OAI.SharpPlanar.CachedData.atomKernel49_0_eq line 712
  169. lemma OAI.SharpPlanar.CachedData.atomKernel49_0_contains line 714
  170. def OAI.SharpPlanar.CachedData.atomKernel49_1 line 720
  171. lemma OAI.SharpPlanar.CachedData.atomKernel49_1_eq line 721
  172. lemma OAI.SharpPlanar.CachedData.atomKernel49_1_contains line 723
  173. def OAI.SharpPlanar.CachedData.atomKernel51_0 line 736
  174. lemma OAI.SharpPlanar.CachedData.atomKernel51_0_eq line 737
  175. lemma OAI.SharpPlanar.CachedData.atomKernel51_0_contains line 739
  176. def OAI.SharpPlanar.CachedData.atomKernel51_1 line 745
  177. lemma OAI.SharpPlanar.CachedData.atomKernel51_1_eq line 746
  178. lemma OAI.SharpPlanar.CachedData.atomKernel51_1_contains line 748
  179. def OAI.SharpPlanar.CachedData.atomKernel52_0 line 761
  180. lemma OAI.SharpPlanar.CachedData.atomKernel52_0_eq line 762
  181. lemma OAI.SharpPlanar.CachedData.atomKernel52_0_contains line 764
  182. def OAI.SharpPlanar.CachedData.atomKernel52_1 line 770
  183. lemma OAI.SharpPlanar.CachedData.atomKernel52_1_eq line 771
  184. lemma OAI.SharpPlanar.CachedData.atomKernel52_1_contains line 773
  185. def OAI.SharpPlanar.CachedData.atomKernel55_0 line 786
  186. lemma OAI.SharpPlanar.CachedData.atomKernel55_0_eq line 787
  187. lemma OAI.SharpPlanar.CachedData.atomKernel55_0_contains line 789
  188. def OAI.SharpPlanar.CachedData.atomKernel55_1 line 795
  189. lemma OAI.SharpPlanar.CachedData.atomKernel55_1_eq line 796
  190. lemma OAI.SharpPlanar.CachedData.atomKernel55_1_contains line 798
  191. def OAI.SharpPlanar.CachedData.atomKernel57_0 line 811
  192. lemma OAI.SharpPlanar.CachedData.atomKernel57_0_eq line 812
  193. lemma OAI.SharpPlanar.CachedData.atomKernel57_0_contains line 814
  194. def OAI.SharpPlanar.CachedData.atomKernel57_1 line 820
  195. lemma OAI.SharpPlanar.CachedData.atomKernel57_1_eq line 821
  196. lemma OAI.SharpPlanar.CachedData.atomKernel57_1_contains line 823
  197. def OAI.SharpPlanar.CachedData.atomKernel60_0 line 836
  198. lemma OAI.SharpPlanar.CachedData.atomKernel60_0_eq line 837
  199. lemma OAI.SharpPlanar.CachedData.atomKernel60_0_contains line 839
  200. def OAI.SharpPlanar.CachedData.atomKernel60_1 line 845
  201. lemma OAI.SharpPlanar.CachedData.atomKernel60_1_eq line 846
  202. lemma OAI.SharpPlanar.CachedData.atomKernel60_1_contains line 848
  203. def OAI.SharpPlanar.CachedData.atomKernel61_0 line 861
  204. lemma OAI.SharpPlanar.CachedData.atomKernel61_0_eq line 862
  205. lemma OAI.SharpPlanar.CachedData.atomKernel61_0_contains line 864
  206. def OAI.SharpPlanar.CachedData.atomKernel61_1 line 870
  207. lemma OAI.SharpPlanar.CachedData.atomKernel61_1_eq line 871
  208. lemma OAI.SharpPlanar.CachedData.atomKernel61_1_contains line 873
  209. def OAI.SharpPlanar.CachedData.atomKernel63_0 line 886
  210. lemma OAI.SharpPlanar.CachedData.atomKernel63_0_eq line 887
  211. lemma OAI.SharpPlanar.CachedData.atomKernel63_0_contains line 889
  212. def OAI.SharpPlanar.CachedData.atomKernel63_1 line 895
  213. lemma OAI.SharpPlanar.CachedData.atomKernel63_1_eq line 896
  214. lemma OAI.SharpPlanar.CachedData.atomKernel63_1_contains line 898
  215. def OAI.SharpPlanar.CachedData.atomKernel64_0 line 911
  216. lemma OAI.SharpPlanar.CachedData.atomKernel64_0_eq line 912
  217. lemma OAI.SharpPlanar.CachedData.atomKernel64_0_contains line 914
  218. def OAI.SharpPlanar.CachedData.atomKernel64_1 line 920
  219. lemma OAI.SharpPlanar.CachedData.atomKernel64_1_eq line 921
  220. lemma OAI.SharpPlanar.CachedData.atomKernel64_1_contains line 923
  221. def OAI.SharpPlanar.CachedData.atomKernel67_0 line 936
  222. lemma OAI.SharpPlanar.CachedData.atomKernel67_0_eq line 937
  223. lemma OAI.SharpPlanar.CachedData.atomKernel67_0_contains line 939
  224. def OAI.SharpPlanar.CachedData.atomKernel67_1 line 945
  225. lemma OAI.SharpPlanar.CachedData.atomKernel67_1_eq line 946
  226. lemma OAI.SharpPlanar.CachedData.atomKernel67_1_contains line 948
  227. def OAI.SharpPlanar.CachedData.atomKernel69_0 line 961
  228. lemma OAI.SharpPlanar.CachedData.atomKernel69_0_eq line 962
  229. lemma OAI.SharpPlanar.CachedData.atomKernel69_0_contains line 964
  230. def OAI.SharpPlanar.CachedData.atomKernel69_1 line 970
  231. lemma OAI.SharpPlanar.CachedData.atomKernel69_1_eq line 971
  232. lemma OAI.SharpPlanar.CachedData.atomKernel69_1_contains line 973
  233. def OAI.SharpPlanar.CachedData.atomKernel72_0 line 986
  234. lemma OAI.SharpPlanar.CachedData.atomKernel72_0_eq line 987
  235. lemma OAI.SharpPlanar.CachedData.atomKernel72_0_contains line 989
  236. def OAI.SharpPlanar.CachedData.atomKernel72_1 line 995
  237. lemma OAI.SharpPlanar.CachedData.atomKernel72_1_eq line 996
  238. lemma OAI.SharpPlanar.CachedData.atomKernel72_1_contains line 998
  239. def OAI.SharpPlanar.CachedData.atomKernel73_0 line 1011
  240. lemma OAI.SharpPlanar.CachedData.atomKernel73_0_eq line 1012
  241. lemma OAI.SharpPlanar.CachedData.atomKernel73_0_contains line 1014
  242. def OAI.SharpPlanar.CachedData.atomKernel73_1 line 1020
  243. lemma OAI.SharpPlanar.CachedData.atomKernel73_1_eq line 1021
  244. lemma OAI.SharpPlanar.CachedData.atomKernel73_1_contains line 1023
  245. def OAI.SharpPlanar.CachedData.atomKernel75_0 line 1036
  246. lemma OAI.SharpPlanar.CachedData.atomKernel75_0_eq line 1037
  247. lemma OAI.SharpPlanar.CachedData.atomKernel75_0_contains line 1039
  248. def OAI.SharpPlanar.CachedData.atomKernel75_1 line 1045
  249. lemma OAI.SharpPlanar.CachedData.atomKernel75_1_eq line 1046
  250. lemma OAI.SharpPlanar.CachedData.atomKernel75_1_contains line 1048
  251. def OAI.SharpPlanar.CachedData.atomKernel76_0 line 1061
  252. lemma OAI.SharpPlanar.CachedData.atomKernel76_0_eq line 1062
  253. lemma OAI.SharpPlanar.CachedData.atomKernel76_0_contains line 1064
  254. def OAI.SharpPlanar.CachedData.atomKernel76_1 line 1070
  255. lemma OAI.SharpPlanar.CachedData.atomKernel76_1_eq line 1071
  256. lemma OAI.SharpPlanar.CachedData.atomKernel76_1_contains line 1073
  257. def OAI.SharpPlanar.CachedData.atomKernel79_0 line 1086
  258. lemma OAI.SharpPlanar.CachedData.atomKernel79_0_eq line 1087
  259. lemma OAI.SharpPlanar.CachedData.atomKernel79_0_contains line 1089
  260. def OAI.SharpPlanar.CachedData.atomKernel79_1 line 1095
  261. lemma OAI.SharpPlanar.CachedData.atomKernel79_1_eq line 1096
  262. lemma OAI.SharpPlanar.CachedData.atomKernel79_1_contains line 1098
  263. def OAI.SharpPlanar.CachedData.atomKernel81_0 line 1111
  264. lemma OAI.SharpPlanar.CachedData.atomKernel81_0_eq line 1112
  265. lemma OAI.SharpPlanar.CachedData.atomKernel81_0_contains line 1114
  266. def OAI.SharpPlanar.CachedData.atomKernel81_1 line 1120
  267. lemma OAI.SharpPlanar.CachedData.atomKernel81_1_eq line 1121
  268. lemma OAI.SharpPlanar.CachedData.atomKernel81_1_contains line 1123
  269. def OAI.SharpPlanar.CachedData.atomKernel84_0 line 1136
  270. lemma OAI.SharpPlanar.CachedData.atomKernel84_0_eq line 1137
  271. lemma OAI.SharpPlanar.CachedData.atomKernel84_0_contains line 1139
  272. def OAI.SharpPlanar.CachedData.atomKernel84_1 line 1145
  273. lemma OAI.SharpPlanar.CachedData.atomKernel84_1_eq line 1146
  274. lemma OAI.SharpPlanar.CachedData.atomKernel84_1_contains line 1148
  275. def OAI.SharpPlanar.CachedData.atomKernel85_0 line 1161
  276. lemma OAI.SharpPlanar.CachedData.atomKernel85_0_eq line 1162
  277. lemma OAI.SharpPlanar.CachedData.atomKernel85_0_contains line 1164
  278. def OAI.SharpPlanar.CachedData.atomKernel85_1 line 1170
  279. lemma OAI.SharpPlanar.CachedData.atomKernel85_1_eq line 1171
  280. lemma OAI.SharpPlanar.CachedData.atomKernel85_1_contains line 1173
  281. def OAI.SharpPlanar.CachedData.atomKernel87_0 line 1186
  282. lemma OAI.SharpPlanar.CachedData.atomKernel87_0_eq line 1187
  283. lemma OAI.SharpPlanar.CachedData.atomKernel87_0_contains line 1189
  284. def OAI.SharpPlanar.CachedData.atomKernel87_1 line 1195
  285. lemma OAI.SharpPlanar.CachedData.atomKernel87_1_eq line 1196
  286. lemma OAI.SharpPlanar.CachedData.atomKernel87_1_contains line 1198
  287. def OAI.SharpPlanar.CachedData.atomKernel88_0 line 1211
  288. lemma OAI.SharpPlanar.CachedData.atomKernel88_0_eq line 1212
  289. lemma OAI.SharpPlanar.CachedData.atomKernel88_0_contains line 1214
  290. def OAI.SharpPlanar.CachedData.atomKernel88_1 line 1220
  291. lemma OAI.SharpPlanar.CachedData.atomKernel88_1_eq line 1221
  292. lemma OAI.SharpPlanar.CachedData.atomKernel88_1_contains line 1223
  293. def OAI.SharpPlanar.CachedData.atomKernel91_0 line 1236
  294. lemma OAI.SharpPlanar.CachedData.atomKernel91_0_eq line 1237
  295. lemma OAI.SharpPlanar.CachedData.atomKernel91_0_contains line 1239
  296. def OAI.SharpPlanar.CachedData.atomKernel91_1 line 1245
  297. lemma OAI.SharpPlanar.CachedData.atomKernel91_1_eq line 1246
  298. lemma OAI.SharpPlanar.CachedData.atomKernel91_1_contains line 1248
  299. def OAI.SharpPlanar.CachedData.atomKernel93_0 line 1261
  300. lemma OAI.SharpPlanar.CachedData.atomKernel93_0_eq line 1262
  301. lemma OAI.SharpPlanar.CachedData.atomKernel93_0_contains line 1264
  302. def OAI.SharpPlanar.CachedData.atomKernel93_1 line 1270
  303. lemma OAI.SharpPlanar.CachedData.atomKernel93_1_eq line 1271
  304. lemma OAI.SharpPlanar.CachedData.atomKernel93_1_contains line 1273
  305. def OAI.SharpPlanar.CachedData.atomKernel96_0 line 1286
  306. lemma OAI.SharpPlanar.CachedData.atomKernel96_0_eq line 1287
  307. lemma OAI.SharpPlanar.CachedData.atomKernel96_0_contains line 1289
  308. def OAI.SharpPlanar.CachedData.atomKernel96_1 line 1295
  309. lemma OAI.SharpPlanar.CachedData.atomKernel96_1_eq line 1296
  310. lemma OAI.SharpPlanar.CachedData.atomKernel96_1_contains line 1298
  311. def OAI.SharpPlanar.CachedData.atomKernel97_0 line 1311
  312. lemma OAI.SharpPlanar.CachedData.atomKernel97_0_eq line 1312
  313. lemma OAI.SharpPlanar.CachedData.atomKernel97_0_contains line 1314
  314. def OAI.SharpPlanar.CachedData.atomKernel97_1 line 1320
  315. lemma OAI.SharpPlanar.CachedData.atomKernel97_1_eq line 1321
  316. lemma OAI.SharpPlanar.CachedData.atomKernel97_1_contains line 1323
  317. def OAI.SharpPlanar.CachedData.atomKernel99_0 line 1336
  318. lemma OAI.SharpPlanar.CachedData.atomKernel99_0_eq line 1337
  319. lemma OAI.SharpPlanar.CachedData.atomKernel99_0_contains line 1339
  320. def OAI.SharpPlanar.CachedData.atomKernel99_1 line 1345
  321. lemma OAI.SharpPlanar.CachedData.atomKernel99_1_eq line 1346
  322. lemma OAI.SharpPlanar.CachedData.atomKernel99_1_contains line 1348
  323. def OAI.SharpPlanar.CachedData.atomKernel100_0 line 1361
  324. lemma OAI.SharpPlanar.CachedData.atomKernel100_0_eq line 1362
  325. lemma OAI.SharpPlanar.CachedData.atomKernel100_0_contains line 1364
  326. def OAI.SharpPlanar.CachedData.atomKernel100_1 line 1370
  327. lemma OAI.SharpPlanar.CachedData.atomKernel100_1_eq line 1371
  328. lemma OAI.SharpPlanar.CachedData.atomKernel100_1_contains line 1373