OAI/Analysis/PlanarPacking/Certificate/HighHeaders28.lean

GitHub source file

310 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.hk28_0_0 line 17
  2. lemma OAI.SharpPlanar.CachedData.hk28_0_0_contains line 18
  3. def OAI.SharpPlanar.CachedData.ha28_0_0 line 21
  4. lemma OAI.SharpPlanar.CachedData.ha28_0_0_eq line 22
  5. lemma OAI.SharpPlanar.CachedData.ha28_0_0_contains line 23
  6. def OAI.SharpPlanar.CachedData.hk28_0_1 line 26
  7. lemma OAI.SharpPlanar.CachedData.hk28_0_1_contains line 27
  8. def OAI.SharpPlanar.CachedData.ha28_0_1 line 30
  9. lemma OAI.SharpPlanar.CachedData.ha28_0_1_eq line 31
  10. lemma OAI.SharpPlanar.CachedData.ha28_0_1_contains line 32
  11. def OAI.SharpPlanar.CachedData.hk28_0_2 line 35
  12. lemma OAI.SharpPlanar.CachedData.hk28_0_2_contains line 36
  13. def OAI.SharpPlanar.CachedData.ha28_0_2 line 39
  14. lemma OAI.SharpPlanar.CachedData.ha28_0_2_eq line 40
  15. lemma OAI.SharpPlanar.CachedData.ha28_0_2_contains line 41
  16. def OAI.SharpPlanar.CachedData.hk28_0_3 line 44
  17. lemma OAI.SharpPlanar.CachedData.hk28_0_3_contains line 45
  18. def OAI.SharpPlanar.CachedData.ha28_0_3 line 48
  19. lemma OAI.SharpPlanar.CachedData.ha28_0_3_eq line 49
  20. lemma OAI.SharpPlanar.CachedData.ha28_0_3_contains line 50
  21. def OAI.SharpPlanar.CachedData.hk28_0_4 line 53
  22. lemma OAI.SharpPlanar.CachedData.hk28_0_4_contains line 54
  23. def OAI.SharpPlanar.CachedData.ha28_0_4 line 57
  24. lemma OAI.SharpPlanar.CachedData.ha28_0_4_eq line 58
  25. lemma OAI.SharpPlanar.CachedData.ha28_0_4_contains line 59
  26. def OAI.SharpPlanar.CachedData.hk28_0_5 line 62
  27. lemma OAI.SharpPlanar.CachedData.hk28_0_5_contains line 63
  28. def OAI.SharpPlanar.CachedData.ha28_0_5 line 66
  29. lemma OAI.SharpPlanar.CachedData.ha28_0_5_eq line 67
  30. lemma OAI.SharpPlanar.CachedData.ha28_0_5_contains line 68
  31. def OAI.SharpPlanar.CachedData.hk28_0_6 line 71
  32. lemma OAI.SharpPlanar.CachedData.hk28_0_6_contains line 72
  33. def OAI.SharpPlanar.CachedData.ha28_0_6 line 75
  34. lemma OAI.SharpPlanar.CachedData.ha28_0_6_eq line 76
  35. lemma OAI.SharpPlanar.CachedData.ha28_0_6_contains line 77
  36. def OAI.SharpPlanar.CachedData.hk28_0_7 line 80
  37. lemma OAI.SharpPlanar.CachedData.hk28_0_7_contains line 81
  38. def OAI.SharpPlanar.CachedData.ha28_0_7 line 84
  39. lemma OAI.SharpPlanar.CachedData.ha28_0_7_eq line 85
  40. lemma OAI.SharpPlanar.CachedData.ha28_0_7_contains line 86
  41. def OAI.SharpPlanar.CachedData.hk28_0_8 line 89
  42. lemma OAI.SharpPlanar.CachedData.hk28_0_8_contains line 90
  43. def OAI.SharpPlanar.CachedData.ha28_0_8 line 93
  44. lemma OAI.SharpPlanar.CachedData.ha28_0_8_eq line 94
  45. lemma OAI.SharpPlanar.CachedData.ha28_0_8_contains line 95
  46. def OAI.SharpPlanar.CachedData.hk28_0_9 line 98
  47. lemma OAI.SharpPlanar.CachedData.hk28_0_9_contains line 99
  48. def OAI.SharpPlanar.CachedData.ha28_0_9 line 102
  49. lemma OAI.SharpPlanar.CachedData.ha28_0_9_eq line 103
  50. lemma OAI.SharpPlanar.CachedData.ha28_0_9_contains line 104
  51. def OAI.SharpPlanar.CachedData.hk28_0_10 line 107
  52. lemma OAI.SharpPlanar.CachedData.hk28_0_10_contains line 108
  53. def OAI.SharpPlanar.CachedData.ha28_0_10 line 111
  54. lemma OAI.SharpPlanar.CachedData.ha28_0_10_eq line 112
  55. lemma OAI.SharpPlanar.CachedData.ha28_0_10_contains line 113
  56. def OAI.SharpPlanar.CachedData.hk28_0_11 line 116
  57. lemma OAI.SharpPlanar.CachedData.hk28_0_11_contains line 117
  58. def OAI.SharpPlanar.CachedData.ha28_0_11 line 120
  59. lemma OAI.SharpPlanar.CachedData.ha28_0_11_eq line 121
  60. lemma OAI.SharpPlanar.CachedData.ha28_0_11_contains line 122
  61. def OAI.SharpPlanar.CachedData.hk28_0_12 line 125
  62. lemma OAI.SharpPlanar.CachedData.hk28_0_12_contains line 126
  63. def OAI.SharpPlanar.CachedData.ha28_0_12 line 129
  64. lemma OAI.SharpPlanar.CachedData.ha28_0_12_eq line 130
  65. lemma OAI.SharpPlanar.CachedData.ha28_0_12_contains line 131
  66. def OAI.SharpPlanar.CachedData.hk28_0_13 line 134
  67. lemma OAI.SharpPlanar.CachedData.hk28_0_13_contains line 135
  68. def OAI.SharpPlanar.CachedData.ha28_0_13 line 138
  69. lemma OAI.SharpPlanar.CachedData.ha28_0_13_eq line 139
  70. lemma OAI.SharpPlanar.CachedData.ha28_0_13_contains line 140
  71. def OAI.SharpPlanar.CachedData.hk28_0_14 line 143
  72. lemma OAI.SharpPlanar.CachedData.hk28_0_14_contains line 144
  73. def OAI.SharpPlanar.CachedData.ha28_0_14 line 147
  74. lemma OAI.SharpPlanar.CachedData.ha28_0_14_eq line 148
  75. lemma OAI.SharpPlanar.CachedData.ha28_0_14_contains line 149
  76. def OAI.SharpPlanar.CachedData.hk28_0_15 line 152
  77. lemma OAI.SharpPlanar.CachedData.hk28_0_15_contains line 153
  78. def OAI.SharpPlanar.CachedData.ha28_0_15 line 156
  79. lemma OAI.SharpPlanar.CachedData.ha28_0_15_eq line 157
  80. lemma OAI.SharpPlanar.CachedData.ha28_0_15_contains line 158
  81. def OAI.SharpPlanar.CachedData.hk28_0_16 line 161
  82. lemma OAI.SharpPlanar.CachedData.hk28_0_16_contains line 162
  83. def OAI.SharpPlanar.CachedData.ha28_0_16 line 165
  84. lemma OAI.SharpPlanar.CachedData.ha28_0_16_eq line 166
  85. lemma OAI.SharpPlanar.CachedData.ha28_0_16_contains line 167
  86. def OAI.SharpPlanar.CachedData.hk28_0_17 line 170
  87. lemma OAI.SharpPlanar.CachedData.hk28_0_17_contains line 171
  88. def OAI.SharpPlanar.CachedData.ha28_0_17 line 174
  89. lemma OAI.SharpPlanar.CachedData.ha28_0_17_eq line 175
  90. lemma OAI.SharpPlanar.CachedData.ha28_0_17_contains line 176
  91. def OAI.SharpPlanar.CachedData.hk28_0_18 line 179
  92. lemma OAI.SharpPlanar.CachedData.hk28_0_18_contains line 180
  93. def OAI.SharpPlanar.CachedData.ha28_0_18 line 183
  94. lemma OAI.SharpPlanar.CachedData.ha28_0_18_eq line 184
  95. lemma OAI.SharpPlanar.CachedData.ha28_0_18_contains line 185
  96. def OAI.SharpPlanar.CachedData.hk28_0_19 line 188
  97. lemma OAI.SharpPlanar.CachedData.hk28_0_19_contains line 189
  98. def OAI.SharpPlanar.CachedData.ha28_0_19 line 192
  99. lemma OAI.SharpPlanar.CachedData.ha28_0_19_eq line 193
  100. lemma OAI.SharpPlanar.CachedData.ha28_0_19_contains line 194
  101. def OAI.SharpPlanar.CachedData.hk28_0_20 line 197
  102. lemma OAI.SharpPlanar.CachedData.hk28_0_20_contains line 198
  103. def OAI.SharpPlanar.CachedData.ha28_0_20 line 201
  104. lemma OAI.SharpPlanar.CachedData.ha28_0_20_eq line 202
  105. lemma OAI.SharpPlanar.CachedData.ha28_0_20_contains line 203
  106. def OAI.SharpPlanar.CachedData.hk28_0_21 line 206
  107. lemma OAI.SharpPlanar.CachedData.hk28_0_21_contains line 207
  108. def OAI.SharpPlanar.CachedData.ha28_0_21 line 210
  109. lemma OAI.SharpPlanar.CachedData.ha28_0_21_eq line 211
  110. lemma OAI.SharpPlanar.CachedData.ha28_0_21_contains line 212
  111. def OAI.SharpPlanar.CachedData.hk28_0_22 line 215
  112. lemma OAI.SharpPlanar.CachedData.hk28_0_22_contains line 216
  113. def OAI.SharpPlanar.CachedData.ha28_0_22 line 219
  114. lemma OAI.SharpPlanar.CachedData.ha28_0_22_eq line 220
  115. lemma OAI.SharpPlanar.CachedData.ha28_0_22_contains line 221
  116. def OAI.SharpPlanar.CachedData.hk28_0_23 line 224
  117. lemma OAI.SharpPlanar.CachedData.hk28_0_23_contains line 225
  118. def OAI.SharpPlanar.CachedData.ha28_0_23 line 228
  119. lemma OAI.SharpPlanar.CachedData.ha28_0_23_eq line 229
  120. lemma OAI.SharpPlanar.CachedData.ha28_0_23_contains line 230
  121. def OAI.SharpPlanar.CachedData.hk28_0_24 line 233
  122. lemma OAI.SharpPlanar.CachedData.hk28_0_24_contains line 234
  123. def OAI.SharpPlanar.CachedData.ha28_0_24 line 237
  124. lemma OAI.SharpPlanar.CachedData.ha28_0_24_eq line 238
  125. lemma OAI.SharpPlanar.CachedData.ha28_0_24_contains line 239
  126. def OAI.SharpPlanar.CachedData.hk28_0_25 line 242
  127. lemma OAI.SharpPlanar.CachedData.hk28_0_25_contains line 243
  128. def OAI.SharpPlanar.CachedData.ha28_0_25 line 246
  129. lemma OAI.SharpPlanar.CachedData.ha28_0_25_eq line 247
  130. lemma OAI.SharpPlanar.CachedData.ha28_0_25_contains line 248
  131. def OAI.SharpPlanar.CachedData.hk28_0_26 line 251
  132. lemma OAI.SharpPlanar.CachedData.hk28_0_26_contains line 252
  133. def OAI.SharpPlanar.CachedData.ha28_0_26 line 255
  134. lemma OAI.SharpPlanar.CachedData.ha28_0_26_eq line 256
  135. lemma OAI.SharpPlanar.CachedData.ha28_0_26_contains line 257
  136. def OAI.SharpPlanar.CachedData.hk28_0_27 line 260
  137. lemma OAI.SharpPlanar.CachedData.hk28_0_27_contains line 261
  138. def OAI.SharpPlanar.CachedData.ha28_0_27 line 264
  139. lemma OAI.SharpPlanar.CachedData.ha28_0_27_eq line 265
  140. lemma OAI.SharpPlanar.CachedData.ha28_0_27_contains line 266
  141. def OAI.SharpPlanar.CachedData.hk28_0_28 line 269
  142. lemma OAI.SharpPlanar.CachedData.hk28_0_28_contains line 270
  143. def OAI.SharpPlanar.CachedData.ha28_0_28 line 273
  144. lemma OAI.SharpPlanar.CachedData.ha28_0_28_eq line 274
  145. lemma OAI.SharpPlanar.CachedData.ha28_0_28_contains line 275
  146. def OAI.SharpPlanar.CachedData.hk28_0_29 line 278
  147. lemma OAI.SharpPlanar.CachedData.hk28_0_29_contains line 279
  148. def OAI.SharpPlanar.CachedData.ha28_0_29 line 282
  149. lemma OAI.SharpPlanar.CachedData.ha28_0_29_eq line 283
  150. lemma OAI.SharpPlanar.CachedData.ha28_0_29_contains line 284
  151. def OAI.SharpPlanar.CachedData.hk28_0_30 line 287
  152. lemma OAI.SharpPlanar.CachedData.hk28_0_30_contains line 288
  153. def OAI.SharpPlanar.CachedData.ha28_0_30 line 291
  154. lemma OAI.SharpPlanar.CachedData.ha28_0_30_eq line 292
  155. lemma OAI.SharpPlanar.CachedData.ha28_0_30_contains line 293
  156. def OAI.SharpPlanar.CachedData.hk28_1_0 line 296
  157. lemma OAI.SharpPlanar.CachedData.hk28_1_0_contains line 297
  158. def OAI.SharpPlanar.CachedData.ha28_1_0 line 300
  159. lemma OAI.SharpPlanar.CachedData.ha28_1_0_eq line 301
  160. lemma OAI.SharpPlanar.CachedData.ha28_1_0_contains line 302
  161. def OAI.SharpPlanar.CachedData.hk28_1_1 line 305
  162. lemma OAI.SharpPlanar.CachedData.hk28_1_1_contains line 306
  163. def OAI.SharpPlanar.CachedData.ha28_1_1 line 309
  164. lemma OAI.SharpPlanar.CachedData.ha28_1_1_eq line 310
  165. lemma OAI.SharpPlanar.CachedData.ha28_1_1_contains line 311
  166. def OAI.SharpPlanar.CachedData.hk28_1_2 line 314
  167. lemma OAI.SharpPlanar.CachedData.hk28_1_2_contains line 315
  168. def OAI.SharpPlanar.CachedData.ha28_1_2 line 318
  169. lemma OAI.SharpPlanar.CachedData.ha28_1_2_eq line 319
  170. lemma OAI.SharpPlanar.CachedData.ha28_1_2_contains line 320
  171. def OAI.SharpPlanar.CachedData.hk28_1_3 line 323
  172. lemma OAI.SharpPlanar.CachedData.hk28_1_3_contains line 324
  173. def OAI.SharpPlanar.CachedData.ha28_1_3 line 327
  174. lemma OAI.SharpPlanar.CachedData.ha28_1_3_eq line 328
  175. lemma OAI.SharpPlanar.CachedData.ha28_1_3_contains line 329
  176. def OAI.SharpPlanar.CachedData.hk28_1_4 line 332
  177. lemma OAI.SharpPlanar.CachedData.hk28_1_4_contains line 333
  178. def OAI.SharpPlanar.CachedData.ha28_1_4 line 336
  179. lemma OAI.SharpPlanar.CachedData.ha28_1_4_eq line 337
  180. lemma OAI.SharpPlanar.CachedData.ha28_1_4_contains line 338
  181. def OAI.SharpPlanar.CachedData.hk28_1_5 line 341
  182. lemma OAI.SharpPlanar.CachedData.hk28_1_5_contains line 342
  183. def OAI.SharpPlanar.CachedData.ha28_1_5 line 345
  184. lemma OAI.SharpPlanar.CachedData.ha28_1_5_eq line 346
  185. lemma OAI.SharpPlanar.CachedData.ha28_1_5_contains line 347
  186. def OAI.SharpPlanar.CachedData.hk28_1_6 line 350
  187. lemma OAI.SharpPlanar.CachedData.hk28_1_6_contains line 351
  188. def OAI.SharpPlanar.CachedData.ha28_1_6 line 354
  189. lemma OAI.SharpPlanar.CachedData.ha28_1_6_eq line 355
  190. lemma OAI.SharpPlanar.CachedData.ha28_1_6_contains line 356
  191. def OAI.SharpPlanar.CachedData.hk28_1_7 line 359
  192. lemma OAI.SharpPlanar.CachedData.hk28_1_7_contains line 360
  193. def OAI.SharpPlanar.CachedData.ha28_1_7 line 363
  194. lemma OAI.SharpPlanar.CachedData.ha28_1_7_eq line 364
  195. lemma OAI.SharpPlanar.CachedData.ha28_1_7_contains line 365
  196. def OAI.SharpPlanar.CachedData.hk28_1_8 line 368
  197. lemma OAI.SharpPlanar.CachedData.hk28_1_8_contains line 369
  198. def OAI.SharpPlanar.CachedData.ha28_1_8 line 372
  199. lemma OAI.SharpPlanar.CachedData.ha28_1_8_eq line 373
  200. lemma OAI.SharpPlanar.CachedData.ha28_1_8_contains line 374
  201. def OAI.SharpPlanar.CachedData.hk28_1_9 line 377
  202. lemma OAI.SharpPlanar.CachedData.hk28_1_9_contains line 378
  203. def OAI.SharpPlanar.CachedData.ha28_1_9 line 381
  204. lemma OAI.SharpPlanar.CachedData.ha28_1_9_eq line 382
  205. lemma OAI.SharpPlanar.CachedData.ha28_1_9_contains line 383
  206. def OAI.SharpPlanar.CachedData.hk28_1_10 line 386
  207. lemma OAI.SharpPlanar.CachedData.hk28_1_10_contains line 387
  208. def OAI.SharpPlanar.CachedData.ha28_1_10 line 390
  209. lemma OAI.SharpPlanar.CachedData.ha28_1_10_eq line 391
  210. lemma OAI.SharpPlanar.CachedData.ha28_1_10_contains line 392
  211. def OAI.SharpPlanar.CachedData.hk28_1_11 line 395
  212. lemma OAI.SharpPlanar.CachedData.hk28_1_11_contains line 396
  213. def OAI.SharpPlanar.CachedData.ha28_1_11 line 399
  214. lemma OAI.SharpPlanar.CachedData.ha28_1_11_eq line 400
  215. lemma OAI.SharpPlanar.CachedData.ha28_1_11_contains line 401
  216. def OAI.SharpPlanar.CachedData.hk28_1_12 line 404
  217. lemma OAI.SharpPlanar.CachedData.hk28_1_12_contains line 405
  218. def OAI.SharpPlanar.CachedData.ha28_1_12 line 408
  219. lemma OAI.SharpPlanar.CachedData.ha28_1_12_eq line 409
  220. lemma OAI.SharpPlanar.CachedData.ha28_1_12_contains line 410
  221. def OAI.SharpPlanar.CachedData.hk28_1_13 line 413
  222. lemma OAI.SharpPlanar.CachedData.hk28_1_13_contains line 414
  223. def OAI.SharpPlanar.CachedData.ha28_1_13 line 417
  224. lemma OAI.SharpPlanar.CachedData.ha28_1_13_eq line 418
  225. lemma OAI.SharpPlanar.CachedData.ha28_1_13_contains line 419
  226. def OAI.SharpPlanar.CachedData.hk28_1_14 line 422
  227. lemma OAI.SharpPlanar.CachedData.hk28_1_14_contains line 423
  228. def OAI.SharpPlanar.CachedData.ha28_1_14 line 426
  229. lemma OAI.SharpPlanar.CachedData.ha28_1_14_eq line 427
  230. lemma OAI.SharpPlanar.CachedData.ha28_1_14_contains line 428
  231. def OAI.SharpPlanar.CachedData.hk28_1_15 line 431
  232. lemma OAI.SharpPlanar.CachedData.hk28_1_15_contains line 432
  233. def OAI.SharpPlanar.CachedData.ha28_1_15 line 435
  234. lemma OAI.SharpPlanar.CachedData.ha28_1_15_eq line 436
  235. lemma OAI.SharpPlanar.CachedData.ha28_1_15_contains line 437
  236. def OAI.SharpPlanar.CachedData.hk28_1_16 line 440
  237. lemma OAI.SharpPlanar.CachedData.hk28_1_16_contains line 441
  238. def OAI.SharpPlanar.CachedData.ha28_1_16 line 444
  239. lemma OAI.SharpPlanar.CachedData.ha28_1_16_eq line 445
  240. lemma OAI.SharpPlanar.CachedData.ha28_1_16_contains line 446
  241. def OAI.SharpPlanar.CachedData.hk28_1_17 line 449
  242. lemma OAI.SharpPlanar.CachedData.hk28_1_17_contains line 450
  243. def OAI.SharpPlanar.CachedData.ha28_1_17 line 453
  244. lemma OAI.SharpPlanar.CachedData.ha28_1_17_eq line 454
  245. lemma OAI.SharpPlanar.CachedData.ha28_1_17_contains line 455
  246. def OAI.SharpPlanar.CachedData.hk28_1_18 line 458
  247. lemma OAI.SharpPlanar.CachedData.hk28_1_18_contains line 459
  248. def OAI.SharpPlanar.CachedData.ha28_1_18 line 462
  249. lemma OAI.SharpPlanar.CachedData.ha28_1_18_eq line 463
  250. lemma OAI.SharpPlanar.CachedData.ha28_1_18_contains line 464
  251. def OAI.SharpPlanar.CachedData.hk28_1_19 line 467
  252. lemma OAI.SharpPlanar.CachedData.hk28_1_19_contains line 468
  253. def OAI.SharpPlanar.CachedData.ha28_1_19 line 471
  254. lemma OAI.SharpPlanar.CachedData.ha28_1_19_eq line 472
  255. lemma OAI.SharpPlanar.CachedData.ha28_1_19_contains line 473
  256. def OAI.SharpPlanar.CachedData.hk28_1_20 line 476
  257. lemma OAI.SharpPlanar.CachedData.hk28_1_20_contains line 477
  258. def OAI.SharpPlanar.CachedData.ha28_1_20 line 480
  259. lemma OAI.SharpPlanar.CachedData.ha28_1_20_eq line 481
  260. lemma OAI.SharpPlanar.CachedData.ha28_1_20_contains line 482
  261. def OAI.SharpPlanar.CachedData.hk28_1_21 line 485
  262. lemma OAI.SharpPlanar.CachedData.hk28_1_21_contains line 486
  263. def OAI.SharpPlanar.CachedData.ha28_1_21 line 489
  264. lemma OAI.SharpPlanar.CachedData.ha28_1_21_eq line 490
  265. lemma OAI.SharpPlanar.CachedData.ha28_1_21_contains line 491
  266. def OAI.SharpPlanar.CachedData.hk28_1_22 line 494
  267. lemma OAI.SharpPlanar.CachedData.hk28_1_22_contains line 495
  268. def OAI.SharpPlanar.CachedData.ha28_1_22 line 498
  269. lemma OAI.SharpPlanar.CachedData.ha28_1_22_eq line 499
  270. lemma OAI.SharpPlanar.CachedData.ha28_1_22_contains line 500
  271. def OAI.SharpPlanar.CachedData.hk28_1_23 line 503
  272. lemma OAI.SharpPlanar.CachedData.hk28_1_23_contains line 504
  273. def OAI.SharpPlanar.CachedData.ha28_1_23 line 507
  274. lemma OAI.SharpPlanar.CachedData.ha28_1_23_eq line 508
  275. lemma OAI.SharpPlanar.CachedData.ha28_1_23_contains line 509
  276. def OAI.SharpPlanar.CachedData.hk28_1_24 line 512
  277. lemma OAI.SharpPlanar.CachedData.hk28_1_24_contains line 513
  278. def OAI.SharpPlanar.CachedData.ha28_1_24 line 516
  279. lemma OAI.SharpPlanar.CachedData.ha28_1_24_eq line 517
  280. lemma OAI.SharpPlanar.CachedData.ha28_1_24_contains line 518
  281. def OAI.SharpPlanar.CachedData.hk28_1_25 line 521
  282. lemma OAI.SharpPlanar.CachedData.hk28_1_25_contains line 522
  283. def OAI.SharpPlanar.CachedData.ha28_1_25 line 525
  284. lemma OAI.SharpPlanar.CachedData.ha28_1_25_eq line 526
  285. lemma OAI.SharpPlanar.CachedData.ha28_1_25_contains line 527
  286. def OAI.SharpPlanar.CachedData.hk28_1_26 line 530
  287. lemma OAI.SharpPlanar.CachedData.hk28_1_26_contains line 531
  288. def OAI.SharpPlanar.CachedData.ha28_1_26 line 534
  289. lemma OAI.SharpPlanar.CachedData.ha28_1_26_eq line 535
  290. lemma OAI.SharpPlanar.CachedData.ha28_1_26_contains line 536
  291. def OAI.SharpPlanar.CachedData.hk28_1_27 line 539
  292. lemma OAI.SharpPlanar.CachedData.hk28_1_27_contains line 540
  293. def OAI.SharpPlanar.CachedData.ha28_1_27 line 543
  294. lemma OAI.SharpPlanar.CachedData.ha28_1_27_eq line 544
  295. lemma OAI.SharpPlanar.CachedData.ha28_1_27_contains line 545
  296. def OAI.SharpPlanar.CachedData.hk28_1_28 line 548
  297. lemma OAI.SharpPlanar.CachedData.hk28_1_28_contains line 549
  298. def OAI.SharpPlanar.CachedData.ha28_1_28 line 552
  299. lemma OAI.SharpPlanar.CachedData.ha28_1_28_eq line 553
  300. lemma OAI.SharpPlanar.CachedData.ha28_1_28_contains line 554
  301. def OAI.SharpPlanar.CachedData.hk28_1_29 line 557
  302. lemma OAI.SharpPlanar.CachedData.hk28_1_29_contains line 558
  303. def OAI.SharpPlanar.CachedData.ha28_1_29 line 561
  304. lemma OAI.SharpPlanar.CachedData.ha28_1_29_eq line 562
  305. lemma OAI.SharpPlanar.CachedData.ha28_1_29_contains line 563
  306. def OAI.SharpPlanar.CachedData.hk28_1_30 line 566
  307. lemma OAI.SharpPlanar.CachedData.hk28_1_30_contains line 567
  308. def OAI.SharpPlanar.CachedData.ha28_1_30 line 570
  309. lemma OAI.SharpPlanar.CachedData.ha28_1_30_eq line 571
  310. lemma OAI.SharpPlanar.CachedData.ha28_1_30_contains line 572