OAI/Analysis/PlanarPacking/Certificate/Bernstein24.lean

GitHub source file

424 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.Bernstein24.N0_right.t0 line 20
  2. lemma OAI.SharpPlanar.Bernstein24.N0_right.t0_checked line 21
  3. lemma OAI.SharpPlanar.Bernstein24.N0_right.t0_contains line 22
  4. def OAI.SharpPlanar.Bernstein24.N0_right.t1 line 26
  5. lemma OAI.SharpPlanar.Bernstein24.N0_right.t1_checked line 27
  6. lemma OAI.SharpPlanar.Bernstein24.N0_right.t1_contains line 28
  7. def OAI.SharpPlanar.Bernstein24.N0_right.t2 line 32
  8. lemma OAI.SharpPlanar.Bernstein24.N0_right.t2_checked line 33
  9. lemma OAI.SharpPlanar.Bernstein24.N0_right.t2_contains line 34
  10. def OAI.SharpPlanar.Bernstein24.N0_right.t3 line 38
  11. lemma OAI.SharpPlanar.Bernstein24.N0_right.t3_checked line 39
  12. lemma OAI.SharpPlanar.Bernstein24.N0_right.t3_contains line 40
  13. def OAI.SharpPlanar.Bernstein24.N0_right.t4 line 44
  14. lemma OAI.SharpPlanar.Bernstein24.N0_right.t4_checked line 45
  15. lemma OAI.SharpPlanar.Bernstein24.N0_right.t4_contains line 46
  16. def OAI.SharpPlanar.Bernstein24.N0_right.t5 line 50
  17. lemma OAI.SharpPlanar.Bernstein24.N0_right.t5_checked line 51
  18. lemma OAI.SharpPlanar.Bernstein24.N0_right.t5_contains line 52
  19. def OAI.SharpPlanar.Bernstein24.N0_right.t6 line 56
  20. lemma OAI.SharpPlanar.Bernstein24.N0_right.t6_checked line 57
  21. lemma OAI.SharpPlanar.Bernstein24.N0_right.t6_contains line 58
  22. def OAI.SharpPlanar.Bernstein24.N0_right.t7 line 62
  23. lemma OAI.SharpPlanar.Bernstein24.N0_right.t7_checked line 63
  24. lemma OAI.SharpPlanar.Bernstein24.N0_right.t7_contains line 64
  25. def OAI.SharpPlanar.Bernstein24.N0_right.t8 line 68
  26. lemma OAI.SharpPlanar.Bernstein24.N0_right.t8_checked line 69
  27. lemma OAI.SharpPlanar.Bernstein24.N0_right.t8_contains line 70
  28. def OAI.SharpPlanar.Bernstein24.N0_right.t9 line 74
  29. lemma OAI.SharpPlanar.Bernstein24.N0_right.t9_checked line 75
  30. lemma OAI.SharpPlanar.Bernstein24.N0_right.t9_contains line 76
  31. def OAI.SharpPlanar.Bernstein24.N0_right.tr10 line 80
  32. lemma OAI.SharpPlanar.Bernstein24.N0_right.tr10_contains line 81
  33. def OAI.SharpPlanar.Bernstein24.N0_right.t10 line 83
  34. lemma OAI.SharpPlanar.Bernstein24.N0_right.t10_checked line 84
  35. lemma OAI.SharpPlanar.Bernstein24.N0_right.t10_contains line 85
  36. def OAI.SharpPlanar.Bernstein24.N0_right.tr11 line 89
  37. lemma OAI.SharpPlanar.Bernstein24.N0_right.tr11_contains line 90
  38. def OAI.SharpPlanar.Bernstein24.N0_right.t11 line 92
  39. lemma OAI.SharpPlanar.Bernstein24.N0_right.t11_checked line 93
  40. lemma OAI.SharpPlanar.Bernstein24.N0_right.t11_contains line 94
  41. def OAI.SharpPlanar.Bernstein24.N0_right.t12 line 98
  42. lemma OAI.SharpPlanar.Bernstein24.N0_right.t12_contains line 99
  43. def OAI.SharpPlanar.Bernstein24.N0_right.t13 line 101
  44. lemma OAI.SharpPlanar.Bernstein24.N0_right.t13_contains line 102
  45. def OAI.SharpPlanar.Bernstein24.N0_right.t14 line 104
  46. lemma OAI.SharpPlanar.Bernstein24.N0_right.t14_contains line 105
  47. def OAI.SharpPlanar.Bernstein24.N0_right.t15 line 107
  48. lemma OAI.SharpPlanar.Bernstein24.N0_right.t15_contains line 108
  49. def OAI.SharpPlanar.Bernstein24.N0_right.t16 line 110
  50. lemma OAI.SharpPlanar.Bernstein24.N0_right.t16_contains line 111
  51. def OAI.SharpPlanar.Bernstein24.N0_right.t17 line 113
  52. lemma OAI.SharpPlanar.Bernstein24.N0_right.t17_contains line 114
  53. def OAI.SharpPlanar.Bernstein24.N0_right.t18 line 116
  54. lemma OAI.SharpPlanar.Bernstein24.N0_right.t18_contains line 117
  55. def OAI.SharpPlanar.Bernstein24.N0_right.t19 line 119
  56. lemma OAI.SharpPlanar.Bernstein24.N0_right.t19_contains line 120
  57. def OAI.SharpPlanar.Bernstein24.N0_right.t20 line 122
  58. lemma OAI.SharpPlanar.Bernstein24.N0_right.t20_contains line 123
  59. def OAI.SharpPlanar.Bernstein24.N0_right.t21 line 125
  60. lemma OAI.SharpPlanar.Bernstein24.N0_right.t21_contains line 126
  61. def OAI.SharpPlanar.Bernstein24.N0_right.t22 line 128
  62. lemma OAI.SharpPlanar.Bernstein24.N0_right.t22_contains line 129
  63. def OAI.SharpPlanar.Bernstein24.N0_right.t23 line 131
  64. lemma OAI.SharpPlanar.Bernstein24.N0_right.t23_contains line 132
  65. def OAI.SharpPlanar.Bernstein24.N0_right.t24 line 134
  66. lemma OAI.SharpPlanar.Bernstein24.N0_right.t24_contains line 135
  67. def OAI.SharpPlanar.Bernstein24.N0_right.t25 line 137
  68. lemma OAI.SharpPlanar.Bernstein24.N0_right.t25_contains line 138
  69. def OAI.SharpPlanar.Bernstein24.N0_right.t26 line 140
  70. lemma OAI.SharpPlanar.Bernstein24.N0_right.t26_contains line 141
  71. def OAI.SharpPlanar.Bernstein24.N0_right.t27 line 143
  72. lemma OAI.SharpPlanar.Bernstein24.N0_right.t27_contains line 144
  73. def OAI.SharpPlanar.Bernstein24.N0_right.t28 line 146
  74. lemma OAI.SharpPlanar.Bernstein24.N0_right.t28_contains line 147
  75. def OAI.SharpPlanar.Bernstein24.N0_right.ts line 149
  76. lemma OAI.SharpPlanar.Bernstein24.N0_right.ts_contains line 150
  77. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound0 line 181
  78. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound1 line 183
  79. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound2 line 185
  80. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound3 line 187
  81. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound4 line 189
  82. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound5 line 191
  83. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound6 line 193
  84. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound7 line 195
  85. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound8 line 197
  86. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound9 line 199
  87. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound10 line 201
  88. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound11 line 203
  89. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound12 line 205
  90. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound13 line 207
  91. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound14 line 209
  92. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound15 line 211
  93. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound16 line 213
  94. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound17 line 215
  95. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound18 line 217
  96. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound19 line 219
  97. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound20 line 221
  98. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound21 line 223
  99. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound22 line 225
  100. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound23 line 227
  101. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound24 line 229
  102. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound25 line 231
  103. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound26 line 233
  104. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound27 line 235
  105. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound28 line 237
  106. lemma OAI.SharpPlanar.Bernstein24.N0_right.bound line 239
  107. def OAI.SharpPlanar.Bernstein24.N1_right.t0 line 272
  108. lemma OAI.SharpPlanar.Bernstein24.N1_right.t0_checked line 273
  109. lemma OAI.SharpPlanar.Bernstein24.N1_right.t0_contains line 274
  110. def OAI.SharpPlanar.Bernstein24.N1_right.t1 line 278
  111. lemma OAI.SharpPlanar.Bernstein24.N1_right.t1_checked line 279
  112. lemma OAI.SharpPlanar.Bernstein24.N1_right.t1_contains line 280
  113. def OAI.SharpPlanar.Bernstein24.N1_right.t2 line 284
  114. lemma OAI.SharpPlanar.Bernstein24.N1_right.t2_checked line 285
  115. lemma OAI.SharpPlanar.Bernstein24.N1_right.t2_contains line 286
  116. def OAI.SharpPlanar.Bernstein24.N1_right.t3 line 290
  117. lemma OAI.SharpPlanar.Bernstein24.N1_right.t3_checked line 291
  118. lemma OAI.SharpPlanar.Bernstein24.N1_right.t3_contains line 292
  119. def OAI.SharpPlanar.Bernstein24.N1_right.t4 line 296
  120. lemma OAI.SharpPlanar.Bernstein24.N1_right.t4_checked line 297
  121. lemma OAI.SharpPlanar.Bernstein24.N1_right.t4_contains line 298
  122. def OAI.SharpPlanar.Bernstein24.N1_right.t5 line 302
  123. lemma OAI.SharpPlanar.Bernstein24.N1_right.t5_checked line 303
  124. lemma OAI.SharpPlanar.Bernstein24.N1_right.t5_contains line 304
  125. def OAI.SharpPlanar.Bernstein24.N1_right.t6 line 308
  126. lemma OAI.SharpPlanar.Bernstein24.N1_right.t6_checked line 309
  127. lemma OAI.SharpPlanar.Bernstein24.N1_right.t6_contains line 310
  128. def OAI.SharpPlanar.Bernstein24.N1_right.t7 line 314
  129. lemma OAI.SharpPlanar.Bernstein24.N1_right.t7_checked line 315
  130. lemma OAI.SharpPlanar.Bernstein24.N1_right.t7_contains line 316
  131. def OAI.SharpPlanar.Bernstein24.N1_right.t8 line 320
  132. lemma OAI.SharpPlanar.Bernstein24.N1_right.t8_checked line 321
  133. lemma OAI.SharpPlanar.Bernstein24.N1_right.t8_contains line 322
  134. def OAI.SharpPlanar.Bernstein24.N1_right.t9 line 326
  135. lemma OAI.SharpPlanar.Bernstein24.N1_right.t9_checked line 327
  136. lemma OAI.SharpPlanar.Bernstein24.N1_right.t9_contains line 328
  137. def OAI.SharpPlanar.Bernstein24.N1_right.tr10 line 332
  138. lemma OAI.SharpPlanar.Bernstein24.N1_right.tr10_contains line 333
  139. def OAI.SharpPlanar.Bernstein24.N1_right.t10 line 335
  140. lemma OAI.SharpPlanar.Bernstein24.N1_right.t10_checked line 336
  141. lemma OAI.SharpPlanar.Bernstein24.N1_right.t10_contains line 337
  142. def OAI.SharpPlanar.Bernstein24.N1_right.tr11 line 341
  143. lemma OAI.SharpPlanar.Bernstein24.N1_right.tr11_contains line 342
  144. def OAI.SharpPlanar.Bernstein24.N1_right.t11 line 344
  145. lemma OAI.SharpPlanar.Bernstein24.N1_right.t11_checked line 345
  146. lemma OAI.SharpPlanar.Bernstein24.N1_right.t11_contains line 346
  147. def OAI.SharpPlanar.Bernstein24.N1_right.t12 line 350
  148. lemma OAI.SharpPlanar.Bernstein24.N1_right.t12_contains line 351
  149. def OAI.SharpPlanar.Bernstein24.N1_right.t13 line 353
  150. lemma OAI.SharpPlanar.Bernstein24.N1_right.t13_contains line 354
  151. def OAI.SharpPlanar.Bernstein24.N1_right.t14 line 356
  152. lemma OAI.SharpPlanar.Bernstein24.N1_right.t14_contains line 357
  153. def OAI.SharpPlanar.Bernstein24.N1_right.t15 line 359
  154. lemma OAI.SharpPlanar.Bernstein24.N1_right.t15_contains line 360
  155. def OAI.SharpPlanar.Bernstein24.N1_right.t16 line 362
  156. lemma OAI.SharpPlanar.Bernstein24.N1_right.t16_contains line 363
  157. def OAI.SharpPlanar.Bernstein24.N1_right.t17 line 365
  158. lemma OAI.SharpPlanar.Bernstein24.N1_right.t17_contains line 366
  159. def OAI.SharpPlanar.Bernstein24.N1_right.t18 line 368
  160. lemma OAI.SharpPlanar.Bernstein24.N1_right.t18_contains line 369
  161. def OAI.SharpPlanar.Bernstein24.N1_right.t19 line 371
  162. lemma OAI.SharpPlanar.Bernstein24.N1_right.t19_contains line 372
  163. def OAI.SharpPlanar.Bernstein24.N1_right.t20 line 374
  164. lemma OAI.SharpPlanar.Bernstein24.N1_right.t20_contains line 375
  165. def OAI.SharpPlanar.Bernstein24.N1_right.t21 line 377
  166. lemma OAI.SharpPlanar.Bernstein24.N1_right.t21_contains line 378
  167. def OAI.SharpPlanar.Bernstein24.N1_right.t22 line 380
  168. lemma OAI.SharpPlanar.Bernstein24.N1_right.t22_contains line 381
  169. def OAI.SharpPlanar.Bernstein24.N1_right.t23 line 383
  170. lemma OAI.SharpPlanar.Bernstein24.N1_right.t23_contains line 384
  171. def OAI.SharpPlanar.Bernstein24.N1_right.t24 line 386
  172. lemma OAI.SharpPlanar.Bernstein24.N1_right.t24_contains line 387
  173. def OAI.SharpPlanar.Bernstein24.N1_right.t25 line 389
  174. lemma OAI.SharpPlanar.Bernstein24.N1_right.t25_contains line 390
  175. def OAI.SharpPlanar.Bernstein24.N1_right.t26 line 392
  176. lemma OAI.SharpPlanar.Bernstein24.N1_right.t26_contains line 393
  177. def OAI.SharpPlanar.Bernstein24.N1_right.t27 line 395
  178. lemma OAI.SharpPlanar.Bernstein24.N1_right.t27_contains line 396
  179. def OAI.SharpPlanar.Bernstein24.N1_right.t28 line 398
  180. lemma OAI.SharpPlanar.Bernstein24.N1_right.t28_contains line 399
  181. def OAI.SharpPlanar.Bernstein24.N1_right.ts line 401
  182. lemma OAI.SharpPlanar.Bernstein24.N1_right.ts_contains line 402
  183. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound0 line 433
  184. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound1 line 435
  185. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound2 line 437
  186. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound3 line 439
  187. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound4 line 441
  188. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound5 line 443
  189. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound6 line 445
  190. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound7 line 447
  191. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound8 line 449
  192. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound9 line 451
  193. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound10 line 453
  194. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound11 line 455
  195. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound12 line 457
  196. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound13 line 459
  197. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound14 line 461
  198. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound15 line 463
  199. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound16 line 465
  200. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound17 line 467
  201. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound18 line 469
  202. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound19 line 471
  203. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound20 line 473
  204. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound21 line 475
  205. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound22 line 477
  206. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound23 line 479
  207. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound24 line 481
  208. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound25 line 483
  209. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound26 line 485
  210. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound27 line 487
  211. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound28 line 489
  212. lemma OAI.SharpPlanar.Bernstein24.N1_right.bound line 491
  213. def OAI.SharpPlanar.Bernstein24.N0_left.t0 line 524
  214. lemma OAI.SharpPlanar.Bernstein24.N0_left.t0_checked line 525
  215. lemma OAI.SharpPlanar.Bernstein24.N0_left.t0_contains line 526
  216. def OAI.SharpPlanar.Bernstein24.N0_left.t1 line 530
  217. lemma OAI.SharpPlanar.Bernstein24.N0_left.t1_checked line 531
  218. lemma OAI.SharpPlanar.Bernstein24.N0_left.t1_contains line 532
  219. def OAI.SharpPlanar.Bernstein24.N0_left.t2 line 536
  220. lemma OAI.SharpPlanar.Bernstein24.N0_left.t2_checked line 537
  221. lemma OAI.SharpPlanar.Bernstein24.N0_left.t2_contains line 538
  222. def OAI.SharpPlanar.Bernstein24.N0_left.t3 line 542
  223. lemma OAI.SharpPlanar.Bernstein24.N0_left.t3_checked line 543
  224. lemma OAI.SharpPlanar.Bernstein24.N0_left.t3_contains line 544
  225. def OAI.SharpPlanar.Bernstein24.N0_left.t4 line 548
  226. lemma OAI.SharpPlanar.Bernstein24.N0_left.t4_checked line 549
  227. lemma OAI.SharpPlanar.Bernstein24.N0_left.t4_contains line 550
  228. def OAI.SharpPlanar.Bernstein24.N0_left.t5 line 554
  229. lemma OAI.SharpPlanar.Bernstein24.N0_left.t5_checked line 555
  230. lemma OAI.SharpPlanar.Bernstein24.N0_left.t5_contains line 556
  231. def OAI.SharpPlanar.Bernstein24.N0_left.t6 line 560
  232. lemma OAI.SharpPlanar.Bernstein24.N0_left.t6_checked line 561
  233. lemma OAI.SharpPlanar.Bernstein24.N0_left.t6_contains line 562
  234. def OAI.SharpPlanar.Bernstein24.N0_left.t7 line 566
  235. lemma OAI.SharpPlanar.Bernstein24.N0_left.t7_checked line 567
  236. lemma OAI.SharpPlanar.Bernstein24.N0_left.t7_contains line 568
  237. def OAI.SharpPlanar.Bernstein24.N0_left.t8 line 572
  238. lemma OAI.SharpPlanar.Bernstein24.N0_left.t8_checked line 573
  239. lemma OAI.SharpPlanar.Bernstein24.N0_left.t8_contains line 574
  240. def OAI.SharpPlanar.Bernstein24.N0_left.t9 line 578
  241. lemma OAI.SharpPlanar.Bernstein24.N0_left.t9_checked line 579
  242. lemma OAI.SharpPlanar.Bernstein24.N0_left.t9_contains line 580
  243. def OAI.SharpPlanar.Bernstein24.N0_left.tr10 line 584
  244. lemma OAI.SharpPlanar.Bernstein24.N0_left.tr10_contains line 585
  245. def OAI.SharpPlanar.Bernstein24.N0_left.t10 line 587
  246. lemma OAI.SharpPlanar.Bernstein24.N0_left.t10_checked line 588
  247. lemma OAI.SharpPlanar.Bernstein24.N0_left.t10_contains line 589
  248. def OAI.SharpPlanar.Bernstein24.N0_left.tr11 line 593
  249. lemma OAI.SharpPlanar.Bernstein24.N0_left.tr11_contains line 594
  250. def OAI.SharpPlanar.Bernstein24.N0_left.t11 line 596
  251. lemma OAI.SharpPlanar.Bernstein24.N0_left.t11_checked line 597
  252. lemma OAI.SharpPlanar.Bernstein24.N0_left.t11_contains line 598
  253. def OAI.SharpPlanar.Bernstein24.N0_left.t12 line 602
  254. lemma OAI.SharpPlanar.Bernstein24.N0_left.t12_contains line 603
  255. def OAI.SharpPlanar.Bernstein24.N0_left.t13 line 605
  256. lemma OAI.SharpPlanar.Bernstein24.N0_left.t13_contains line 606
  257. def OAI.SharpPlanar.Bernstein24.N0_left.t14 line 608
  258. lemma OAI.SharpPlanar.Bernstein24.N0_left.t14_contains line 609
  259. def OAI.SharpPlanar.Bernstein24.N0_left.t15 line 611
  260. lemma OAI.SharpPlanar.Bernstein24.N0_left.t15_contains line 612
  261. def OAI.SharpPlanar.Bernstein24.N0_left.t16 line 614
  262. lemma OAI.SharpPlanar.Bernstein24.N0_left.t16_contains line 615
  263. def OAI.SharpPlanar.Bernstein24.N0_left.t17 line 617
  264. lemma OAI.SharpPlanar.Bernstein24.N0_left.t17_contains line 618
  265. def OAI.SharpPlanar.Bernstein24.N0_left.t18 line 620
  266. lemma OAI.SharpPlanar.Bernstein24.N0_left.t18_contains line 621
  267. def OAI.SharpPlanar.Bernstein24.N0_left.t19 line 623
  268. lemma OAI.SharpPlanar.Bernstein24.N0_left.t19_contains line 624
  269. def OAI.SharpPlanar.Bernstein24.N0_left.t20 line 626
  270. lemma OAI.SharpPlanar.Bernstein24.N0_left.t20_contains line 627
  271. def OAI.SharpPlanar.Bernstein24.N0_left.t21 line 629
  272. lemma OAI.SharpPlanar.Bernstein24.N0_left.t21_contains line 630
  273. def OAI.SharpPlanar.Bernstein24.N0_left.t22 line 632
  274. lemma OAI.SharpPlanar.Bernstein24.N0_left.t22_contains line 633
  275. def OAI.SharpPlanar.Bernstein24.N0_left.t23 line 635
  276. lemma OAI.SharpPlanar.Bernstein24.N0_left.t23_contains line 636
  277. def OAI.SharpPlanar.Bernstein24.N0_left.t24 line 638
  278. lemma OAI.SharpPlanar.Bernstein24.N0_left.t24_contains line 639
  279. def OAI.SharpPlanar.Bernstein24.N0_left.t25 line 641
  280. lemma OAI.SharpPlanar.Bernstein24.N0_left.t25_contains line 642
  281. def OAI.SharpPlanar.Bernstein24.N0_left.t26 line 644
  282. lemma OAI.SharpPlanar.Bernstein24.N0_left.t26_contains line 645
  283. def OAI.SharpPlanar.Bernstein24.N0_left.t27 line 647
  284. lemma OAI.SharpPlanar.Bernstein24.N0_left.t27_contains line 648
  285. def OAI.SharpPlanar.Bernstein24.N0_left.t28 line 650
  286. lemma OAI.SharpPlanar.Bernstein24.N0_left.t28_contains line 651
  287. def OAI.SharpPlanar.Bernstein24.N0_left.ts line 653
  288. lemma OAI.SharpPlanar.Bernstein24.N0_left.ts_contains line 654
  289. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound0 line 685
  290. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound1 line 687
  291. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound2 line 689
  292. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound3 line 691
  293. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound4 line 693
  294. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound5 line 695
  295. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound6 line 697
  296. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound7 line 699
  297. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound8 line 701
  298. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound9 line 703
  299. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound10 line 705
  300. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound11 line 707
  301. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound12 line 709
  302. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound13 line 711
  303. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound14 line 713
  304. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound15 line 715
  305. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound16 line 717
  306. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound17 line 719
  307. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound18 line 721
  308. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound19 line 723
  309. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound20 line 725
  310. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound21 line 727
  311. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound22 line 729
  312. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound23 line 731
  313. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound24 line 733
  314. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound25 line 735
  315. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound26 line 737
  316. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound27 line 739
  317. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound28 line 741
  318. lemma OAI.SharpPlanar.Bernstein24.N0_left.bound line 743
  319. def OAI.SharpPlanar.Bernstein24.N1_left.t0 line 776
  320. lemma OAI.SharpPlanar.Bernstein24.N1_left.t0_checked line 777
  321. lemma OAI.SharpPlanar.Bernstein24.N1_left.t0_contains line 778
  322. def OAI.SharpPlanar.Bernstein24.N1_left.t1 line 782
  323. lemma OAI.SharpPlanar.Bernstein24.N1_left.t1_checked line 783
  324. lemma OAI.SharpPlanar.Bernstein24.N1_left.t1_contains line 784
  325. def OAI.SharpPlanar.Bernstein24.N1_left.t2 line 788
  326. lemma OAI.SharpPlanar.Bernstein24.N1_left.t2_checked line 789
  327. lemma OAI.SharpPlanar.Bernstein24.N1_left.t2_contains line 790
  328. def OAI.SharpPlanar.Bernstein24.N1_left.t3 line 794
  329. lemma OAI.SharpPlanar.Bernstein24.N1_left.t3_checked line 795
  330. lemma OAI.SharpPlanar.Bernstein24.N1_left.t3_contains line 796
  331. def OAI.SharpPlanar.Bernstein24.N1_left.t4 line 800
  332. lemma OAI.SharpPlanar.Bernstein24.N1_left.t4_checked line 801
  333. lemma OAI.SharpPlanar.Bernstein24.N1_left.t4_contains line 802
  334. def OAI.SharpPlanar.Bernstein24.N1_left.t5 line 806
  335. lemma OAI.SharpPlanar.Bernstein24.N1_left.t5_checked line 807
  336. lemma OAI.SharpPlanar.Bernstein24.N1_left.t5_contains line 808
  337. def OAI.SharpPlanar.Bernstein24.N1_left.t6 line 812
  338. lemma OAI.SharpPlanar.Bernstein24.N1_left.t6_checked line 813
  339. lemma OAI.SharpPlanar.Bernstein24.N1_left.t6_contains line 814
  340. def OAI.SharpPlanar.Bernstein24.N1_left.t7 line 818
  341. lemma OAI.SharpPlanar.Bernstein24.N1_left.t7_checked line 819
  342. lemma OAI.SharpPlanar.Bernstein24.N1_left.t7_contains line 820
  343. def OAI.SharpPlanar.Bernstein24.N1_left.t8 line 824
  344. lemma OAI.SharpPlanar.Bernstein24.N1_left.t8_checked line 825
  345. lemma OAI.SharpPlanar.Bernstein24.N1_left.t8_contains line 826
  346. def OAI.SharpPlanar.Bernstein24.N1_left.t9 line 830
  347. lemma OAI.SharpPlanar.Bernstein24.N1_left.t9_checked line 831
  348. lemma OAI.SharpPlanar.Bernstein24.N1_left.t9_contains line 832
  349. def OAI.SharpPlanar.Bernstein24.N1_left.tr10 line 836
  350. lemma OAI.SharpPlanar.Bernstein24.N1_left.tr10_contains line 837
  351. def OAI.SharpPlanar.Bernstein24.N1_left.t10 line 839
  352. lemma OAI.SharpPlanar.Bernstein24.N1_left.t10_checked line 840
  353. lemma OAI.SharpPlanar.Bernstein24.N1_left.t10_contains line 841
  354. def OAI.SharpPlanar.Bernstein24.N1_left.tr11 line 845
  355. lemma OAI.SharpPlanar.Bernstein24.N1_left.tr11_contains line 846
  356. def OAI.SharpPlanar.Bernstein24.N1_left.t11 line 848
  357. lemma OAI.SharpPlanar.Bernstein24.N1_left.t11_checked line 849
  358. lemma OAI.SharpPlanar.Bernstein24.N1_left.t11_contains line 850
  359. def OAI.SharpPlanar.Bernstein24.N1_left.t12 line 854
  360. lemma OAI.SharpPlanar.Bernstein24.N1_left.t12_contains line 855
  361. def OAI.SharpPlanar.Bernstein24.N1_left.t13 line 857
  362. lemma OAI.SharpPlanar.Bernstein24.N1_left.t13_contains line 858
  363. def OAI.SharpPlanar.Bernstein24.N1_left.t14 line 860
  364. lemma OAI.SharpPlanar.Bernstein24.N1_left.t14_contains line 861
  365. def OAI.SharpPlanar.Bernstein24.N1_left.t15 line 863
  366. lemma OAI.SharpPlanar.Bernstein24.N1_left.t15_contains line 864
  367. def OAI.SharpPlanar.Bernstein24.N1_left.t16 line 866
  368. lemma OAI.SharpPlanar.Bernstein24.N1_left.t16_contains line 867
  369. def OAI.SharpPlanar.Bernstein24.N1_left.t17 line 869
  370. lemma OAI.SharpPlanar.Bernstein24.N1_left.t17_contains line 870
  371. def OAI.SharpPlanar.Bernstein24.N1_left.t18 line 872
  372. lemma OAI.SharpPlanar.Bernstein24.N1_left.t18_contains line 873
  373. def OAI.SharpPlanar.Bernstein24.N1_left.t19 line 875
  374. lemma OAI.SharpPlanar.Bernstein24.N1_left.t19_contains line 876
  375. def OAI.SharpPlanar.Bernstein24.N1_left.t20 line 878
  376. lemma OAI.SharpPlanar.Bernstein24.N1_left.t20_contains line 879
  377. def OAI.SharpPlanar.Bernstein24.N1_left.t21 line 881
  378. lemma OAI.SharpPlanar.Bernstein24.N1_left.t21_contains line 882
  379. def OAI.SharpPlanar.Bernstein24.N1_left.t22 line 884
  380. lemma OAI.SharpPlanar.Bernstein24.N1_left.t22_contains line 885
  381. def OAI.SharpPlanar.Bernstein24.N1_left.t23 line 887
  382. lemma OAI.SharpPlanar.Bernstein24.N1_left.t23_contains line 888
  383. def OAI.SharpPlanar.Bernstein24.N1_left.t24 line 890
  384. lemma OAI.SharpPlanar.Bernstein24.N1_left.t24_contains line 891
  385. def OAI.SharpPlanar.Bernstein24.N1_left.t25 line 893
  386. lemma OAI.SharpPlanar.Bernstein24.N1_left.t25_contains line 894
  387. def OAI.SharpPlanar.Bernstein24.N1_left.t26 line 896
  388. lemma OAI.SharpPlanar.Bernstein24.N1_left.t26_contains line 897
  389. def OAI.SharpPlanar.Bernstein24.N1_left.t27 line 899
  390. lemma OAI.SharpPlanar.Bernstein24.N1_left.t27_contains line 900
  391. def OAI.SharpPlanar.Bernstein24.N1_left.t28 line 902
  392. lemma OAI.SharpPlanar.Bernstein24.N1_left.t28_contains line 903
  393. def OAI.SharpPlanar.Bernstein24.N1_left.ts line 905
  394. lemma OAI.SharpPlanar.Bernstein24.N1_left.ts_contains line 906
  395. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound0 line 937
  396. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound1 line 939
  397. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound2 line 941
  398. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound3 line 943
  399. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound4 line 945
  400. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound5 line 947
  401. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound6 line 949
  402. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound7 line 951
  403. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound8 line 953
  404. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound9 line 955
  405. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound10 line 957
  406. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound11 line 959
  407. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound12 line 961
  408. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound13 line 963
  409. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound14 line 965
  410. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound15 line 967
  411. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound16 line 969
  412. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound17 line 971
  413. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound18 line 973
  414. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound19 line 975
  415. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound20 line 977
  416. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound21 line 979
  417. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound22 line 981
  418. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound23 line 983
  419. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound24 line 985
  420. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound25 line 987
  421. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound26 line 989
  422. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound27 line 991
  423. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound28 line 993
  424. lemma OAI.SharpPlanar.Bernstein24.N1_left.bound line 995