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