OAI/Analysis/PlanarPacking/Certificate/Bernstein28.lean

GitHub source file

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