OAI/Analysis/PlanarPacking/Certificate/Bernstein40.lean

GitHub source file

488 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.Bernstein40.N0_right.t0 line 19
  2. lemma OAI.SharpPlanar.Bernstein40.N0_right.t0_checked line 20
  3. lemma OAI.SharpPlanar.Bernstein40.N0_right.t0_contains line 21
  4. def OAI.SharpPlanar.Bernstein40.N0_right.t1 line 25
  5. lemma OAI.SharpPlanar.Bernstein40.N0_right.t1_checked line 26
  6. lemma OAI.SharpPlanar.Bernstein40.N0_right.t1_contains line 27
  7. def OAI.SharpPlanar.Bernstein40.N0_right.tr2 line 31
  8. lemma OAI.SharpPlanar.Bernstein40.N0_right.tr2_contains line 32
  9. def OAI.SharpPlanar.Bernstein40.N0_right.t2 line 34
  10. lemma OAI.SharpPlanar.Bernstein40.N0_right.t2_checked line 35
  11. lemma OAI.SharpPlanar.Bernstein40.N0_right.t2_contains line 36
  12. def OAI.SharpPlanar.Bernstein40.N0_right.tr3 line 40
  13. lemma OAI.SharpPlanar.Bernstein40.N0_right.tr3_contains line 41
  14. def OAI.SharpPlanar.Bernstein40.N0_right.t3 line 43
  15. lemma OAI.SharpPlanar.Bernstein40.N0_right.t3_checked line 44
  16. lemma OAI.SharpPlanar.Bernstein40.N0_right.t3_contains line 45
  17. def OAI.SharpPlanar.Bernstein40.N0_right.tr4 line 49
  18. lemma OAI.SharpPlanar.Bernstein40.N0_right.tr4_contains line 50
  19. def OAI.SharpPlanar.Bernstein40.N0_right.t4 line 52
  20. lemma OAI.SharpPlanar.Bernstein40.N0_right.t4_checked line 53
  21. lemma OAI.SharpPlanar.Bernstein40.N0_right.t4_contains line 54
  22. def OAI.SharpPlanar.Bernstein40.N0_right.tr5 line 58
  23. lemma OAI.SharpPlanar.Bernstein40.N0_right.tr5_contains line 59
  24. def OAI.SharpPlanar.Bernstein40.N0_right.t5 line 61
  25. lemma OAI.SharpPlanar.Bernstein40.N0_right.t5_checked line 62
  26. lemma OAI.SharpPlanar.Bernstein40.N0_right.t5_contains line 63
  27. def OAI.SharpPlanar.Bernstein40.N0_right.tr6 line 67
  28. lemma OAI.SharpPlanar.Bernstein40.N0_right.tr6_contains line 68
  29. def OAI.SharpPlanar.Bernstein40.N0_right.t6 line 70
  30. lemma OAI.SharpPlanar.Bernstein40.N0_right.t6_checked line 71
  31. lemma OAI.SharpPlanar.Bernstein40.N0_right.t6_contains line 72
  32. def OAI.SharpPlanar.Bernstein40.N0_right.tr7 line 76
  33. lemma OAI.SharpPlanar.Bernstein40.N0_right.tr7_contains line 77
  34. def OAI.SharpPlanar.Bernstein40.N0_right.t7 line 79
  35. lemma OAI.SharpPlanar.Bernstein40.N0_right.t7_checked line 80
  36. lemma OAI.SharpPlanar.Bernstein40.N0_right.t7_contains line 81
  37. def OAI.SharpPlanar.Bernstein40.N0_right.tr8 line 85
  38. lemma OAI.SharpPlanar.Bernstein40.N0_right.tr8_contains line 86
  39. def OAI.SharpPlanar.Bernstein40.N0_right.t8 line 88
  40. lemma OAI.SharpPlanar.Bernstein40.N0_right.t8_checked line 89
  41. lemma OAI.SharpPlanar.Bernstein40.N0_right.t8_contains line 90
  42. def OAI.SharpPlanar.Bernstein40.N0_right.tr9 line 94
  43. lemma OAI.SharpPlanar.Bernstein40.N0_right.tr9_contains line 95
  44. def OAI.SharpPlanar.Bernstein40.N0_right.t9 line 97
  45. lemma OAI.SharpPlanar.Bernstein40.N0_right.t9_checked line 98
  46. lemma OAI.SharpPlanar.Bernstein40.N0_right.t9_contains line 99
  47. def OAI.SharpPlanar.Bernstein40.N0_right.tr10 line 103
  48. lemma OAI.SharpPlanar.Bernstein40.N0_right.tr10_contains line 104
  49. def OAI.SharpPlanar.Bernstein40.N0_right.t10 line 106
  50. lemma OAI.SharpPlanar.Bernstein40.N0_right.t10_checked line 107
  51. lemma OAI.SharpPlanar.Bernstein40.N0_right.t10_contains line 108
  52. def OAI.SharpPlanar.Bernstein40.N0_right.tr11 line 112
  53. lemma OAI.SharpPlanar.Bernstein40.N0_right.tr11_contains line 113
  54. def OAI.SharpPlanar.Bernstein40.N0_right.t11 line 115
  55. lemma OAI.SharpPlanar.Bernstein40.N0_right.t11_checked line 116
  56. lemma OAI.SharpPlanar.Bernstein40.N0_right.t11_contains line 117
  57. def OAI.SharpPlanar.Bernstein40.N0_right.t12 line 121
  58. lemma OAI.SharpPlanar.Bernstein40.N0_right.t12_contains line 122
  59. def OAI.SharpPlanar.Bernstein40.N0_right.t13 line 124
  60. lemma OAI.SharpPlanar.Bernstein40.N0_right.t13_contains line 125
  61. def OAI.SharpPlanar.Bernstein40.N0_right.t14 line 127
  62. lemma OAI.SharpPlanar.Bernstein40.N0_right.t14_contains line 128
  63. def OAI.SharpPlanar.Bernstein40.N0_right.t15 line 130
  64. lemma OAI.SharpPlanar.Bernstein40.N0_right.t15_contains line 131
  65. def OAI.SharpPlanar.Bernstein40.N0_right.t16 line 133
  66. lemma OAI.SharpPlanar.Bernstein40.N0_right.t16_contains line 134
  67. def OAI.SharpPlanar.Bernstein40.N0_right.t17 line 136
  68. lemma OAI.SharpPlanar.Bernstein40.N0_right.t17_contains line 137
  69. def OAI.SharpPlanar.Bernstein40.N0_right.t18 line 139
  70. lemma OAI.SharpPlanar.Bernstein40.N0_right.t18_contains line 140
  71. def OAI.SharpPlanar.Bernstein40.N0_right.t19 line 142
  72. lemma OAI.SharpPlanar.Bernstein40.N0_right.t19_contains line 143
  73. def OAI.SharpPlanar.Bernstein40.N0_right.t20 line 145
  74. lemma OAI.SharpPlanar.Bernstein40.N0_right.t20_contains line 146
  75. def OAI.SharpPlanar.Bernstein40.N0_right.t21 line 148
  76. lemma OAI.SharpPlanar.Bernstein40.N0_right.t21_contains line 149
  77. def OAI.SharpPlanar.Bernstein40.N0_right.t22 line 151
  78. lemma OAI.SharpPlanar.Bernstein40.N0_right.t22_contains line 152
  79. def OAI.SharpPlanar.Bernstein40.N0_right.t23 line 154
  80. lemma OAI.SharpPlanar.Bernstein40.N0_right.t23_contains line 155
  81. def OAI.SharpPlanar.Bernstein40.N0_right.t24 line 157
  82. lemma OAI.SharpPlanar.Bernstein40.N0_right.t24_contains line 158
  83. def OAI.SharpPlanar.Bernstein40.N0_right.t25 line 160
  84. lemma OAI.SharpPlanar.Bernstein40.N0_right.t25_contains line 161
  85. def OAI.SharpPlanar.Bernstein40.N0_right.t26 line 163
  86. lemma OAI.SharpPlanar.Bernstein40.N0_right.t26_contains line 164
  87. def OAI.SharpPlanar.Bernstein40.N0_right.t27 line 166
  88. lemma OAI.SharpPlanar.Bernstein40.N0_right.t27_contains line 167
  89. def OAI.SharpPlanar.Bernstein40.N0_right.t28 line 169
  90. lemma OAI.SharpPlanar.Bernstein40.N0_right.t28_contains line 170
  91. def OAI.SharpPlanar.Bernstein40.N0_right.ts line 172
  92. lemma OAI.SharpPlanar.Bernstein40.N0_right.ts_contains line 173
  93. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound0 line 204
  94. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound1 line 206
  95. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound2 line 208
  96. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound3 line 210
  97. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound4 line 212
  98. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound5 line 214
  99. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound6 line 216
  100. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound7 line 218
  101. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound8 line 220
  102. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound9 line 222
  103. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound10 line 224
  104. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound11 line 226
  105. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound12 line 228
  106. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound13 line 230
  107. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound14 line 232
  108. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound15 line 234
  109. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound16 line 236
  110. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound17 line 238
  111. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound18 line 240
  112. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound19 line 242
  113. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound20 line 244
  114. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound21 line 246
  115. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound22 line 248
  116. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound23 line 250
  117. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound24 line 252
  118. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound25 line 254
  119. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound26 line 256
  120. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound27 line 258
  121. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound28 line 260
  122. lemma OAI.SharpPlanar.Bernstein40.N0_right.bound line 262
  123. def OAI.SharpPlanar.Bernstein40.N1_right.t0 line 295
  124. lemma OAI.SharpPlanar.Bernstein40.N1_right.t0_checked line 296
  125. lemma OAI.SharpPlanar.Bernstein40.N1_right.t0_contains line 297
  126. def OAI.SharpPlanar.Bernstein40.N1_right.t1 line 301
  127. lemma OAI.SharpPlanar.Bernstein40.N1_right.t1_checked line 302
  128. lemma OAI.SharpPlanar.Bernstein40.N1_right.t1_contains line 303
  129. def OAI.SharpPlanar.Bernstein40.N1_right.tr2 line 307
  130. lemma OAI.SharpPlanar.Bernstein40.N1_right.tr2_contains line 308
  131. def OAI.SharpPlanar.Bernstein40.N1_right.t2 line 310
  132. lemma OAI.SharpPlanar.Bernstein40.N1_right.t2_checked line 311
  133. lemma OAI.SharpPlanar.Bernstein40.N1_right.t2_contains line 312
  134. def OAI.SharpPlanar.Bernstein40.N1_right.tr3 line 316
  135. lemma OAI.SharpPlanar.Bernstein40.N1_right.tr3_contains line 317
  136. def OAI.SharpPlanar.Bernstein40.N1_right.t3 line 319
  137. lemma OAI.SharpPlanar.Bernstein40.N1_right.t3_checked line 320
  138. lemma OAI.SharpPlanar.Bernstein40.N1_right.t3_contains line 321
  139. def OAI.SharpPlanar.Bernstein40.N1_right.tr4 line 325
  140. lemma OAI.SharpPlanar.Bernstein40.N1_right.tr4_contains line 326
  141. def OAI.SharpPlanar.Bernstein40.N1_right.t4 line 328
  142. lemma OAI.SharpPlanar.Bernstein40.N1_right.t4_checked line 329
  143. lemma OAI.SharpPlanar.Bernstein40.N1_right.t4_contains line 330
  144. def OAI.SharpPlanar.Bernstein40.N1_right.tr5 line 334
  145. lemma OAI.SharpPlanar.Bernstein40.N1_right.tr5_contains line 335
  146. def OAI.SharpPlanar.Bernstein40.N1_right.t5 line 337
  147. lemma OAI.SharpPlanar.Bernstein40.N1_right.t5_checked line 338
  148. lemma OAI.SharpPlanar.Bernstein40.N1_right.t5_contains line 339
  149. def OAI.SharpPlanar.Bernstein40.N1_right.tr6 line 343
  150. lemma OAI.SharpPlanar.Bernstein40.N1_right.tr6_contains line 344
  151. def OAI.SharpPlanar.Bernstein40.N1_right.t6 line 346
  152. lemma OAI.SharpPlanar.Bernstein40.N1_right.t6_checked line 347
  153. lemma OAI.SharpPlanar.Bernstein40.N1_right.t6_contains line 348
  154. def OAI.SharpPlanar.Bernstein40.N1_right.tr7 line 352
  155. lemma OAI.SharpPlanar.Bernstein40.N1_right.tr7_contains line 353
  156. def OAI.SharpPlanar.Bernstein40.N1_right.t7 line 355
  157. lemma OAI.SharpPlanar.Bernstein40.N1_right.t7_checked line 356
  158. lemma OAI.SharpPlanar.Bernstein40.N1_right.t7_contains line 357
  159. def OAI.SharpPlanar.Bernstein40.N1_right.tr8 line 361
  160. lemma OAI.SharpPlanar.Bernstein40.N1_right.tr8_contains line 362
  161. def OAI.SharpPlanar.Bernstein40.N1_right.t8 line 364
  162. lemma OAI.SharpPlanar.Bernstein40.N1_right.t8_checked line 365
  163. lemma OAI.SharpPlanar.Bernstein40.N1_right.t8_contains line 366
  164. def OAI.SharpPlanar.Bernstein40.N1_right.tr9 line 370
  165. lemma OAI.SharpPlanar.Bernstein40.N1_right.tr9_contains line 371
  166. def OAI.SharpPlanar.Bernstein40.N1_right.t9 line 373
  167. lemma OAI.SharpPlanar.Bernstein40.N1_right.t9_checked line 374
  168. lemma OAI.SharpPlanar.Bernstein40.N1_right.t9_contains line 375
  169. def OAI.SharpPlanar.Bernstein40.N1_right.tr10 line 379
  170. lemma OAI.SharpPlanar.Bernstein40.N1_right.tr10_contains line 380
  171. def OAI.SharpPlanar.Bernstein40.N1_right.t10 line 382
  172. lemma OAI.SharpPlanar.Bernstein40.N1_right.t10_checked line 383
  173. lemma OAI.SharpPlanar.Bernstein40.N1_right.t10_contains line 384
  174. def OAI.SharpPlanar.Bernstein40.N1_right.tr11 line 388
  175. lemma OAI.SharpPlanar.Bernstein40.N1_right.tr11_contains line 389
  176. def OAI.SharpPlanar.Bernstein40.N1_right.t11 line 391
  177. lemma OAI.SharpPlanar.Bernstein40.N1_right.t11_checked line 392
  178. lemma OAI.SharpPlanar.Bernstein40.N1_right.t11_contains line 393
  179. def OAI.SharpPlanar.Bernstein40.N1_right.t12 line 397
  180. lemma OAI.SharpPlanar.Bernstein40.N1_right.t12_contains line 398
  181. def OAI.SharpPlanar.Bernstein40.N1_right.t13 line 400
  182. lemma OAI.SharpPlanar.Bernstein40.N1_right.t13_contains line 401
  183. def OAI.SharpPlanar.Bernstein40.N1_right.t14 line 403
  184. lemma OAI.SharpPlanar.Bernstein40.N1_right.t14_contains line 404
  185. def OAI.SharpPlanar.Bernstein40.N1_right.t15 line 406
  186. lemma OAI.SharpPlanar.Bernstein40.N1_right.t15_contains line 407
  187. def OAI.SharpPlanar.Bernstein40.N1_right.t16 line 409
  188. lemma OAI.SharpPlanar.Bernstein40.N1_right.t16_contains line 410
  189. def OAI.SharpPlanar.Bernstein40.N1_right.t17 line 412
  190. lemma OAI.SharpPlanar.Bernstein40.N1_right.t17_contains line 413
  191. def OAI.SharpPlanar.Bernstein40.N1_right.t18 line 415
  192. lemma OAI.SharpPlanar.Bernstein40.N1_right.t18_contains line 416
  193. def OAI.SharpPlanar.Bernstein40.N1_right.t19 line 418
  194. lemma OAI.SharpPlanar.Bernstein40.N1_right.t19_contains line 419
  195. def OAI.SharpPlanar.Bernstein40.N1_right.t20 line 421
  196. lemma OAI.SharpPlanar.Bernstein40.N1_right.t20_contains line 422
  197. def OAI.SharpPlanar.Bernstein40.N1_right.t21 line 424
  198. lemma OAI.SharpPlanar.Bernstein40.N1_right.t21_contains line 425
  199. def OAI.SharpPlanar.Bernstein40.N1_right.t22 line 427
  200. lemma OAI.SharpPlanar.Bernstein40.N1_right.t22_contains line 428
  201. def OAI.SharpPlanar.Bernstein40.N1_right.t23 line 430
  202. lemma OAI.SharpPlanar.Bernstein40.N1_right.t23_contains line 431
  203. def OAI.SharpPlanar.Bernstein40.N1_right.t24 line 433
  204. lemma OAI.SharpPlanar.Bernstein40.N1_right.t24_contains line 434
  205. def OAI.SharpPlanar.Bernstein40.N1_right.t25 line 436
  206. lemma OAI.SharpPlanar.Bernstein40.N1_right.t25_contains line 437
  207. def OAI.SharpPlanar.Bernstein40.N1_right.t26 line 439
  208. lemma OAI.SharpPlanar.Bernstein40.N1_right.t26_contains line 440
  209. def OAI.SharpPlanar.Bernstein40.N1_right.t27 line 442
  210. lemma OAI.SharpPlanar.Bernstein40.N1_right.t27_contains line 443
  211. def OAI.SharpPlanar.Bernstein40.N1_right.t28 line 445
  212. lemma OAI.SharpPlanar.Bernstein40.N1_right.t28_contains line 446
  213. def OAI.SharpPlanar.Bernstein40.N1_right.ts line 448
  214. lemma OAI.SharpPlanar.Bernstein40.N1_right.ts_contains line 449
  215. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound0 line 480
  216. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound1 line 482
  217. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound2 line 484
  218. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound3 line 486
  219. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound4 line 488
  220. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound5 line 490
  221. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound6 line 492
  222. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound7 line 494
  223. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound8 line 496
  224. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound9 line 498
  225. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound10 line 500
  226. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound11 line 502
  227. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound12 line 504
  228. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound13 line 506
  229. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound14 line 508
  230. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound15 line 510
  231. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound16 line 512
  232. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound17 line 514
  233. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound18 line 516
  234. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound19 line 518
  235. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound20 line 520
  236. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound21 line 522
  237. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound22 line 524
  238. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound23 line 526
  239. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound24 line 528
  240. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound25 line 530
  241. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound26 line 532
  242. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound27 line 534
  243. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound28 line 536
  244. lemma OAI.SharpPlanar.Bernstein40.N1_right.bound line 538
  245. def OAI.SharpPlanar.Bernstein40.N0_left.t0 line 571
  246. lemma OAI.SharpPlanar.Bernstein40.N0_left.t0_checked line 572
  247. lemma OAI.SharpPlanar.Bernstein40.N0_left.t0_contains line 573
  248. def OAI.SharpPlanar.Bernstein40.N0_left.t1 line 577
  249. lemma OAI.SharpPlanar.Bernstein40.N0_left.t1_checked line 578
  250. lemma OAI.SharpPlanar.Bernstein40.N0_left.t1_contains line 579
  251. def OAI.SharpPlanar.Bernstein40.N0_left.tr2 line 583
  252. lemma OAI.SharpPlanar.Bernstein40.N0_left.tr2_contains line 584
  253. def OAI.SharpPlanar.Bernstein40.N0_left.t2 line 586
  254. lemma OAI.SharpPlanar.Bernstein40.N0_left.t2_checked line 587
  255. lemma OAI.SharpPlanar.Bernstein40.N0_left.t2_contains line 588
  256. def OAI.SharpPlanar.Bernstein40.N0_left.tr3 line 592
  257. lemma OAI.SharpPlanar.Bernstein40.N0_left.tr3_contains line 593
  258. def OAI.SharpPlanar.Bernstein40.N0_left.t3 line 595
  259. lemma OAI.SharpPlanar.Bernstein40.N0_left.t3_checked line 596
  260. lemma OAI.SharpPlanar.Bernstein40.N0_left.t3_contains line 597
  261. def OAI.SharpPlanar.Bernstein40.N0_left.tr4 line 601
  262. lemma OAI.SharpPlanar.Bernstein40.N0_left.tr4_contains line 602
  263. def OAI.SharpPlanar.Bernstein40.N0_left.t4 line 604
  264. lemma OAI.SharpPlanar.Bernstein40.N0_left.t4_checked line 605
  265. lemma OAI.SharpPlanar.Bernstein40.N0_left.t4_contains line 606
  266. def OAI.SharpPlanar.Bernstein40.N0_left.tr5 line 610
  267. lemma OAI.SharpPlanar.Bernstein40.N0_left.tr5_contains line 611
  268. def OAI.SharpPlanar.Bernstein40.N0_left.t5 line 613
  269. lemma OAI.SharpPlanar.Bernstein40.N0_left.t5_checked line 614
  270. lemma OAI.SharpPlanar.Bernstein40.N0_left.t5_contains line 615
  271. def OAI.SharpPlanar.Bernstein40.N0_left.tr6 line 619
  272. lemma OAI.SharpPlanar.Bernstein40.N0_left.tr6_contains line 620
  273. def OAI.SharpPlanar.Bernstein40.N0_left.t6 line 622
  274. lemma OAI.SharpPlanar.Bernstein40.N0_left.t6_checked line 623
  275. lemma OAI.SharpPlanar.Bernstein40.N0_left.t6_contains line 624
  276. def OAI.SharpPlanar.Bernstein40.N0_left.tr7 line 628
  277. lemma OAI.SharpPlanar.Bernstein40.N0_left.tr7_contains line 629
  278. def OAI.SharpPlanar.Bernstein40.N0_left.t7 line 631
  279. lemma OAI.SharpPlanar.Bernstein40.N0_left.t7_checked line 632
  280. lemma OAI.SharpPlanar.Bernstein40.N0_left.t7_contains line 633
  281. def OAI.SharpPlanar.Bernstein40.N0_left.tr8 line 637
  282. lemma OAI.SharpPlanar.Bernstein40.N0_left.tr8_contains line 638
  283. def OAI.SharpPlanar.Bernstein40.N0_left.t8 line 640
  284. lemma OAI.SharpPlanar.Bernstein40.N0_left.t8_checked line 641
  285. lemma OAI.SharpPlanar.Bernstein40.N0_left.t8_contains line 642
  286. def OAI.SharpPlanar.Bernstein40.N0_left.tr9 line 646
  287. lemma OAI.SharpPlanar.Bernstein40.N0_left.tr9_contains line 647
  288. def OAI.SharpPlanar.Bernstein40.N0_left.t9 line 649
  289. lemma OAI.SharpPlanar.Bernstein40.N0_left.t9_checked line 650
  290. lemma OAI.SharpPlanar.Bernstein40.N0_left.t9_contains line 651
  291. def OAI.SharpPlanar.Bernstein40.N0_left.tr10 line 655
  292. lemma OAI.SharpPlanar.Bernstein40.N0_left.tr10_contains line 656
  293. def OAI.SharpPlanar.Bernstein40.N0_left.t10 line 658
  294. lemma OAI.SharpPlanar.Bernstein40.N0_left.t10_checked line 659
  295. lemma OAI.SharpPlanar.Bernstein40.N0_left.t10_contains line 660
  296. def OAI.SharpPlanar.Bernstein40.N0_left.tr11 line 664
  297. lemma OAI.SharpPlanar.Bernstein40.N0_left.tr11_contains line 665
  298. def OAI.SharpPlanar.Bernstein40.N0_left.t11 line 667
  299. lemma OAI.SharpPlanar.Bernstein40.N0_left.t11_checked line 668
  300. lemma OAI.SharpPlanar.Bernstein40.N0_left.t11_contains line 669
  301. def OAI.SharpPlanar.Bernstein40.N0_left.t12 line 673
  302. lemma OAI.SharpPlanar.Bernstein40.N0_left.t12_contains line 674
  303. def OAI.SharpPlanar.Bernstein40.N0_left.t13 line 676
  304. lemma OAI.SharpPlanar.Bernstein40.N0_left.t13_contains line 677
  305. def OAI.SharpPlanar.Bernstein40.N0_left.t14 line 679
  306. lemma OAI.SharpPlanar.Bernstein40.N0_left.t14_contains line 680
  307. def OAI.SharpPlanar.Bernstein40.N0_left.t15 line 682
  308. lemma OAI.SharpPlanar.Bernstein40.N0_left.t15_contains line 683
  309. def OAI.SharpPlanar.Bernstein40.N0_left.t16 line 685
  310. lemma OAI.SharpPlanar.Bernstein40.N0_left.t16_contains line 686
  311. def OAI.SharpPlanar.Bernstein40.N0_left.t17 line 688
  312. lemma OAI.SharpPlanar.Bernstein40.N0_left.t17_contains line 689
  313. def OAI.SharpPlanar.Bernstein40.N0_left.t18 line 691
  314. lemma OAI.SharpPlanar.Bernstein40.N0_left.t18_contains line 692
  315. def OAI.SharpPlanar.Bernstein40.N0_left.t19 line 694
  316. lemma OAI.SharpPlanar.Bernstein40.N0_left.t19_contains line 695
  317. def OAI.SharpPlanar.Bernstein40.N0_left.t20 line 697
  318. lemma OAI.SharpPlanar.Bernstein40.N0_left.t20_contains line 698
  319. def OAI.SharpPlanar.Bernstein40.N0_left.t21 line 700
  320. lemma OAI.SharpPlanar.Bernstein40.N0_left.t21_contains line 701
  321. def OAI.SharpPlanar.Bernstein40.N0_left.t22 line 703
  322. lemma OAI.SharpPlanar.Bernstein40.N0_left.t22_contains line 704
  323. def OAI.SharpPlanar.Bernstein40.N0_left.t23 line 706
  324. lemma OAI.SharpPlanar.Bernstein40.N0_left.t23_contains line 707
  325. def OAI.SharpPlanar.Bernstein40.N0_left.t24 line 709
  326. lemma OAI.SharpPlanar.Bernstein40.N0_left.t24_contains line 710
  327. def OAI.SharpPlanar.Bernstein40.N0_left.t25 line 712
  328. lemma OAI.SharpPlanar.Bernstein40.N0_left.t25_contains line 713
  329. def OAI.SharpPlanar.Bernstein40.N0_left.t26 line 715
  330. lemma OAI.SharpPlanar.Bernstein40.N0_left.t26_contains line 716
  331. def OAI.SharpPlanar.Bernstein40.N0_left.t27 line 718
  332. lemma OAI.SharpPlanar.Bernstein40.N0_left.t27_contains line 719
  333. def OAI.SharpPlanar.Bernstein40.N0_left.t28 line 721
  334. lemma OAI.SharpPlanar.Bernstein40.N0_left.t28_contains line 722
  335. def OAI.SharpPlanar.Bernstein40.N0_left.ts line 724
  336. lemma OAI.SharpPlanar.Bernstein40.N0_left.ts_contains line 725
  337. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound0 line 756
  338. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound1 line 758
  339. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound2 line 760
  340. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound3 line 762
  341. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound4 line 764
  342. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound5 line 766
  343. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound6 line 768
  344. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound7 line 770
  345. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound8 line 772
  346. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound9 line 774
  347. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound10 line 776
  348. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound11 line 778
  349. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound12 line 780
  350. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound13 line 782
  351. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound14 line 784
  352. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound15 line 786
  353. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound16 line 788
  354. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound17 line 790
  355. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound18 line 792
  356. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound19 line 794
  357. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound20 line 796
  358. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound21 line 798
  359. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound22 line 800
  360. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound23 line 802
  361. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound24 line 804
  362. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound25 line 806
  363. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound26 line 808
  364. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound27 line 810
  365. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound28 line 812
  366. lemma OAI.SharpPlanar.Bernstein40.N0_left.bound line 814
  367. def OAI.SharpPlanar.Bernstein40.N1_left.t0 line 847
  368. lemma OAI.SharpPlanar.Bernstein40.N1_left.t0_checked line 848
  369. lemma OAI.SharpPlanar.Bernstein40.N1_left.t0_contains line 849
  370. def OAI.SharpPlanar.Bernstein40.N1_left.t1 line 853
  371. lemma OAI.SharpPlanar.Bernstein40.N1_left.t1_checked line 854
  372. lemma OAI.SharpPlanar.Bernstein40.N1_left.t1_contains line 855
  373. def OAI.SharpPlanar.Bernstein40.N1_left.tr2 line 859
  374. lemma OAI.SharpPlanar.Bernstein40.N1_left.tr2_contains line 860
  375. def OAI.SharpPlanar.Bernstein40.N1_left.t2 line 862
  376. lemma OAI.SharpPlanar.Bernstein40.N1_left.t2_checked line 863
  377. lemma OAI.SharpPlanar.Bernstein40.N1_left.t2_contains line 864
  378. def OAI.SharpPlanar.Bernstein40.N1_left.tr3 line 868
  379. lemma OAI.SharpPlanar.Bernstein40.N1_left.tr3_contains line 869
  380. def OAI.SharpPlanar.Bernstein40.N1_left.t3 line 871
  381. lemma OAI.SharpPlanar.Bernstein40.N1_left.t3_checked line 872
  382. lemma OAI.SharpPlanar.Bernstein40.N1_left.t3_contains line 873
  383. def OAI.SharpPlanar.Bernstein40.N1_left.tr4 line 877
  384. lemma OAI.SharpPlanar.Bernstein40.N1_left.tr4_contains line 878
  385. def OAI.SharpPlanar.Bernstein40.N1_left.t4 line 880
  386. lemma OAI.SharpPlanar.Bernstein40.N1_left.t4_checked line 881
  387. lemma OAI.SharpPlanar.Bernstein40.N1_left.t4_contains line 882
  388. def OAI.SharpPlanar.Bernstein40.N1_left.tr5 line 886
  389. lemma OAI.SharpPlanar.Bernstein40.N1_left.tr5_contains line 887
  390. def OAI.SharpPlanar.Bernstein40.N1_left.t5 line 889
  391. lemma OAI.SharpPlanar.Bernstein40.N1_left.t5_checked line 890
  392. lemma OAI.SharpPlanar.Bernstein40.N1_left.t5_contains line 891
  393. def OAI.SharpPlanar.Bernstein40.N1_left.tr6 line 895
  394. lemma OAI.SharpPlanar.Bernstein40.N1_left.tr6_contains line 896
  395. def OAI.SharpPlanar.Bernstein40.N1_left.t6 line 898
  396. lemma OAI.SharpPlanar.Bernstein40.N1_left.t6_checked line 899
  397. lemma OAI.SharpPlanar.Bernstein40.N1_left.t6_contains line 900
  398. def OAI.SharpPlanar.Bernstein40.N1_left.tr7 line 904
  399. lemma OAI.SharpPlanar.Bernstein40.N1_left.tr7_contains line 905
  400. def OAI.SharpPlanar.Bernstein40.N1_left.t7 line 907
  401. lemma OAI.SharpPlanar.Bernstein40.N1_left.t7_checked line 908
  402. lemma OAI.SharpPlanar.Bernstein40.N1_left.t7_contains line 909
  403. def OAI.SharpPlanar.Bernstein40.N1_left.tr8 line 913
  404. lemma OAI.SharpPlanar.Bernstein40.N1_left.tr8_contains line 914
  405. def OAI.SharpPlanar.Bernstein40.N1_left.t8 line 916
  406. lemma OAI.SharpPlanar.Bernstein40.N1_left.t8_checked line 917
  407. lemma OAI.SharpPlanar.Bernstein40.N1_left.t8_contains line 918
  408. def OAI.SharpPlanar.Bernstein40.N1_left.tr9 line 922
  409. lemma OAI.SharpPlanar.Bernstein40.N1_left.tr9_contains line 923
  410. def OAI.SharpPlanar.Bernstein40.N1_left.t9 line 925
  411. lemma OAI.SharpPlanar.Bernstein40.N1_left.t9_checked line 926
  412. lemma OAI.SharpPlanar.Bernstein40.N1_left.t9_contains line 927
  413. def OAI.SharpPlanar.Bernstein40.N1_left.tr10 line 931
  414. lemma OAI.SharpPlanar.Bernstein40.N1_left.tr10_contains line 932
  415. def OAI.SharpPlanar.Bernstein40.N1_left.t10 line 934
  416. lemma OAI.SharpPlanar.Bernstein40.N1_left.t10_checked line 935
  417. lemma OAI.SharpPlanar.Bernstein40.N1_left.t10_contains line 936
  418. def OAI.SharpPlanar.Bernstein40.N1_left.tr11 line 940
  419. lemma OAI.SharpPlanar.Bernstein40.N1_left.tr11_contains line 941
  420. def OAI.SharpPlanar.Bernstein40.N1_left.t11 line 943
  421. lemma OAI.SharpPlanar.Bernstein40.N1_left.t11_checked line 944
  422. lemma OAI.SharpPlanar.Bernstein40.N1_left.t11_contains line 945
  423. def OAI.SharpPlanar.Bernstein40.N1_left.t12 line 949
  424. lemma OAI.SharpPlanar.Bernstein40.N1_left.t12_contains line 950
  425. def OAI.SharpPlanar.Bernstein40.N1_left.t13 line 952
  426. lemma OAI.SharpPlanar.Bernstein40.N1_left.t13_contains line 953
  427. def OAI.SharpPlanar.Bernstein40.N1_left.t14 line 955
  428. lemma OAI.SharpPlanar.Bernstein40.N1_left.t14_contains line 956
  429. def OAI.SharpPlanar.Bernstein40.N1_left.t15 line 958
  430. lemma OAI.SharpPlanar.Bernstein40.N1_left.t15_contains line 959
  431. def OAI.SharpPlanar.Bernstein40.N1_left.t16 line 961
  432. lemma OAI.SharpPlanar.Bernstein40.N1_left.t16_contains line 962
  433. def OAI.SharpPlanar.Bernstein40.N1_left.t17 line 964
  434. lemma OAI.SharpPlanar.Bernstein40.N1_left.t17_contains line 965
  435. def OAI.SharpPlanar.Bernstein40.N1_left.t18 line 967
  436. lemma OAI.SharpPlanar.Bernstein40.N1_left.t18_contains line 968
  437. def OAI.SharpPlanar.Bernstein40.N1_left.t19 line 970
  438. lemma OAI.SharpPlanar.Bernstein40.N1_left.t19_contains line 971
  439. def OAI.SharpPlanar.Bernstein40.N1_left.t20 line 973
  440. lemma OAI.SharpPlanar.Bernstein40.N1_left.t20_contains line 974
  441. def OAI.SharpPlanar.Bernstein40.N1_left.t21 line 976
  442. lemma OAI.SharpPlanar.Bernstein40.N1_left.t21_contains line 977
  443. def OAI.SharpPlanar.Bernstein40.N1_left.t22 line 979
  444. lemma OAI.SharpPlanar.Bernstein40.N1_left.t22_contains line 980
  445. def OAI.SharpPlanar.Bernstein40.N1_left.t23 line 982
  446. lemma OAI.SharpPlanar.Bernstein40.N1_left.t23_contains line 983
  447. def OAI.SharpPlanar.Bernstein40.N1_left.t24 line 985
  448. lemma OAI.SharpPlanar.Bernstein40.N1_left.t24_contains line 986
  449. def OAI.SharpPlanar.Bernstein40.N1_left.t25 line 988
  450. lemma OAI.SharpPlanar.Bernstein40.N1_left.t25_contains line 989
  451. def OAI.SharpPlanar.Bernstein40.N1_left.t26 line 991
  452. lemma OAI.SharpPlanar.Bernstein40.N1_left.t26_contains line 992
  453. def OAI.SharpPlanar.Bernstein40.N1_left.t27 line 994
  454. lemma OAI.SharpPlanar.Bernstein40.N1_left.t27_contains line 995
  455. def OAI.SharpPlanar.Bernstein40.N1_left.t28 line 997
  456. lemma OAI.SharpPlanar.Bernstein40.N1_left.t28_contains line 998
  457. def OAI.SharpPlanar.Bernstein40.N1_left.ts line 1000
  458. lemma OAI.SharpPlanar.Bernstein40.N1_left.ts_contains line 1001
  459. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound0 line 1032
  460. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound1 line 1034
  461. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound2 line 1036
  462. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound3 line 1038
  463. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound4 line 1040
  464. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound5 line 1042
  465. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound6 line 1044
  466. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound7 line 1046
  467. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound8 line 1048
  468. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound9 line 1050
  469. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound10 line 1052
  470. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound11 line 1054
  471. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound12 line 1056
  472. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound13 line 1058
  473. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound14 line 1060
  474. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound15 line 1062
  475. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound16 line 1064
  476. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound17 line 1066
  477. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound18 line 1068
  478. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound19 line 1070
  479. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound20 line 1072
  480. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound21 line 1074
  481. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound22 line 1076
  482. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound23 line 1078
  483. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound24 line 1080
  484. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound25 line 1082
  485. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound26 line 1084
  486. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound27 line 1086
  487. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound28 line 1088
  488. lemma OAI.SharpPlanar.Bernstein40.N1_left.bound line 1090