OAI/Analysis/PlanarPacking/Certificate/Bernstein1.lean

GitHub source file

357 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.Bernstein1.N0_right.t0 line 23
  2. lemma OAI.SharpPlanar.Bernstein1.N0_right.t0_checked line 24
  3. lemma OAI.SharpPlanar.Bernstein1.N0_right.t0_contains line 25
  4. def OAI.SharpPlanar.Bernstein1.N0_right.t1 line 29
  5. lemma OAI.SharpPlanar.Bernstein1.N0_right.t1_checked line 30
  6. lemma OAI.SharpPlanar.Bernstein1.N0_right.t1_contains line 31
  7. def OAI.SharpPlanar.Bernstein1.N0_right.t2 line 35
  8. lemma OAI.SharpPlanar.Bernstein1.N0_right.t2_checked line 36
  9. lemma OAI.SharpPlanar.Bernstein1.N0_right.t2_contains line 37
  10. def OAI.SharpPlanar.Bernstein1.N0_right.t3 line 41
  11. lemma OAI.SharpPlanar.Bernstein1.N0_right.t3_checked line 42
  12. lemma OAI.SharpPlanar.Bernstein1.N0_right.t3_contains line 43
  13. def OAI.SharpPlanar.Bernstein1.N0_right.t4 line 47
  14. lemma OAI.SharpPlanar.Bernstein1.N0_right.t4_checked line 48
  15. lemma OAI.SharpPlanar.Bernstein1.N0_right.t4_contains line 49
  16. def OAI.SharpPlanar.Bernstein1.N0_right.t5 line 53
  17. lemma OAI.SharpPlanar.Bernstein1.N0_right.t5_checked line 54
  18. lemma OAI.SharpPlanar.Bernstein1.N0_right.t5_contains line 55
  19. def OAI.SharpPlanar.Bernstein1.N0_right.t6 line 59
  20. lemma OAI.SharpPlanar.Bernstein1.N0_right.t6_checked line 60
  21. lemma OAI.SharpPlanar.Bernstein1.N0_right.t6_contains line 61
  22. def OAI.SharpPlanar.Bernstein1.N0_right.t7 line 65
  23. lemma OAI.SharpPlanar.Bernstein1.N0_right.t7_checked line 66
  24. lemma OAI.SharpPlanar.Bernstein1.N0_right.t7_contains line 67
  25. def OAI.SharpPlanar.Bernstein1.N0_right.t8 line 71
  26. lemma OAI.SharpPlanar.Bernstein1.N0_right.t8_checked line 72
  27. lemma OAI.SharpPlanar.Bernstein1.N0_right.t8_contains line 73
  28. def OAI.SharpPlanar.Bernstein1.N0_right.t9 line 77
  29. lemma OAI.SharpPlanar.Bernstein1.N0_right.t9_checked line 78
  30. lemma OAI.SharpPlanar.Bernstein1.N0_right.t9_contains line 79
  31. def OAI.SharpPlanar.Bernstein1.N0_right.t10 line 83
  32. lemma OAI.SharpPlanar.Bernstein1.N0_right.t10_checked line 84
  33. lemma OAI.SharpPlanar.Bernstein1.N0_right.t10_contains line 85
  34. def OAI.SharpPlanar.Bernstein1.N0_right.t11 line 89
  35. lemma OAI.SharpPlanar.Bernstein1.N0_right.t11_checked line 90
  36. lemma OAI.SharpPlanar.Bernstein1.N0_right.t11_contains line 91
  37. def OAI.SharpPlanar.Bernstein1.N0_right.t12 line 95
  38. lemma OAI.SharpPlanar.Bernstein1.N0_right.t12_checked line 96
  39. lemma OAI.SharpPlanar.Bernstein1.N0_right.t12_contains line 97
  40. def OAI.SharpPlanar.Bernstein1.N0_right.t13 line 101
  41. lemma OAI.SharpPlanar.Bernstein1.N0_right.t13_checked line 102
  42. lemma OAI.SharpPlanar.Bernstein1.N0_right.t13_contains line 103
  43. def OAI.SharpPlanar.Bernstein1.N0_right.t14 line 107
  44. lemma OAI.SharpPlanar.Bernstein1.N0_right.t14_checked line 108
  45. lemma OAI.SharpPlanar.Bernstein1.N0_right.t14_contains line 109
  46. def OAI.SharpPlanar.Bernstein1.N0_right.t15 line 113
  47. lemma OAI.SharpPlanar.Bernstein1.N0_right.t15_checked line 114
  48. lemma OAI.SharpPlanar.Bernstein1.N0_right.t15_contains line 115
  49. def OAI.SharpPlanar.Bernstein1.N0_right.t16 line 119
  50. lemma OAI.SharpPlanar.Bernstein1.N0_right.t16_checked line 120
  51. lemma OAI.SharpPlanar.Bernstein1.N0_right.t16_contains line 121
  52. def OAI.SharpPlanar.Bernstein1.N0_right.t17 line 125
  53. lemma OAI.SharpPlanar.Bernstein1.N0_right.t17_checked line 126
  54. lemma OAI.SharpPlanar.Bernstein1.N0_right.t17_contains line 127
  55. def OAI.SharpPlanar.Bernstein1.N0_right.t18 line 131
  56. lemma OAI.SharpPlanar.Bernstein1.N0_right.t18_checked line 132
  57. lemma OAI.SharpPlanar.Bernstein1.N0_right.t18_contains line 133
  58. def OAI.SharpPlanar.Bernstein1.N0_right.t19 line 137
  59. lemma OAI.SharpPlanar.Bernstein1.N0_right.t19_checked line 138
  60. lemma OAI.SharpPlanar.Bernstein1.N0_right.t19_contains line 139
  61. def OAI.SharpPlanar.Bernstein1.N0_right.t20 line 143
  62. lemma OAI.SharpPlanar.Bernstein1.N0_right.t20_checked line 144
  63. lemma OAI.SharpPlanar.Bernstein1.N0_right.t20_contains line 145
  64. def OAI.SharpPlanar.Bernstein1.N0_right.t21 line 149
  65. lemma OAI.SharpPlanar.Bernstein1.N0_right.t21_checked line 150
  66. lemma OAI.SharpPlanar.Bernstein1.N0_right.t21_contains line 151
  67. def OAI.SharpPlanar.Bernstein1.N0_right.t22 line 155
  68. lemma OAI.SharpPlanar.Bernstein1.N0_right.t22_checked line 156
  69. lemma OAI.SharpPlanar.Bernstein1.N0_right.t22_contains line 157
  70. def OAI.SharpPlanar.Bernstein1.N0_right.t23 line 161
  71. lemma OAI.SharpPlanar.Bernstein1.N0_right.t23_checked line 162
  72. lemma OAI.SharpPlanar.Bernstein1.N0_right.t23_contains line 163
  73. def OAI.SharpPlanar.Bernstein1.N0_right.t24 line 167
  74. lemma OAI.SharpPlanar.Bernstein1.N0_right.t24_checked line 168
  75. lemma OAI.SharpPlanar.Bernstein1.N0_right.t24_contains line 169
  76. def OAI.SharpPlanar.Bernstein1.N0_right.t25 line 173
  77. lemma OAI.SharpPlanar.Bernstein1.N0_right.t25_checked line 174
  78. lemma OAI.SharpPlanar.Bernstein1.N0_right.t25_contains line 175
  79. def OAI.SharpPlanar.Bernstein1.N0_right.t26 line 179
  80. lemma OAI.SharpPlanar.Bernstein1.N0_right.t26_checked line 180
  81. lemma OAI.SharpPlanar.Bernstein1.N0_right.t26_contains line 181
  82. def OAI.SharpPlanar.Bernstein1.N0_right.t27 line 185
  83. lemma OAI.SharpPlanar.Bernstein1.N0_right.t27_checked line 186
  84. lemma OAI.SharpPlanar.Bernstein1.N0_right.t27_contains line 187
  85. def OAI.SharpPlanar.Bernstein1.N0_right.t28 line 191
  86. lemma OAI.SharpPlanar.Bernstein1.N0_right.t28_checked line 192
  87. lemma OAI.SharpPlanar.Bernstein1.N0_right.t28_contains line 193
  88. def OAI.SharpPlanar.Bernstein1.N0_right.ts line 197
  89. lemma OAI.SharpPlanar.Bernstein1.N0_right.ts_contains line 198
  90. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound0 line 229
  91. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound1 line 231
  92. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound2 line 233
  93. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound3 line 235
  94. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound4 line 237
  95. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound5 line 239
  96. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound6 line 241
  97. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound7 line 243
  98. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound8 line 245
  99. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound9 line 247
  100. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound10 line 249
  101. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound11 line 251
  102. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound12 line 253
  103. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound13 line 255
  104. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound14 line 257
  105. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound15 line 259
  106. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound16 line 261
  107. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound17 line 263
  108. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound18 line 265
  109. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound19 line 267
  110. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound20 line 269
  111. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound21 line 271
  112. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound22 line 273
  113. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound23 line 275
  114. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound24 line 277
  115. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound25 line 279
  116. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound26 line 281
  117. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound27 line 283
  118. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound28 line 285
  119. lemma OAI.SharpPlanar.Bernstein1.N0_right.bound line 287
  120. def OAI.SharpPlanar.Bernstein1.N1_right.t0 line 320
  121. lemma OAI.SharpPlanar.Bernstein1.N1_right.t0_checked line 321
  122. lemma OAI.SharpPlanar.Bernstein1.N1_right.t0_contains line 322
  123. def OAI.SharpPlanar.Bernstein1.N1_right.t1 line 326
  124. lemma OAI.SharpPlanar.Bernstein1.N1_right.t1_checked line 327
  125. lemma OAI.SharpPlanar.Bernstein1.N1_right.t1_contains line 328
  126. def OAI.SharpPlanar.Bernstein1.N1_right.t2 line 332
  127. lemma OAI.SharpPlanar.Bernstein1.N1_right.t2_checked line 333
  128. lemma OAI.SharpPlanar.Bernstein1.N1_right.t2_contains line 334
  129. def OAI.SharpPlanar.Bernstein1.N1_right.t3 line 338
  130. lemma OAI.SharpPlanar.Bernstein1.N1_right.t3_checked line 339
  131. lemma OAI.SharpPlanar.Bernstein1.N1_right.t3_contains line 340
  132. def OAI.SharpPlanar.Bernstein1.N1_right.t4 line 344
  133. lemma OAI.SharpPlanar.Bernstein1.N1_right.t4_checked line 345
  134. lemma OAI.SharpPlanar.Bernstein1.N1_right.t4_contains line 346
  135. def OAI.SharpPlanar.Bernstein1.N1_right.t5 line 350
  136. lemma OAI.SharpPlanar.Bernstein1.N1_right.t5_checked line 351
  137. lemma OAI.SharpPlanar.Bernstein1.N1_right.t5_contains line 352
  138. def OAI.SharpPlanar.Bernstein1.N1_right.t6 line 356
  139. lemma OAI.SharpPlanar.Bernstein1.N1_right.t6_checked line 357
  140. lemma OAI.SharpPlanar.Bernstein1.N1_right.t6_contains line 358
  141. def OAI.SharpPlanar.Bernstein1.N1_right.t7 line 362
  142. lemma OAI.SharpPlanar.Bernstein1.N1_right.t7_checked line 363
  143. lemma OAI.SharpPlanar.Bernstein1.N1_right.t7_contains line 364
  144. def OAI.SharpPlanar.Bernstein1.N1_right.t8 line 368
  145. lemma OAI.SharpPlanar.Bernstein1.N1_right.t8_checked line 369
  146. lemma OAI.SharpPlanar.Bernstein1.N1_right.t8_contains line 370
  147. def OAI.SharpPlanar.Bernstein1.N1_right.t9 line 374
  148. lemma OAI.SharpPlanar.Bernstein1.N1_right.t9_checked line 375
  149. lemma OAI.SharpPlanar.Bernstein1.N1_right.t9_contains line 376
  150. def OAI.SharpPlanar.Bernstein1.N1_right.t10 line 380
  151. lemma OAI.SharpPlanar.Bernstein1.N1_right.t10_checked line 381
  152. lemma OAI.SharpPlanar.Bernstein1.N1_right.t10_contains line 382
  153. def OAI.SharpPlanar.Bernstein1.N1_right.t11 line 386
  154. lemma OAI.SharpPlanar.Bernstein1.N1_right.t11_checked line 387
  155. lemma OAI.SharpPlanar.Bernstein1.N1_right.t11_contains line 388
  156. def OAI.SharpPlanar.Bernstein1.N1_right.t12 line 392
  157. lemma OAI.SharpPlanar.Bernstein1.N1_right.t12_checked line 393
  158. lemma OAI.SharpPlanar.Bernstein1.N1_right.t12_contains line 394
  159. def OAI.SharpPlanar.Bernstein1.N1_right.t13 line 398
  160. lemma OAI.SharpPlanar.Bernstein1.N1_right.t13_checked line 399
  161. lemma OAI.SharpPlanar.Bernstein1.N1_right.t13_contains line 400
  162. def OAI.SharpPlanar.Bernstein1.N1_right.t14 line 404
  163. lemma OAI.SharpPlanar.Bernstein1.N1_right.t14_checked line 405
  164. lemma OAI.SharpPlanar.Bernstein1.N1_right.t14_contains line 406
  165. def OAI.SharpPlanar.Bernstein1.N1_right.t15 line 410
  166. lemma OAI.SharpPlanar.Bernstein1.N1_right.t15_checked line 411
  167. lemma OAI.SharpPlanar.Bernstein1.N1_right.t15_contains line 412
  168. def OAI.SharpPlanar.Bernstein1.N1_right.t16 line 416
  169. lemma OAI.SharpPlanar.Bernstein1.N1_right.t16_checked line 417
  170. lemma OAI.SharpPlanar.Bernstein1.N1_right.t16_contains line 418
  171. def OAI.SharpPlanar.Bernstein1.N1_right.t17 line 422
  172. lemma OAI.SharpPlanar.Bernstein1.N1_right.t17_checked line 423
  173. lemma OAI.SharpPlanar.Bernstein1.N1_right.t17_contains line 424
  174. def OAI.SharpPlanar.Bernstein1.N1_right.t18 line 428
  175. lemma OAI.SharpPlanar.Bernstein1.N1_right.t18_checked line 429
  176. lemma OAI.SharpPlanar.Bernstein1.N1_right.t18_contains line 430
  177. def OAI.SharpPlanar.Bernstein1.N1_right.t19 line 434
  178. lemma OAI.SharpPlanar.Bernstein1.N1_right.t19_checked line 435
  179. lemma OAI.SharpPlanar.Bernstein1.N1_right.t19_contains line 436
  180. def OAI.SharpPlanar.Bernstein1.N1_right.t20 line 440
  181. lemma OAI.SharpPlanar.Bernstein1.N1_right.t20_checked line 441
  182. lemma OAI.SharpPlanar.Bernstein1.N1_right.t20_contains line 442
  183. def OAI.SharpPlanar.Bernstein1.N1_right.t21 line 446
  184. lemma OAI.SharpPlanar.Bernstein1.N1_right.t21_checked line 447
  185. lemma OAI.SharpPlanar.Bernstein1.N1_right.t21_contains line 448
  186. def OAI.SharpPlanar.Bernstein1.N1_right.t22 line 452
  187. lemma OAI.SharpPlanar.Bernstein1.N1_right.t22_checked line 453
  188. lemma OAI.SharpPlanar.Bernstein1.N1_right.t22_contains line 454
  189. def OAI.SharpPlanar.Bernstein1.N1_right.t23 line 458
  190. lemma OAI.SharpPlanar.Bernstein1.N1_right.t23_checked line 459
  191. lemma OAI.SharpPlanar.Bernstein1.N1_right.t23_contains line 460
  192. def OAI.SharpPlanar.Bernstein1.N1_right.t24 line 464
  193. lemma OAI.SharpPlanar.Bernstein1.N1_right.t24_checked line 465
  194. lemma OAI.SharpPlanar.Bernstein1.N1_right.t24_contains line 466
  195. def OAI.SharpPlanar.Bernstein1.N1_right.t25 line 470
  196. lemma OAI.SharpPlanar.Bernstein1.N1_right.t25_checked line 471
  197. lemma OAI.SharpPlanar.Bernstein1.N1_right.t25_contains line 472
  198. def OAI.SharpPlanar.Bernstein1.N1_right.t26 line 476
  199. lemma OAI.SharpPlanar.Bernstein1.N1_right.t26_checked line 477
  200. lemma OAI.SharpPlanar.Bernstein1.N1_right.t26_contains line 478
  201. def OAI.SharpPlanar.Bernstein1.N1_right.t27 line 482
  202. lemma OAI.SharpPlanar.Bernstein1.N1_right.t27_checked line 483
  203. lemma OAI.SharpPlanar.Bernstein1.N1_right.t27_contains line 484
  204. def OAI.SharpPlanar.Bernstein1.N1_right.t28 line 488
  205. lemma OAI.SharpPlanar.Bernstein1.N1_right.t28_checked line 489
  206. lemma OAI.SharpPlanar.Bernstein1.N1_right.t28_contains line 490
  207. def OAI.SharpPlanar.Bernstein1.N1_right.ts line 494
  208. lemma OAI.SharpPlanar.Bernstein1.N1_right.ts_contains line 495
  209. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound0 line 526
  210. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound1 line 528
  211. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound2 line 530
  212. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound3 line 532
  213. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound4 line 534
  214. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound5 line 536
  215. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound6 line 538
  216. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound7 line 540
  217. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound8 line 542
  218. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound9 line 544
  219. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound10 line 546
  220. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound11 line 548
  221. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound12 line 550
  222. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound13 line 552
  223. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound14 line 554
  224. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound15 line 556
  225. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound16 line 558
  226. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound17 line 560
  227. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound18 line 562
  228. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound19 line 564
  229. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound20 line 566
  230. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound21 line 568
  231. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound22 line 570
  232. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound23 line 572
  233. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound24 line 574
  234. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound25 line 576
  235. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound26 line 578
  236. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound27 line 580
  237. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound28 line 582
  238. lemma OAI.SharpPlanar.Bernstein1.N1_right.bound line 584
  239. def OAI.SharpPlanar.Bernstein1.N1_left.t0 line 617
  240. lemma OAI.SharpPlanar.Bernstein1.N1_left.t0_checked line 618
  241. lemma OAI.SharpPlanar.Bernstein1.N1_left.t0_contains line 619
  242. def OAI.SharpPlanar.Bernstein1.N1_left.t1 line 623
  243. lemma OAI.SharpPlanar.Bernstein1.N1_left.t1_checked line 624
  244. lemma OAI.SharpPlanar.Bernstein1.N1_left.t1_contains line 625
  245. def OAI.SharpPlanar.Bernstein1.N1_left.t2 line 629
  246. lemma OAI.SharpPlanar.Bernstein1.N1_left.t2_checked line 630
  247. lemma OAI.SharpPlanar.Bernstein1.N1_left.t2_contains line 631
  248. def OAI.SharpPlanar.Bernstein1.N1_left.t3 line 635
  249. lemma OAI.SharpPlanar.Bernstein1.N1_left.t3_checked line 636
  250. lemma OAI.SharpPlanar.Bernstein1.N1_left.t3_contains line 637
  251. def OAI.SharpPlanar.Bernstein1.N1_left.t4 line 641
  252. lemma OAI.SharpPlanar.Bernstein1.N1_left.t4_checked line 642
  253. lemma OAI.SharpPlanar.Bernstein1.N1_left.t4_contains line 643
  254. def OAI.SharpPlanar.Bernstein1.N1_left.t5 line 647
  255. lemma OAI.SharpPlanar.Bernstein1.N1_left.t5_checked line 648
  256. lemma OAI.SharpPlanar.Bernstein1.N1_left.t5_contains line 649
  257. def OAI.SharpPlanar.Bernstein1.N1_left.t6 line 653
  258. lemma OAI.SharpPlanar.Bernstein1.N1_left.t6_checked line 654
  259. lemma OAI.SharpPlanar.Bernstein1.N1_left.t6_contains line 655
  260. def OAI.SharpPlanar.Bernstein1.N1_left.t7 line 659
  261. lemma OAI.SharpPlanar.Bernstein1.N1_left.t7_checked line 660
  262. lemma OAI.SharpPlanar.Bernstein1.N1_left.t7_contains line 661
  263. def OAI.SharpPlanar.Bernstein1.N1_left.t8 line 665
  264. lemma OAI.SharpPlanar.Bernstein1.N1_left.t8_checked line 666
  265. lemma OAI.SharpPlanar.Bernstein1.N1_left.t8_contains line 667
  266. def OAI.SharpPlanar.Bernstein1.N1_left.t9 line 671
  267. lemma OAI.SharpPlanar.Bernstein1.N1_left.t9_checked line 672
  268. lemma OAI.SharpPlanar.Bernstein1.N1_left.t9_contains line 673
  269. def OAI.SharpPlanar.Bernstein1.N1_left.t10 line 677
  270. lemma OAI.SharpPlanar.Bernstein1.N1_left.t10_checked line 678
  271. lemma OAI.SharpPlanar.Bernstein1.N1_left.t10_contains line 679
  272. def OAI.SharpPlanar.Bernstein1.N1_left.t11 line 683
  273. lemma OAI.SharpPlanar.Bernstein1.N1_left.t11_checked line 684
  274. lemma OAI.SharpPlanar.Bernstein1.N1_left.t11_contains line 685
  275. def OAI.SharpPlanar.Bernstein1.N1_left.t12 line 689
  276. lemma OAI.SharpPlanar.Bernstein1.N1_left.t12_checked line 690
  277. lemma OAI.SharpPlanar.Bernstein1.N1_left.t12_contains line 691
  278. def OAI.SharpPlanar.Bernstein1.N1_left.t13 line 695
  279. lemma OAI.SharpPlanar.Bernstein1.N1_left.t13_checked line 696
  280. lemma OAI.SharpPlanar.Bernstein1.N1_left.t13_contains line 697
  281. def OAI.SharpPlanar.Bernstein1.N1_left.t14 line 701
  282. lemma OAI.SharpPlanar.Bernstein1.N1_left.t14_checked line 702
  283. lemma OAI.SharpPlanar.Bernstein1.N1_left.t14_contains line 703
  284. def OAI.SharpPlanar.Bernstein1.N1_left.t15 line 707
  285. lemma OAI.SharpPlanar.Bernstein1.N1_left.t15_checked line 708
  286. lemma OAI.SharpPlanar.Bernstein1.N1_left.t15_contains line 709
  287. def OAI.SharpPlanar.Bernstein1.N1_left.t16 line 713
  288. lemma OAI.SharpPlanar.Bernstein1.N1_left.t16_checked line 714
  289. lemma OAI.SharpPlanar.Bernstein1.N1_left.t16_contains line 715
  290. def OAI.SharpPlanar.Bernstein1.N1_left.t17 line 719
  291. lemma OAI.SharpPlanar.Bernstein1.N1_left.t17_checked line 720
  292. lemma OAI.SharpPlanar.Bernstein1.N1_left.t17_contains line 721
  293. def OAI.SharpPlanar.Bernstein1.N1_left.t18 line 725
  294. lemma OAI.SharpPlanar.Bernstein1.N1_left.t18_checked line 726
  295. lemma OAI.SharpPlanar.Bernstein1.N1_left.t18_contains line 727
  296. def OAI.SharpPlanar.Bernstein1.N1_left.t19 line 731
  297. lemma OAI.SharpPlanar.Bernstein1.N1_left.t19_checked line 732
  298. lemma OAI.SharpPlanar.Bernstein1.N1_left.t19_contains line 733
  299. def OAI.SharpPlanar.Bernstein1.N1_left.t20 line 737
  300. lemma OAI.SharpPlanar.Bernstein1.N1_left.t20_checked line 738
  301. lemma OAI.SharpPlanar.Bernstein1.N1_left.t20_contains line 739
  302. def OAI.SharpPlanar.Bernstein1.N1_left.t21 line 743
  303. lemma OAI.SharpPlanar.Bernstein1.N1_left.t21_checked line 744
  304. lemma OAI.SharpPlanar.Bernstein1.N1_left.t21_contains line 745
  305. def OAI.SharpPlanar.Bernstein1.N1_left.t22 line 749
  306. lemma OAI.SharpPlanar.Bernstein1.N1_left.t22_checked line 750
  307. lemma OAI.SharpPlanar.Bernstein1.N1_left.t22_contains line 751
  308. def OAI.SharpPlanar.Bernstein1.N1_left.t23 line 755
  309. lemma OAI.SharpPlanar.Bernstein1.N1_left.t23_checked line 756
  310. lemma OAI.SharpPlanar.Bernstein1.N1_left.t23_contains line 757
  311. def OAI.SharpPlanar.Bernstein1.N1_left.t24 line 761
  312. lemma OAI.SharpPlanar.Bernstein1.N1_left.t24_checked line 762
  313. lemma OAI.SharpPlanar.Bernstein1.N1_left.t24_contains line 763
  314. def OAI.SharpPlanar.Bernstein1.N1_left.t25 line 767
  315. lemma OAI.SharpPlanar.Bernstein1.N1_left.t25_checked line 768
  316. lemma OAI.SharpPlanar.Bernstein1.N1_left.t25_contains line 769
  317. def OAI.SharpPlanar.Bernstein1.N1_left.t26 line 773
  318. lemma OAI.SharpPlanar.Bernstein1.N1_left.t26_checked line 774
  319. lemma OAI.SharpPlanar.Bernstein1.N1_left.t26_contains line 775
  320. def OAI.SharpPlanar.Bernstein1.N1_left.t27 line 779
  321. lemma OAI.SharpPlanar.Bernstein1.N1_left.t27_checked line 780
  322. lemma OAI.SharpPlanar.Bernstein1.N1_left.t27_contains line 781
  323. def OAI.SharpPlanar.Bernstein1.N1_left.t28 line 785
  324. lemma OAI.SharpPlanar.Bernstein1.N1_left.t28_checked line 786
  325. lemma OAI.SharpPlanar.Bernstein1.N1_left.t28_contains line 787
  326. def OAI.SharpPlanar.Bernstein1.N1_left.ts line 791
  327. lemma OAI.SharpPlanar.Bernstein1.N1_left.ts_contains line 792
  328. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound0 line 823
  329. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound1 line 825
  330. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound2 line 827
  331. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound3 line 829
  332. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound4 line 831
  333. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound5 line 833
  334. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound6 line 835
  335. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound7 line 837
  336. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound8 line 839
  337. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound9 line 841
  338. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound10 line 843
  339. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound11 line 845
  340. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound12 line 847
  341. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound13 line 849
  342. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound14 line 851
  343. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound15 line 853
  344. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound16 line 855
  345. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound17 line 857
  346. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound18 line 859
  347. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound19 line 861
  348. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound20 line 863
  349. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound21 line 865
  350. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound22 line 867
  351. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound23 line 869
  352. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound24 line 871
  353. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound25 line 873
  354. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound26 line 875
  355. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound27 line 877
  356. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound28 line 879
  357. lemma OAI.SharpPlanar.Bernstein1.N1_left.bound line 881