OAI/Analysis/PlanarPacking/Certificate/TableMoments48.lean

GitHub source file

864 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.CachedData.tm0_48_0.chunk line 18
  2. def OAI.SharpPlanar.CachedData.tm0_48_0.s0_0 line 19
  3. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c0_0 line 20
  4. def OAI.SharpPlanar.CachedData.tm0_48_0.s0_1 line 21
  5. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c0_1 line 22
  6. def OAI.SharpPlanar.CachedData.tm0_48_0.s0_2 line 23
  7. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c0_2 line 24
  8. def OAI.SharpPlanar.CachedData.tm0_48_0.s0_3 line 25
  9. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c0_3 line 26
  10. def OAI.SharpPlanar.CachedData.tm0_48_0.s0_4 line 27
  11. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c0_4 line 28
  12. def OAI.SharpPlanar.CachedData.tm0_48_0.s0_5 line 29
  13. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c0_5 line 30
  14. def OAI.SharpPlanar.CachedData.tm0_48_0.s0_6 line 31
  15. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c0_6 line 32
  16. def OAI.SharpPlanar.CachedData.tm0_48_0.s0_7 line 33
  17. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c0_7 line 34
  18. def OAI.SharpPlanar.CachedData.tm0_48_0.s0_8 line 35
  19. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c0_8 line 36
  20. def OAI.SharpPlanar.CachedData.tm0_48_0.s0_9 line 37
  21. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c0_9 line 38
  22. def OAI.SharpPlanar.CachedData.tm0_48_0.s0_10 line 39
  23. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c0_10 line 40
  24. def OAI.SharpPlanar.CachedData.tm0_48_0.s0_11 line 41
  25. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c0_11 line 42
  26. def OAI.SharpPlanar.CachedData.tm0_48_0.s0_12 line 43
  27. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c0_12 line 44
  28. def OAI.SharpPlanar.CachedData.tm0_48_0.s0_13 line 45
  29. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c0_13 line 46
  30. def OAI.SharpPlanar.CachedData.tm0_48_0.s0_14 line 47
  31. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c0_14 line 48
  32. def OAI.SharpPlanar.CachedData.tm0_48_0.s0_15 line 49
  33. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c0_15 line 50
  34. def OAI.SharpPlanar.CachedData.tm0_48_0.s0 line 51
  35. lemma OAI.SharpPlanar.CachedData.tm0_48_0.s0_eq line 52
  36. def OAI.SharpPlanar.CachedData.tm0_48_0.s1_0 line 70
  37. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c1_0 line 71
  38. def OAI.SharpPlanar.CachedData.tm0_48_0.s1_1 line 72
  39. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c1_1 line 73
  40. def OAI.SharpPlanar.CachedData.tm0_48_0.s1_2 line 74
  41. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c1_2 line 75
  42. def OAI.SharpPlanar.CachedData.tm0_48_0.s1_3 line 76
  43. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c1_3 line 77
  44. def OAI.SharpPlanar.CachedData.tm0_48_0.s1_4 line 78
  45. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c1_4 line 79
  46. def OAI.SharpPlanar.CachedData.tm0_48_0.s1_5 line 80
  47. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c1_5 line 81
  48. def OAI.SharpPlanar.CachedData.tm0_48_0.s1_6 line 82
  49. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c1_6 line 83
  50. def OAI.SharpPlanar.CachedData.tm0_48_0.s1_7 line 84
  51. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c1_7 line 85
  52. def OAI.SharpPlanar.CachedData.tm0_48_0.s1_8 line 86
  53. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c1_8 line 87
  54. def OAI.SharpPlanar.CachedData.tm0_48_0.s1_9 line 88
  55. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c1_9 line 89
  56. def OAI.SharpPlanar.CachedData.tm0_48_0.s1_10 line 90
  57. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c1_10 line 91
  58. def OAI.SharpPlanar.CachedData.tm0_48_0.s1_11 line 92
  59. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c1_11 line 93
  60. def OAI.SharpPlanar.CachedData.tm0_48_0.s1_12 line 94
  61. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c1_12 line 95
  62. def OAI.SharpPlanar.CachedData.tm0_48_0.s1_13 line 96
  63. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c1_13 line 97
  64. def OAI.SharpPlanar.CachedData.tm0_48_0.s1_14 line 98
  65. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c1_14 line 99
  66. def OAI.SharpPlanar.CachedData.tm0_48_0.s1_15 line 100
  67. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c1_15 line 101
  68. def OAI.SharpPlanar.CachedData.tm0_48_0.s1 line 102
  69. lemma OAI.SharpPlanar.CachedData.tm0_48_0.s1_eq line 103
  70. def OAI.SharpPlanar.CachedData.tm0_48_0.s2_0 line 121
  71. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c2_0 line 122
  72. def OAI.SharpPlanar.CachedData.tm0_48_0.s2_1 line 123
  73. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c2_1 line 124
  74. def OAI.SharpPlanar.CachedData.tm0_48_0.s2_2 line 125
  75. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c2_2 line 126
  76. def OAI.SharpPlanar.CachedData.tm0_48_0.s2_3 line 127
  77. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c2_3 line 128
  78. def OAI.SharpPlanar.CachedData.tm0_48_0.s2_4 line 129
  79. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c2_4 line 130
  80. def OAI.SharpPlanar.CachedData.tm0_48_0.s2_5 line 131
  81. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c2_5 line 132
  82. def OAI.SharpPlanar.CachedData.tm0_48_0.s2_6 line 133
  83. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c2_6 line 134
  84. def OAI.SharpPlanar.CachedData.tm0_48_0.s2_7 line 135
  85. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c2_7 line 136
  86. def OAI.SharpPlanar.CachedData.tm0_48_0.s2_8 line 137
  87. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c2_8 line 138
  88. def OAI.SharpPlanar.CachedData.tm0_48_0.s2_9 line 139
  89. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c2_9 line 140
  90. def OAI.SharpPlanar.CachedData.tm0_48_0.s2_10 line 141
  91. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c2_10 line 142
  92. def OAI.SharpPlanar.CachedData.tm0_48_0.s2_11 line 143
  93. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c2_11 line 144
  94. def OAI.SharpPlanar.CachedData.tm0_48_0.s2_12 line 145
  95. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c2_12 line 146
  96. def OAI.SharpPlanar.CachedData.tm0_48_0.s2_13 line 147
  97. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c2_13 line 148
  98. def OAI.SharpPlanar.CachedData.tm0_48_0.s2_14 line 149
  99. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c2_14 line 150
  100. def OAI.SharpPlanar.CachedData.tm0_48_0.s2_15 line 151
  101. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c2_15 line 152
  102. def OAI.SharpPlanar.CachedData.tm0_48_0.s2 line 153
  103. lemma OAI.SharpPlanar.CachedData.tm0_48_0.s2_eq line 154
  104. def OAI.SharpPlanar.CachedData.tm0_48_0.s3_0 line 172
  105. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c3_0 line 173
  106. def OAI.SharpPlanar.CachedData.tm0_48_0.s3_1 line 174
  107. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c3_1 line 175
  108. def OAI.SharpPlanar.CachedData.tm0_48_0.s3_2 line 176
  109. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c3_2 line 177
  110. def OAI.SharpPlanar.CachedData.tm0_48_0.s3_3 line 178
  111. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c3_3 line 179
  112. def OAI.SharpPlanar.CachedData.tm0_48_0.s3_4 line 180
  113. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c3_4 line 181
  114. def OAI.SharpPlanar.CachedData.tm0_48_0.s3_5 line 182
  115. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c3_5 line 183
  116. def OAI.SharpPlanar.CachedData.tm0_48_0.s3_6 line 184
  117. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c3_6 line 185
  118. def OAI.SharpPlanar.CachedData.tm0_48_0.s3_7 line 186
  119. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c3_7 line 187
  120. def OAI.SharpPlanar.CachedData.tm0_48_0.s3_8 line 188
  121. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c3_8 line 189
  122. def OAI.SharpPlanar.CachedData.tm0_48_0.s3_9 line 190
  123. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c3_9 line 191
  124. def OAI.SharpPlanar.CachedData.tm0_48_0.s3_10 line 192
  125. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c3_10 line 193
  126. def OAI.SharpPlanar.CachedData.tm0_48_0.s3_11 line 194
  127. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c3_11 line 195
  128. def OAI.SharpPlanar.CachedData.tm0_48_0.s3_12 line 196
  129. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c3_12 line 197
  130. def OAI.SharpPlanar.CachedData.tm0_48_0.s3_13 line 198
  131. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c3_13 line 199
  132. def OAI.SharpPlanar.CachedData.tm0_48_0.s3_14 line 200
  133. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c3_14 line 201
  134. def OAI.SharpPlanar.CachedData.tm0_48_0.s3_15 line 202
  135. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c3_15 line 203
  136. def OAI.SharpPlanar.CachedData.tm0_48_0.s3 line 204
  137. lemma OAI.SharpPlanar.CachedData.tm0_48_0.s3_eq line 205
  138. def OAI.SharpPlanar.CachedData.tm0_48_0.s4_0 line 223
  139. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c4_0 line 224
  140. def OAI.SharpPlanar.CachedData.tm0_48_0.s4_1 line 225
  141. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c4_1 line 226
  142. def OAI.SharpPlanar.CachedData.tm0_48_0.s4_2 line 227
  143. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c4_2 line 228
  144. def OAI.SharpPlanar.CachedData.tm0_48_0.s4_3 line 229
  145. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c4_3 line 230
  146. def OAI.SharpPlanar.CachedData.tm0_48_0.s4_4 line 231
  147. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c4_4 line 232
  148. def OAI.SharpPlanar.CachedData.tm0_48_0.s4_5 line 233
  149. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c4_5 line 234
  150. def OAI.SharpPlanar.CachedData.tm0_48_0.s4_6 line 235
  151. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c4_6 line 236
  152. def OAI.SharpPlanar.CachedData.tm0_48_0.s4_7 line 237
  153. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c4_7 line 238
  154. def OAI.SharpPlanar.CachedData.tm0_48_0.s4_8 line 239
  155. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c4_8 line 240
  156. def OAI.SharpPlanar.CachedData.tm0_48_0.s4_9 line 241
  157. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c4_9 line 242
  158. def OAI.SharpPlanar.CachedData.tm0_48_0.s4_10 line 243
  159. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c4_10 line 244
  160. def OAI.SharpPlanar.CachedData.tm0_48_0.s4_11 line 245
  161. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c4_11 line 246
  162. def OAI.SharpPlanar.CachedData.tm0_48_0.s4_12 line 247
  163. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c4_12 line 248
  164. def OAI.SharpPlanar.CachedData.tm0_48_0.s4_13 line 249
  165. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c4_13 line 250
  166. def OAI.SharpPlanar.CachedData.tm0_48_0.s4_14 line 251
  167. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c4_14 line 252
  168. def OAI.SharpPlanar.CachedData.tm0_48_0.s4_15 line 253
  169. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c4_15 line 254
  170. def OAI.SharpPlanar.CachedData.tm0_48_0.s4 line 255
  171. lemma OAI.SharpPlanar.CachedData.tm0_48_0.s4_eq line 256
  172. def OAI.SharpPlanar.CachedData.tm0_48_0.s5_0 line 274
  173. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c5_0 line 275
  174. def OAI.SharpPlanar.CachedData.tm0_48_0.s5_1 line 276
  175. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c5_1 line 277
  176. def OAI.SharpPlanar.CachedData.tm0_48_0.s5_2 line 278
  177. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c5_2 line 279
  178. def OAI.SharpPlanar.CachedData.tm0_48_0.s5_3 line 280
  179. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c5_3 line 281
  180. def OAI.SharpPlanar.CachedData.tm0_48_0.s5_4 line 282
  181. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c5_4 line 283
  182. def OAI.SharpPlanar.CachedData.tm0_48_0.s5_5 line 284
  183. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c5_5 line 285
  184. def OAI.SharpPlanar.CachedData.tm0_48_0.s5_6 line 286
  185. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c5_6 line 287
  186. def OAI.SharpPlanar.CachedData.tm0_48_0.s5_7 line 288
  187. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c5_7 line 289
  188. def OAI.SharpPlanar.CachedData.tm0_48_0.s5_8 line 290
  189. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c5_8 line 291
  190. def OAI.SharpPlanar.CachedData.tm0_48_0.s5_9 line 292
  191. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c5_9 line 293
  192. def OAI.SharpPlanar.CachedData.tm0_48_0.s5_10 line 294
  193. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c5_10 line 295
  194. def OAI.SharpPlanar.CachedData.tm0_48_0.s5_11 line 296
  195. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c5_11 line 297
  196. def OAI.SharpPlanar.CachedData.tm0_48_0.s5_12 line 298
  197. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c5_12 line 299
  198. def OAI.SharpPlanar.CachedData.tm0_48_0.s5_13 line 300
  199. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c5_13 line 301
  200. def OAI.SharpPlanar.CachedData.tm0_48_0.s5_14 line 302
  201. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c5_14 line 303
  202. def OAI.SharpPlanar.CachedData.tm0_48_0.s5_15 line 304
  203. lemma OAI.SharpPlanar.CachedData.tm0_48_0.c5_15 line 305
  204. def OAI.SharpPlanar.CachedData.tm0_48_0.s5 line 306
  205. lemma OAI.SharpPlanar.CachedData.tm0_48_0.s5_eq line 307
  206. def OAI.SharpPlanar.CachedData.tm0_48_0.sums line 325
  207. lemma OAI.SharpPlanar.CachedData.tm0_48_0.sums_eq line 326
  208. def OAI.SharpPlanar.CachedData.tm0_48_0.ans line 334
  209. lemma OAI.SharpPlanar.CachedData.tm0_48_0.checked line 335
  210. lemma OAI.SharpPlanar.CachedData.tm0_48_0.contains line 339
  211. def OAI.SharpPlanar.CachedData.tm0_48_0.atomAnswer line 343
  212. lemma OAI.SharpPlanar.CachedData.tm0_48_0.atomChecked line 344
  213. lemma OAI.SharpPlanar.CachedData.tm0_48_0.atomContains line 345
  214. def OAI.SharpPlanar.CachedData.tm0_48_0.realAnswer line 348
  215. lemma OAI.SharpPlanar.CachedData.tm0_48_0.realChecked line 349
  216. lemma OAI.SharpPlanar.CachedData.tm0_48_0.KContains line 350
  217. def OAI.SharpPlanar.CachedData.tm0_48_1.chunk line 356
  218. def OAI.SharpPlanar.CachedData.tm0_48_1.s0_0 line 357
  219. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c0_0 line 358
  220. def OAI.SharpPlanar.CachedData.tm0_48_1.s0_1 line 359
  221. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c0_1 line 360
  222. def OAI.SharpPlanar.CachedData.tm0_48_1.s0_2 line 361
  223. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c0_2 line 362
  224. def OAI.SharpPlanar.CachedData.tm0_48_1.s0_3 line 363
  225. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c0_3 line 364
  226. def OAI.SharpPlanar.CachedData.tm0_48_1.s0_4 line 365
  227. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c0_4 line 366
  228. def OAI.SharpPlanar.CachedData.tm0_48_1.s0_5 line 367
  229. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c0_5 line 368
  230. def OAI.SharpPlanar.CachedData.tm0_48_1.s0_6 line 369
  231. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c0_6 line 370
  232. def OAI.SharpPlanar.CachedData.tm0_48_1.s0_7 line 371
  233. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c0_7 line 372
  234. def OAI.SharpPlanar.CachedData.tm0_48_1.s0_8 line 373
  235. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c0_8 line 374
  236. def OAI.SharpPlanar.CachedData.tm0_48_1.s0_9 line 375
  237. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c0_9 line 376
  238. def OAI.SharpPlanar.CachedData.tm0_48_1.s0_10 line 377
  239. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c0_10 line 378
  240. def OAI.SharpPlanar.CachedData.tm0_48_1.s0_11 line 379
  241. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c0_11 line 380
  242. def OAI.SharpPlanar.CachedData.tm0_48_1.s0_12 line 381
  243. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c0_12 line 382
  244. def OAI.SharpPlanar.CachedData.tm0_48_1.s0_13 line 383
  245. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c0_13 line 384
  246. def OAI.SharpPlanar.CachedData.tm0_48_1.s0_14 line 385
  247. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c0_14 line 386
  248. def OAI.SharpPlanar.CachedData.tm0_48_1.s0_15 line 387
  249. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c0_15 line 388
  250. def OAI.SharpPlanar.CachedData.tm0_48_1.s0 line 389
  251. lemma OAI.SharpPlanar.CachedData.tm0_48_1.s0_eq line 390
  252. def OAI.SharpPlanar.CachedData.tm0_48_1.s1_0 line 408
  253. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c1_0 line 409
  254. def OAI.SharpPlanar.CachedData.tm0_48_1.s1_1 line 410
  255. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c1_1 line 411
  256. def OAI.SharpPlanar.CachedData.tm0_48_1.s1_2 line 412
  257. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c1_2 line 413
  258. def OAI.SharpPlanar.CachedData.tm0_48_1.s1_3 line 414
  259. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c1_3 line 415
  260. def OAI.SharpPlanar.CachedData.tm0_48_1.s1_4 line 416
  261. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c1_4 line 417
  262. def OAI.SharpPlanar.CachedData.tm0_48_1.s1_5 line 418
  263. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c1_5 line 419
  264. def OAI.SharpPlanar.CachedData.tm0_48_1.s1_6 line 420
  265. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c1_6 line 421
  266. def OAI.SharpPlanar.CachedData.tm0_48_1.s1_7 line 422
  267. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c1_7 line 423
  268. def OAI.SharpPlanar.CachedData.tm0_48_1.s1_8 line 424
  269. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c1_8 line 425
  270. def OAI.SharpPlanar.CachedData.tm0_48_1.s1_9 line 426
  271. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c1_9 line 427
  272. def OAI.SharpPlanar.CachedData.tm0_48_1.s1_10 line 428
  273. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c1_10 line 429
  274. def OAI.SharpPlanar.CachedData.tm0_48_1.s1_11 line 430
  275. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c1_11 line 431
  276. def OAI.SharpPlanar.CachedData.tm0_48_1.s1_12 line 432
  277. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c1_12 line 433
  278. def OAI.SharpPlanar.CachedData.tm0_48_1.s1_13 line 434
  279. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c1_13 line 435
  280. def OAI.SharpPlanar.CachedData.tm0_48_1.s1_14 line 436
  281. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c1_14 line 437
  282. def OAI.SharpPlanar.CachedData.tm0_48_1.s1_15 line 438
  283. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c1_15 line 439
  284. def OAI.SharpPlanar.CachedData.tm0_48_1.s1 line 440
  285. lemma OAI.SharpPlanar.CachedData.tm0_48_1.s1_eq line 441
  286. def OAI.SharpPlanar.CachedData.tm0_48_1.s2_0 line 459
  287. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c2_0 line 460
  288. def OAI.SharpPlanar.CachedData.tm0_48_1.s2_1 line 461
  289. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c2_1 line 462
  290. def OAI.SharpPlanar.CachedData.tm0_48_1.s2_2 line 463
  291. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c2_2 line 464
  292. def OAI.SharpPlanar.CachedData.tm0_48_1.s2_3 line 465
  293. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c2_3 line 466
  294. def OAI.SharpPlanar.CachedData.tm0_48_1.s2_4 line 467
  295. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c2_4 line 468
  296. def OAI.SharpPlanar.CachedData.tm0_48_1.s2_5 line 469
  297. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c2_5 line 470
  298. def OAI.SharpPlanar.CachedData.tm0_48_1.s2_6 line 471
  299. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c2_6 line 472
  300. def OAI.SharpPlanar.CachedData.tm0_48_1.s2_7 line 473
  301. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c2_7 line 474
  302. def OAI.SharpPlanar.CachedData.tm0_48_1.s2_8 line 475
  303. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c2_8 line 476
  304. def OAI.SharpPlanar.CachedData.tm0_48_1.s2_9 line 477
  305. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c2_9 line 478
  306. def OAI.SharpPlanar.CachedData.tm0_48_1.s2_10 line 479
  307. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c2_10 line 480
  308. def OAI.SharpPlanar.CachedData.tm0_48_1.s2_11 line 481
  309. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c2_11 line 482
  310. def OAI.SharpPlanar.CachedData.tm0_48_1.s2_12 line 483
  311. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c2_12 line 484
  312. def OAI.SharpPlanar.CachedData.tm0_48_1.s2_13 line 485
  313. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c2_13 line 486
  314. def OAI.SharpPlanar.CachedData.tm0_48_1.s2_14 line 487
  315. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c2_14 line 488
  316. def OAI.SharpPlanar.CachedData.tm0_48_1.s2_15 line 489
  317. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c2_15 line 490
  318. def OAI.SharpPlanar.CachedData.tm0_48_1.s2 line 491
  319. lemma OAI.SharpPlanar.CachedData.tm0_48_1.s2_eq line 492
  320. def OAI.SharpPlanar.CachedData.tm0_48_1.s3_0 line 510
  321. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c3_0 line 511
  322. def OAI.SharpPlanar.CachedData.tm0_48_1.s3_1 line 512
  323. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c3_1 line 513
  324. def OAI.SharpPlanar.CachedData.tm0_48_1.s3_2 line 514
  325. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c3_2 line 515
  326. def OAI.SharpPlanar.CachedData.tm0_48_1.s3_3 line 516
  327. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c3_3 line 517
  328. def OAI.SharpPlanar.CachedData.tm0_48_1.s3_4 line 518
  329. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c3_4 line 519
  330. def OAI.SharpPlanar.CachedData.tm0_48_1.s3_5 line 520
  331. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c3_5 line 521
  332. def OAI.SharpPlanar.CachedData.tm0_48_1.s3_6 line 522
  333. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c3_6 line 523
  334. def OAI.SharpPlanar.CachedData.tm0_48_1.s3_7 line 524
  335. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c3_7 line 525
  336. def OAI.SharpPlanar.CachedData.tm0_48_1.s3_8 line 526
  337. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c3_8 line 527
  338. def OAI.SharpPlanar.CachedData.tm0_48_1.s3_9 line 528
  339. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c3_9 line 529
  340. def OAI.SharpPlanar.CachedData.tm0_48_1.s3_10 line 530
  341. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c3_10 line 531
  342. def OAI.SharpPlanar.CachedData.tm0_48_1.s3_11 line 532
  343. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c3_11 line 533
  344. def OAI.SharpPlanar.CachedData.tm0_48_1.s3_12 line 534
  345. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c3_12 line 535
  346. def OAI.SharpPlanar.CachedData.tm0_48_1.s3_13 line 536
  347. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c3_13 line 537
  348. def OAI.SharpPlanar.CachedData.tm0_48_1.s3_14 line 538
  349. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c3_14 line 539
  350. def OAI.SharpPlanar.CachedData.tm0_48_1.s3_15 line 540
  351. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c3_15 line 541
  352. def OAI.SharpPlanar.CachedData.tm0_48_1.s3 line 542
  353. lemma OAI.SharpPlanar.CachedData.tm0_48_1.s3_eq line 543
  354. def OAI.SharpPlanar.CachedData.tm0_48_1.s4_0 line 561
  355. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c4_0 line 562
  356. def OAI.SharpPlanar.CachedData.tm0_48_1.s4_1 line 563
  357. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c4_1 line 564
  358. def OAI.SharpPlanar.CachedData.tm0_48_1.s4_2 line 565
  359. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c4_2 line 566
  360. def OAI.SharpPlanar.CachedData.tm0_48_1.s4_3 line 567
  361. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c4_3 line 568
  362. def OAI.SharpPlanar.CachedData.tm0_48_1.s4_4 line 569
  363. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c4_4 line 570
  364. def OAI.SharpPlanar.CachedData.tm0_48_1.s4_5 line 571
  365. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c4_5 line 572
  366. def OAI.SharpPlanar.CachedData.tm0_48_1.s4_6 line 573
  367. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c4_6 line 574
  368. def OAI.SharpPlanar.CachedData.tm0_48_1.s4_7 line 575
  369. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c4_7 line 576
  370. def OAI.SharpPlanar.CachedData.tm0_48_1.s4_8 line 577
  371. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c4_8 line 578
  372. def OAI.SharpPlanar.CachedData.tm0_48_1.s4_9 line 579
  373. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c4_9 line 580
  374. def OAI.SharpPlanar.CachedData.tm0_48_1.s4_10 line 581
  375. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c4_10 line 582
  376. def OAI.SharpPlanar.CachedData.tm0_48_1.s4_11 line 583
  377. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c4_11 line 584
  378. def OAI.SharpPlanar.CachedData.tm0_48_1.s4_12 line 585
  379. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c4_12 line 586
  380. def OAI.SharpPlanar.CachedData.tm0_48_1.s4_13 line 587
  381. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c4_13 line 588
  382. def OAI.SharpPlanar.CachedData.tm0_48_1.s4_14 line 589
  383. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c4_14 line 590
  384. def OAI.SharpPlanar.CachedData.tm0_48_1.s4_15 line 591
  385. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c4_15 line 592
  386. def OAI.SharpPlanar.CachedData.tm0_48_1.s4 line 593
  387. lemma OAI.SharpPlanar.CachedData.tm0_48_1.s4_eq line 594
  388. def OAI.SharpPlanar.CachedData.tm0_48_1.s5_0 line 612
  389. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c5_0 line 613
  390. def OAI.SharpPlanar.CachedData.tm0_48_1.s5_1 line 614
  391. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c5_1 line 615
  392. def OAI.SharpPlanar.CachedData.tm0_48_1.s5_2 line 616
  393. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c5_2 line 617
  394. def OAI.SharpPlanar.CachedData.tm0_48_1.s5_3 line 618
  395. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c5_3 line 619
  396. def OAI.SharpPlanar.CachedData.tm0_48_1.s5_4 line 620
  397. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c5_4 line 621
  398. def OAI.SharpPlanar.CachedData.tm0_48_1.s5_5 line 622
  399. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c5_5 line 623
  400. def OAI.SharpPlanar.CachedData.tm0_48_1.s5_6 line 624
  401. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c5_6 line 625
  402. def OAI.SharpPlanar.CachedData.tm0_48_1.s5_7 line 626
  403. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c5_7 line 627
  404. def OAI.SharpPlanar.CachedData.tm0_48_1.s5_8 line 628
  405. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c5_8 line 629
  406. def OAI.SharpPlanar.CachedData.tm0_48_1.s5_9 line 630
  407. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c5_9 line 631
  408. def OAI.SharpPlanar.CachedData.tm0_48_1.s5_10 line 632
  409. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c5_10 line 633
  410. def OAI.SharpPlanar.CachedData.tm0_48_1.s5_11 line 634
  411. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c5_11 line 635
  412. def OAI.SharpPlanar.CachedData.tm0_48_1.s5_12 line 636
  413. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c5_12 line 637
  414. def OAI.SharpPlanar.CachedData.tm0_48_1.s5_13 line 638
  415. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c5_13 line 639
  416. def OAI.SharpPlanar.CachedData.tm0_48_1.s5_14 line 640
  417. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c5_14 line 641
  418. def OAI.SharpPlanar.CachedData.tm0_48_1.s5_15 line 642
  419. lemma OAI.SharpPlanar.CachedData.tm0_48_1.c5_15 line 643
  420. def OAI.SharpPlanar.CachedData.tm0_48_1.s5 line 644
  421. lemma OAI.SharpPlanar.CachedData.tm0_48_1.s5_eq line 645
  422. def OAI.SharpPlanar.CachedData.tm0_48_1.sums line 663
  423. lemma OAI.SharpPlanar.CachedData.tm0_48_1.sums_eq line 664
  424. def OAI.SharpPlanar.CachedData.tm0_48_1.ans line 672
  425. lemma OAI.SharpPlanar.CachedData.tm0_48_1.checked line 673
  426. lemma OAI.SharpPlanar.CachedData.tm0_48_1.contains line 677
  427. def OAI.SharpPlanar.CachedData.tm0_48_1.atomAnswer line 681
  428. lemma OAI.SharpPlanar.CachedData.tm0_48_1.atomChecked line 682
  429. lemma OAI.SharpPlanar.CachedData.tm0_48_1.atomContains line 683
  430. def OAI.SharpPlanar.CachedData.tm0_48_1.realAnswer line 686
  431. lemma OAI.SharpPlanar.CachedData.tm0_48_1.realChecked line 687
  432. lemma OAI.SharpPlanar.CachedData.tm0_48_1.KContains line 688
  433. def OAI.SharpPlanar.CachedData.tm1_48_0.chunk line 694
  434. def OAI.SharpPlanar.CachedData.tm1_48_0.s0_0 line 695
  435. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c0_0 line 696
  436. def OAI.SharpPlanar.CachedData.tm1_48_0.s0_1 line 697
  437. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c0_1 line 698
  438. def OAI.SharpPlanar.CachedData.tm1_48_0.s0_2 line 699
  439. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c0_2 line 700
  440. def OAI.SharpPlanar.CachedData.tm1_48_0.s0_3 line 701
  441. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c0_3 line 702
  442. def OAI.SharpPlanar.CachedData.tm1_48_0.s0_4 line 703
  443. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c0_4 line 704
  444. def OAI.SharpPlanar.CachedData.tm1_48_0.s0_5 line 705
  445. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c0_5 line 706
  446. def OAI.SharpPlanar.CachedData.tm1_48_0.s0_6 line 707
  447. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c0_6 line 708
  448. def OAI.SharpPlanar.CachedData.tm1_48_0.s0_7 line 709
  449. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c0_7 line 710
  450. def OAI.SharpPlanar.CachedData.tm1_48_0.s0_8 line 711
  451. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c0_8 line 712
  452. def OAI.SharpPlanar.CachedData.tm1_48_0.s0_9 line 713
  453. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c0_9 line 714
  454. def OAI.SharpPlanar.CachedData.tm1_48_0.s0_10 line 715
  455. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c0_10 line 716
  456. def OAI.SharpPlanar.CachedData.tm1_48_0.s0_11 line 717
  457. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c0_11 line 718
  458. def OAI.SharpPlanar.CachedData.tm1_48_0.s0_12 line 719
  459. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c0_12 line 720
  460. def OAI.SharpPlanar.CachedData.tm1_48_0.s0_13 line 721
  461. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c0_13 line 722
  462. def OAI.SharpPlanar.CachedData.tm1_48_0.s0_14 line 723
  463. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c0_14 line 724
  464. def OAI.SharpPlanar.CachedData.tm1_48_0.s0_15 line 725
  465. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c0_15 line 726
  466. def OAI.SharpPlanar.CachedData.tm1_48_0.s0 line 727
  467. lemma OAI.SharpPlanar.CachedData.tm1_48_0.s0_eq line 728
  468. def OAI.SharpPlanar.CachedData.tm1_48_0.s1_0 line 746
  469. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c1_0 line 747
  470. def OAI.SharpPlanar.CachedData.tm1_48_0.s1_1 line 748
  471. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c1_1 line 749
  472. def OAI.SharpPlanar.CachedData.tm1_48_0.s1_2 line 750
  473. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c1_2 line 751
  474. def OAI.SharpPlanar.CachedData.tm1_48_0.s1_3 line 752
  475. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c1_3 line 753
  476. def OAI.SharpPlanar.CachedData.tm1_48_0.s1_4 line 754
  477. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c1_4 line 755
  478. def OAI.SharpPlanar.CachedData.tm1_48_0.s1_5 line 756
  479. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c1_5 line 757
  480. def OAI.SharpPlanar.CachedData.tm1_48_0.s1_6 line 758
  481. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c1_6 line 759
  482. def OAI.SharpPlanar.CachedData.tm1_48_0.s1_7 line 760
  483. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c1_7 line 761
  484. def OAI.SharpPlanar.CachedData.tm1_48_0.s1_8 line 762
  485. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c1_8 line 763
  486. def OAI.SharpPlanar.CachedData.tm1_48_0.s1_9 line 764
  487. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c1_9 line 765
  488. def OAI.SharpPlanar.CachedData.tm1_48_0.s1_10 line 766
  489. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c1_10 line 767
  490. def OAI.SharpPlanar.CachedData.tm1_48_0.s1_11 line 768
  491. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c1_11 line 769
  492. def OAI.SharpPlanar.CachedData.tm1_48_0.s1_12 line 770
  493. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c1_12 line 771
  494. def OAI.SharpPlanar.CachedData.tm1_48_0.s1_13 line 772
  495. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c1_13 line 773
  496. def OAI.SharpPlanar.CachedData.tm1_48_0.s1_14 line 774
  497. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c1_14 line 775
  498. def OAI.SharpPlanar.CachedData.tm1_48_0.s1_15 line 776
  499. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c1_15 line 777
  500. def OAI.SharpPlanar.CachedData.tm1_48_0.s1 line 778
  501. lemma OAI.SharpPlanar.CachedData.tm1_48_0.s1_eq line 779
  502. def OAI.SharpPlanar.CachedData.tm1_48_0.s2_0 line 797
  503. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c2_0 line 798
  504. def OAI.SharpPlanar.CachedData.tm1_48_0.s2_1 line 799
  505. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c2_1 line 800
  506. def OAI.SharpPlanar.CachedData.tm1_48_0.s2_2 line 801
  507. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c2_2 line 802
  508. def OAI.SharpPlanar.CachedData.tm1_48_0.s2_3 line 803
  509. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c2_3 line 804
  510. def OAI.SharpPlanar.CachedData.tm1_48_0.s2_4 line 805
  511. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c2_4 line 806
  512. def OAI.SharpPlanar.CachedData.tm1_48_0.s2_5 line 807
  513. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c2_5 line 808
  514. def OAI.SharpPlanar.CachedData.tm1_48_0.s2_6 line 809
  515. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c2_6 line 810
  516. def OAI.SharpPlanar.CachedData.tm1_48_0.s2_7 line 811
  517. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c2_7 line 812
  518. def OAI.SharpPlanar.CachedData.tm1_48_0.s2_8 line 813
  519. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c2_8 line 814
  520. def OAI.SharpPlanar.CachedData.tm1_48_0.s2_9 line 815
  521. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c2_9 line 816
  522. def OAI.SharpPlanar.CachedData.tm1_48_0.s2_10 line 817
  523. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c2_10 line 818
  524. def OAI.SharpPlanar.CachedData.tm1_48_0.s2_11 line 819
  525. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c2_11 line 820
  526. def OAI.SharpPlanar.CachedData.tm1_48_0.s2_12 line 821
  527. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c2_12 line 822
  528. def OAI.SharpPlanar.CachedData.tm1_48_0.s2_13 line 823
  529. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c2_13 line 824
  530. def OAI.SharpPlanar.CachedData.tm1_48_0.s2_14 line 825
  531. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c2_14 line 826
  532. def OAI.SharpPlanar.CachedData.tm1_48_0.s2_15 line 827
  533. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c2_15 line 828
  534. def OAI.SharpPlanar.CachedData.tm1_48_0.s2 line 829
  535. lemma OAI.SharpPlanar.CachedData.tm1_48_0.s2_eq line 830
  536. def OAI.SharpPlanar.CachedData.tm1_48_0.s3_0 line 848
  537. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c3_0 line 849
  538. def OAI.SharpPlanar.CachedData.tm1_48_0.s3_1 line 850
  539. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c3_1 line 851
  540. def OAI.SharpPlanar.CachedData.tm1_48_0.s3_2 line 852
  541. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c3_2 line 853
  542. def OAI.SharpPlanar.CachedData.tm1_48_0.s3_3 line 854
  543. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c3_3 line 855
  544. def OAI.SharpPlanar.CachedData.tm1_48_0.s3_4 line 856
  545. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c3_4 line 857
  546. def OAI.SharpPlanar.CachedData.tm1_48_0.s3_5 line 858
  547. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c3_5 line 859
  548. def OAI.SharpPlanar.CachedData.tm1_48_0.s3_6 line 860
  549. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c3_6 line 861
  550. def OAI.SharpPlanar.CachedData.tm1_48_0.s3_7 line 862
  551. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c3_7 line 863
  552. def OAI.SharpPlanar.CachedData.tm1_48_0.s3_8 line 864
  553. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c3_8 line 865
  554. def OAI.SharpPlanar.CachedData.tm1_48_0.s3_9 line 866
  555. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c3_9 line 867
  556. def OAI.SharpPlanar.CachedData.tm1_48_0.s3_10 line 868
  557. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c3_10 line 869
  558. def OAI.SharpPlanar.CachedData.tm1_48_0.s3_11 line 870
  559. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c3_11 line 871
  560. def OAI.SharpPlanar.CachedData.tm1_48_0.s3_12 line 872
  561. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c3_12 line 873
  562. def OAI.SharpPlanar.CachedData.tm1_48_0.s3_13 line 874
  563. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c3_13 line 875
  564. def OAI.SharpPlanar.CachedData.tm1_48_0.s3_14 line 876
  565. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c3_14 line 877
  566. def OAI.SharpPlanar.CachedData.tm1_48_0.s3_15 line 878
  567. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c3_15 line 879
  568. def OAI.SharpPlanar.CachedData.tm1_48_0.s3 line 880
  569. lemma OAI.SharpPlanar.CachedData.tm1_48_0.s3_eq line 881
  570. def OAI.SharpPlanar.CachedData.tm1_48_0.s4_0 line 899
  571. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c4_0 line 900
  572. def OAI.SharpPlanar.CachedData.tm1_48_0.s4_1 line 901
  573. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c4_1 line 902
  574. def OAI.SharpPlanar.CachedData.tm1_48_0.s4_2 line 903
  575. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c4_2 line 904
  576. def OAI.SharpPlanar.CachedData.tm1_48_0.s4_3 line 905
  577. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c4_3 line 906
  578. def OAI.SharpPlanar.CachedData.tm1_48_0.s4_4 line 907
  579. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c4_4 line 908
  580. def OAI.SharpPlanar.CachedData.tm1_48_0.s4_5 line 909
  581. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c4_5 line 910
  582. def OAI.SharpPlanar.CachedData.tm1_48_0.s4_6 line 911
  583. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c4_6 line 912
  584. def OAI.SharpPlanar.CachedData.tm1_48_0.s4_7 line 913
  585. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c4_7 line 914
  586. def OAI.SharpPlanar.CachedData.tm1_48_0.s4_8 line 915
  587. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c4_8 line 916
  588. def OAI.SharpPlanar.CachedData.tm1_48_0.s4_9 line 917
  589. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c4_9 line 918
  590. def OAI.SharpPlanar.CachedData.tm1_48_0.s4_10 line 919
  591. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c4_10 line 920
  592. def OAI.SharpPlanar.CachedData.tm1_48_0.s4_11 line 921
  593. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c4_11 line 922
  594. def OAI.SharpPlanar.CachedData.tm1_48_0.s4_12 line 923
  595. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c4_12 line 924
  596. def OAI.SharpPlanar.CachedData.tm1_48_0.s4_13 line 925
  597. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c4_13 line 926
  598. def OAI.SharpPlanar.CachedData.tm1_48_0.s4_14 line 927
  599. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c4_14 line 928
  600. def OAI.SharpPlanar.CachedData.tm1_48_0.s4_15 line 929
  601. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c4_15 line 930
  602. def OAI.SharpPlanar.CachedData.tm1_48_0.s4 line 931
  603. lemma OAI.SharpPlanar.CachedData.tm1_48_0.s4_eq line 932
  604. def OAI.SharpPlanar.CachedData.tm1_48_0.s5_0 line 950
  605. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c5_0 line 951
  606. def OAI.SharpPlanar.CachedData.tm1_48_0.s5_1 line 952
  607. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c5_1 line 953
  608. def OAI.SharpPlanar.CachedData.tm1_48_0.s5_2 line 954
  609. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c5_2 line 955
  610. def OAI.SharpPlanar.CachedData.tm1_48_0.s5_3 line 956
  611. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c5_3 line 957
  612. def OAI.SharpPlanar.CachedData.tm1_48_0.s5_4 line 958
  613. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c5_4 line 959
  614. def OAI.SharpPlanar.CachedData.tm1_48_0.s5_5 line 960
  615. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c5_5 line 961
  616. def OAI.SharpPlanar.CachedData.tm1_48_0.s5_6 line 962
  617. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c5_6 line 963
  618. def OAI.SharpPlanar.CachedData.tm1_48_0.s5_7 line 964
  619. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c5_7 line 965
  620. def OAI.SharpPlanar.CachedData.tm1_48_0.s5_8 line 966
  621. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c5_8 line 967
  622. def OAI.SharpPlanar.CachedData.tm1_48_0.s5_9 line 968
  623. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c5_9 line 969
  624. def OAI.SharpPlanar.CachedData.tm1_48_0.s5_10 line 970
  625. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c5_10 line 971
  626. def OAI.SharpPlanar.CachedData.tm1_48_0.s5_11 line 972
  627. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c5_11 line 973
  628. def OAI.SharpPlanar.CachedData.tm1_48_0.s5_12 line 974
  629. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c5_12 line 975
  630. def OAI.SharpPlanar.CachedData.tm1_48_0.s5_13 line 976
  631. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c5_13 line 977
  632. def OAI.SharpPlanar.CachedData.tm1_48_0.s5_14 line 978
  633. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c5_14 line 979
  634. def OAI.SharpPlanar.CachedData.tm1_48_0.s5_15 line 980
  635. lemma OAI.SharpPlanar.CachedData.tm1_48_0.c5_15 line 981
  636. def OAI.SharpPlanar.CachedData.tm1_48_0.s5 line 982
  637. lemma OAI.SharpPlanar.CachedData.tm1_48_0.s5_eq line 983
  638. def OAI.SharpPlanar.CachedData.tm1_48_0.sums line 1001
  639. lemma OAI.SharpPlanar.CachedData.tm1_48_0.sums_eq line 1002
  640. def OAI.SharpPlanar.CachedData.tm1_48_0.ans line 1010
  641. lemma OAI.SharpPlanar.CachedData.tm1_48_0.checked line 1011
  642. lemma OAI.SharpPlanar.CachedData.tm1_48_0.contains line 1015
  643. def OAI.SharpPlanar.CachedData.tm1_48_0.atomAnswer line 1019
  644. lemma OAI.SharpPlanar.CachedData.tm1_48_0.atomChecked line 1020
  645. lemma OAI.SharpPlanar.CachedData.tm1_48_0.atomContains line 1021
  646. def OAI.SharpPlanar.CachedData.tm1_48_0.realAnswer line 1024
  647. lemma OAI.SharpPlanar.CachedData.tm1_48_0.realChecked line 1025
  648. lemma OAI.SharpPlanar.CachedData.tm1_48_0.KContains line 1026
  649. def OAI.SharpPlanar.CachedData.tm1_48_1.chunk line 1032
  650. def OAI.SharpPlanar.CachedData.tm1_48_1.s0_0 line 1033
  651. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c0_0 line 1034
  652. def OAI.SharpPlanar.CachedData.tm1_48_1.s0_1 line 1035
  653. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c0_1 line 1036
  654. def OAI.SharpPlanar.CachedData.tm1_48_1.s0_2 line 1037
  655. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c0_2 line 1038
  656. def OAI.SharpPlanar.CachedData.tm1_48_1.s0_3 line 1039
  657. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c0_3 line 1040
  658. def OAI.SharpPlanar.CachedData.tm1_48_1.s0_4 line 1041
  659. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c0_4 line 1042
  660. def OAI.SharpPlanar.CachedData.tm1_48_1.s0_5 line 1043
  661. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c0_5 line 1044
  662. def OAI.SharpPlanar.CachedData.tm1_48_1.s0_6 line 1045
  663. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c0_6 line 1046
  664. def OAI.SharpPlanar.CachedData.tm1_48_1.s0_7 line 1047
  665. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c0_7 line 1048
  666. def OAI.SharpPlanar.CachedData.tm1_48_1.s0_8 line 1049
  667. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c0_8 line 1050
  668. def OAI.SharpPlanar.CachedData.tm1_48_1.s0_9 line 1051
  669. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c0_9 line 1052
  670. def OAI.SharpPlanar.CachedData.tm1_48_1.s0_10 line 1053
  671. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c0_10 line 1054
  672. def OAI.SharpPlanar.CachedData.tm1_48_1.s0_11 line 1055
  673. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c0_11 line 1056
  674. def OAI.SharpPlanar.CachedData.tm1_48_1.s0_12 line 1057
  675. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c0_12 line 1058
  676. def OAI.SharpPlanar.CachedData.tm1_48_1.s0_13 line 1059
  677. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c0_13 line 1060
  678. def OAI.SharpPlanar.CachedData.tm1_48_1.s0_14 line 1061
  679. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c0_14 line 1062
  680. def OAI.SharpPlanar.CachedData.tm1_48_1.s0_15 line 1063
  681. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c0_15 line 1064
  682. def OAI.SharpPlanar.CachedData.tm1_48_1.s0 line 1065
  683. lemma OAI.SharpPlanar.CachedData.tm1_48_1.s0_eq line 1066
  684. def OAI.SharpPlanar.CachedData.tm1_48_1.s1_0 line 1084
  685. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c1_0 line 1085
  686. def OAI.SharpPlanar.CachedData.tm1_48_1.s1_1 line 1086
  687. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c1_1 line 1087
  688. def OAI.SharpPlanar.CachedData.tm1_48_1.s1_2 line 1088
  689. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c1_2 line 1089
  690. def OAI.SharpPlanar.CachedData.tm1_48_1.s1_3 line 1090
  691. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c1_3 line 1091
  692. def OAI.SharpPlanar.CachedData.tm1_48_1.s1_4 line 1092
  693. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c1_4 line 1093
  694. def OAI.SharpPlanar.CachedData.tm1_48_1.s1_5 line 1094
  695. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c1_5 line 1095
  696. def OAI.SharpPlanar.CachedData.tm1_48_1.s1_6 line 1096
  697. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c1_6 line 1097
  698. def OAI.SharpPlanar.CachedData.tm1_48_1.s1_7 line 1098
  699. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c1_7 line 1099
  700. def OAI.SharpPlanar.CachedData.tm1_48_1.s1_8 line 1100
  701. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c1_8 line 1101
  702. def OAI.SharpPlanar.CachedData.tm1_48_1.s1_9 line 1102
  703. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c1_9 line 1103
  704. def OAI.SharpPlanar.CachedData.tm1_48_1.s1_10 line 1104
  705. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c1_10 line 1105
  706. def OAI.SharpPlanar.CachedData.tm1_48_1.s1_11 line 1106
  707. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c1_11 line 1107
  708. def OAI.SharpPlanar.CachedData.tm1_48_1.s1_12 line 1108
  709. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c1_12 line 1109
  710. def OAI.SharpPlanar.CachedData.tm1_48_1.s1_13 line 1110
  711. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c1_13 line 1111
  712. def OAI.SharpPlanar.CachedData.tm1_48_1.s1_14 line 1112
  713. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c1_14 line 1113
  714. def OAI.SharpPlanar.CachedData.tm1_48_1.s1_15 line 1114
  715. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c1_15 line 1115
  716. def OAI.SharpPlanar.CachedData.tm1_48_1.s1 line 1116
  717. lemma OAI.SharpPlanar.CachedData.tm1_48_1.s1_eq line 1117
  718. def OAI.SharpPlanar.CachedData.tm1_48_1.s2_0 line 1135
  719. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c2_0 line 1136
  720. def OAI.SharpPlanar.CachedData.tm1_48_1.s2_1 line 1137
  721. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c2_1 line 1138
  722. def OAI.SharpPlanar.CachedData.tm1_48_1.s2_2 line 1139
  723. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c2_2 line 1140
  724. def OAI.SharpPlanar.CachedData.tm1_48_1.s2_3 line 1141
  725. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c2_3 line 1142
  726. def OAI.SharpPlanar.CachedData.tm1_48_1.s2_4 line 1143
  727. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c2_4 line 1144
  728. def OAI.SharpPlanar.CachedData.tm1_48_1.s2_5 line 1145
  729. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c2_5 line 1146
  730. def OAI.SharpPlanar.CachedData.tm1_48_1.s2_6 line 1147
  731. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c2_6 line 1148
  732. def OAI.SharpPlanar.CachedData.tm1_48_1.s2_7 line 1149
  733. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c2_7 line 1150
  734. def OAI.SharpPlanar.CachedData.tm1_48_1.s2_8 line 1151
  735. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c2_8 line 1152
  736. def OAI.SharpPlanar.CachedData.tm1_48_1.s2_9 line 1153
  737. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c2_9 line 1154
  738. def OAI.SharpPlanar.CachedData.tm1_48_1.s2_10 line 1155
  739. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c2_10 line 1156
  740. def OAI.SharpPlanar.CachedData.tm1_48_1.s2_11 line 1157
  741. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c2_11 line 1158
  742. def OAI.SharpPlanar.CachedData.tm1_48_1.s2_12 line 1159
  743. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c2_12 line 1160
  744. def OAI.SharpPlanar.CachedData.tm1_48_1.s2_13 line 1161
  745. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c2_13 line 1162
  746. def OAI.SharpPlanar.CachedData.tm1_48_1.s2_14 line 1163
  747. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c2_14 line 1164
  748. def OAI.SharpPlanar.CachedData.tm1_48_1.s2_15 line 1165
  749. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c2_15 line 1166
  750. def OAI.SharpPlanar.CachedData.tm1_48_1.s2 line 1167
  751. lemma OAI.SharpPlanar.CachedData.tm1_48_1.s2_eq line 1168
  752. def OAI.SharpPlanar.CachedData.tm1_48_1.s3_0 line 1186
  753. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c3_0 line 1187
  754. def OAI.SharpPlanar.CachedData.tm1_48_1.s3_1 line 1188
  755. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c3_1 line 1189
  756. def OAI.SharpPlanar.CachedData.tm1_48_1.s3_2 line 1190
  757. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c3_2 line 1191
  758. def OAI.SharpPlanar.CachedData.tm1_48_1.s3_3 line 1192
  759. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c3_3 line 1193
  760. def OAI.SharpPlanar.CachedData.tm1_48_1.s3_4 line 1194
  761. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c3_4 line 1195
  762. def OAI.SharpPlanar.CachedData.tm1_48_1.s3_5 line 1196
  763. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c3_5 line 1197
  764. def OAI.SharpPlanar.CachedData.tm1_48_1.s3_6 line 1198
  765. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c3_6 line 1199
  766. def OAI.SharpPlanar.CachedData.tm1_48_1.s3_7 line 1200
  767. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c3_7 line 1201
  768. def OAI.SharpPlanar.CachedData.tm1_48_1.s3_8 line 1202
  769. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c3_8 line 1203
  770. def OAI.SharpPlanar.CachedData.tm1_48_1.s3_9 line 1204
  771. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c3_9 line 1205
  772. def OAI.SharpPlanar.CachedData.tm1_48_1.s3_10 line 1206
  773. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c3_10 line 1207
  774. def OAI.SharpPlanar.CachedData.tm1_48_1.s3_11 line 1208
  775. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c3_11 line 1209
  776. def OAI.SharpPlanar.CachedData.tm1_48_1.s3_12 line 1210
  777. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c3_12 line 1211
  778. def OAI.SharpPlanar.CachedData.tm1_48_1.s3_13 line 1212
  779. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c3_13 line 1213
  780. def OAI.SharpPlanar.CachedData.tm1_48_1.s3_14 line 1214
  781. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c3_14 line 1215
  782. def OAI.SharpPlanar.CachedData.tm1_48_1.s3_15 line 1216
  783. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c3_15 line 1217
  784. def OAI.SharpPlanar.CachedData.tm1_48_1.s3 line 1218
  785. lemma OAI.SharpPlanar.CachedData.tm1_48_1.s3_eq line 1219
  786. def OAI.SharpPlanar.CachedData.tm1_48_1.s4_0 line 1237
  787. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c4_0 line 1238
  788. def OAI.SharpPlanar.CachedData.tm1_48_1.s4_1 line 1239
  789. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c4_1 line 1240
  790. def OAI.SharpPlanar.CachedData.tm1_48_1.s4_2 line 1241
  791. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c4_2 line 1242
  792. def OAI.SharpPlanar.CachedData.tm1_48_1.s4_3 line 1243
  793. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c4_3 line 1244
  794. def OAI.SharpPlanar.CachedData.tm1_48_1.s4_4 line 1245
  795. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c4_4 line 1246
  796. def OAI.SharpPlanar.CachedData.tm1_48_1.s4_5 line 1247
  797. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c4_5 line 1248
  798. def OAI.SharpPlanar.CachedData.tm1_48_1.s4_6 line 1249
  799. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c4_6 line 1250
  800. def OAI.SharpPlanar.CachedData.tm1_48_1.s4_7 line 1251
  801. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c4_7 line 1252
  802. def OAI.SharpPlanar.CachedData.tm1_48_1.s4_8 line 1253
  803. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c4_8 line 1254
  804. def OAI.SharpPlanar.CachedData.tm1_48_1.s4_9 line 1255
  805. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c4_9 line 1256
  806. def OAI.SharpPlanar.CachedData.tm1_48_1.s4_10 line 1257
  807. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c4_10 line 1258
  808. def OAI.SharpPlanar.CachedData.tm1_48_1.s4_11 line 1259
  809. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c4_11 line 1260
  810. def OAI.SharpPlanar.CachedData.tm1_48_1.s4_12 line 1261
  811. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c4_12 line 1262
  812. def OAI.SharpPlanar.CachedData.tm1_48_1.s4_13 line 1263
  813. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c4_13 line 1264
  814. def OAI.SharpPlanar.CachedData.tm1_48_1.s4_14 line 1265
  815. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c4_14 line 1266
  816. def OAI.SharpPlanar.CachedData.tm1_48_1.s4_15 line 1267
  817. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c4_15 line 1268
  818. def OAI.SharpPlanar.CachedData.tm1_48_1.s4 line 1269
  819. lemma OAI.SharpPlanar.CachedData.tm1_48_1.s4_eq line 1270
  820. def OAI.SharpPlanar.CachedData.tm1_48_1.s5_0 line 1288
  821. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c5_0 line 1289
  822. def OAI.SharpPlanar.CachedData.tm1_48_1.s5_1 line 1290
  823. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c5_1 line 1291
  824. def OAI.SharpPlanar.CachedData.tm1_48_1.s5_2 line 1292
  825. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c5_2 line 1293
  826. def OAI.SharpPlanar.CachedData.tm1_48_1.s5_3 line 1294
  827. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c5_3 line 1295
  828. def OAI.SharpPlanar.CachedData.tm1_48_1.s5_4 line 1296
  829. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c5_4 line 1297
  830. def OAI.SharpPlanar.CachedData.tm1_48_1.s5_5 line 1298
  831. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c5_5 line 1299
  832. def OAI.SharpPlanar.CachedData.tm1_48_1.s5_6 line 1300
  833. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c5_6 line 1301
  834. def OAI.SharpPlanar.CachedData.tm1_48_1.s5_7 line 1302
  835. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c5_7 line 1303
  836. def OAI.SharpPlanar.CachedData.tm1_48_1.s5_8 line 1304
  837. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c5_8 line 1305
  838. def OAI.SharpPlanar.CachedData.tm1_48_1.s5_9 line 1306
  839. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c5_9 line 1307
  840. def OAI.SharpPlanar.CachedData.tm1_48_1.s5_10 line 1308
  841. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c5_10 line 1309
  842. def OAI.SharpPlanar.CachedData.tm1_48_1.s5_11 line 1310
  843. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c5_11 line 1311
  844. def OAI.SharpPlanar.CachedData.tm1_48_1.s5_12 line 1312
  845. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c5_12 line 1313
  846. def OAI.SharpPlanar.CachedData.tm1_48_1.s5_13 line 1314
  847. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c5_13 line 1315
  848. def OAI.SharpPlanar.CachedData.tm1_48_1.s5_14 line 1316
  849. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c5_14 line 1317
  850. def OAI.SharpPlanar.CachedData.tm1_48_1.s5_15 line 1318
  851. lemma OAI.SharpPlanar.CachedData.tm1_48_1.c5_15 line 1319
  852. def OAI.SharpPlanar.CachedData.tm1_48_1.s5 line 1320
  853. lemma OAI.SharpPlanar.CachedData.tm1_48_1.s5_eq line 1321
  854. def OAI.SharpPlanar.CachedData.tm1_48_1.sums line 1339
  855. lemma OAI.SharpPlanar.CachedData.tm1_48_1.sums_eq line 1340
  856. def OAI.SharpPlanar.CachedData.tm1_48_1.ans line 1348
  857. lemma OAI.SharpPlanar.CachedData.tm1_48_1.checked line 1349
  858. lemma OAI.SharpPlanar.CachedData.tm1_48_1.contains line 1353
  859. def OAI.SharpPlanar.CachedData.tm1_48_1.atomAnswer line 1357
  860. lemma OAI.SharpPlanar.CachedData.tm1_48_1.atomChecked line 1358
  861. lemma OAI.SharpPlanar.CachedData.tm1_48_1.atomContains line 1359
  862. def OAI.SharpPlanar.CachedData.tm1_48_1.realAnswer line 1362
  863. lemma OAI.SharpPlanar.CachedData.tm1_48_1.realChecked line 1363
  864. lemma OAI.SharpPlanar.CachedData.tm1_48_1.KContains line 1364