OAI/Analysis/PlanarPacking/Certificate/Bernstein27.lean

GitHub source file

428 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.Bernstein27.N0_right.t0 line 20
  2. lemma OAI.SharpPlanar.Bernstein27.N0_right.t0_checked line 21
  3. lemma OAI.SharpPlanar.Bernstein27.N0_right.t0_contains line 22
  4. def OAI.SharpPlanar.Bernstein27.N0_right.t1 line 26
  5. lemma OAI.SharpPlanar.Bernstein27.N0_right.t1_checked line 27
  6. lemma OAI.SharpPlanar.Bernstein27.N0_right.t1_contains line 28
  7. def OAI.SharpPlanar.Bernstein27.N0_right.t2 line 32
  8. lemma OAI.SharpPlanar.Bernstein27.N0_right.t2_checked line 33
  9. lemma OAI.SharpPlanar.Bernstein27.N0_right.t2_contains line 34
  10. def OAI.SharpPlanar.Bernstein27.N0_right.t3 line 38
  11. lemma OAI.SharpPlanar.Bernstein27.N0_right.t3_checked line 39
  12. lemma OAI.SharpPlanar.Bernstein27.N0_right.t3_contains line 40
  13. def OAI.SharpPlanar.Bernstein27.N0_right.t4 line 44
  14. lemma OAI.SharpPlanar.Bernstein27.N0_right.t4_checked line 45
  15. lemma OAI.SharpPlanar.Bernstein27.N0_right.t4_contains line 46
  16. def OAI.SharpPlanar.Bernstein27.N0_right.t5 line 50
  17. lemma OAI.SharpPlanar.Bernstein27.N0_right.t5_checked line 51
  18. lemma OAI.SharpPlanar.Bernstein27.N0_right.t5_contains line 52
  19. def OAI.SharpPlanar.Bernstein27.N0_right.t6 line 56
  20. lemma OAI.SharpPlanar.Bernstein27.N0_right.t6_checked line 57
  21. lemma OAI.SharpPlanar.Bernstein27.N0_right.t6_contains line 58
  22. def OAI.SharpPlanar.Bernstein27.N0_right.t7 line 62
  23. lemma OAI.SharpPlanar.Bernstein27.N0_right.t7_checked line 63
  24. lemma OAI.SharpPlanar.Bernstein27.N0_right.t7_contains line 64
  25. def OAI.SharpPlanar.Bernstein27.N0_right.tr8 line 68
  26. lemma OAI.SharpPlanar.Bernstein27.N0_right.tr8_contains line 69
  27. def OAI.SharpPlanar.Bernstein27.N0_right.t8 line 71
  28. lemma OAI.SharpPlanar.Bernstein27.N0_right.t8_checked line 72
  29. lemma OAI.SharpPlanar.Bernstein27.N0_right.t8_contains line 73
  30. def OAI.SharpPlanar.Bernstein27.N0_right.tr9 line 77
  31. lemma OAI.SharpPlanar.Bernstein27.N0_right.tr9_contains line 78
  32. def OAI.SharpPlanar.Bernstein27.N0_right.t9 line 80
  33. lemma OAI.SharpPlanar.Bernstein27.N0_right.t9_checked line 81
  34. lemma OAI.SharpPlanar.Bernstein27.N0_right.t9_contains line 82
  35. def OAI.SharpPlanar.Bernstein27.N0_right.tr10 line 86
  36. lemma OAI.SharpPlanar.Bernstein27.N0_right.tr10_contains line 87
  37. def OAI.SharpPlanar.Bernstein27.N0_right.t10 line 89
  38. lemma OAI.SharpPlanar.Bernstein27.N0_right.t10_checked line 90
  39. lemma OAI.SharpPlanar.Bernstein27.N0_right.t10_contains line 91
  40. def OAI.SharpPlanar.Bernstein27.N0_right.t11 line 95
  41. lemma OAI.SharpPlanar.Bernstein27.N0_right.t11_contains line 96
  42. def OAI.SharpPlanar.Bernstein27.N0_right.t12 line 98
  43. lemma OAI.SharpPlanar.Bernstein27.N0_right.t12_contains line 99
  44. def OAI.SharpPlanar.Bernstein27.N0_right.t13 line 101
  45. lemma OAI.SharpPlanar.Bernstein27.N0_right.t13_contains line 102
  46. def OAI.SharpPlanar.Bernstein27.N0_right.t14 line 104
  47. lemma OAI.SharpPlanar.Bernstein27.N0_right.t14_contains line 105
  48. def OAI.SharpPlanar.Bernstein27.N0_right.t15 line 107
  49. lemma OAI.SharpPlanar.Bernstein27.N0_right.t15_contains line 108
  50. def OAI.SharpPlanar.Bernstein27.N0_right.t16 line 110
  51. lemma OAI.SharpPlanar.Bernstein27.N0_right.t16_contains line 111
  52. def OAI.SharpPlanar.Bernstein27.N0_right.t17 line 113
  53. lemma OAI.SharpPlanar.Bernstein27.N0_right.t17_contains line 114
  54. def OAI.SharpPlanar.Bernstein27.N0_right.t18 line 116
  55. lemma OAI.SharpPlanar.Bernstein27.N0_right.t18_contains line 117
  56. def OAI.SharpPlanar.Bernstein27.N0_right.t19 line 119
  57. lemma OAI.SharpPlanar.Bernstein27.N0_right.t19_contains line 120
  58. def OAI.SharpPlanar.Bernstein27.N0_right.t20 line 122
  59. lemma OAI.SharpPlanar.Bernstein27.N0_right.t20_contains line 123
  60. def OAI.SharpPlanar.Bernstein27.N0_right.t21 line 125
  61. lemma OAI.SharpPlanar.Bernstein27.N0_right.t21_contains line 126
  62. def OAI.SharpPlanar.Bernstein27.N0_right.t22 line 128
  63. lemma OAI.SharpPlanar.Bernstein27.N0_right.t22_contains line 129
  64. def OAI.SharpPlanar.Bernstein27.N0_right.t23 line 131
  65. lemma OAI.SharpPlanar.Bernstein27.N0_right.t23_contains line 132
  66. def OAI.SharpPlanar.Bernstein27.N0_right.t24 line 134
  67. lemma OAI.SharpPlanar.Bernstein27.N0_right.t24_contains line 135
  68. def OAI.SharpPlanar.Bernstein27.N0_right.t25 line 137
  69. lemma OAI.SharpPlanar.Bernstein27.N0_right.t25_contains line 138
  70. def OAI.SharpPlanar.Bernstein27.N0_right.t26 line 140
  71. lemma OAI.SharpPlanar.Bernstein27.N0_right.t26_contains line 141
  72. def OAI.SharpPlanar.Bernstein27.N0_right.t27 line 143
  73. lemma OAI.SharpPlanar.Bernstein27.N0_right.t27_contains line 144
  74. def OAI.SharpPlanar.Bernstein27.N0_right.t28 line 146
  75. lemma OAI.SharpPlanar.Bernstein27.N0_right.t28_contains line 147
  76. def OAI.SharpPlanar.Bernstein27.N0_right.ts line 149
  77. lemma OAI.SharpPlanar.Bernstein27.N0_right.ts_contains line 150
  78. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound0 line 181
  79. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound1 line 183
  80. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound2 line 185
  81. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound3 line 187
  82. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound4 line 189
  83. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound5 line 191
  84. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound6 line 193
  85. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound7 line 195
  86. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound8 line 197
  87. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound9 line 199
  88. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound10 line 201
  89. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound11 line 203
  90. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound12 line 205
  91. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound13 line 207
  92. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound14 line 209
  93. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound15 line 211
  94. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound16 line 213
  95. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound17 line 215
  96. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound18 line 217
  97. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound19 line 219
  98. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound20 line 221
  99. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound21 line 223
  100. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound22 line 225
  101. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound23 line 227
  102. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound24 line 229
  103. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound25 line 231
  104. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound26 line 233
  105. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound27 line 235
  106. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound28 line 237
  107. lemma OAI.SharpPlanar.Bernstein27.N0_right.bound line 239
  108. def OAI.SharpPlanar.Bernstein27.N1_right.t0 line 272
  109. lemma OAI.SharpPlanar.Bernstein27.N1_right.t0_checked line 273
  110. lemma OAI.SharpPlanar.Bernstein27.N1_right.t0_contains line 274
  111. def OAI.SharpPlanar.Bernstein27.N1_right.t1 line 278
  112. lemma OAI.SharpPlanar.Bernstein27.N1_right.t1_checked line 279
  113. lemma OAI.SharpPlanar.Bernstein27.N1_right.t1_contains line 280
  114. def OAI.SharpPlanar.Bernstein27.N1_right.t2 line 284
  115. lemma OAI.SharpPlanar.Bernstein27.N1_right.t2_checked line 285
  116. lemma OAI.SharpPlanar.Bernstein27.N1_right.t2_contains line 286
  117. def OAI.SharpPlanar.Bernstein27.N1_right.t3 line 290
  118. lemma OAI.SharpPlanar.Bernstein27.N1_right.t3_checked line 291
  119. lemma OAI.SharpPlanar.Bernstein27.N1_right.t3_contains line 292
  120. def OAI.SharpPlanar.Bernstein27.N1_right.t4 line 296
  121. lemma OAI.SharpPlanar.Bernstein27.N1_right.t4_checked line 297
  122. lemma OAI.SharpPlanar.Bernstein27.N1_right.t4_contains line 298
  123. def OAI.SharpPlanar.Bernstein27.N1_right.t5 line 302
  124. lemma OAI.SharpPlanar.Bernstein27.N1_right.t5_checked line 303
  125. lemma OAI.SharpPlanar.Bernstein27.N1_right.t5_contains line 304
  126. def OAI.SharpPlanar.Bernstein27.N1_right.t6 line 308
  127. lemma OAI.SharpPlanar.Bernstein27.N1_right.t6_checked line 309
  128. lemma OAI.SharpPlanar.Bernstein27.N1_right.t6_contains line 310
  129. def OAI.SharpPlanar.Bernstein27.N1_right.t7 line 314
  130. lemma OAI.SharpPlanar.Bernstein27.N1_right.t7_checked line 315
  131. lemma OAI.SharpPlanar.Bernstein27.N1_right.t7_contains line 316
  132. def OAI.SharpPlanar.Bernstein27.N1_right.tr8 line 320
  133. lemma OAI.SharpPlanar.Bernstein27.N1_right.tr8_contains line 321
  134. def OAI.SharpPlanar.Bernstein27.N1_right.t8 line 323
  135. lemma OAI.SharpPlanar.Bernstein27.N1_right.t8_checked line 324
  136. lemma OAI.SharpPlanar.Bernstein27.N1_right.t8_contains line 325
  137. def OAI.SharpPlanar.Bernstein27.N1_right.tr9 line 329
  138. lemma OAI.SharpPlanar.Bernstein27.N1_right.tr9_contains line 330
  139. def OAI.SharpPlanar.Bernstein27.N1_right.t9 line 332
  140. lemma OAI.SharpPlanar.Bernstein27.N1_right.t9_checked line 333
  141. lemma OAI.SharpPlanar.Bernstein27.N1_right.t9_contains line 334
  142. def OAI.SharpPlanar.Bernstein27.N1_right.tr10 line 338
  143. lemma OAI.SharpPlanar.Bernstein27.N1_right.tr10_contains line 339
  144. def OAI.SharpPlanar.Bernstein27.N1_right.t10 line 341
  145. lemma OAI.SharpPlanar.Bernstein27.N1_right.t10_checked line 342
  146. lemma OAI.SharpPlanar.Bernstein27.N1_right.t10_contains line 343
  147. def OAI.SharpPlanar.Bernstein27.N1_right.t11 line 347
  148. lemma OAI.SharpPlanar.Bernstein27.N1_right.t11_contains line 348
  149. def OAI.SharpPlanar.Bernstein27.N1_right.t12 line 350
  150. lemma OAI.SharpPlanar.Bernstein27.N1_right.t12_contains line 351
  151. def OAI.SharpPlanar.Bernstein27.N1_right.t13 line 353
  152. lemma OAI.SharpPlanar.Bernstein27.N1_right.t13_contains line 354
  153. def OAI.SharpPlanar.Bernstein27.N1_right.t14 line 356
  154. lemma OAI.SharpPlanar.Bernstein27.N1_right.t14_contains line 357
  155. def OAI.SharpPlanar.Bernstein27.N1_right.t15 line 359
  156. lemma OAI.SharpPlanar.Bernstein27.N1_right.t15_contains line 360
  157. def OAI.SharpPlanar.Bernstein27.N1_right.t16 line 362
  158. lemma OAI.SharpPlanar.Bernstein27.N1_right.t16_contains line 363
  159. def OAI.SharpPlanar.Bernstein27.N1_right.t17 line 365
  160. lemma OAI.SharpPlanar.Bernstein27.N1_right.t17_contains line 366
  161. def OAI.SharpPlanar.Bernstein27.N1_right.t18 line 368
  162. lemma OAI.SharpPlanar.Bernstein27.N1_right.t18_contains line 369
  163. def OAI.SharpPlanar.Bernstein27.N1_right.t19 line 371
  164. lemma OAI.SharpPlanar.Bernstein27.N1_right.t19_contains line 372
  165. def OAI.SharpPlanar.Bernstein27.N1_right.t20 line 374
  166. lemma OAI.SharpPlanar.Bernstein27.N1_right.t20_contains line 375
  167. def OAI.SharpPlanar.Bernstein27.N1_right.t21 line 377
  168. lemma OAI.SharpPlanar.Bernstein27.N1_right.t21_contains line 378
  169. def OAI.SharpPlanar.Bernstein27.N1_right.t22 line 380
  170. lemma OAI.SharpPlanar.Bernstein27.N1_right.t22_contains line 381
  171. def OAI.SharpPlanar.Bernstein27.N1_right.t23 line 383
  172. lemma OAI.SharpPlanar.Bernstein27.N1_right.t23_contains line 384
  173. def OAI.SharpPlanar.Bernstein27.N1_right.t24 line 386
  174. lemma OAI.SharpPlanar.Bernstein27.N1_right.t24_contains line 387
  175. def OAI.SharpPlanar.Bernstein27.N1_right.t25 line 389
  176. lemma OAI.SharpPlanar.Bernstein27.N1_right.t25_contains line 390
  177. def OAI.SharpPlanar.Bernstein27.N1_right.t26 line 392
  178. lemma OAI.SharpPlanar.Bernstein27.N1_right.t26_contains line 393
  179. def OAI.SharpPlanar.Bernstein27.N1_right.t27 line 395
  180. lemma OAI.SharpPlanar.Bernstein27.N1_right.t27_contains line 396
  181. def OAI.SharpPlanar.Bernstein27.N1_right.t28 line 398
  182. lemma OAI.SharpPlanar.Bernstein27.N1_right.t28_contains line 399
  183. def OAI.SharpPlanar.Bernstein27.N1_right.ts line 401
  184. lemma OAI.SharpPlanar.Bernstein27.N1_right.ts_contains line 402
  185. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound0 line 433
  186. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound1 line 435
  187. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound2 line 437
  188. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound3 line 439
  189. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound4 line 441
  190. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound5 line 443
  191. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound6 line 445
  192. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound7 line 447
  193. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound8 line 449
  194. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound9 line 451
  195. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound10 line 453
  196. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound11 line 455
  197. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound12 line 457
  198. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound13 line 459
  199. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound14 line 461
  200. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound15 line 463
  201. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound16 line 465
  202. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound17 line 467
  203. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound18 line 469
  204. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound19 line 471
  205. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound20 line 473
  206. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound21 line 475
  207. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound22 line 477
  208. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound23 line 479
  209. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound24 line 481
  210. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound25 line 483
  211. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound26 line 485
  212. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound27 line 487
  213. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound28 line 489
  214. lemma OAI.SharpPlanar.Bernstein27.N1_right.bound line 491
  215. def OAI.SharpPlanar.Bernstein27.N0_left.t0 line 524
  216. lemma OAI.SharpPlanar.Bernstein27.N0_left.t0_checked line 525
  217. lemma OAI.SharpPlanar.Bernstein27.N0_left.t0_contains line 526
  218. def OAI.SharpPlanar.Bernstein27.N0_left.t1 line 530
  219. lemma OAI.SharpPlanar.Bernstein27.N0_left.t1_checked line 531
  220. lemma OAI.SharpPlanar.Bernstein27.N0_left.t1_contains line 532
  221. def OAI.SharpPlanar.Bernstein27.N0_left.t2 line 536
  222. lemma OAI.SharpPlanar.Bernstein27.N0_left.t2_checked line 537
  223. lemma OAI.SharpPlanar.Bernstein27.N0_left.t2_contains line 538
  224. def OAI.SharpPlanar.Bernstein27.N0_left.t3 line 542
  225. lemma OAI.SharpPlanar.Bernstein27.N0_left.t3_checked line 543
  226. lemma OAI.SharpPlanar.Bernstein27.N0_left.t3_contains line 544
  227. def OAI.SharpPlanar.Bernstein27.N0_left.t4 line 548
  228. lemma OAI.SharpPlanar.Bernstein27.N0_left.t4_checked line 549
  229. lemma OAI.SharpPlanar.Bernstein27.N0_left.t4_contains line 550
  230. def OAI.SharpPlanar.Bernstein27.N0_left.t5 line 554
  231. lemma OAI.SharpPlanar.Bernstein27.N0_left.t5_checked line 555
  232. lemma OAI.SharpPlanar.Bernstein27.N0_left.t5_contains line 556
  233. def OAI.SharpPlanar.Bernstein27.N0_left.t6 line 560
  234. lemma OAI.SharpPlanar.Bernstein27.N0_left.t6_checked line 561
  235. lemma OAI.SharpPlanar.Bernstein27.N0_left.t6_contains line 562
  236. def OAI.SharpPlanar.Bernstein27.N0_left.t7 line 566
  237. lemma OAI.SharpPlanar.Bernstein27.N0_left.t7_checked line 567
  238. lemma OAI.SharpPlanar.Bernstein27.N0_left.t7_contains line 568
  239. def OAI.SharpPlanar.Bernstein27.N0_left.tr8 line 572
  240. lemma OAI.SharpPlanar.Bernstein27.N0_left.tr8_contains line 573
  241. def OAI.SharpPlanar.Bernstein27.N0_left.t8 line 575
  242. lemma OAI.SharpPlanar.Bernstein27.N0_left.t8_checked line 576
  243. lemma OAI.SharpPlanar.Bernstein27.N0_left.t8_contains line 577
  244. def OAI.SharpPlanar.Bernstein27.N0_left.tr9 line 581
  245. lemma OAI.SharpPlanar.Bernstein27.N0_left.tr9_contains line 582
  246. def OAI.SharpPlanar.Bernstein27.N0_left.t9 line 584
  247. lemma OAI.SharpPlanar.Bernstein27.N0_left.t9_checked line 585
  248. lemma OAI.SharpPlanar.Bernstein27.N0_left.t9_contains line 586
  249. def OAI.SharpPlanar.Bernstein27.N0_left.tr10 line 590
  250. lemma OAI.SharpPlanar.Bernstein27.N0_left.tr10_contains line 591
  251. def OAI.SharpPlanar.Bernstein27.N0_left.t10 line 593
  252. lemma OAI.SharpPlanar.Bernstein27.N0_left.t10_checked line 594
  253. lemma OAI.SharpPlanar.Bernstein27.N0_left.t10_contains line 595
  254. def OAI.SharpPlanar.Bernstein27.N0_left.t11 line 599
  255. lemma OAI.SharpPlanar.Bernstein27.N0_left.t11_contains line 600
  256. def OAI.SharpPlanar.Bernstein27.N0_left.t12 line 602
  257. lemma OAI.SharpPlanar.Bernstein27.N0_left.t12_contains line 603
  258. def OAI.SharpPlanar.Bernstein27.N0_left.t13 line 605
  259. lemma OAI.SharpPlanar.Bernstein27.N0_left.t13_contains line 606
  260. def OAI.SharpPlanar.Bernstein27.N0_left.t14 line 608
  261. lemma OAI.SharpPlanar.Bernstein27.N0_left.t14_contains line 609
  262. def OAI.SharpPlanar.Bernstein27.N0_left.t15 line 611
  263. lemma OAI.SharpPlanar.Bernstein27.N0_left.t15_contains line 612
  264. def OAI.SharpPlanar.Bernstein27.N0_left.t16 line 614
  265. lemma OAI.SharpPlanar.Bernstein27.N0_left.t16_contains line 615
  266. def OAI.SharpPlanar.Bernstein27.N0_left.t17 line 617
  267. lemma OAI.SharpPlanar.Bernstein27.N0_left.t17_contains line 618
  268. def OAI.SharpPlanar.Bernstein27.N0_left.t18 line 620
  269. lemma OAI.SharpPlanar.Bernstein27.N0_left.t18_contains line 621
  270. def OAI.SharpPlanar.Bernstein27.N0_left.t19 line 623
  271. lemma OAI.SharpPlanar.Bernstein27.N0_left.t19_contains line 624
  272. def OAI.SharpPlanar.Bernstein27.N0_left.t20 line 626
  273. lemma OAI.SharpPlanar.Bernstein27.N0_left.t20_contains line 627
  274. def OAI.SharpPlanar.Bernstein27.N0_left.t21 line 629
  275. lemma OAI.SharpPlanar.Bernstein27.N0_left.t21_contains line 630
  276. def OAI.SharpPlanar.Bernstein27.N0_left.t22 line 632
  277. lemma OAI.SharpPlanar.Bernstein27.N0_left.t22_contains line 633
  278. def OAI.SharpPlanar.Bernstein27.N0_left.t23 line 635
  279. lemma OAI.SharpPlanar.Bernstein27.N0_left.t23_contains line 636
  280. def OAI.SharpPlanar.Bernstein27.N0_left.t24 line 638
  281. lemma OAI.SharpPlanar.Bernstein27.N0_left.t24_contains line 639
  282. def OAI.SharpPlanar.Bernstein27.N0_left.t25 line 641
  283. lemma OAI.SharpPlanar.Bernstein27.N0_left.t25_contains line 642
  284. def OAI.SharpPlanar.Bernstein27.N0_left.t26 line 644
  285. lemma OAI.SharpPlanar.Bernstein27.N0_left.t26_contains line 645
  286. def OAI.SharpPlanar.Bernstein27.N0_left.t27 line 647
  287. lemma OAI.SharpPlanar.Bernstein27.N0_left.t27_contains line 648
  288. def OAI.SharpPlanar.Bernstein27.N0_left.t28 line 650
  289. lemma OAI.SharpPlanar.Bernstein27.N0_left.t28_contains line 651
  290. def OAI.SharpPlanar.Bernstein27.N0_left.ts line 653
  291. lemma OAI.SharpPlanar.Bernstein27.N0_left.ts_contains line 654
  292. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound0 line 685
  293. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound1 line 687
  294. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound2 line 689
  295. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound3 line 691
  296. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound4 line 693
  297. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound5 line 695
  298. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound6 line 697
  299. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound7 line 699
  300. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound8 line 701
  301. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound9 line 703
  302. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound10 line 705
  303. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound11 line 707
  304. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound12 line 709
  305. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound13 line 711
  306. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound14 line 713
  307. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound15 line 715
  308. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound16 line 717
  309. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound17 line 719
  310. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound18 line 721
  311. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound19 line 723
  312. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound20 line 725
  313. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound21 line 727
  314. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound22 line 729
  315. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound23 line 731
  316. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound24 line 733
  317. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound25 line 735
  318. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound26 line 737
  319. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound27 line 739
  320. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound28 line 741
  321. lemma OAI.SharpPlanar.Bernstein27.N0_left.bound line 743
  322. def OAI.SharpPlanar.Bernstein27.N1_left.t0 line 776
  323. lemma OAI.SharpPlanar.Bernstein27.N1_left.t0_checked line 777
  324. lemma OAI.SharpPlanar.Bernstein27.N1_left.t0_contains line 778
  325. def OAI.SharpPlanar.Bernstein27.N1_left.t1 line 782
  326. lemma OAI.SharpPlanar.Bernstein27.N1_left.t1_checked line 783
  327. lemma OAI.SharpPlanar.Bernstein27.N1_left.t1_contains line 784
  328. def OAI.SharpPlanar.Bernstein27.N1_left.t2 line 788
  329. lemma OAI.SharpPlanar.Bernstein27.N1_left.t2_checked line 789
  330. lemma OAI.SharpPlanar.Bernstein27.N1_left.t2_contains line 790
  331. def OAI.SharpPlanar.Bernstein27.N1_left.t3 line 794
  332. lemma OAI.SharpPlanar.Bernstein27.N1_left.t3_checked line 795
  333. lemma OAI.SharpPlanar.Bernstein27.N1_left.t3_contains line 796
  334. def OAI.SharpPlanar.Bernstein27.N1_left.t4 line 800
  335. lemma OAI.SharpPlanar.Bernstein27.N1_left.t4_checked line 801
  336. lemma OAI.SharpPlanar.Bernstein27.N1_left.t4_contains line 802
  337. def OAI.SharpPlanar.Bernstein27.N1_left.t5 line 806
  338. lemma OAI.SharpPlanar.Bernstein27.N1_left.t5_checked line 807
  339. lemma OAI.SharpPlanar.Bernstein27.N1_left.t5_contains line 808
  340. def OAI.SharpPlanar.Bernstein27.N1_left.t6 line 812
  341. lemma OAI.SharpPlanar.Bernstein27.N1_left.t6_checked line 813
  342. lemma OAI.SharpPlanar.Bernstein27.N1_left.t6_contains line 814
  343. def OAI.SharpPlanar.Bernstein27.N1_left.t7 line 818
  344. lemma OAI.SharpPlanar.Bernstein27.N1_left.t7_checked line 819
  345. lemma OAI.SharpPlanar.Bernstein27.N1_left.t7_contains line 820
  346. def OAI.SharpPlanar.Bernstein27.N1_left.tr8 line 824
  347. lemma OAI.SharpPlanar.Bernstein27.N1_left.tr8_contains line 825
  348. def OAI.SharpPlanar.Bernstein27.N1_left.t8 line 827
  349. lemma OAI.SharpPlanar.Bernstein27.N1_left.t8_checked line 828
  350. lemma OAI.SharpPlanar.Bernstein27.N1_left.t8_contains line 829
  351. def OAI.SharpPlanar.Bernstein27.N1_left.tr9 line 833
  352. lemma OAI.SharpPlanar.Bernstein27.N1_left.tr9_contains line 834
  353. def OAI.SharpPlanar.Bernstein27.N1_left.t9 line 836
  354. lemma OAI.SharpPlanar.Bernstein27.N1_left.t9_checked line 837
  355. lemma OAI.SharpPlanar.Bernstein27.N1_left.t9_contains line 838
  356. def OAI.SharpPlanar.Bernstein27.N1_left.tr10 line 842
  357. lemma OAI.SharpPlanar.Bernstein27.N1_left.tr10_contains line 843
  358. def OAI.SharpPlanar.Bernstein27.N1_left.t10 line 845
  359. lemma OAI.SharpPlanar.Bernstein27.N1_left.t10_checked line 846
  360. lemma OAI.SharpPlanar.Bernstein27.N1_left.t10_contains line 847
  361. def OAI.SharpPlanar.Bernstein27.N1_left.t11 line 851
  362. lemma OAI.SharpPlanar.Bernstein27.N1_left.t11_contains line 852
  363. def OAI.SharpPlanar.Bernstein27.N1_left.t12 line 854
  364. lemma OAI.SharpPlanar.Bernstein27.N1_left.t12_contains line 855
  365. def OAI.SharpPlanar.Bernstein27.N1_left.t13 line 857
  366. lemma OAI.SharpPlanar.Bernstein27.N1_left.t13_contains line 858
  367. def OAI.SharpPlanar.Bernstein27.N1_left.t14 line 860
  368. lemma OAI.SharpPlanar.Bernstein27.N1_left.t14_contains line 861
  369. def OAI.SharpPlanar.Bernstein27.N1_left.t15 line 863
  370. lemma OAI.SharpPlanar.Bernstein27.N1_left.t15_contains line 864
  371. def OAI.SharpPlanar.Bernstein27.N1_left.t16 line 866
  372. lemma OAI.SharpPlanar.Bernstein27.N1_left.t16_contains line 867
  373. def OAI.SharpPlanar.Bernstein27.N1_left.t17 line 869
  374. lemma OAI.SharpPlanar.Bernstein27.N1_left.t17_contains line 870
  375. def OAI.SharpPlanar.Bernstein27.N1_left.t18 line 872
  376. lemma OAI.SharpPlanar.Bernstein27.N1_left.t18_contains line 873
  377. def OAI.SharpPlanar.Bernstein27.N1_left.t19 line 875
  378. lemma OAI.SharpPlanar.Bernstein27.N1_left.t19_contains line 876
  379. def OAI.SharpPlanar.Bernstein27.N1_left.t20 line 878
  380. lemma OAI.SharpPlanar.Bernstein27.N1_left.t20_contains line 879
  381. def OAI.SharpPlanar.Bernstein27.N1_left.t21 line 881
  382. lemma OAI.SharpPlanar.Bernstein27.N1_left.t21_contains line 882
  383. def OAI.SharpPlanar.Bernstein27.N1_left.t22 line 884
  384. lemma OAI.SharpPlanar.Bernstein27.N1_left.t22_contains line 885
  385. def OAI.SharpPlanar.Bernstein27.N1_left.t23 line 887
  386. lemma OAI.SharpPlanar.Bernstein27.N1_left.t23_contains line 888
  387. def OAI.SharpPlanar.Bernstein27.N1_left.t24 line 890
  388. lemma OAI.SharpPlanar.Bernstein27.N1_left.t24_contains line 891
  389. def OAI.SharpPlanar.Bernstein27.N1_left.t25 line 893
  390. lemma OAI.SharpPlanar.Bernstein27.N1_left.t25_contains line 894
  391. def OAI.SharpPlanar.Bernstein27.N1_left.t26 line 896
  392. lemma OAI.SharpPlanar.Bernstein27.N1_left.t26_contains line 897
  393. def OAI.SharpPlanar.Bernstein27.N1_left.t27 line 899
  394. lemma OAI.SharpPlanar.Bernstein27.N1_left.t27_contains line 900
  395. def OAI.SharpPlanar.Bernstein27.N1_left.t28 line 902
  396. lemma OAI.SharpPlanar.Bernstein27.N1_left.t28_contains line 903
  397. def OAI.SharpPlanar.Bernstein27.N1_left.ts line 905
  398. lemma OAI.SharpPlanar.Bernstein27.N1_left.ts_contains line 906
  399. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound0 line 937
  400. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound1 line 939
  401. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound2 line 941
  402. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound3 line 943
  403. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound4 line 945
  404. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound5 line 947
  405. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound6 line 949
  406. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound7 line 951
  407. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound8 line 953
  408. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound9 line 955
  409. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound10 line 957
  410. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound11 line 959
  411. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound12 line 961
  412. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound13 line 963
  413. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound14 line 965
  414. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound15 line 967
  415. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound16 line 969
  416. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound17 line 971
  417. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound18 line 973
  418. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound19 line 975
  419. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound20 line 977
  420. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound21 line 979
  421. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound22 line 981
  422. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound23 line 983
  423. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound24 line 985
  424. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound25 line 987
  425. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound26 line 989
  426. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound27 line 991
  427. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound28 line 993
  428. lemma OAI.SharpPlanar.Bernstein27.N1_left.bound line 995