OAI/Analysis/PlanarPacking/Certificate/Bernstein4.lean

GitHub source file

432 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.Bernstein4.N0_right.t0 line 21
  2. lemma OAI.SharpPlanar.Bernstein4.N0_right.t0_checked line 22
  3. lemma OAI.SharpPlanar.Bernstein4.N0_right.t0_contains line 23
  4. def OAI.SharpPlanar.Bernstein4.N0_right.t1 line 27
  5. lemma OAI.SharpPlanar.Bernstein4.N0_right.t1_checked line 28
  6. lemma OAI.SharpPlanar.Bernstein4.N0_right.t1_contains line 29
  7. def OAI.SharpPlanar.Bernstein4.N0_right.t2 line 33
  8. lemma OAI.SharpPlanar.Bernstein4.N0_right.t2_checked line 34
  9. lemma OAI.SharpPlanar.Bernstein4.N0_right.t2_contains line 35
  10. def OAI.SharpPlanar.Bernstein4.N0_right.t3 line 39
  11. lemma OAI.SharpPlanar.Bernstein4.N0_right.t3_checked line 40
  12. lemma OAI.SharpPlanar.Bernstein4.N0_right.t3_contains line 41
  13. def OAI.SharpPlanar.Bernstein4.N0_right.t4 line 45
  14. lemma OAI.SharpPlanar.Bernstein4.N0_right.t4_checked line 46
  15. lemma OAI.SharpPlanar.Bernstein4.N0_right.t4_contains line 47
  16. def OAI.SharpPlanar.Bernstein4.N0_right.t5 line 51
  17. lemma OAI.SharpPlanar.Bernstein4.N0_right.t5_checked line 52
  18. lemma OAI.SharpPlanar.Bernstein4.N0_right.t5_contains line 53
  19. def OAI.SharpPlanar.Bernstein4.N0_right.t6 line 57
  20. lemma OAI.SharpPlanar.Bernstein4.N0_right.t6_checked line 58
  21. lemma OAI.SharpPlanar.Bernstein4.N0_right.t6_contains line 59
  22. def OAI.SharpPlanar.Bernstein4.N0_right.t7 line 63
  23. lemma OAI.SharpPlanar.Bernstein4.N0_right.t7_checked line 64
  24. lemma OAI.SharpPlanar.Bernstein4.N0_right.t7_contains line 65
  25. def OAI.SharpPlanar.Bernstein4.N0_right.t8 line 69
  26. lemma OAI.SharpPlanar.Bernstein4.N0_right.t8_checked line 70
  27. lemma OAI.SharpPlanar.Bernstein4.N0_right.t8_contains line 71
  28. def OAI.SharpPlanar.Bernstein4.N0_right.t9 line 75
  29. lemma OAI.SharpPlanar.Bernstein4.N0_right.t9_checked line 76
  30. lemma OAI.SharpPlanar.Bernstein4.N0_right.t9_contains line 77
  31. def OAI.SharpPlanar.Bernstein4.N0_right.t10 line 81
  32. lemma OAI.SharpPlanar.Bernstein4.N0_right.t10_checked line 82
  33. lemma OAI.SharpPlanar.Bernstein4.N0_right.t10_contains line 83
  34. def OAI.SharpPlanar.Bernstein4.N0_right.t11 line 87
  35. lemma OAI.SharpPlanar.Bernstein4.N0_right.t11_checked line 88
  36. lemma OAI.SharpPlanar.Bernstein4.N0_right.t11_contains line 89
  37. def OAI.SharpPlanar.Bernstein4.N0_right.t12 line 93
  38. lemma OAI.SharpPlanar.Bernstein4.N0_right.t12_checked line 94
  39. lemma OAI.SharpPlanar.Bernstein4.N0_right.t12_contains line 95
  40. def OAI.SharpPlanar.Bernstein4.N0_right.t13 line 99
  41. lemma OAI.SharpPlanar.Bernstein4.N0_right.t13_checked line 100
  42. lemma OAI.SharpPlanar.Bernstein4.N0_right.t13_contains line 101
  43. def OAI.SharpPlanar.Bernstein4.N0_right.t14 line 105
  44. lemma OAI.SharpPlanar.Bernstein4.N0_right.t14_checked line 106
  45. lemma OAI.SharpPlanar.Bernstein4.N0_right.t14_contains line 107
  46. def OAI.SharpPlanar.Bernstein4.N0_right.t15 line 111
  47. lemma OAI.SharpPlanar.Bernstein4.N0_right.t15_checked line 112
  48. lemma OAI.SharpPlanar.Bernstein4.N0_right.t15_contains line 113
  49. def OAI.SharpPlanar.Bernstein4.N0_right.t16 line 117
  50. lemma OAI.SharpPlanar.Bernstein4.N0_right.t16_checked line 118
  51. lemma OAI.SharpPlanar.Bernstein4.N0_right.t16_contains line 119
  52. def OAI.SharpPlanar.Bernstein4.N0_right.t17 line 123
  53. lemma OAI.SharpPlanar.Bernstein4.N0_right.t17_checked line 124
  54. lemma OAI.SharpPlanar.Bernstein4.N0_right.t17_contains line 125
  55. def OAI.SharpPlanar.Bernstein4.N0_right.t18 line 129
  56. lemma OAI.SharpPlanar.Bernstein4.N0_right.t18_contains line 130
  57. def OAI.SharpPlanar.Bernstein4.N0_right.t19 line 132
  58. lemma OAI.SharpPlanar.Bernstein4.N0_right.t19_contains line 133
  59. def OAI.SharpPlanar.Bernstein4.N0_right.t20 line 135
  60. lemma OAI.SharpPlanar.Bernstein4.N0_right.t20_contains line 136
  61. def OAI.SharpPlanar.Bernstein4.N0_right.t21 line 138
  62. lemma OAI.SharpPlanar.Bernstein4.N0_right.t21_contains line 139
  63. def OAI.SharpPlanar.Bernstein4.N0_right.t22 line 141
  64. lemma OAI.SharpPlanar.Bernstein4.N0_right.t22_contains line 142
  65. def OAI.SharpPlanar.Bernstein4.N0_right.t23 line 144
  66. lemma OAI.SharpPlanar.Bernstein4.N0_right.t23_contains line 145
  67. def OAI.SharpPlanar.Bernstein4.N0_right.t24 line 147
  68. lemma OAI.SharpPlanar.Bernstein4.N0_right.t24_contains line 148
  69. def OAI.SharpPlanar.Bernstein4.N0_right.t25 line 150
  70. lemma OAI.SharpPlanar.Bernstein4.N0_right.t25_contains line 151
  71. def OAI.SharpPlanar.Bernstein4.N0_right.t26 line 153
  72. lemma OAI.SharpPlanar.Bernstein4.N0_right.t26_contains line 154
  73. def OAI.SharpPlanar.Bernstein4.N0_right.t27 line 156
  74. lemma OAI.SharpPlanar.Bernstein4.N0_right.t27_contains line 157
  75. def OAI.SharpPlanar.Bernstein4.N0_right.t28 line 159
  76. lemma OAI.SharpPlanar.Bernstein4.N0_right.t28_contains line 160
  77. def OAI.SharpPlanar.Bernstein4.N0_right.ts line 162
  78. lemma OAI.SharpPlanar.Bernstein4.N0_right.ts_contains line 163
  79. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound0 line 194
  80. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound1 line 196
  81. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound2 line 198
  82. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound3 line 200
  83. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound4 line 202
  84. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound5 line 204
  85. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound6 line 206
  86. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound7 line 208
  87. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound8 line 210
  88. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound9 line 212
  89. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound10 line 214
  90. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound11 line 216
  91. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound12 line 218
  92. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound13 line 220
  93. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound14 line 222
  94. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound15 line 224
  95. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound16 line 226
  96. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound17 line 228
  97. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound18 line 230
  98. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound19 line 232
  99. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound20 line 234
  100. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound21 line 236
  101. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound22 line 238
  102. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound23 line 240
  103. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound24 line 242
  104. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound25 line 244
  105. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound26 line 246
  106. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound27 line 248
  107. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound28 line 250
  108. lemma OAI.SharpPlanar.Bernstein4.N0_right.bound line 252
  109. def OAI.SharpPlanar.Bernstein4.N1_right.t0 line 285
  110. lemma OAI.SharpPlanar.Bernstein4.N1_right.t0_checked line 286
  111. lemma OAI.SharpPlanar.Bernstein4.N1_right.t0_contains line 287
  112. def OAI.SharpPlanar.Bernstein4.N1_right.t1 line 291
  113. lemma OAI.SharpPlanar.Bernstein4.N1_right.t1_checked line 292
  114. lemma OAI.SharpPlanar.Bernstein4.N1_right.t1_contains line 293
  115. def OAI.SharpPlanar.Bernstein4.N1_right.t2 line 297
  116. lemma OAI.SharpPlanar.Bernstein4.N1_right.t2_checked line 298
  117. lemma OAI.SharpPlanar.Bernstein4.N1_right.t2_contains line 299
  118. def OAI.SharpPlanar.Bernstein4.N1_right.t3 line 303
  119. lemma OAI.SharpPlanar.Bernstein4.N1_right.t3_checked line 304
  120. lemma OAI.SharpPlanar.Bernstein4.N1_right.t3_contains line 305
  121. def OAI.SharpPlanar.Bernstein4.N1_right.t4 line 309
  122. lemma OAI.SharpPlanar.Bernstein4.N1_right.t4_checked line 310
  123. lemma OAI.SharpPlanar.Bernstein4.N1_right.t4_contains line 311
  124. def OAI.SharpPlanar.Bernstein4.N1_right.t5 line 315
  125. lemma OAI.SharpPlanar.Bernstein4.N1_right.t5_checked line 316
  126. lemma OAI.SharpPlanar.Bernstein4.N1_right.t5_contains line 317
  127. def OAI.SharpPlanar.Bernstein4.N1_right.t6 line 321
  128. lemma OAI.SharpPlanar.Bernstein4.N1_right.t6_checked line 322
  129. lemma OAI.SharpPlanar.Bernstein4.N1_right.t6_contains line 323
  130. def OAI.SharpPlanar.Bernstein4.N1_right.t7 line 327
  131. lemma OAI.SharpPlanar.Bernstein4.N1_right.t7_checked line 328
  132. lemma OAI.SharpPlanar.Bernstein4.N1_right.t7_contains line 329
  133. def OAI.SharpPlanar.Bernstein4.N1_right.t8 line 333
  134. lemma OAI.SharpPlanar.Bernstein4.N1_right.t8_checked line 334
  135. lemma OAI.SharpPlanar.Bernstein4.N1_right.t8_contains line 335
  136. def OAI.SharpPlanar.Bernstein4.N1_right.t9 line 339
  137. lemma OAI.SharpPlanar.Bernstein4.N1_right.t9_checked line 340
  138. lemma OAI.SharpPlanar.Bernstein4.N1_right.t9_contains line 341
  139. def OAI.SharpPlanar.Bernstein4.N1_right.t10 line 345
  140. lemma OAI.SharpPlanar.Bernstein4.N1_right.t10_checked line 346
  141. lemma OAI.SharpPlanar.Bernstein4.N1_right.t10_contains line 347
  142. def OAI.SharpPlanar.Bernstein4.N1_right.t11 line 351
  143. lemma OAI.SharpPlanar.Bernstein4.N1_right.t11_checked line 352
  144. lemma OAI.SharpPlanar.Bernstein4.N1_right.t11_contains line 353
  145. def OAI.SharpPlanar.Bernstein4.N1_right.t12 line 357
  146. lemma OAI.SharpPlanar.Bernstein4.N1_right.t12_checked line 358
  147. lemma OAI.SharpPlanar.Bernstein4.N1_right.t12_contains line 359
  148. def OAI.SharpPlanar.Bernstein4.N1_right.t13 line 363
  149. lemma OAI.SharpPlanar.Bernstein4.N1_right.t13_checked line 364
  150. lemma OAI.SharpPlanar.Bernstein4.N1_right.t13_contains line 365
  151. def OAI.SharpPlanar.Bernstein4.N1_right.t14 line 369
  152. lemma OAI.SharpPlanar.Bernstein4.N1_right.t14_checked line 370
  153. lemma OAI.SharpPlanar.Bernstein4.N1_right.t14_contains line 371
  154. def OAI.SharpPlanar.Bernstein4.N1_right.t15 line 375
  155. lemma OAI.SharpPlanar.Bernstein4.N1_right.t15_checked line 376
  156. lemma OAI.SharpPlanar.Bernstein4.N1_right.t15_contains line 377
  157. def OAI.SharpPlanar.Bernstein4.N1_right.t16 line 381
  158. lemma OAI.SharpPlanar.Bernstein4.N1_right.t16_checked line 382
  159. lemma OAI.SharpPlanar.Bernstein4.N1_right.t16_contains line 383
  160. def OAI.SharpPlanar.Bernstein4.N1_right.t17 line 387
  161. lemma OAI.SharpPlanar.Bernstein4.N1_right.t17_checked line 388
  162. lemma OAI.SharpPlanar.Bernstein4.N1_right.t17_contains line 389
  163. def OAI.SharpPlanar.Bernstein4.N1_right.t18 line 393
  164. lemma OAI.SharpPlanar.Bernstein4.N1_right.t18_contains line 394
  165. def OAI.SharpPlanar.Bernstein4.N1_right.t19 line 396
  166. lemma OAI.SharpPlanar.Bernstein4.N1_right.t19_contains line 397
  167. def OAI.SharpPlanar.Bernstein4.N1_right.t20 line 399
  168. lemma OAI.SharpPlanar.Bernstein4.N1_right.t20_contains line 400
  169. def OAI.SharpPlanar.Bernstein4.N1_right.t21 line 402
  170. lemma OAI.SharpPlanar.Bernstein4.N1_right.t21_contains line 403
  171. def OAI.SharpPlanar.Bernstein4.N1_right.t22 line 405
  172. lemma OAI.SharpPlanar.Bernstein4.N1_right.t22_contains line 406
  173. def OAI.SharpPlanar.Bernstein4.N1_right.t23 line 408
  174. lemma OAI.SharpPlanar.Bernstein4.N1_right.t23_contains line 409
  175. def OAI.SharpPlanar.Bernstein4.N1_right.t24 line 411
  176. lemma OAI.SharpPlanar.Bernstein4.N1_right.t24_contains line 412
  177. def OAI.SharpPlanar.Bernstein4.N1_right.t25 line 414
  178. lemma OAI.SharpPlanar.Bernstein4.N1_right.t25_contains line 415
  179. def OAI.SharpPlanar.Bernstein4.N1_right.t26 line 417
  180. lemma OAI.SharpPlanar.Bernstein4.N1_right.t26_contains line 418
  181. def OAI.SharpPlanar.Bernstein4.N1_right.t27 line 420
  182. lemma OAI.SharpPlanar.Bernstein4.N1_right.t27_contains line 421
  183. def OAI.SharpPlanar.Bernstein4.N1_right.t28 line 423
  184. lemma OAI.SharpPlanar.Bernstein4.N1_right.t28_contains line 424
  185. def OAI.SharpPlanar.Bernstein4.N1_right.ts line 426
  186. lemma OAI.SharpPlanar.Bernstein4.N1_right.ts_contains line 427
  187. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound0 line 458
  188. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound1 line 460
  189. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound2 line 462
  190. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound3 line 464
  191. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound4 line 466
  192. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound5 line 468
  193. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound6 line 470
  194. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound7 line 472
  195. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound8 line 474
  196. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound9 line 476
  197. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound10 line 478
  198. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound11 line 480
  199. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound12 line 482
  200. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound13 line 484
  201. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound14 line 486
  202. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound15 line 488
  203. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound16 line 490
  204. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound17 line 492
  205. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound18 line 494
  206. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound19 line 496
  207. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound20 line 498
  208. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound21 line 500
  209. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound22 line 502
  210. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound23 line 504
  211. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound24 line 506
  212. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound25 line 508
  213. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound26 line 510
  214. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound27 line 512
  215. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound28 line 514
  216. lemma OAI.SharpPlanar.Bernstein4.N1_right.bound line 516
  217. def OAI.SharpPlanar.Bernstein4.N0_left.t0 line 549
  218. lemma OAI.SharpPlanar.Bernstein4.N0_left.t0_checked line 550
  219. lemma OAI.SharpPlanar.Bernstein4.N0_left.t0_contains line 551
  220. def OAI.SharpPlanar.Bernstein4.N0_left.t1 line 555
  221. lemma OAI.SharpPlanar.Bernstein4.N0_left.t1_checked line 556
  222. lemma OAI.SharpPlanar.Bernstein4.N0_left.t1_contains line 557
  223. def OAI.SharpPlanar.Bernstein4.N0_left.t2 line 561
  224. lemma OAI.SharpPlanar.Bernstein4.N0_left.t2_checked line 562
  225. lemma OAI.SharpPlanar.Bernstein4.N0_left.t2_contains line 563
  226. def OAI.SharpPlanar.Bernstein4.N0_left.t3 line 567
  227. lemma OAI.SharpPlanar.Bernstein4.N0_left.t3_checked line 568
  228. lemma OAI.SharpPlanar.Bernstein4.N0_left.t3_contains line 569
  229. def OAI.SharpPlanar.Bernstein4.N0_left.t4 line 573
  230. lemma OAI.SharpPlanar.Bernstein4.N0_left.t4_checked line 574
  231. lemma OAI.SharpPlanar.Bernstein4.N0_left.t4_contains line 575
  232. def OAI.SharpPlanar.Bernstein4.N0_left.t5 line 579
  233. lemma OAI.SharpPlanar.Bernstein4.N0_left.t5_checked line 580
  234. lemma OAI.SharpPlanar.Bernstein4.N0_left.t5_contains line 581
  235. def OAI.SharpPlanar.Bernstein4.N0_left.t6 line 585
  236. lemma OAI.SharpPlanar.Bernstein4.N0_left.t6_checked line 586
  237. lemma OAI.SharpPlanar.Bernstein4.N0_left.t6_contains line 587
  238. def OAI.SharpPlanar.Bernstein4.N0_left.t7 line 591
  239. lemma OAI.SharpPlanar.Bernstein4.N0_left.t7_checked line 592
  240. lemma OAI.SharpPlanar.Bernstein4.N0_left.t7_contains line 593
  241. def OAI.SharpPlanar.Bernstein4.N0_left.t8 line 597
  242. lemma OAI.SharpPlanar.Bernstein4.N0_left.t8_checked line 598
  243. lemma OAI.SharpPlanar.Bernstein4.N0_left.t8_contains line 599
  244. def OAI.SharpPlanar.Bernstein4.N0_left.t9 line 603
  245. lemma OAI.SharpPlanar.Bernstein4.N0_left.t9_checked line 604
  246. lemma OAI.SharpPlanar.Bernstein4.N0_left.t9_contains line 605
  247. def OAI.SharpPlanar.Bernstein4.N0_left.t10 line 609
  248. lemma OAI.SharpPlanar.Bernstein4.N0_left.t10_checked line 610
  249. lemma OAI.SharpPlanar.Bernstein4.N0_left.t10_contains line 611
  250. def OAI.SharpPlanar.Bernstein4.N0_left.t11 line 615
  251. lemma OAI.SharpPlanar.Bernstein4.N0_left.t11_checked line 616
  252. lemma OAI.SharpPlanar.Bernstein4.N0_left.t11_contains line 617
  253. def OAI.SharpPlanar.Bernstein4.N0_left.t12 line 621
  254. lemma OAI.SharpPlanar.Bernstein4.N0_left.t12_checked line 622
  255. lemma OAI.SharpPlanar.Bernstein4.N0_left.t12_contains line 623
  256. def OAI.SharpPlanar.Bernstein4.N0_left.t13 line 627
  257. lemma OAI.SharpPlanar.Bernstein4.N0_left.t13_checked line 628
  258. lemma OAI.SharpPlanar.Bernstein4.N0_left.t13_contains line 629
  259. def OAI.SharpPlanar.Bernstein4.N0_left.t14 line 633
  260. lemma OAI.SharpPlanar.Bernstein4.N0_left.t14_checked line 634
  261. lemma OAI.SharpPlanar.Bernstein4.N0_left.t14_contains line 635
  262. def OAI.SharpPlanar.Bernstein4.N0_left.t15 line 639
  263. lemma OAI.SharpPlanar.Bernstein4.N0_left.t15_checked line 640
  264. lemma OAI.SharpPlanar.Bernstein4.N0_left.t15_contains line 641
  265. def OAI.SharpPlanar.Bernstein4.N0_left.t16 line 645
  266. lemma OAI.SharpPlanar.Bernstein4.N0_left.t16_checked line 646
  267. lemma OAI.SharpPlanar.Bernstein4.N0_left.t16_contains line 647
  268. def OAI.SharpPlanar.Bernstein4.N0_left.t17 line 651
  269. lemma OAI.SharpPlanar.Bernstein4.N0_left.t17_checked line 652
  270. lemma OAI.SharpPlanar.Bernstein4.N0_left.t17_contains line 653
  271. def OAI.SharpPlanar.Bernstein4.N0_left.t18 line 657
  272. lemma OAI.SharpPlanar.Bernstein4.N0_left.t18_contains line 658
  273. def OAI.SharpPlanar.Bernstein4.N0_left.t19 line 660
  274. lemma OAI.SharpPlanar.Bernstein4.N0_left.t19_contains line 661
  275. def OAI.SharpPlanar.Bernstein4.N0_left.t20 line 663
  276. lemma OAI.SharpPlanar.Bernstein4.N0_left.t20_contains line 664
  277. def OAI.SharpPlanar.Bernstein4.N0_left.t21 line 666
  278. lemma OAI.SharpPlanar.Bernstein4.N0_left.t21_contains line 667
  279. def OAI.SharpPlanar.Bernstein4.N0_left.t22 line 669
  280. lemma OAI.SharpPlanar.Bernstein4.N0_left.t22_contains line 670
  281. def OAI.SharpPlanar.Bernstein4.N0_left.t23 line 672
  282. lemma OAI.SharpPlanar.Bernstein4.N0_left.t23_contains line 673
  283. def OAI.SharpPlanar.Bernstein4.N0_left.t24 line 675
  284. lemma OAI.SharpPlanar.Bernstein4.N0_left.t24_contains line 676
  285. def OAI.SharpPlanar.Bernstein4.N0_left.t25 line 678
  286. lemma OAI.SharpPlanar.Bernstein4.N0_left.t25_contains line 679
  287. def OAI.SharpPlanar.Bernstein4.N0_left.t26 line 681
  288. lemma OAI.SharpPlanar.Bernstein4.N0_left.t26_contains line 682
  289. def OAI.SharpPlanar.Bernstein4.N0_left.t27 line 684
  290. lemma OAI.SharpPlanar.Bernstein4.N0_left.t27_contains line 685
  291. def OAI.SharpPlanar.Bernstein4.N0_left.t28 line 687
  292. lemma OAI.SharpPlanar.Bernstein4.N0_left.t28_contains line 688
  293. def OAI.SharpPlanar.Bernstein4.N0_left.ts line 690
  294. lemma OAI.SharpPlanar.Bernstein4.N0_left.ts_contains line 691
  295. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound0 line 722
  296. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound1 line 724
  297. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound2 line 726
  298. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound3 line 728
  299. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound4 line 730
  300. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound5 line 732
  301. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound6 line 734
  302. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound7 line 736
  303. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound8 line 738
  304. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound9 line 740
  305. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound10 line 742
  306. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound11 line 744
  307. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound12 line 746
  308. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound13 line 748
  309. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound14 line 750
  310. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound15 line 752
  311. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound16 line 754
  312. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound17 line 756
  313. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound18 line 758
  314. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound19 line 760
  315. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound20 line 762
  316. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound21 line 764
  317. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound22 line 766
  318. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound23 line 768
  319. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound24 line 770
  320. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound25 line 772
  321. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound26 line 774
  322. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound27 line 776
  323. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound28 line 778
  324. lemma OAI.SharpPlanar.Bernstein4.N0_left.bound line 780
  325. def OAI.SharpPlanar.Bernstein4.N1_left.t0 line 813
  326. lemma OAI.SharpPlanar.Bernstein4.N1_left.t0_checked line 814
  327. lemma OAI.SharpPlanar.Bernstein4.N1_left.t0_contains line 815
  328. def OAI.SharpPlanar.Bernstein4.N1_left.t1 line 819
  329. lemma OAI.SharpPlanar.Bernstein4.N1_left.t1_checked line 820
  330. lemma OAI.SharpPlanar.Bernstein4.N1_left.t1_contains line 821
  331. def OAI.SharpPlanar.Bernstein4.N1_left.t2 line 825
  332. lemma OAI.SharpPlanar.Bernstein4.N1_left.t2_checked line 826
  333. lemma OAI.SharpPlanar.Bernstein4.N1_left.t2_contains line 827
  334. def OAI.SharpPlanar.Bernstein4.N1_left.t3 line 831
  335. lemma OAI.SharpPlanar.Bernstein4.N1_left.t3_checked line 832
  336. lemma OAI.SharpPlanar.Bernstein4.N1_left.t3_contains line 833
  337. def OAI.SharpPlanar.Bernstein4.N1_left.t4 line 837
  338. lemma OAI.SharpPlanar.Bernstein4.N1_left.t4_checked line 838
  339. lemma OAI.SharpPlanar.Bernstein4.N1_left.t4_contains line 839
  340. def OAI.SharpPlanar.Bernstein4.N1_left.t5 line 843
  341. lemma OAI.SharpPlanar.Bernstein4.N1_left.t5_checked line 844
  342. lemma OAI.SharpPlanar.Bernstein4.N1_left.t5_contains line 845
  343. def OAI.SharpPlanar.Bernstein4.N1_left.t6 line 849
  344. lemma OAI.SharpPlanar.Bernstein4.N1_left.t6_checked line 850
  345. lemma OAI.SharpPlanar.Bernstein4.N1_left.t6_contains line 851
  346. def OAI.SharpPlanar.Bernstein4.N1_left.t7 line 855
  347. lemma OAI.SharpPlanar.Bernstein4.N1_left.t7_checked line 856
  348. lemma OAI.SharpPlanar.Bernstein4.N1_left.t7_contains line 857
  349. def OAI.SharpPlanar.Bernstein4.N1_left.t8 line 861
  350. lemma OAI.SharpPlanar.Bernstein4.N1_left.t8_checked line 862
  351. lemma OAI.SharpPlanar.Bernstein4.N1_left.t8_contains line 863
  352. def OAI.SharpPlanar.Bernstein4.N1_left.t9 line 867
  353. lemma OAI.SharpPlanar.Bernstein4.N1_left.t9_checked line 868
  354. lemma OAI.SharpPlanar.Bernstein4.N1_left.t9_contains line 869
  355. def OAI.SharpPlanar.Bernstein4.N1_left.t10 line 873
  356. lemma OAI.SharpPlanar.Bernstein4.N1_left.t10_checked line 874
  357. lemma OAI.SharpPlanar.Bernstein4.N1_left.t10_contains line 875
  358. def OAI.SharpPlanar.Bernstein4.N1_left.t11 line 879
  359. lemma OAI.SharpPlanar.Bernstein4.N1_left.t11_checked line 880
  360. lemma OAI.SharpPlanar.Bernstein4.N1_left.t11_contains line 881
  361. def OAI.SharpPlanar.Bernstein4.N1_left.t12 line 885
  362. lemma OAI.SharpPlanar.Bernstein4.N1_left.t12_checked line 886
  363. lemma OAI.SharpPlanar.Bernstein4.N1_left.t12_contains line 887
  364. def OAI.SharpPlanar.Bernstein4.N1_left.t13 line 891
  365. lemma OAI.SharpPlanar.Bernstein4.N1_left.t13_checked line 892
  366. lemma OAI.SharpPlanar.Bernstein4.N1_left.t13_contains line 893
  367. def OAI.SharpPlanar.Bernstein4.N1_left.t14 line 897
  368. lemma OAI.SharpPlanar.Bernstein4.N1_left.t14_checked line 898
  369. lemma OAI.SharpPlanar.Bernstein4.N1_left.t14_contains line 899
  370. def OAI.SharpPlanar.Bernstein4.N1_left.t15 line 903
  371. lemma OAI.SharpPlanar.Bernstein4.N1_left.t15_checked line 904
  372. lemma OAI.SharpPlanar.Bernstein4.N1_left.t15_contains line 905
  373. def OAI.SharpPlanar.Bernstein4.N1_left.t16 line 909
  374. lemma OAI.SharpPlanar.Bernstein4.N1_left.t16_checked line 910
  375. lemma OAI.SharpPlanar.Bernstein4.N1_left.t16_contains line 911
  376. def OAI.SharpPlanar.Bernstein4.N1_left.t17 line 915
  377. lemma OAI.SharpPlanar.Bernstein4.N1_left.t17_checked line 916
  378. lemma OAI.SharpPlanar.Bernstein4.N1_left.t17_contains line 917
  379. def OAI.SharpPlanar.Bernstein4.N1_left.t18 line 921
  380. lemma OAI.SharpPlanar.Bernstein4.N1_left.t18_contains line 922
  381. def OAI.SharpPlanar.Bernstein4.N1_left.t19 line 924
  382. lemma OAI.SharpPlanar.Bernstein4.N1_left.t19_contains line 925
  383. def OAI.SharpPlanar.Bernstein4.N1_left.t20 line 927
  384. lemma OAI.SharpPlanar.Bernstein4.N1_left.t20_contains line 928
  385. def OAI.SharpPlanar.Bernstein4.N1_left.t21 line 930
  386. lemma OAI.SharpPlanar.Bernstein4.N1_left.t21_contains line 931
  387. def OAI.SharpPlanar.Bernstein4.N1_left.t22 line 933
  388. lemma OAI.SharpPlanar.Bernstein4.N1_left.t22_contains line 934
  389. def OAI.SharpPlanar.Bernstein4.N1_left.t23 line 936
  390. lemma OAI.SharpPlanar.Bernstein4.N1_left.t23_contains line 937
  391. def OAI.SharpPlanar.Bernstein4.N1_left.t24 line 939
  392. lemma OAI.SharpPlanar.Bernstein4.N1_left.t24_contains line 940
  393. def OAI.SharpPlanar.Bernstein4.N1_left.t25 line 942
  394. lemma OAI.SharpPlanar.Bernstein4.N1_left.t25_contains line 943
  395. def OAI.SharpPlanar.Bernstein4.N1_left.t26 line 945
  396. lemma OAI.SharpPlanar.Bernstein4.N1_left.t26_contains line 946
  397. def OAI.SharpPlanar.Bernstein4.N1_left.t27 line 948
  398. lemma OAI.SharpPlanar.Bernstein4.N1_left.t27_contains line 949
  399. def OAI.SharpPlanar.Bernstein4.N1_left.t28 line 951
  400. lemma OAI.SharpPlanar.Bernstein4.N1_left.t28_contains line 952
  401. def OAI.SharpPlanar.Bernstein4.N1_left.ts line 954
  402. lemma OAI.SharpPlanar.Bernstein4.N1_left.ts_contains line 955
  403. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound0 line 986
  404. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound1 line 988
  405. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound2 line 990
  406. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound3 line 992
  407. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound4 line 994
  408. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound5 line 996
  409. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound6 line 998
  410. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound7 line 1000
  411. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound8 line 1002
  412. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound9 line 1004
  413. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound10 line 1006
  414. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound11 line 1008
  415. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound12 line 1010
  416. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound13 line 1012
  417. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound14 line 1014
  418. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound15 line 1016
  419. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound16 line 1018
  420. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound17 line 1020
  421. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound18 line 1022
  422. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound19 line 1024
  423. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound20 line 1026
  424. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound21 line 1028
  425. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound22 line 1030
  426. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound23 line 1032
  427. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound24 line 1034
  428. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound25 line 1036
  429. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound26 line 1038
  430. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound27 line 1040
  431. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound28 line 1042
  432. lemma OAI.SharpPlanar.Bernstein4.N1_left.bound line 1044