OAI/Analysis/PlanarPacking/Certificate/Bernstein36.lean

GitHub source file

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