OAI/Analysis/PlanarPacking/Certificate/Bernstein7.lean

GitHub source file

416 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.Bernstein7.N0_right.t0 line 21
  2. lemma OAI.SharpPlanar.Bernstein7.N0_right.t0_checked line 22
  3. lemma OAI.SharpPlanar.Bernstein7.N0_right.t0_contains line 23
  4. def OAI.SharpPlanar.Bernstein7.N0_right.t1 line 27
  5. lemma OAI.SharpPlanar.Bernstein7.N0_right.t1_checked line 28
  6. lemma OAI.SharpPlanar.Bernstein7.N0_right.t1_contains line 29
  7. def OAI.SharpPlanar.Bernstein7.N0_right.t2 line 33
  8. lemma OAI.SharpPlanar.Bernstein7.N0_right.t2_checked line 34
  9. lemma OAI.SharpPlanar.Bernstein7.N0_right.t2_contains line 35
  10. def OAI.SharpPlanar.Bernstein7.N0_right.t3 line 39
  11. lemma OAI.SharpPlanar.Bernstein7.N0_right.t3_checked line 40
  12. lemma OAI.SharpPlanar.Bernstein7.N0_right.t3_contains line 41
  13. def OAI.SharpPlanar.Bernstein7.N0_right.t4 line 45
  14. lemma OAI.SharpPlanar.Bernstein7.N0_right.t4_checked line 46
  15. lemma OAI.SharpPlanar.Bernstein7.N0_right.t4_contains line 47
  16. def OAI.SharpPlanar.Bernstein7.N0_right.t5 line 51
  17. lemma OAI.SharpPlanar.Bernstein7.N0_right.t5_checked line 52
  18. lemma OAI.SharpPlanar.Bernstein7.N0_right.t5_contains line 53
  19. def OAI.SharpPlanar.Bernstein7.N0_right.t6 line 57
  20. lemma OAI.SharpPlanar.Bernstein7.N0_right.t6_checked line 58
  21. lemma OAI.SharpPlanar.Bernstein7.N0_right.t6_contains line 59
  22. def OAI.SharpPlanar.Bernstein7.N0_right.t7 line 63
  23. lemma OAI.SharpPlanar.Bernstein7.N0_right.t7_checked line 64
  24. lemma OAI.SharpPlanar.Bernstein7.N0_right.t7_contains line 65
  25. def OAI.SharpPlanar.Bernstein7.N0_right.t8 line 69
  26. lemma OAI.SharpPlanar.Bernstein7.N0_right.t8_checked line 70
  27. lemma OAI.SharpPlanar.Bernstein7.N0_right.t8_contains line 71
  28. def OAI.SharpPlanar.Bernstein7.N0_right.t9 line 75
  29. lemma OAI.SharpPlanar.Bernstein7.N0_right.t9_checked line 76
  30. lemma OAI.SharpPlanar.Bernstein7.N0_right.t9_contains line 77
  31. def OAI.SharpPlanar.Bernstein7.N0_right.t10 line 81
  32. lemma OAI.SharpPlanar.Bernstein7.N0_right.t10_checked line 82
  33. lemma OAI.SharpPlanar.Bernstein7.N0_right.t10_contains line 83
  34. def OAI.SharpPlanar.Bernstein7.N0_right.t11 line 87
  35. lemma OAI.SharpPlanar.Bernstein7.N0_right.t11_checked line 88
  36. lemma OAI.SharpPlanar.Bernstein7.N0_right.t11_contains line 89
  37. def OAI.SharpPlanar.Bernstein7.N0_right.t12 line 93
  38. lemma OAI.SharpPlanar.Bernstein7.N0_right.t12_checked line 94
  39. lemma OAI.SharpPlanar.Bernstein7.N0_right.t12_contains line 95
  40. def OAI.SharpPlanar.Bernstein7.N0_right.t13 line 99
  41. lemma OAI.SharpPlanar.Bernstein7.N0_right.t13_checked line 100
  42. lemma OAI.SharpPlanar.Bernstein7.N0_right.t13_contains line 101
  43. def OAI.SharpPlanar.Bernstein7.N0_right.t14 line 105
  44. lemma OAI.SharpPlanar.Bernstein7.N0_right.t14_contains line 106
  45. def OAI.SharpPlanar.Bernstein7.N0_right.t15 line 108
  46. lemma OAI.SharpPlanar.Bernstein7.N0_right.t15_contains line 109
  47. def OAI.SharpPlanar.Bernstein7.N0_right.t16 line 111
  48. lemma OAI.SharpPlanar.Bernstein7.N0_right.t16_contains line 112
  49. def OAI.SharpPlanar.Bernstein7.N0_right.t17 line 114
  50. lemma OAI.SharpPlanar.Bernstein7.N0_right.t17_contains line 115
  51. def OAI.SharpPlanar.Bernstein7.N0_right.t18 line 117
  52. lemma OAI.SharpPlanar.Bernstein7.N0_right.t18_contains line 118
  53. def OAI.SharpPlanar.Bernstein7.N0_right.t19 line 120
  54. lemma OAI.SharpPlanar.Bernstein7.N0_right.t19_contains line 121
  55. def OAI.SharpPlanar.Bernstein7.N0_right.t20 line 123
  56. lemma OAI.SharpPlanar.Bernstein7.N0_right.t20_contains line 124
  57. def OAI.SharpPlanar.Bernstein7.N0_right.t21 line 126
  58. lemma OAI.SharpPlanar.Bernstein7.N0_right.t21_contains line 127
  59. def OAI.SharpPlanar.Bernstein7.N0_right.t22 line 129
  60. lemma OAI.SharpPlanar.Bernstein7.N0_right.t22_contains line 130
  61. def OAI.SharpPlanar.Bernstein7.N0_right.t23 line 132
  62. lemma OAI.SharpPlanar.Bernstein7.N0_right.t23_contains line 133
  63. def OAI.SharpPlanar.Bernstein7.N0_right.t24 line 135
  64. lemma OAI.SharpPlanar.Bernstein7.N0_right.t24_contains line 136
  65. def OAI.SharpPlanar.Bernstein7.N0_right.t25 line 138
  66. lemma OAI.SharpPlanar.Bernstein7.N0_right.t25_contains line 139
  67. def OAI.SharpPlanar.Bernstein7.N0_right.t26 line 141
  68. lemma OAI.SharpPlanar.Bernstein7.N0_right.t26_contains line 142
  69. def OAI.SharpPlanar.Bernstein7.N0_right.t27 line 144
  70. lemma OAI.SharpPlanar.Bernstein7.N0_right.t27_contains line 145
  71. def OAI.SharpPlanar.Bernstein7.N0_right.t28 line 147
  72. lemma OAI.SharpPlanar.Bernstein7.N0_right.t28_contains line 148
  73. def OAI.SharpPlanar.Bernstein7.N0_right.ts line 150
  74. lemma OAI.SharpPlanar.Bernstein7.N0_right.ts_contains line 151
  75. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound0 line 182
  76. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound1 line 184
  77. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound2 line 186
  78. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound3 line 188
  79. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound4 line 190
  80. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound5 line 192
  81. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound6 line 194
  82. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound7 line 196
  83. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound8 line 198
  84. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound9 line 200
  85. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound10 line 202
  86. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound11 line 204
  87. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound12 line 206
  88. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound13 line 208
  89. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound14 line 210
  90. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound15 line 212
  91. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound16 line 214
  92. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound17 line 216
  93. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound18 line 218
  94. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound19 line 220
  95. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound20 line 222
  96. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound21 line 224
  97. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound22 line 226
  98. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound23 line 228
  99. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound24 line 230
  100. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound25 line 232
  101. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound26 line 234
  102. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound27 line 236
  103. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound28 line 238
  104. lemma OAI.SharpPlanar.Bernstein7.N0_right.bound line 240
  105. def OAI.SharpPlanar.Bernstein7.N1_right.t0 line 273
  106. lemma OAI.SharpPlanar.Bernstein7.N1_right.t0_checked line 274
  107. lemma OAI.SharpPlanar.Bernstein7.N1_right.t0_contains line 275
  108. def OAI.SharpPlanar.Bernstein7.N1_right.t1 line 279
  109. lemma OAI.SharpPlanar.Bernstein7.N1_right.t1_checked line 280
  110. lemma OAI.SharpPlanar.Bernstein7.N1_right.t1_contains line 281
  111. def OAI.SharpPlanar.Bernstein7.N1_right.t2 line 285
  112. lemma OAI.SharpPlanar.Bernstein7.N1_right.t2_checked line 286
  113. lemma OAI.SharpPlanar.Bernstein7.N1_right.t2_contains line 287
  114. def OAI.SharpPlanar.Bernstein7.N1_right.t3 line 291
  115. lemma OAI.SharpPlanar.Bernstein7.N1_right.t3_checked line 292
  116. lemma OAI.SharpPlanar.Bernstein7.N1_right.t3_contains line 293
  117. def OAI.SharpPlanar.Bernstein7.N1_right.t4 line 297
  118. lemma OAI.SharpPlanar.Bernstein7.N1_right.t4_checked line 298
  119. lemma OAI.SharpPlanar.Bernstein7.N1_right.t4_contains line 299
  120. def OAI.SharpPlanar.Bernstein7.N1_right.t5 line 303
  121. lemma OAI.SharpPlanar.Bernstein7.N1_right.t5_checked line 304
  122. lemma OAI.SharpPlanar.Bernstein7.N1_right.t5_contains line 305
  123. def OAI.SharpPlanar.Bernstein7.N1_right.t6 line 309
  124. lemma OAI.SharpPlanar.Bernstein7.N1_right.t6_checked line 310
  125. lemma OAI.SharpPlanar.Bernstein7.N1_right.t6_contains line 311
  126. def OAI.SharpPlanar.Bernstein7.N1_right.t7 line 315
  127. lemma OAI.SharpPlanar.Bernstein7.N1_right.t7_checked line 316
  128. lemma OAI.SharpPlanar.Bernstein7.N1_right.t7_contains line 317
  129. def OAI.SharpPlanar.Bernstein7.N1_right.t8 line 321
  130. lemma OAI.SharpPlanar.Bernstein7.N1_right.t8_checked line 322
  131. lemma OAI.SharpPlanar.Bernstein7.N1_right.t8_contains line 323
  132. def OAI.SharpPlanar.Bernstein7.N1_right.t9 line 327
  133. lemma OAI.SharpPlanar.Bernstein7.N1_right.t9_checked line 328
  134. lemma OAI.SharpPlanar.Bernstein7.N1_right.t9_contains line 329
  135. def OAI.SharpPlanar.Bernstein7.N1_right.t10 line 333
  136. lemma OAI.SharpPlanar.Bernstein7.N1_right.t10_checked line 334
  137. lemma OAI.SharpPlanar.Bernstein7.N1_right.t10_contains line 335
  138. def OAI.SharpPlanar.Bernstein7.N1_right.t11 line 339
  139. lemma OAI.SharpPlanar.Bernstein7.N1_right.t11_checked line 340
  140. lemma OAI.SharpPlanar.Bernstein7.N1_right.t11_contains line 341
  141. def OAI.SharpPlanar.Bernstein7.N1_right.t12 line 345
  142. lemma OAI.SharpPlanar.Bernstein7.N1_right.t12_checked line 346
  143. lemma OAI.SharpPlanar.Bernstein7.N1_right.t12_contains line 347
  144. def OAI.SharpPlanar.Bernstein7.N1_right.t13 line 351
  145. lemma OAI.SharpPlanar.Bernstein7.N1_right.t13_checked line 352
  146. lemma OAI.SharpPlanar.Bernstein7.N1_right.t13_contains line 353
  147. def OAI.SharpPlanar.Bernstein7.N1_right.t14 line 357
  148. lemma OAI.SharpPlanar.Bernstein7.N1_right.t14_contains line 358
  149. def OAI.SharpPlanar.Bernstein7.N1_right.t15 line 360
  150. lemma OAI.SharpPlanar.Bernstein7.N1_right.t15_contains line 361
  151. def OAI.SharpPlanar.Bernstein7.N1_right.t16 line 363
  152. lemma OAI.SharpPlanar.Bernstein7.N1_right.t16_contains line 364
  153. def OAI.SharpPlanar.Bernstein7.N1_right.t17 line 366
  154. lemma OAI.SharpPlanar.Bernstein7.N1_right.t17_contains line 367
  155. def OAI.SharpPlanar.Bernstein7.N1_right.t18 line 369
  156. lemma OAI.SharpPlanar.Bernstein7.N1_right.t18_contains line 370
  157. def OAI.SharpPlanar.Bernstein7.N1_right.t19 line 372
  158. lemma OAI.SharpPlanar.Bernstein7.N1_right.t19_contains line 373
  159. def OAI.SharpPlanar.Bernstein7.N1_right.t20 line 375
  160. lemma OAI.SharpPlanar.Bernstein7.N1_right.t20_contains line 376
  161. def OAI.SharpPlanar.Bernstein7.N1_right.t21 line 378
  162. lemma OAI.SharpPlanar.Bernstein7.N1_right.t21_contains line 379
  163. def OAI.SharpPlanar.Bernstein7.N1_right.t22 line 381
  164. lemma OAI.SharpPlanar.Bernstein7.N1_right.t22_contains line 382
  165. def OAI.SharpPlanar.Bernstein7.N1_right.t23 line 384
  166. lemma OAI.SharpPlanar.Bernstein7.N1_right.t23_contains line 385
  167. def OAI.SharpPlanar.Bernstein7.N1_right.t24 line 387
  168. lemma OAI.SharpPlanar.Bernstein7.N1_right.t24_contains line 388
  169. def OAI.SharpPlanar.Bernstein7.N1_right.t25 line 390
  170. lemma OAI.SharpPlanar.Bernstein7.N1_right.t25_contains line 391
  171. def OAI.SharpPlanar.Bernstein7.N1_right.t26 line 393
  172. lemma OAI.SharpPlanar.Bernstein7.N1_right.t26_contains line 394
  173. def OAI.SharpPlanar.Bernstein7.N1_right.t27 line 396
  174. lemma OAI.SharpPlanar.Bernstein7.N1_right.t27_contains line 397
  175. def OAI.SharpPlanar.Bernstein7.N1_right.t28 line 399
  176. lemma OAI.SharpPlanar.Bernstein7.N1_right.t28_contains line 400
  177. def OAI.SharpPlanar.Bernstein7.N1_right.ts line 402
  178. lemma OAI.SharpPlanar.Bernstein7.N1_right.ts_contains line 403
  179. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound0 line 434
  180. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound1 line 436
  181. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound2 line 438
  182. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound3 line 440
  183. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound4 line 442
  184. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound5 line 444
  185. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound6 line 446
  186. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound7 line 448
  187. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound8 line 450
  188. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound9 line 452
  189. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound10 line 454
  190. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound11 line 456
  191. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound12 line 458
  192. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound13 line 460
  193. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound14 line 462
  194. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound15 line 464
  195. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound16 line 466
  196. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound17 line 468
  197. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound18 line 470
  198. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound19 line 472
  199. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound20 line 474
  200. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound21 line 476
  201. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound22 line 478
  202. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound23 line 480
  203. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound24 line 482
  204. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound25 line 484
  205. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound26 line 486
  206. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound27 line 488
  207. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound28 line 490
  208. lemma OAI.SharpPlanar.Bernstein7.N1_right.bound line 492
  209. def OAI.SharpPlanar.Bernstein7.N0_left.t0 line 525
  210. lemma OAI.SharpPlanar.Bernstein7.N0_left.t0_checked line 526
  211. lemma OAI.SharpPlanar.Bernstein7.N0_left.t0_contains line 527
  212. def OAI.SharpPlanar.Bernstein7.N0_left.t1 line 531
  213. lemma OAI.SharpPlanar.Bernstein7.N0_left.t1_checked line 532
  214. lemma OAI.SharpPlanar.Bernstein7.N0_left.t1_contains line 533
  215. def OAI.SharpPlanar.Bernstein7.N0_left.t2 line 537
  216. lemma OAI.SharpPlanar.Bernstein7.N0_left.t2_checked line 538
  217. lemma OAI.SharpPlanar.Bernstein7.N0_left.t2_contains line 539
  218. def OAI.SharpPlanar.Bernstein7.N0_left.t3 line 543
  219. lemma OAI.SharpPlanar.Bernstein7.N0_left.t3_checked line 544
  220. lemma OAI.SharpPlanar.Bernstein7.N0_left.t3_contains line 545
  221. def OAI.SharpPlanar.Bernstein7.N0_left.t4 line 549
  222. lemma OAI.SharpPlanar.Bernstein7.N0_left.t4_checked line 550
  223. lemma OAI.SharpPlanar.Bernstein7.N0_left.t4_contains line 551
  224. def OAI.SharpPlanar.Bernstein7.N0_left.t5 line 555
  225. lemma OAI.SharpPlanar.Bernstein7.N0_left.t5_checked line 556
  226. lemma OAI.SharpPlanar.Bernstein7.N0_left.t5_contains line 557
  227. def OAI.SharpPlanar.Bernstein7.N0_left.t6 line 561
  228. lemma OAI.SharpPlanar.Bernstein7.N0_left.t6_checked line 562
  229. lemma OAI.SharpPlanar.Bernstein7.N0_left.t6_contains line 563
  230. def OAI.SharpPlanar.Bernstein7.N0_left.t7 line 567
  231. lemma OAI.SharpPlanar.Bernstein7.N0_left.t7_checked line 568
  232. lemma OAI.SharpPlanar.Bernstein7.N0_left.t7_contains line 569
  233. def OAI.SharpPlanar.Bernstein7.N0_left.t8 line 573
  234. lemma OAI.SharpPlanar.Bernstein7.N0_left.t8_checked line 574
  235. lemma OAI.SharpPlanar.Bernstein7.N0_left.t8_contains line 575
  236. def OAI.SharpPlanar.Bernstein7.N0_left.t9 line 579
  237. lemma OAI.SharpPlanar.Bernstein7.N0_left.t9_checked line 580
  238. lemma OAI.SharpPlanar.Bernstein7.N0_left.t9_contains line 581
  239. def OAI.SharpPlanar.Bernstein7.N0_left.t10 line 585
  240. lemma OAI.SharpPlanar.Bernstein7.N0_left.t10_checked line 586
  241. lemma OAI.SharpPlanar.Bernstein7.N0_left.t10_contains line 587
  242. def OAI.SharpPlanar.Bernstein7.N0_left.t11 line 591
  243. lemma OAI.SharpPlanar.Bernstein7.N0_left.t11_checked line 592
  244. lemma OAI.SharpPlanar.Bernstein7.N0_left.t11_contains line 593
  245. def OAI.SharpPlanar.Bernstein7.N0_left.t12 line 597
  246. lemma OAI.SharpPlanar.Bernstein7.N0_left.t12_checked line 598
  247. lemma OAI.SharpPlanar.Bernstein7.N0_left.t12_contains line 599
  248. def OAI.SharpPlanar.Bernstein7.N0_left.t13 line 603
  249. lemma OAI.SharpPlanar.Bernstein7.N0_left.t13_checked line 604
  250. lemma OAI.SharpPlanar.Bernstein7.N0_left.t13_contains line 605
  251. def OAI.SharpPlanar.Bernstein7.N0_left.t14 line 609
  252. lemma OAI.SharpPlanar.Bernstein7.N0_left.t14_contains line 610
  253. def OAI.SharpPlanar.Bernstein7.N0_left.t15 line 612
  254. lemma OAI.SharpPlanar.Bernstein7.N0_left.t15_contains line 613
  255. def OAI.SharpPlanar.Bernstein7.N0_left.t16 line 615
  256. lemma OAI.SharpPlanar.Bernstein7.N0_left.t16_contains line 616
  257. def OAI.SharpPlanar.Bernstein7.N0_left.t17 line 618
  258. lemma OAI.SharpPlanar.Bernstein7.N0_left.t17_contains line 619
  259. def OAI.SharpPlanar.Bernstein7.N0_left.t18 line 621
  260. lemma OAI.SharpPlanar.Bernstein7.N0_left.t18_contains line 622
  261. def OAI.SharpPlanar.Bernstein7.N0_left.t19 line 624
  262. lemma OAI.SharpPlanar.Bernstein7.N0_left.t19_contains line 625
  263. def OAI.SharpPlanar.Bernstein7.N0_left.t20 line 627
  264. lemma OAI.SharpPlanar.Bernstein7.N0_left.t20_contains line 628
  265. def OAI.SharpPlanar.Bernstein7.N0_left.t21 line 630
  266. lemma OAI.SharpPlanar.Bernstein7.N0_left.t21_contains line 631
  267. def OAI.SharpPlanar.Bernstein7.N0_left.t22 line 633
  268. lemma OAI.SharpPlanar.Bernstein7.N0_left.t22_contains line 634
  269. def OAI.SharpPlanar.Bernstein7.N0_left.t23 line 636
  270. lemma OAI.SharpPlanar.Bernstein7.N0_left.t23_contains line 637
  271. def OAI.SharpPlanar.Bernstein7.N0_left.t24 line 639
  272. lemma OAI.SharpPlanar.Bernstein7.N0_left.t24_contains line 640
  273. def OAI.SharpPlanar.Bernstein7.N0_left.t25 line 642
  274. lemma OAI.SharpPlanar.Bernstein7.N0_left.t25_contains line 643
  275. def OAI.SharpPlanar.Bernstein7.N0_left.t26 line 645
  276. lemma OAI.SharpPlanar.Bernstein7.N0_left.t26_contains line 646
  277. def OAI.SharpPlanar.Bernstein7.N0_left.t27 line 648
  278. lemma OAI.SharpPlanar.Bernstein7.N0_left.t27_contains line 649
  279. def OAI.SharpPlanar.Bernstein7.N0_left.t28 line 651
  280. lemma OAI.SharpPlanar.Bernstein7.N0_left.t28_contains line 652
  281. def OAI.SharpPlanar.Bernstein7.N0_left.ts line 654
  282. lemma OAI.SharpPlanar.Bernstein7.N0_left.ts_contains line 655
  283. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound0 line 686
  284. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound1 line 688
  285. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound2 line 690
  286. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound3 line 692
  287. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound4 line 694
  288. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound5 line 696
  289. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound6 line 698
  290. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound7 line 700
  291. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound8 line 702
  292. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound9 line 704
  293. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound10 line 706
  294. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound11 line 708
  295. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound12 line 710
  296. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound13 line 712
  297. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound14 line 714
  298. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound15 line 716
  299. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound16 line 718
  300. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound17 line 720
  301. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound18 line 722
  302. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound19 line 724
  303. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound20 line 726
  304. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound21 line 728
  305. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound22 line 730
  306. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound23 line 732
  307. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound24 line 734
  308. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound25 line 736
  309. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound26 line 738
  310. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound27 line 740
  311. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound28 line 742
  312. lemma OAI.SharpPlanar.Bernstein7.N0_left.bound line 744
  313. def OAI.SharpPlanar.Bernstein7.N1_left.t0 line 777
  314. lemma OAI.SharpPlanar.Bernstein7.N1_left.t0_checked line 778
  315. lemma OAI.SharpPlanar.Bernstein7.N1_left.t0_contains line 779
  316. def OAI.SharpPlanar.Bernstein7.N1_left.t1 line 783
  317. lemma OAI.SharpPlanar.Bernstein7.N1_left.t1_checked line 784
  318. lemma OAI.SharpPlanar.Bernstein7.N1_left.t1_contains line 785
  319. def OAI.SharpPlanar.Bernstein7.N1_left.t2 line 789
  320. lemma OAI.SharpPlanar.Bernstein7.N1_left.t2_checked line 790
  321. lemma OAI.SharpPlanar.Bernstein7.N1_left.t2_contains line 791
  322. def OAI.SharpPlanar.Bernstein7.N1_left.t3 line 795
  323. lemma OAI.SharpPlanar.Bernstein7.N1_left.t3_checked line 796
  324. lemma OAI.SharpPlanar.Bernstein7.N1_left.t3_contains line 797
  325. def OAI.SharpPlanar.Bernstein7.N1_left.t4 line 801
  326. lemma OAI.SharpPlanar.Bernstein7.N1_left.t4_checked line 802
  327. lemma OAI.SharpPlanar.Bernstein7.N1_left.t4_contains line 803
  328. def OAI.SharpPlanar.Bernstein7.N1_left.t5 line 807
  329. lemma OAI.SharpPlanar.Bernstein7.N1_left.t5_checked line 808
  330. lemma OAI.SharpPlanar.Bernstein7.N1_left.t5_contains line 809
  331. def OAI.SharpPlanar.Bernstein7.N1_left.t6 line 813
  332. lemma OAI.SharpPlanar.Bernstein7.N1_left.t6_checked line 814
  333. lemma OAI.SharpPlanar.Bernstein7.N1_left.t6_contains line 815
  334. def OAI.SharpPlanar.Bernstein7.N1_left.t7 line 819
  335. lemma OAI.SharpPlanar.Bernstein7.N1_left.t7_checked line 820
  336. lemma OAI.SharpPlanar.Bernstein7.N1_left.t7_contains line 821
  337. def OAI.SharpPlanar.Bernstein7.N1_left.t8 line 825
  338. lemma OAI.SharpPlanar.Bernstein7.N1_left.t8_checked line 826
  339. lemma OAI.SharpPlanar.Bernstein7.N1_left.t8_contains line 827
  340. def OAI.SharpPlanar.Bernstein7.N1_left.t9 line 831
  341. lemma OAI.SharpPlanar.Bernstein7.N1_left.t9_checked line 832
  342. lemma OAI.SharpPlanar.Bernstein7.N1_left.t9_contains line 833
  343. def OAI.SharpPlanar.Bernstein7.N1_left.t10 line 837
  344. lemma OAI.SharpPlanar.Bernstein7.N1_left.t10_checked line 838
  345. lemma OAI.SharpPlanar.Bernstein7.N1_left.t10_contains line 839
  346. def OAI.SharpPlanar.Bernstein7.N1_left.t11 line 843
  347. lemma OAI.SharpPlanar.Bernstein7.N1_left.t11_checked line 844
  348. lemma OAI.SharpPlanar.Bernstein7.N1_left.t11_contains line 845
  349. def OAI.SharpPlanar.Bernstein7.N1_left.t12 line 849
  350. lemma OAI.SharpPlanar.Bernstein7.N1_left.t12_checked line 850
  351. lemma OAI.SharpPlanar.Bernstein7.N1_left.t12_contains line 851
  352. def OAI.SharpPlanar.Bernstein7.N1_left.t13 line 855
  353. lemma OAI.SharpPlanar.Bernstein7.N1_left.t13_checked line 856
  354. lemma OAI.SharpPlanar.Bernstein7.N1_left.t13_contains line 857
  355. def OAI.SharpPlanar.Bernstein7.N1_left.t14 line 861
  356. lemma OAI.SharpPlanar.Bernstein7.N1_left.t14_contains line 862
  357. def OAI.SharpPlanar.Bernstein7.N1_left.t15 line 864
  358. lemma OAI.SharpPlanar.Bernstein7.N1_left.t15_contains line 865
  359. def OAI.SharpPlanar.Bernstein7.N1_left.t16 line 867
  360. lemma OAI.SharpPlanar.Bernstein7.N1_left.t16_contains line 868
  361. def OAI.SharpPlanar.Bernstein7.N1_left.t17 line 870
  362. lemma OAI.SharpPlanar.Bernstein7.N1_left.t17_contains line 871
  363. def OAI.SharpPlanar.Bernstein7.N1_left.t18 line 873
  364. lemma OAI.SharpPlanar.Bernstein7.N1_left.t18_contains line 874
  365. def OAI.SharpPlanar.Bernstein7.N1_left.t19 line 876
  366. lemma OAI.SharpPlanar.Bernstein7.N1_left.t19_contains line 877
  367. def OAI.SharpPlanar.Bernstein7.N1_left.t20 line 879
  368. lemma OAI.SharpPlanar.Bernstein7.N1_left.t20_contains line 880
  369. def OAI.SharpPlanar.Bernstein7.N1_left.t21 line 882
  370. lemma OAI.SharpPlanar.Bernstein7.N1_left.t21_contains line 883
  371. def OAI.SharpPlanar.Bernstein7.N1_left.t22 line 885
  372. lemma OAI.SharpPlanar.Bernstein7.N1_left.t22_contains line 886
  373. def OAI.SharpPlanar.Bernstein7.N1_left.t23 line 888
  374. lemma OAI.SharpPlanar.Bernstein7.N1_left.t23_contains line 889
  375. def OAI.SharpPlanar.Bernstein7.N1_left.t24 line 891
  376. lemma OAI.SharpPlanar.Bernstein7.N1_left.t24_contains line 892
  377. def OAI.SharpPlanar.Bernstein7.N1_left.t25 line 894
  378. lemma OAI.SharpPlanar.Bernstein7.N1_left.t25_contains line 895
  379. def OAI.SharpPlanar.Bernstein7.N1_left.t26 line 897
  380. lemma OAI.SharpPlanar.Bernstein7.N1_left.t26_contains line 898
  381. def OAI.SharpPlanar.Bernstein7.N1_left.t27 line 900
  382. lemma OAI.SharpPlanar.Bernstein7.N1_left.t27_contains line 901
  383. def OAI.SharpPlanar.Bernstein7.N1_left.t28 line 903
  384. lemma OAI.SharpPlanar.Bernstein7.N1_left.t28_contains line 904
  385. def OAI.SharpPlanar.Bernstein7.N1_left.ts line 906
  386. lemma OAI.SharpPlanar.Bernstein7.N1_left.ts_contains line 907
  387. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound0 line 938
  388. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound1 line 940
  389. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound2 line 942
  390. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound3 line 944
  391. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound4 line 946
  392. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound5 line 948
  393. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound6 line 950
  394. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound7 line 952
  395. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound8 line 954
  396. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound9 line 956
  397. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound10 line 958
  398. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound11 line 960
  399. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound12 line 962
  400. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound13 line 964
  401. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound14 line 966
  402. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound15 line 968
  403. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound16 line 970
  404. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound17 line 972
  405. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound18 line 974
  406. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound19 line 976
  407. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound20 line 978
  408. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound21 line 980
  409. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound22 line 982
  410. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound23 line 984
  411. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound24 line 986
  412. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound25 line 988
  413. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound26 line 990
  414. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound27 line 992
  415. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound28 line 994
  416. lemma OAI.SharpPlanar.Bernstein7.N1_left.bound line 996