OAI/Analysis/PlanarPacking/Certificate/TransformedPowers40.lean

GitHub source file

2080 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.trans31Expr line 14
  2. def OAI.SharpPlanar.CachedData.trans31_r0_0 line 15
  3. lemma OAI.SharpPlanar.CachedData.trans31_r0_0_eq line 16
  4. def OAI.SharpPlanar.CachedData.trans31_r0_1 line 17
  5. lemma OAI.SharpPlanar.CachedData.trans31_r0_1_eq line 18
  6. def OAI.SharpPlanar.CachedData.trans31_r0_2 line 19
  7. lemma OAI.SharpPlanar.CachedData.trans31_r0_2_eq line 20
  8. def OAI.SharpPlanar.CachedData.trans31_r0_3 line 21
  9. lemma OAI.SharpPlanar.CachedData.trans31_r0_3_eq line 22
  10. def OAI.SharpPlanar.CachedData.trans31_r0_4 line 23
  11. lemma OAI.SharpPlanar.CachedData.trans31_r0_4_eq line 24
  12. def OAI.SharpPlanar.CachedData.trans31_r0_5 line 25
  13. lemma OAI.SharpPlanar.CachedData.trans31_r0_5_eq line 26
  14. def OAI.SharpPlanar.CachedData.trans31_r0_6 line 27
  15. lemma OAI.SharpPlanar.CachedData.trans31_r0_6_eq line 28
  16. def OAI.SharpPlanar.CachedData.trans31_r0_7 line 29
  17. lemma OAI.SharpPlanar.CachedData.trans31_r0_7_eq line 30
  18. def OAI.SharpPlanar.CachedData.trans31_r0_8 line 31
  19. lemma OAI.SharpPlanar.CachedData.trans31_r0_8_eq line 32
  20. def OAI.SharpPlanar.CachedData.trans31_r0_9 line 33
  21. lemma OAI.SharpPlanar.CachedData.trans31_r0_9_eq line 34
  22. def OAI.SharpPlanar.CachedData.trans31_r0_10 line 35
  23. lemma OAI.SharpPlanar.CachedData.trans31_r0_10_eq line 36
  24. def OAI.SharpPlanar.CachedData.trans31_r0_11 line 37
  25. lemma OAI.SharpPlanar.CachedData.trans31_r0_11_eq line 38
  26. def OAI.SharpPlanar.CachedData.trans31_r0_12 line 39
  27. lemma OAI.SharpPlanar.CachedData.trans31_r0_12_eq line 40
  28. def OAI.SharpPlanar.CachedData.trans31_r0_13 line 41
  29. lemma OAI.SharpPlanar.CachedData.trans31_r0_13_eq line 42
  30. def OAI.SharpPlanar.CachedData.trans31_r0_14 line 43
  31. lemma OAI.SharpPlanar.CachedData.trans31_r0_14_eq line 44
  32. def OAI.SharpPlanar.CachedData.trans31_r0_15 line 45
  33. lemma OAI.SharpPlanar.CachedData.trans31_r0_15_eq line 46
  34. def OAI.SharpPlanar.CachedData.trans31_r0 line 47
  35. lemma OAI.SharpPlanar.CachedData.trans31_r0_eq line 48
  36. def OAI.SharpPlanar.CachedData.trans31_r1_0 line 66
  37. lemma OAI.SharpPlanar.CachedData.trans31_r1_0_eq line 67
  38. def OAI.SharpPlanar.CachedData.trans31_r1_1 line 68
  39. lemma OAI.SharpPlanar.CachedData.trans31_r1_1_eq line 69
  40. def OAI.SharpPlanar.CachedData.trans31_r1_2 line 70
  41. lemma OAI.SharpPlanar.CachedData.trans31_r1_2_eq line 71
  42. def OAI.SharpPlanar.CachedData.trans31_r1_3 line 72
  43. lemma OAI.SharpPlanar.CachedData.trans31_r1_3_eq line 73
  44. def OAI.SharpPlanar.CachedData.trans31_r1_4 line 74
  45. lemma OAI.SharpPlanar.CachedData.trans31_r1_4_eq line 75
  46. def OAI.SharpPlanar.CachedData.trans31_r1_5 line 76
  47. lemma OAI.SharpPlanar.CachedData.trans31_r1_5_eq line 77
  48. def OAI.SharpPlanar.CachedData.trans31_r1_6 line 78
  49. lemma OAI.SharpPlanar.CachedData.trans31_r1_6_eq line 79
  50. def OAI.SharpPlanar.CachedData.trans31_r1_7 line 80
  51. lemma OAI.SharpPlanar.CachedData.trans31_r1_7_eq line 81
  52. def OAI.SharpPlanar.CachedData.trans31_r1_8 line 82
  53. lemma OAI.SharpPlanar.CachedData.trans31_r1_8_eq line 83
  54. def OAI.SharpPlanar.CachedData.trans31_r1_9 line 84
  55. lemma OAI.SharpPlanar.CachedData.trans31_r1_9_eq line 85
  56. def OAI.SharpPlanar.CachedData.trans31_r1_10 line 86
  57. lemma OAI.SharpPlanar.CachedData.trans31_r1_10_eq line 87
  58. def OAI.SharpPlanar.CachedData.trans31_r1_11 line 88
  59. lemma OAI.SharpPlanar.CachedData.trans31_r1_11_eq line 89
  60. def OAI.SharpPlanar.CachedData.trans31_r1_12 line 90
  61. lemma OAI.SharpPlanar.CachedData.trans31_r1_12_eq line 91
  62. def OAI.SharpPlanar.CachedData.trans31_r1_13 line 92
  63. lemma OAI.SharpPlanar.CachedData.trans31_r1_13_eq line 93
  64. def OAI.SharpPlanar.CachedData.trans31_r1_14 line 94
  65. lemma OAI.SharpPlanar.CachedData.trans31_r1_14_eq line 95
  66. def OAI.SharpPlanar.CachedData.trans31_r1_15 line 96
  67. lemma OAI.SharpPlanar.CachedData.trans31_r1_15_eq line 97
  68. def OAI.SharpPlanar.CachedData.trans31_r1 line 98
  69. lemma OAI.SharpPlanar.CachedData.trans31_r1_eq line 99
  70. def OAI.SharpPlanar.CachedData.trans31_r2_0 line 117
  71. lemma OAI.SharpPlanar.CachedData.trans31_r2_0_eq line 118
  72. def OAI.SharpPlanar.CachedData.trans31_r2_1 line 119
  73. lemma OAI.SharpPlanar.CachedData.trans31_r2_1_eq line 120
  74. def OAI.SharpPlanar.CachedData.trans31_r2_2 line 121
  75. lemma OAI.SharpPlanar.CachedData.trans31_r2_2_eq line 122
  76. def OAI.SharpPlanar.CachedData.trans31_r2_3 line 123
  77. lemma OAI.SharpPlanar.CachedData.trans31_r2_3_eq line 124
  78. def OAI.SharpPlanar.CachedData.trans31_r2_4 line 125
  79. lemma OAI.SharpPlanar.CachedData.trans31_r2_4_eq line 126
  80. def OAI.SharpPlanar.CachedData.trans31_r2_5 line 127
  81. lemma OAI.SharpPlanar.CachedData.trans31_r2_5_eq line 128
  82. def OAI.SharpPlanar.CachedData.trans31_r2_6 line 129
  83. lemma OAI.SharpPlanar.CachedData.trans31_r2_6_eq line 130
  84. def OAI.SharpPlanar.CachedData.trans31_r2_7 line 131
  85. lemma OAI.SharpPlanar.CachedData.trans31_r2_7_eq line 132
  86. def OAI.SharpPlanar.CachedData.trans31_r2_8 line 133
  87. lemma OAI.SharpPlanar.CachedData.trans31_r2_8_eq line 134
  88. def OAI.SharpPlanar.CachedData.trans31_r2_9 line 135
  89. lemma OAI.SharpPlanar.CachedData.trans31_r2_9_eq line 136
  90. def OAI.SharpPlanar.CachedData.trans31_r2_10 line 137
  91. lemma OAI.SharpPlanar.CachedData.trans31_r2_10_eq line 138
  92. def OAI.SharpPlanar.CachedData.trans31_r2_11 line 139
  93. lemma OAI.SharpPlanar.CachedData.trans31_r2_11_eq line 140
  94. def OAI.SharpPlanar.CachedData.trans31_r2_12 line 141
  95. lemma OAI.SharpPlanar.CachedData.trans31_r2_12_eq line 142
  96. def OAI.SharpPlanar.CachedData.trans31_r2_13 line 143
  97. lemma OAI.SharpPlanar.CachedData.trans31_r2_13_eq line 144
  98. def OAI.SharpPlanar.CachedData.trans31_r2_14 line 145
  99. lemma OAI.SharpPlanar.CachedData.trans31_r2_14_eq line 146
  100. def OAI.SharpPlanar.CachedData.trans31_r2_15 line 147
  101. lemma OAI.SharpPlanar.CachedData.trans31_r2_15_eq line 148
  102. def OAI.SharpPlanar.CachedData.trans31_r2 line 149
  103. lemma OAI.SharpPlanar.CachedData.trans31_r2_eq line 150
  104. def OAI.SharpPlanar.CachedData.trans31_r3_0 line 168
  105. lemma OAI.SharpPlanar.CachedData.trans31_r3_0_eq line 169
  106. def OAI.SharpPlanar.CachedData.trans31_r3_1 line 170
  107. lemma OAI.SharpPlanar.CachedData.trans31_r3_1_eq line 171
  108. def OAI.SharpPlanar.CachedData.trans31_r3_2 line 172
  109. lemma OAI.SharpPlanar.CachedData.trans31_r3_2_eq line 173
  110. def OAI.SharpPlanar.CachedData.trans31_r3_3 line 174
  111. lemma OAI.SharpPlanar.CachedData.trans31_r3_3_eq line 175
  112. def OAI.SharpPlanar.CachedData.trans31_r3_4 line 176
  113. lemma OAI.SharpPlanar.CachedData.trans31_r3_4_eq line 177
  114. def OAI.SharpPlanar.CachedData.trans31_r3_5 line 178
  115. lemma OAI.SharpPlanar.CachedData.trans31_r3_5_eq line 179
  116. def OAI.SharpPlanar.CachedData.trans31_r3_6 line 180
  117. lemma OAI.SharpPlanar.CachedData.trans31_r3_6_eq line 181
  118. def OAI.SharpPlanar.CachedData.trans31_r3_7 line 182
  119. lemma OAI.SharpPlanar.CachedData.trans31_r3_7_eq line 183
  120. def OAI.SharpPlanar.CachedData.trans31_r3_8 line 184
  121. lemma OAI.SharpPlanar.CachedData.trans31_r3_8_eq line 185
  122. def OAI.SharpPlanar.CachedData.trans31_r3_9 line 186
  123. lemma OAI.SharpPlanar.CachedData.trans31_r3_9_eq line 187
  124. def OAI.SharpPlanar.CachedData.trans31_r3_10 line 188
  125. lemma OAI.SharpPlanar.CachedData.trans31_r3_10_eq line 189
  126. def OAI.SharpPlanar.CachedData.trans31_r3_11 line 190
  127. lemma OAI.SharpPlanar.CachedData.trans31_r3_11_eq line 191
  128. def OAI.SharpPlanar.CachedData.trans31_r3_12 line 192
  129. lemma OAI.SharpPlanar.CachedData.trans31_r3_12_eq line 193
  130. def OAI.SharpPlanar.CachedData.trans31_r3_13 line 194
  131. lemma OAI.SharpPlanar.CachedData.trans31_r3_13_eq line 195
  132. def OAI.SharpPlanar.CachedData.trans31_r3_14 line 196
  133. lemma OAI.SharpPlanar.CachedData.trans31_r3_14_eq line 197
  134. def OAI.SharpPlanar.CachedData.trans31_r3_15 line 198
  135. lemma OAI.SharpPlanar.CachedData.trans31_r3_15_eq line 199
  136. def OAI.SharpPlanar.CachedData.trans31_r3 line 200
  137. lemma OAI.SharpPlanar.CachedData.trans31_r3_eq line 201
  138. def OAI.SharpPlanar.CachedData.trans31_r4_0 line 219
  139. lemma OAI.SharpPlanar.CachedData.trans31_r4_0_eq line 220
  140. def OAI.SharpPlanar.CachedData.trans31_r4_1 line 221
  141. lemma OAI.SharpPlanar.CachedData.trans31_r4_1_eq line 222
  142. def OAI.SharpPlanar.CachedData.trans31_r4_2 line 223
  143. lemma OAI.SharpPlanar.CachedData.trans31_r4_2_eq line 224
  144. def OAI.SharpPlanar.CachedData.trans31_r4_3 line 225
  145. lemma OAI.SharpPlanar.CachedData.trans31_r4_3_eq line 226
  146. def OAI.SharpPlanar.CachedData.trans31_r4_4 line 227
  147. lemma OAI.SharpPlanar.CachedData.trans31_r4_4_eq line 228
  148. def OAI.SharpPlanar.CachedData.trans31_r4_5 line 229
  149. lemma OAI.SharpPlanar.CachedData.trans31_r4_5_eq line 230
  150. def OAI.SharpPlanar.CachedData.trans31_r4_6 line 231
  151. lemma OAI.SharpPlanar.CachedData.trans31_r4_6_eq line 232
  152. def OAI.SharpPlanar.CachedData.trans31_r4_7 line 233
  153. lemma OAI.SharpPlanar.CachedData.trans31_r4_7_eq line 234
  154. def OAI.SharpPlanar.CachedData.trans31_r4_8 line 235
  155. lemma OAI.SharpPlanar.CachedData.trans31_r4_8_eq line 236
  156. def OAI.SharpPlanar.CachedData.trans31_r4_9 line 237
  157. lemma OAI.SharpPlanar.CachedData.trans31_r4_9_eq line 238
  158. def OAI.SharpPlanar.CachedData.trans31_r4_10 line 239
  159. lemma OAI.SharpPlanar.CachedData.trans31_r4_10_eq line 240
  160. def OAI.SharpPlanar.CachedData.trans31_r4_11 line 241
  161. lemma OAI.SharpPlanar.CachedData.trans31_r4_11_eq line 242
  162. def OAI.SharpPlanar.CachedData.trans31_r4_12 line 243
  163. lemma OAI.SharpPlanar.CachedData.trans31_r4_12_eq line 244
  164. def OAI.SharpPlanar.CachedData.trans31_r4_13 line 245
  165. lemma OAI.SharpPlanar.CachedData.trans31_r4_13_eq line 246
  166. def OAI.SharpPlanar.CachedData.trans31_r4_14 line 247
  167. lemma OAI.SharpPlanar.CachedData.trans31_r4_14_eq line 248
  168. def OAI.SharpPlanar.CachedData.trans31_r4_15 line 249
  169. lemma OAI.SharpPlanar.CachedData.trans31_r4_15_eq line 250
  170. def OAI.SharpPlanar.CachedData.trans31_r4 line 251
  171. lemma OAI.SharpPlanar.CachedData.trans31_r4_eq line 252
  172. def OAI.SharpPlanar.CachedData.trans31_r5_0 line 270
  173. lemma OAI.SharpPlanar.CachedData.trans31_r5_0_eq line 271
  174. def OAI.SharpPlanar.CachedData.trans31_r5_1 line 272
  175. lemma OAI.SharpPlanar.CachedData.trans31_r5_1_eq line 273
  176. def OAI.SharpPlanar.CachedData.trans31_r5_2 line 274
  177. lemma OAI.SharpPlanar.CachedData.trans31_r5_2_eq line 275
  178. def OAI.SharpPlanar.CachedData.trans31_r5_3 line 276
  179. lemma OAI.SharpPlanar.CachedData.trans31_r5_3_eq line 277
  180. def OAI.SharpPlanar.CachedData.trans31_r5_4 line 278
  181. lemma OAI.SharpPlanar.CachedData.trans31_r5_4_eq line 279
  182. def OAI.SharpPlanar.CachedData.trans31_r5_5 line 280
  183. lemma OAI.SharpPlanar.CachedData.trans31_r5_5_eq line 281
  184. def OAI.SharpPlanar.CachedData.trans31_r5_6 line 282
  185. lemma OAI.SharpPlanar.CachedData.trans31_r5_6_eq line 283
  186. def OAI.SharpPlanar.CachedData.trans31_r5_7 line 284
  187. lemma OAI.SharpPlanar.CachedData.trans31_r5_7_eq line 285
  188. def OAI.SharpPlanar.CachedData.trans31_r5_8 line 286
  189. lemma OAI.SharpPlanar.CachedData.trans31_r5_8_eq line 287
  190. def OAI.SharpPlanar.CachedData.trans31_r5_9 line 288
  191. lemma OAI.SharpPlanar.CachedData.trans31_r5_9_eq line 289
  192. def OAI.SharpPlanar.CachedData.trans31_r5_10 line 290
  193. lemma OAI.SharpPlanar.CachedData.trans31_r5_10_eq line 291
  194. def OAI.SharpPlanar.CachedData.trans31_r5_11 line 292
  195. lemma OAI.SharpPlanar.CachedData.trans31_r5_11_eq line 293
  196. def OAI.SharpPlanar.CachedData.trans31_r5_12 line 294
  197. lemma OAI.SharpPlanar.CachedData.trans31_r5_12_eq line 295
  198. def OAI.SharpPlanar.CachedData.trans31_r5_13 line 296
  199. lemma OAI.SharpPlanar.CachedData.trans31_r5_13_eq line 297
  200. def OAI.SharpPlanar.CachedData.trans31_r5_14 line 298
  201. lemma OAI.SharpPlanar.CachedData.trans31_r5_14_eq line 299
  202. def OAI.SharpPlanar.CachedData.trans31_r5_15 line 300
  203. lemma OAI.SharpPlanar.CachedData.trans31_r5_15_eq line 301
  204. def OAI.SharpPlanar.CachedData.trans31_r5 line 302
  205. lemma OAI.SharpPlanar.CachedData.trans31_r5_eq line 303
  206. def OAI.SharpPlanar.CachedData.trans31 line 321
  207. lemma OAI.SharpPlanar.CachedData.trans31_eq line 322
  208. lemma OAI.SharpPlanar.CachedData.trans31_contains line 330
  209. def OAI.SharpPlanar.CachedData.trans32Expr line 335
  210. def OAI.SharpPlanar.CachedData.trans32_r0_0 line 336
  211. lemma OAI.SharpPlanar.CachedData.trans32_r0_0_eq line 337
  212. def OAI.SharpPlanar.CachedData.trans32_r0_1 line 338
  213. lemma OAI.SharpPlanar.CachedData.trans32_r0_1_eq line 339
  214. def OAI.SharpPlanar.CachedData.trans32_r0_2 line 340
  215. lemma OAI.SharpPlanar.CachedData.trans32_r0_2_eq line 341
  216. def OAI.SharpPlanar.CachedData.trans32_r0_3 line 342
  217. lemma OAI.SharpPlanar.CachedData.trans32_r0_3_eq line 343
  218. def OAI.SharpPlanar.CachedData.trans32_r0_4 line 344
  219. lemma OAI.SharpPlanar.CachedData.trans32_r0_4_eq line 345
  220. def OAI.SharpPlanar.CachedData.trans32_r0_5 line 346
  221. lemma OAI.SharpPlanar.CachedData.trans32_r0_5_eq line 347
  222. def OAI.SharpPlanar.CachedData.trans32_r0_6 line 348
  223. lemma OAI.SharpPlanar.CachedData.trans32_r0_6_eq line 349
  224. def OAI.SharpPlanar.CachedData.trans32_r0_7 line 350
  225. lemma OAI.SharpPlanar.CachedData.trans32_r0_7_eq line 351
  226. def OAI.SharpPlanar.CachedData.trans32_r0_8 line 352
  227. lemma OAI.SharpPlanar.CachedData.trans32_r0_8_eq line 353
  228. def OAI.SharpPlanar.CachedData.trans32_r0_9 line 354
  229. lemma OAI.SharpPlanar.CachedData.trans32_r0_9_eq line 355
  230. def OAI.SharpPlanar.CachedData.trans32_r0_10 line 356
  231. lemma OAI.SharpPlanar.CachedData.trans32_r0_10_eq line 357
  232. def OAI.SharpPlanar.CachedData.trans32_r0_11 line 358
  233. lemma OAI.SharpPlanar.CachedData.trans32_r0_11_eq line 359
  234. def OAI.SharpPlanar.CachedData.trans32_r0_12 line 360
  235. lemma OAI.SharpPlanar.CachedData.trans32_r0_12_eq line 361
  236. def OAI.SharpPlanar.CachedData.trans32_r0_13 line 362
  237. lemma OAI.SharpPlanar.CachedData.trans32_r0_13_eq line 363
  238. def OAI.SharpPlanar.CachedData.trans32_r0_14 line 364
  239. lemma OAI.SharpPlanar.CachedData.trans32_r0_14_eq line 365
  240. def OAI.SharpPlanar.CachedData.trans32_r0_15 line 366
  241. lemma OAI.SharpPlanar.CachedData.trans32_r0_15_eq line 367
  242. def OAI.SharpPlanar.CachedData.trans32_r0 line 368
  243. lemma OAI.SharpPlanar.CachedData.trans32_r0_eq line 369
  244. def OAI.SharpPlanar.CachedData.trans32_r1_0 line 387
  245. lemma OAI.SharpPlanar.CachedData.trans32_r1_0_eq line 388
  246. def OAI.SharpPlanar.CachedData.trans32_r1_1 line 389
  247. lemma OAI.SharpPlanar.CachedData.trans32_r1_1_eq line 390
  248. def OAI.SharpPlanar.CachedData.trans32_r1_2 line 391
  249. lemma OAI.SharpPlanar.CachedData.trans32_r1_2_eq line 392
  250. def OAI.SharpPlanar.CachedData.trans32_r1_3 line 393
  251. lemma OAI.SharpPlanar.CachedData.trans32_r1_3_eq line 394
  252. def OAI.SharpPlanar.CachedData.trans32_r1_4 line 395
  253. lemma OAI.SharpPlanar.CachedData.trans32_r1_4_eq line 396
  254. def OAI.SharpPlanar.CachedData.trans32_r1_5 line 397
  255. lemma OAI.SharpPlanar.CachedData.trans32_r1_5_eq line 398
  256. def OAI.SharpPlanar.CachedData.trans32_r1_6 line 399
  257. lemma OAI.SharpPlanar.CachedData.trans32_r1_6_eq line 400
  258. def OAI.SharpPlanar.CachedData.trans32_r1_7 line 401
  259. lemma OAI.SharpPlanar.CachedData.trans32_r1_7_eq line 402
  260. def OAI.SharpPlanar.CachedData.trans32_r1_8 line 403
  261. lemma OAI.SharpPlanar.CachedData.trans32_r1_8_eq line 404
  262. def OAI.SharpPlanar.CachedData.trans32_r1_9 line 405
  263. lemma OAI.SharpPlanar.CachedData.trans32_r1_9_eq line 406
  264. def OAI.SharpPlanar.CachedData.trans32_r1_10 line 407
  265. lemma OAI.SharpPlanar.CachedData.trans32_r1_10_eq line 408
  266. def OAI.SharpPlanar.CachedData.trans32_r1_11 line 409
  267. lemma OAI.SharpPlanar.CachedData.trans32_r1_11_eq line 410
  268. def OAI.SharpPlanar.CachedData.trans32_r1_12 line 411
  269. lemma OAI.SharpPlanar.CachedData.trans32_r1_12_eq line 412
  270. def OAI.SharpPlanar.CachedData.trans32_r1_13 line 413
  271. lemma OAI.SharpPlanar.CachedData.trans32_r1_13_eq line 414
  272. def OAI.SharpPlanar.CachedData.trans32_r1_14 line 415
  273. lemma OAI.SharpPlanar.CachedData.trans32_r1_14_eq line 416
  274. def OAI.SharpPlanar.CachedData.trans32_r1_15 line 417
  275. lemma OAI.SharpPlanar.CachedData.trans32_r1_15_eq line 418
  276. def OAI.SharpPlanar.CachedData.trans32_r1 line 419
  277. lemma OAI.SharpPlanar.CachedData.trans32_r1_eq line 420
  278. def OAI.SharpPlanar.CachedData.trans32_r2_0 line 438
  279. lemma OAI.SharpPlanar.CachedData.trans32_r2_0_eq line 439
  280. def OAI.SharpPlanar.CachedData.trans32_r2_1 line 440
  281. lemma OAI.SharpPlanar.CachedData.trans32_r2_1_eq line 441
  282. def OAI.SharpPlanar.CachedData.trans32_r2_2 line 442
  283. lemma OAI.SharpPlanar.CachedData.trans32_r2_2_eq line 443
  284. def OAI.SharpPlanar.CachedData.trans32_r2_3 line 444
  285. lemma OAI.SharpPlanar.CachedData.trans32_r2_3_eq line 445
  286. def OAI.SharpPlanar.CachedData.trans32_r2_4 line 446
  287. lemma OAI.SharpPlanar.CachedData.trans32_r2_4_eq line 447
  288. def OAI.SharpPlanar.CachedData.trans32_r2_5 line 448
  289. lemma OAI.SharpPlanar.CachedData.trans32_r2_5_eq line 449
  290. def OAI.SharpPlanar.CachedData.trans32_r2_6 line 450
  291. lemma OAI.SharpPlanar.CachedData.trans32_r2_6_eq line 451
  292. def OAI.SharpPlanar.CachedData.trans32_r2_7 line 452
  293. lemma OAI.SharpPlanar.CachedData.trans32_r2_7_eq line 453
  294. def OAI.SharpPlanar.CachedData.trans32_r2_8 line 454
  295. lemma OAI.SharpPlanar.CachedData.trans32_r2_8_eq line 455
  296. def OAI.SharpPlanar.CachedData.trans32_r2_9 line 456
  297. lemma OAI.SharpPlanar.CachedData.trans32_r2_9_eq line 457
  298. def OAI.SharpPlanar.CachedData.trans32_r2_10 line 458
  299. lemma OAI.SharpPlanar.CachedData.trans32_r2_10_eq line 459
  300. def OAI.SharpPlanar.CachedData.trans32_r2_11 line 460
  301. lemma OAI.SharpPlanar.CachedData.trans32_r2_11_eq line 461
  302. def OAI.SharpPlanar.CachedData.trans32_r2_12 line 462
  303. lemma OAI.SharpPlanar.CachedData.trans32_r2_12_eq line 463
  304. def OAI.SharpPlanar.CachedData.trans32_r2_13 line 464
  305. lemma OAI.SharpPlanar.CachedData.trans32_r2_13_eq line 465
  306. def OAI.SharpPlanar.CachedData.trans32_r2_14 line 466
  307. lemma OAI.SharpPlanar.CachedData.trans32_r2_14_eq line 467
  308. def OAI.SharpPlanar.CachedData.trans32_r2_15 line 468
  309. lemma OAI.SharpPlanar.CachedData.trans32_r2_15_eq line 469
  310. def OAI.SharpPlanar.CachedData.trans32_r2 line 470
  311. lemma OAI.SharpPlanar.CachedData.trans32_r2_eq line 471
  312. def OAI.SharpPlanar.CachedData.trans32_r3_0 line 489
  313. lemma OAI.SharpPlanar.CachedData.trans32_r3_0_eq line 490
  314. def OAI.SharpPlanar.CachedData.trans32_r3_1 line 491
  315. lemma OAI.SharpPlanar.CachedData.trans32_r3_1_eq line 492
  316. def OAI.SharpPlanar.CachedData.trans32_r3_2 line 493
  317. lemma OAI.SharpPlanar.CachedData.trans32_r3_2_eq line 494
  318. def OAI.SharpPlanar.CachedData.trans32_r3_3 line 495
  319. lemma OAI.SharpPlanar.CachedData.trans32_r3_3_eq line 496
  320. def OAI.SharpPlanar.CachedData.trans32_r3_4 line 497
  321. lemma OAI.SharpPlanar.CachedData.trans32_r3_4_eq line 498
  322. def OAI.SharpPlanar.CachedData.trans32_r3_5 line 499
  323. lemma OAI.SharpPlanar.CachedData.trans32_r3_5_eq line 500
  324. def OAI.SharpPlanar.CachedData.trans32_r3_6 line 501
  325. lemma OAI.SharpPlanar.CachedData.trans32_r3_6_eq line 502
  326. def OAI.SharpPlanar.CachedData.trans32_r3_7 line 503
  327. lemma OAI.SharpPlanar.CachedData.trans32_r3_7_eq line 504
  328. def OAI.SharpPlanar.CachedData.trans32_r3_8 line 505
  329. lemma OAI.SharpPlanar.CachedData.trans32_r3_8_eq line 506
  330. def OAI.SharpPlanar.CachedData.trans32_r3_9 line 507
  331. lemma OAI.SharpPlanar.CachedData.trans32_r3_9_eq line 508
  332. def OAI.SharpPlanar.CachedData.trans32_r3_10 line 509
  333. lemma OAI.SharpPlanar.CachedData.trans32_r3_10_eq line 510
  334. def OAI.SharpPlanar.CachedData.trans32_r3_11 line 511
  335. lemma OAI.SharpPlanar.CachedData.trans32_r3_11_eq line 512
  336. def OAI.SharpPlanar.CachedData.trans32_r3_12 line 513
  337. lemma OAI.SharpPlanar.CachedData.trans32_r3_12_eq line 514
  338. def OAI.SharpPlanar.CachedData.trans32_r3_13 line 515
  339. lemma OAI.SharpPlanar.CachedData.trans32_r3_13_eq line 516
  340. def OAI.SharpPlanar.CachedData.trans32_r3_14 line 517
  341. lemma OAI.SharpPlanar.CachedData.trans32_r3_14_eq line 518
  342. def OAI.SharpPlanar.CachedData.trans32_r3_15 line 519
  343. lemma OAI.SharpPlanar.CachedData.trans32_r3_15_eq line 520
  344. def OAI.SharpPlanar.CachedData.trans32_r3 line 521
  345. lemma OAI.SharpPlanar.CachedData.trans32_r3_eq line 522
  346. def OAI.SharpPlanar.CachedData.trans32_r4_0 line 540
  347. lemma OAI.SharpPlanar.CachedData.trans32_r4_0_eq line 541
  348. def OAI.SharpPlanar.CachedData.trans32_r4_1 line 542
  349. lemma OAI.SharpPlanar.CachedData.trans32_r4_1_eq line 543
  350. def OAI.SharpPlanar.CachedData.trans32_r4_2 line 544
  351. lemma OAI.SharpPlanar.CachedData.trans32_r4_2_eq line 545
  352. def OAI.SharpPlanar.CachedData.trans32_r4_3 line 546
  353. lemma OAI.SharpPlanar.CachedData.trans32_r4_3_eq line 547
  354. def OAI.SharpPlanar.CachedData.trans32_r4_4 line 548
  355. lemma OAI.SharpPlanar.CachedData.trans32_r4_4_eq line 549
  356. def OAI.SharpPlanar.CachedData.trans32_r4_5 line 550
  357. lemma OAI.SharpPlanar.CachedData.trans32_r4_5_eq line 551
  358. def OAI.SharpPlanar.CachedData.trans32_r4_6 line 552
  359. lemma OAI.SharpPlanar.CachedData.trans32_r4_6_eq line 553
  360. def OAI.SharpPlanar.CachedData.trans32_r4_7 line 554
  361. lemma OAI.SharpPlanar.CachedData.trans32_r4_7_eq line 555
  362. def OAI.SharpPlanar.CachedData.trans32_r4_8 line 556
  363. lemma OAI.SharpPlanar.CachedData.trans32_r4_8_eq line 557
  364. def OAI.SharpPlanar.CachedData.trans32_r4_9 line 558
  365. lemma OAI.SharpPlanar.CachedData.trans32_r4_9_eq line 559
  366. def OAI.SharpPlanar.CachedData.trans32_r4_10 line 560
  367. lemma OAI.SharpPlanar.CachedData.trans32_r4_10_eq line 561
  368. def OAI.SharpPlanar.CachedData.trans32_r4_11 line 562
  369. lemma OAI.SharpPlanar.CachedData.trans32_r4_11_eq line 563
  370. def OAI.SharpPlanar.CachedData.trans32_r4_12 line 564
  371. lemma OAI.SharpPlanar.CachedData.trans32_r4_12_eq line 565
  372. def OAI.SharpPlanar.CachedData.trans32_r4_13 line 566
  373. lemma OAI.SharpPlanar.CachedData.trans32_r4_13_eq line 567
  374. def OAI.SharpPlanar.CachedData.trans32_r4_14 line 568
  375. lemma OAI.SharpPlanar.CachedData.trans32_r4_14_eq line 569
  376. def OAI.SharpPlanar.CachedData.trans32_r4_15 line 570
  377. lemma OAI.SharpPlanar.CachedData.trans32_r4_15_eq line 571
  378. def OAI.SharpPlanar.CachedData.trans32_r4 line 572
  379. lemma OAI.SharpPlanar.CachedData.trans32_r4_eq line 573
  380. def OAI.SharpPlanar.CachedData.trans32_r5_0 line 591
  381. lemma OAI.SharpPlanar.CachedData.trans32_r5_0_eq line 592
  382. def OAI.SharpPlanar.CachedData.trans32_r5_1 line 593
  383. lemma OAI.SharpPlanar.CachedData.trans32_r5_1_eq line 594
  384. def OAI.SharpPlanar.CachedData.trans32_r5_2 line 595
  385. lemma OAI.SharpPlanar.CachedData.trans32_r5_2_eq line 596
  386. def OAI.SharpPlanar.CachedData.trans32_r5_3 line 597
  387. lemma OAI.SharpPlanar.CachedData.trans32_r5_3_eq line 598
  388. def OAI.SharpPlanar.CachedData.trans32_r5_4 line 599
  389. lemma OAI.SharpPlanar.CachedData.trans32_r5_4_eq line 600
  390. def OAI.SharpPlanar.CachedData.trans32_r5_5 line 601
  391. lemma OAI.SharpPlanar.CachedData.trans32_r5_5_eq line 602
  392. def OAI.SharpPlanar.CachedData.trans32_r5_6 line 603
  393. lemma OAI.SharpPlanar.CachedData.trans32_r5_6_eq line 604
  394. def OAI.SharpPlanar.CachedData.trans32_r5_7 line 605
  395. lemma OAI.SharpPlanar.CachedData.trans32_r5_7_eq line 606
  396. def OAI.SharpPlanar.CachedData.trans32_r5_8 line 607
  397. lemma OAI.SharpPlanar.CachedData.trans32_r5_8_eq line 608
  398. def OAI.SharpPlanar.CachedData.trans32_r5_9 line 609
  399. lemma OAI.SharpPlanar.CachedData.trans32_r5_9_eq line 610
  400. def OAI.SharpPlanar.CachedData.trans32_r5_10 line 611
  401. lemma OAI.SharpPlanar.CachedData.trans32_r5_10_eq line 612
  402. def OAI.SharpPlanar.CachedData.trans32_r5_11 line 613
  403. lemma OAI.SharpPlanar.CachedData.trans32_r5_11_eq line 614
  404. def OAI.SharpPlanar.CachedData.trans32_r5_12 line 615
  405. lemma OAI.SharpPlanar.CachedData.trans32_r5_12_eq line 616
  406. def OAI.SharpPlanar.CachedData.trans32_r5_13 line 617
  407. lemma OAI.SharpPlanar.CachedData.trans32_r5_13_eq line 618
  408. def OAI.SharpPlanar.CachedData.trans32_r5_14 line 619
  409. lemma OAI.SharpPlanar.CachedData.trans32_r5_14_eq line 620
  410. def OAI.SharpPlanar.CachedData.trans32_r5_15 line 621
  411. lemma OAI.SharpPlanar.CachedData.trans32_r5_15_eq line 622
  412. def OAI.SharpPlanar.CachedData.trans32_r5 line 623
  413. lemma OAI.SharpPlanar.CachedData.trans32_r5_eq line 624
  414. def OAI.SharpPlanar.CachedData.trans32 line 642
  415. lemma OAI.SharpPlanar.CachedData.trans32_eq line 643
  416. lemma OAI.SharpPlanar.CachedData.trans32_contains line 651
  417. def OAI.SharpPlanar.CachedData.trans33Expr line 656
  418. def OAI.SharpPlanar.CachedData.trans33_r0_0 line 657
  419. lemma OAI.SharpPlanar.CachedData.trans33_r0_0_eq line 658
  420. def OAI.SharpPlanar.CachedData.trans33_r0_1 line 659
  421. lemma OAI.SharpPlanar.CachedData.trans33_r0_1_eq line 660
  422. def OAI.SharpPlanar.CachedData.trans33_r0_2 line 661
  423. lemma OAI.SharpPlanar.CachedData.trans33_r0_2_eq line 662
  424. def OAI.SharpPlanar.CachedData.trans33_r0_3 line 663
  425. lemma OAI.SharpPlanar.CachedData.trans33_r0_3_eq line 664
  426. def OAI.SharpPlanar.CachedData.trans33_r0_4 line 665
  427. lemma OAI.SharpPlanar.CachedData.trans33_r0_4_eq line 666
  428. def OAI.SharpPlanar.CachedData.trans33_r0_5 line 667
  429. lemma OAI.SharpPlanar.CachedData.trans33_r0_5_eq line 668
  430. def OAI.SharpPlanar.CachedData.trans33_r0_6 line 669
  431. lemma OAI.SharpPlanar.CachedData.trans33_r0_6_eq line 670
  432. def OAI.SharpPlanar.CachedData.trans33_r0_7 line 671
  433. lemma OAI.SharpPlanar.CachedData.trans33_r0_7_eq line 672
  434. def OAI.SharpPlanar.CachedData.trans33_r0_8 line 673
  435. lemma OAI.SharpPlanar.CachedData.trans33_r0_8_eq line 674
  436. def OAI.SharpPlanar.CachedData.trans33_r0_9 line 675
  437. lemma OAI.SharpPlanar.CachedData.trans33_r0_9_eq line 676
  438. def OAI.SharpPlanar.CachedData.trans33_r0_10 line 677
  439. lemma OAI.SharpPlanar.CachedData.trans33_r0_10_eq line 678
  440. def OAI.SharpPlanar.CachedData.trans33_r0_11 line 679
  441. lemma OAI.SharpPlanar.CachedData.trans33_r0_11_eq line 680
  442. def OAI.SharpPlanar.CachedData.trans33_r0_12 line 681
  443. lemma OAI.SharpPlanar.CachedData.trans33_r0_12_eq line 682
  444. def OAI.SharpPlanar.CachedData.trans33_r0_13 line 683
  445. lemma OAI.SharpPlanar.CachedData.trans33_r0_13_eq line 684
  446. def OAI.SharpPlanar.CachedData.trans33_r0_14 line 685
  447. lemma OAI.SharpPlanar.CachedData.trans33_r0_14_eq line 686
  448. def OAI.SharpPlanar.CachedData.trans33_r0_15 line 687
  449. lemma OAI.SharpPlanar.CachedData.trans33_r0_15_eq line 688
  450. def OAI.SharpPlanar.CachedData.trans33_r0 line 689
  451. lemma OAI.SharpPlanar.CachedData.trans33_r0_eq line 690
  452. def OAI.SharpPlanar.CachedData.trans33_r1_0 line 708
  453. lemma OAI.SharpPlanar.CachedData.trans33_r1_0_eq line 709
  454. def OAI.SharpPlanar.CachedData.trans33_r1_1 line 710
  455. lemma OAI.SharpPlanar.CachedData.trans33_r1_1_eq line 711
  456. def OAI.SharpPlanar.CachedData.trans33_r1_2 line 712
  457. lemma OAI.SharpPlanar.CachedData.trans33_r1_2_eq line 713
  458. def OAI.SharpPlanar.CachedData.trans33_r1_3 line 714
  459. lemma OAI.SharpPlanar.CachedData.trans33_r1_3_eq line 715
  460. def OAI.SharpPlanar.CachedData.trans33_r1_4 line 716
  461. lemma OAI.SharpPlanar.CachedData.trans33_r1_4_eq line 717
  462. def OAI.SharpPlanar.CachedData.trans33_r1_5 line 718
  463. lemma OAI.SharpPlanar.CachedData.trans33_r1_5_eq line 719
  464. def OAI.SharpPlanar.CachedData.trans33_r1_6 line 720
  465. lemma OAI.SharpPlanar.CachedData.trans33_r1_6_eq line 721
  466. def OAI.SharpPlanar.CachedData.trans33_r1_7 line 722
  467. lemma OAI.SharpPlanar.CachedData.trans33_r1_7_eq line 723
  468. def OAI.SharpPlanar.CachedData.trans33_r1_8 line 724
  469. lemma OAI.SharpPlanar.CachedData.trans33_r1_8_eq line 725
  470. def OAI.SharpPlanar.CachedData.trans33_r1_9 line 726
  471. lemma OAI.SharpPlanar.CachedData.trans33_r1_9_eq line 727
  472. def OAI.SharpPlanar.CachedData.trans33_r1_10 line 728
  473. lemma OAI.SharpPlanar.CachedData.trans33_r1_10_eq line 729
  474. def OAI.SharpPlanar.CachedData.trans33_r1_11 line 730
  475. lemma OAI.SharpPlanar.CachedData.trans33_r1_11_eq line 731
  476. def OAI.SharpPlanar.CachedData.trans33_r1_12 line 732
  477. lemma OAI.SharpPlanar.CachedData.trans33_r1_12_eq line 733
  478. def OAI.SharpPlanar.CachedData.trans33_r1_13 line 734
  479. lemma OAI.SharpPlanar.CachedData.trans33_r1_13_eq line 735
  480. def OAI.SharpPlanar.CachedData.trans33_r1_14 line 736
  481. lemma OAI.SharpPlanar.CachedData.trans33_r1_14_eq line 737
  482. def OAI.SharpPlanar.CachedData.trans33_r1_15 line 738
  483. lemma OAI.SharpPlanar.CachedData.trans33_r1_15_eq line 739
  484. def OAI.SharpPlanar.CachedData.trans33_r1 line 740
  485. lemma OAI.SharpPlanar.CachedData.trans33_r1_eq line 741
  486. def OAI.SharpPlanar.CachedData.trans33_r2_0 line 759
  487. lemma OAI.SharpPlanar.CachedData.trans33_r2_0_eq line 760
  488. def OAI.SharpPlanar.CachedData.trans33_r2_1 line 761
  489. lemma OAI.SharpPlanar.CachedData.trans33_r2_1_eq line 762
  490. def OAI.SharpPlanar.CachedData.trans33_r2_2 line 763
  491. lemma OAI.SharpPlanar.CachedData.trans33_r2_2_eq line 764
  492. def OAI.SharpPlanar.CachedData.trans33_r2_3 line 765
  493. lemma OAI.SharpPlanar.CachedData.trans33_r2_3_eq line 766
  494. def OAI.SharpPlanar.CachedData.trans33_r2_4 line 767
  495. lemma OAI.SharpPlanar.CachedData.trans33_r2_4_eq line 768
  496. def OAI.SharpPlanar.CachedData.trans33_r2_5 line 769
  497. lemma OAI.SharpPlanar.CachedData.trans33_r2_5_eq line 770
  498. def OAI.SharpPlanar.CachedData.trans33_r2_6 line 771
  499. lemma OAI.SharpPlanar.CachedData.trans33_r2_6_eq line 772
  500. def OAI.SharpPlanar.CachedData.trans33_r2_7 line 773
  501. lemma OAI.SharpPlanar.CachedData.trans33_r2_7_eq line 774
  502. def OAI.SharpPlanar.CachedData.trans33_r2_8 line 775
  503. lemma OAI.SharpPlanar.CachedData.trans33_r2_8_eq line 776
  504. def OAI.SharpPlanar.CachedData.trans33_r2_9 line 777
  505. lemma OAI.SharpPlanar.CachedData.trans33_r2_9_eq line 778
  506. def OAI.SharpPlanar.CachedData.trans33_r2_10 line 779
  507. lemma OAI.SharpPlanar.CachedData.trans33_r2_10_eq line 780
  508. def OAI.SharpPlanar.CachedData.trans33_r2_11 line 781
  509. lemma OAI.SharpPlanar.CachedData.trans33_r2_11_eq line 782
  510. def OAI.SharpPlanar.CachedData.trans33_r2_12 line 783
  511. lemma OAI.SharpPlanar.CachedData.trans33_r2_12_eq line 784
  512. def OAI.SharpPlanar.CachedData.trans33_r2_13 line 785
  513. lemma OAI.SharpPlanar.CachedData.trans33_r2_13_eq line 786
  514. def OAI.SharpPlanar.CachedData.trans33_r2_14 line 787
  515. lemma OAI.SharpPlanar.CachedData.trans33_r2_14_eq line 788
  516. def OAI.SharpPlanar.CachedData.trans33_r2_15 line 789
  517. lemma OAI.SharpPlanar.CachedData.trans33_r2_15_eq line 790
  518. def OAI.SharpPlanar.CachedData.trans33_r2 line 791
  519. lemma OAI.SharpPlanar.CachedData.trans33_r2_eq line 792
  520. def OAI.SharpPlanar.CachedData.trans33_r3_0 line 810
  521. lemma OAI.SharpPlanar.CachedData.trans33_r3_0_eq line 811
  522. def OAI.SharpPlanar.CachedData.trans33_r3_1 line 812
  523. lemma OAI.SharpPlanar.CachedData.trans33_r3_1_eq line 813
  524. def OAI.SharpPlanar.CachedData.trans33_r3_2 line 814
  525. lemma OAI.SharpPlanar.CachedData.trans33_r3_2_eq line 815
  526. def OAI.SharpPlanar.CachedData.trans33_r3_3 line 816
  527. lemma OAI.SharpPlanar.CachedData.trans33_r3_3_eq line 817
  528. def OAI.SharpPlanar.CachedData.trans33_r3_4 line 818
  529. lemma OAI.SharpPlanar.CachedData.trans33_r3_4_eq line 819
  530. def OAI.SharpPlanar.CachedData.trans33_r3_5 line 820
  531. lemma OAI.SharpPlanar.CachedData.trans33_r3_5_eq line 821
  532. def OAI.SharpPlanar.CachedData.trans33_r3_6 line 822
  533. lemma OAI.SharpPlanar.CachedData.trans33_r3_6_eq line 823
  534. def OAI.SharpPlanar.CachedData.trans33_r3_7 line 824
  535. lemma OAI.SharpPlanar.CachedData.trans33_r3_7_eq line 825
  536. def OAI.SharpPlanar.CachedData.trans33_r3_8 line 826
  537. lemma OAI.SharpPlanar.CachedData.trans33_r3_8_eq line 827
  538. def OAI.SharpPlanar.CachedData.trans33_r3_9 line 828
  539. lemma OAI.SharpPlanar.CachedData.trans33_r3_9_eq line 829
  540. def OAI.SharpPlanar.CachedData.trans33_r3_10 line 830
  541. lemma OAI.SharpPlanar.CachedData.trans33_r3_10_eq line 831
  542. def OAI.SharpPlanar.CachedData.trans33_r3_11 line 832
  543. lemma OAI.SharpPlanar.CachedData.trans33_r3_11_eq line 833
  544. def OAI.SharpPlanar.CachedData.trans33_r3_12 line 834
  545. lemma OAI.SharpPlanar.CachedData.trans33_r3_12_eq line 835
  546. def OAI.SharpPlanar.CachedData.trans33_r3_13 line 836
  547. lemma OAI.SharpPlanar.CachedData.trans33_r3_13_eq line 837
  548. def OAI.SharpPlanar.CachedData.trans33_r3_14 line 838
  549. lemma OAI.SharpPlanar.CachedData.trans33_r3_14_eq line 839
  550. def OAI.SharpPlanar.CachedData.trans33_r3_15 line 840
  551. lemma OAI.SharpPlanar.CachedData.trans33_r3_15_eq line 841
  552. def OAI.SharpPlanar.CachedData.trans33_r3 line 842
  553. lemma OAI.SharpPlanar.CachedData.trans33_r3_eq line 843
  554. def OAI.SharpPlanar.CachedData.trans33_r4_0 line 861
  555. lemma OAI.SharpPlanar.CachedData.trans33_r4_0_eq line 862
  556. def OAI.SharpPlanar.CachedData.trans33_r4_1 line 863
  557. lemma OAI.SharpPlanar.CachedData.trans33_r4_1_eq line 864
  558. def OAI.SharpPlanar.CachedData.trans33_r4_2 line 865
  559. lemma OAI.SharpPlanar.CachedData.trans33_r4_2_eq line 866
  560. def OAI.SharpPlanar.CachedData.trans33_r4_3 line 867
  561. lemma OAI.SharpPlanar.CachedData.trans33_r4_3_eq line 868
  562. def OAI.SharpPlanar.CachedData.trans33_r4_4 line 869
  563. lemma OAI.SharpPlanar.CachedData.trans33_r4_4_eq line 870
  564. def OAI.SharpPlanar.CachedData.trans33_r4_5 line 871
  565. lemma OAI.SharpPlanar.CachedData.trans33_r4_5_eq line 872
  566. def OAI.SharpPlanar.CachedData.trans33_r4_6 line 873
  567. lemma OAI.SharpPlanar.CachedData.trans33_r4_6_eq line 874
  568. def OAI.SharpPlanar.CachedData.trans33_r4_7 line 875
  569. lemma OAI.SharpPlanar.CachedData.trans33_r4_7_eq line 876
  570. def OAI.SharpPlanar.CachedData.trans33_r4_8 line 877
  571. lemma OAI.SharpPlanar.CachedData.trans33_r4_8_eq line 878
  572. def OAI.SharpPlanar.CachedData.trans33_r4_9 line 879
  573. lemma OAI.SharpPlanar.CachedData.trans33_r4_9_eq line 880
  574. def OAI.SharpPlanar.CachedData.trans33_r4_10 line 881
  575. lemma OAI.SharpPlanar.CachedData.trans33_r4_10_eq line 882
  576. def OAI.SharpPlanar.CachedData.trans33_r4_11 line 883
  577. lemma OAI.SharpPlanar.CachedData.trans33_r4_11_eq line 884
  578. def OAI.SharpPlanar.CachedData.trans33_r4_12 line 885
  579. lemma OAI.SharpPlanar.CachedData.trans33_r4_12_eq line 886
  580. def OAI.SharpPlanar.CachedData.trans33_r4_13 line 887
  581. lemma OAI.SharpPlanar.CachedData.trans33_r4_13_eq line 888
  582. def OAI.SharpPlanar.CachedData.trans33_r4_14 line 889
  583. lemma OAI.SharpPlanar.CachedData.trans33_r4_14_eq line 890
  584. def OAI.SharpPlanar.CachedData.trans33_r4_15 line 891
  585. lemma OAI.SharpPlanar.CachedData.trans33_r4_15_eq line 892
  586. def OAI.SharpPlanar.CachedData.trans33_r4 line 893
  587. lemma OAI.SharpPlanar.CachedData.trans33_r4_eq line 894
  588. def OAI.SharpPlanar.CachedData.trans33_r5_0 line 912
  589. lemma OAI.SharpPlanar.CachedData.trans33_r5_0_eq line 913
  590. def OAI.SharpPlanar.CachedData.trans33_r5_1 line 914
  591. lemma OAI.SharpPlanar.CachedData.trans33_r5_1_eq line 915
  592. def OAI.SharpPlanar.CachedData.trans33_r5_2 line 916
  593. lemma OAI.SharpPlanar.CachedData.trans33_r5_2_eq line 917
  594. def OAI.SharpPlanar.CachedData.trans33_r5_3 line 918
  595. lemma OAI.SharpPlanar.CachedData.trans33_r5_3_eq line 919
  596. def OAI.SharpPlanar.CachedData.trans33_r5_4 line 920
  597. lemma OAI.SharpPlanar.CachedData.trans33_r5_4_eq line 921
  598. def OAI.SharpPlanar.CachedData.trans33_r5_5 line 922
  599. lemma OAI.SharpPlanar.CachedData.trans33_r5_5_eq line 923
  600. def OAI.SharpPlanar.CachedData.trans33_r5_6 line 924
  601. lemma OAI.SharpPlanar.CachedData.trans33_r5_6_eq line 925
  602. def OAI.SharpPlanar.CachedData.trans33_r5_7 line 926
  603. lemma OAI.SharpPlanar.CachedData.trans33_r5_7_eq line 927
  604. def OAI.SharpPlanar.CachedData.trans33_r5_8 line 928
  605. lemma OAI.SharpPlanar.CachedData.trans33_r5_8_eq line 929
  606. def OAI.SharpPlanar.CachedData.trans33_r5_9 line 930
  607. lemma OAI.SharpPlanar.CachedData.trans33_r5_9_eq line 931
  608. def OAI.SharpPlanar.CachedData.trans33_r5_10 line 932
  609. lemma OAI.SharpPlanar.CachedData.trans33_r5_10_eq line 933
  610. def OAI.SharpPlanar.CachedData.trans33_r5_11 line 934
  611. lemma OAI.SharpPlanar.CachedData.trans33_r5_11_eq line 935
  612. def OAI.SharpPlanar.CachedData.trans33_r5_12 line 936
  613. lemma OAI.SharpPlanar.CachedData.trans33_r5_12_eq line 937
  614. def OAI.SharpPlanar.CachedData.trans33_r5_13 line 938
  615. lemma OAI.SharpPlanar.CachedData.trans33_r5_13_eq line 939
  616. def OAI.SharpPlanar.CachedData.trans33_r5_14 line 940
  617. lemma OAI.SharpPlanar.CachedData.trans33_r5_14_eq line 941
  618. def OAI.SharpPlanar.CachedData.trans33_r5_15 line 942
  619. lemma OAI.SharpPlanar.CachedData.trans33_r5_15_eq line 943
  620. def OAI.SharpPlanar.CachedData.trans33_r5 line 944
  621. lemma OAI.SharpPlanar.CachedData.trans33_r5_eq line 945
  622. def OAI.SharpPlanar.CachedData.trans33 line 963
  623. lemma OAI.SharpPlanar.CachedData.trans33_eq line 964
  624. lemma OAI.SharpPlanar.CachedData.trans33_contains line 972
  625. def OAI.SharpPlanar.CachedData.trans34Expr line 977
  626. def OAI.SharpPlanar.CachedData.trans34_r0_0 line 978
  627. lemma OAI.SharpPlanar.CachedData.trans34_r0_0_eq line 979
  628. def OAI.SharpPlanar.CachedData.trans34_r0_1 line 980
  629. lemma OAI.SharpPlanar.CachedData.trans34_r0_1_eq line 981
  630. def OAI.SharpPlanar.CachedData.trans34_r0_2 line 982
  631. lemma OAI.SharpPlanar.CachedData.trans34_r0_2_eq line 983
  632. def OAI.SharpPlanar.CachedData.trans34_r0_3 line 984
  633. lemma OAI.SharpPlanar.CachedData.trans34_r0_3_eq line 985
  634. def OAI.SharpPlanar.CachedData.trans34_r0_4 line 986
  635. lemma OAI.SharpPlanar.CachedData.trans34_r0_4_eq line 987
  636. def OAI.SharpPlanar.CachedData.trans34_r0_5 line 988
  637. lemma OAI.SharpPlanar.CachedData.trans34_r0_5_eq line 989
  638. def OAI.SharpPlanar.CachedData.trans34_r0_6 line 990
  639. lemma OAI.SharpPlanar.CachedData.trans34_r0_6_eq line 991
  640. def OAI.SharpPlanar.CachedData.trans34_r0_7 line 992
  641. lemma OAI.SharpPlanar.CachedData.trans34_r0_7_eq line 993
  642. def OAI.SharpPlanar.CachedData.trans34_r0_8 line 994
  643. lemma OAI.SharpPlanar.CachedData.trans34_r0_8_eq line 995
  644. def OAI.SharpPlanar.CachedData.trans34_r0_9 line 996
  645. lemma OAI.SharpPlanar.CachedData.trans34_r0_9_eq line 997
  646. def OAI.SharpPlanar.CachedData.trans34_r0_10 line 998
  647. lemma OAI.SharpPlanar.CachedData.trans34_r0_10_eq line 999
  648. def OAI.SharpPlanar.CachedData.trans34_r0_11 line 1000
  649. lemma OAI.SharpPlanar.CachedData.trans34_r0_11_eq line 1001
  650. def OAI.SharpPlanar.CachedData.trans34_r0_12 line 1002
  651. lemma OAI.SharpPlanar.CachedData.trans34_r0_12_eq line 1003
  652. def OAI.SharpPlanar.CachedData.trans34_r0_13 line 1004
  653. lemma OAI.SharpPlanar.CachedData.trans34_r0_13_eq line 1005
  654. def OAI.SharpPlanar.CachedData.trans34_r0_14 line 1006
  655. lemma OAI.SharpPlanar.CachedData.trans34_r0_14_eq line 1007
  656. def OAI.SharpPlanar.CachedData.trans34_r0_15 line 1008
  657. lemma OAI.SharpPlanar.CachedData.trans34_r0_15_eq line 1009
  658. def OAI.SharpPlanar.CachedData.trans34_r0 line 1010
  659. lemma OAI.SharpPlanar.CachedData.trans34_r0_eq line 1011
  660. def OAI.SharpPlanar.CachedData.trans34_r1_0 line 1029
  661. lemma OAI.SharpPlanar.CachedData.trans34_r1_0_eq line 1030
  662. def OAI.SharpPlanar.CachedData.trans34_r1_1 line 1031
  663. lemma OAI.SharpPlanar.CachedData.trans34_r1_1_eq line 1032
  664. def OAI.SharpPlanar.CachedData.trans34_r1_2 line 1033
  665. lemma OAI.SharpPlanar.CachedData.trans34_r1_2_eq line 1034
  666. def OAI.SharpPlanar.CachedData.trans34_r1_3 line 1035
  667. lemma OAI.SharpPlanar.CachedData.trans34_r1_3_eq line 1036
  668. def OAI.SharpPlanar.CachedData.trans34_r1_4 line 1037
  669. lemma OAI.SharpPlanar.CachedData.trans34_r1_4_eq line 1038
  670. def OAI.SharpPlanar.CachedData.trans34_r1_5 line 1039
  671. lemma OAI.SharpPlanar.CachedData.trans34_r1_5_eq line 1040
  672. def OAI.SharpPlanar.CachedData.trans34_r1_6 line 1041
  673. lemma OAI.SharpPlanar.CachedData.trans34_r1_6_eq line 1042
  674. def OAI.SharpPlanar.CachedData.trans34_r1_7 line 1043
  675. lemma OAI.SharpPlanar.CachedData.trans34_r1_7_eq line 1044
  676. def OAI.SharpPlanar.CachedData.trans34_r1_8 line 1045
  677. lemma OAI.SharpPlanar.CachedData.trans34_r1_8_eq line 1046
  678. def OAI.SharpPlanar.CachedData.trans34_r1_9 line 1047
  679. lemma OAI.SharpPlanar.CachedData.trans34_r1_9_eq line 1048
  680. def OAI.SharpPlanar.CachedData.trans34_r1_10 line 1049
  681. lemma OAI.SharpPlanar.CachedData.trans34_r1_10_eq line 1050
  682. def OAI.SharpPlanar.CachedData.trans34_r1_11 line 1051
  683. lemma OAI.SharpPlanar.CachedData.trans34_r1_11_eq line 1052
  684. def OAI.SharpPlanar.CachedData.trans34_r1_12 line 1053
  685. lemma OAI.SharpPlanar.CachedData.trans34_r1_12_eq line 1054
  686. def OAI.SharpPlanar.CachedData.trans34_r1_13 line 1055
  687. lemma OAI.SharpPlanar.CachedData.trans34_r1_13_eq line 1056
  688. def OAI.SharpPlanar.CachedData.trans34_r1_14 line 1057
  689. lemma OAI.SharpPlanar.CachedData.trans34_r1_14_eq line 1058
  690. def OAI.SharpPlanar.CachedData.trans34_r1_15 line 1059
  691. lemma OAI.SharpPlanar.CachedData.trans34_r1_15_eq line 1060
  692. def OAI.SharpPlanar.CachedData.trans34_r1 line 1061
  693. lemma OAI.SharpPlanar.CachedData.trans34_r1_eq line 1062
  694. def OAI.SharpPlanar.CachedData.trans34_r2_0 line 1080
  695. lemma OAI.SharpPlanar.CachedData.trans34_r2_0_eq line 1081
  696. def OAI.SharpPlanar.CachedData.trans34_r2_1 line 1082
  697. lemma OAI.SharpPlanar.CachedData.trans34_r2_1_eq line 1083
  698. def OAI.SharpPlanar.CachedData.trans34_r2_2 line 1084
  699. lemma OAI.SharpPlanar.CachedData.trans34_r2_2_eq line 1085
  700. def OAI.SharpPlanar.CachedData.trans34_r2_3 line 1086
  701. lemma OAI.SharpPlanar.CachedData.trans34_r2_3_eq line 1087
  702. def OAI.SharpPlanar.CachedData.trans34_r2_4 line 1088
  703. lemma OAI.SharpPlanar.CachedData.trans34_r2_4_eq line 1089
  704. def OAI.SharpPlanar.CachedData.trans34_r2_5 line 1090
  705. lemma OAI.SharpPlanar.CachedData.trans34_r2_5_eq line 1091
  706. def OAI.SharpPlanar.CachedData.trans34_r2_6 line 1092
  707. lemma OAI.SharpPlanar.CachedData.trans34_r2_6_eq line 1093
  708. def OAI.SharpPlanar.CachedData.trans34_r2_7 line 1094
  709. lemma OAI.SharpPlanar.CachedData.trans34_r2_7_eq line 1095
  710. def OAI.SharpPlanar.CachedData.trans34_r2_8 line 1096
  711. lemma OAI.SharpPlanar.CachedData.trans34_r2_8_eq line 1097
  712. def OAI.SharpPlanar.CachedData.trans34_r2_9 line 1098
  713. lemma OAI.SharpPlanar.CachedData.trans34_r2_9_eq line 1099
  714. def OAI.SharpPlanar.CachedData.trans34_r2_10 line 1100
  715. lemma OAI.SharpPlanar.CachedData.trans34_r2_10_eq line 1101
  716. def OAI.SharpPlanar.CachedData.trans34_r2_11 line 1102
  717. lemma OAI.SharpPlanar.CachedData.trans34_r2_11_eq line 1103
  718. def OAI.SharpPlanar.CachedData.trans34_r2_12 line 1104
  719. lemma OAI.SharpPlanar.CachedData.trans34_r2_12_eq line 1105
  720. def OAI.SharpPlanar.CachedData.trans34_r2_13 line 1106
  721. lemma OAI.SharpPlanar.CachedData.trans34_r2_13_eq line 1107
  722. def OAI.SharpPlanar.CachedData.trans34_r2_14 line 1108
  723. lemma OAI.SharpPlanar.CachedData.trans34_r2_14_eq line 1109
  724. def OAI.SharpPlanar.CachedData.trans34_r2_15 line 1110
  725. lemma OAI.SharpPlanar.CachedData.trans34_r2_15_eq line 1111
  726. def OAI.SharpPlanar.CachedData.trans34_r2 line 1112
  727. lemma OAI.SharpPlanar.CachedData.trans34_r2_eq line 1113
  728. def OAI.SharpPlanar.CachedData.trans34_r3_0 line 1131
  729. lemma OAI.SharpPlanar.CachedData.trans34_r3_0_eq line 1132
  730. def OAI.SharpPlanar.CachedData.trans34_r3_1 line 1133
  731. lemma OAI.SharpPlanar.CachedData.trans34_r3_1_eq line 1134
  732. def OAI.SharpPlanar.CachedData.trans34_r3_2 line 1135
  733. lemma OAI.SharpPlanar.CachedData.trans34_r3_2_eq line 1136
  734. def OAI.SharpPlanar.CachedData.trans34_r3_3 line 1137
  735. lemma OAI.SharpPlanar.CachedData.trans34_r3_3_eq line 1138
  736. def OAI.SharpPlanar.CachedData.trans34_r3_4 line 1139
  737. lemma OAI.SharpPlanar.CachedData.trans34_r3_4_eq line 1140
  738. def OAI.SharpPlanar.CachedData.trans34_r3_5 line 1141
  739. lemma OAI.SharpPlanar.CachedData.trans34_r3_5_eq line 1142
  740. def OAI.SharpPlanar.CachedData.trans34_r3_6 line 1143
  741. lemma OAI.SharpPlanar.CachedData.trans34_r3_6_eq line 1144
  742. def OAI.SharpPlanar.CachedData.trans34_r3_7 line 1145
  743. lemma OAI.SharpPlanar.CachedData.trans34_r3_7_eq line 1146
  744. def OAI.SharpPlanar.CachedData.trans34_r3_8 line 1147
  745. lemma OAI.SharpPlanar.CachedData.trans34_r3_8_eq line 1148
  746. def OAI.SharpPlanar.CachedData.trans34_r3_9 line 1149
  747. lemma OAI.SharpPlanar.CachedData.trans34_r3_9_eq line 1150
  748. def OAI.SharpPlanar.CachedData.trans34_r3_10 line 1151
  749. lemma OAI.SharpPlanar.CachedData.trans34_r3_10_eq line 1152
  750. def OAI.SharpPlanar.CachedData.trans34_r3_11 line 1153
  751. lemma OAI.SharpPlanar.CachedData.trans34_r3_11_eq line 1154
  752. def OAI.SharpPlanar.CachedData.trans34_r3_12 line 1155
  753. lemma OAI.SharpPlanar.CachedData.trans34_r3_12_eq line 1156
  754. def OAI.SharpPlanar.CachedData.trans34_r3_13 line 1157
  755. lemma OAI.SharpPlanar.CachedData.trans34_r3_13_eq line 1158
  756. def OAI.SharpPlanar.CachedData.trans34_r3_14 line 1159
  757. lemma OAI.SharpPlanar.CachedData.trans34_r3_14_eq line 1160
  758. def OAI.SharpPlanar.CachedData.trans34_r3_15 line 1161
  759. lemma OAI.SharpPlanar.CachedData.trans34_r3_15_eq line 1162
  760. def OAI.SharpPlanar.CachedData.trans34_r3 line 1163
  761. lemma OAI.SharpPlanar.CachedData.trans34_r3_eq line 1164
  762. def OAI.SharpPlanar.CachedData.trans34_r4_0 line 1182
  763. lemma OAI.SharpPlanar.CachedData.trans34_r4_0_eq line 1183
  764. def OAI.SharpPlanar.CachedData.trans34_r4_1 line 1184
  765. lemma OAI.SharpPlanar.CachedData.trans34_r4_1_eq line 1185
  766. def OAI.SharpPlanar.CachedData.trans34_r4_2 line 1186
  767. lemma OAI.SharpPlanar.CachedData.trans34_r4_2_eq line 1187
  768. def OAI.SharpPlanar.CachedData.trans34_r4_3 line 1188
  769. lemma OAI.SharpPlanar.CachedData.trans34_r4_3_eq line 1189
  770. def OAI.SharpPlanar.CachedData.trans34_r4_4 line 1190
  771. lemma OAI.SharpPlanar.CachedData.trans34_r4_4_eq line 1191
  772. def OAI.SharpPlanar.CachedData.trans34_r4_5 line 1192
  773. lemma OAI.SharpPlanar.CachedData.trans34_r4_5_eq line 1193
  774. def OAI.SharpPlanar.CachedData.trans34_r4_6 line 1194
  775. lemma OAI.SharpPlanar.CachedData.trans34_r4_6_eq line 1195
  776. def OAI.SharpPlanar.CachedData.trans34_r4_7 line 1196
  777. lemma OAI.SharpPlanar.CachedData.trans34_r4_7_eq line 1197
  778. def OAI.SharpPlanar.CachedData.trans34_r4_8 line 1198
  779. lemma OAI.SharpPlanar.CachedData.trans34_r4_8_eq line 1199
  780. def OAI.SharpPlanar.CachedData.trans34_r4_9 line 1200
  781. lemma OAI.SharpPlanar.CachedData.trans34_r4_9_eq line 1201
  782. def OAI.SharpPlanar.CachedData.trans34_r4_10 line 1202
  783. lemma OAI.SharpPlanar.CachedData.trans34_r4_10_eq line 1203
  784. def OAI.SharpPlanar.CachedData.trans34_r4_11 line 1204
  785. lemma OAI.SharpPlanar.CachedData.trans34_r4_11_eq line 1205
  786. def OAI.SharpPlanar.CachedData.trans34_r4_12 line 1206
  787. lemma OAI.SharpPlanar.CachedData.trans34_r4_12_eq line 1207
  788. def OAI.SharpPlanar.CachedData.trans34_r4_13 line 1208
  789. lemma OAI.SharpPlanar.CachedData.trans34_r4_13_eq line 1209
  790. def OAI.SharpPlanar.CachedData.trans34_r4_14 line 1210
  791. lemma OAI.SharpPlanar.CachedData.trans34_r4_14_eq line 1211
  792. def OAI.SharpPlanar.CachedData.trans34_r4_15 line 1212
  793. lemma OAI.SharpPlanar.CachedData.trans34_r4_15_eq line 1213
  794. def OAI.SharpPlanar.CachedData.trans34_r4 line 1214
  795. lemma OAI.SharpPlanar.CachedData.trans34_r4_eq line 1215
  796. def OAI.SharpPlanar.CachedData.trans34_r5_0 line 1233
  797. lemma OAI.SharpPlanar.CachedData.trans34_r5_0_eq line 1234
  798. def OAI.SharpPlanar.CachedData.trans34_r5_1 line 1235
  799. lemma OAI.SharpPlanar.CachedData.trans34_r5_1_eq line 1236
  800. def OAI.SharpPlanar.CachedData.trans34_r5_2 line 1237
  801. lemma OAI.SharpPlanar.CachedData.trans34_r5_2_eq line 1238
  802. def OAI.SharpPlanar.CachedData.trans34_r5_3 line 1239
  803. lemma OAI.SharpPlanar.CachedData.trans34_r5_3_eq line 1240
  804. def OAI.SharpPlanar.CachedData.trans34_r5_4 line 1241
  805. lemma OAI.SharpPlanar.CachedData.trans34_r5_4_eq line 1242
  806. def OAI.SharpPlanar.CachedData.trans34_r5_5 line 1243
  807. lemma OAI.SharpPlanar.CachedData.trans34_r5_5_eq line 1244
  808. def OAI.SharpPlanar.CachedData.trans34_r5_6 line 1245
  809. lemma OAI.SharpPlanar.CachedData.trans34_r5_6_eq line 1246
  810. def OAI.SharpPlanar.CachedData.trans34_r5_7 line 1247
  811. lemma OAI.SharpPlanar.CachedData.trans34_r5_7_eq line 1248
  812. def OAI.SharpPlanar.CachedData.trans34_r5_8 line 1249
  813. lemma OAI.SharpPlanar.CachedData.trans34_r5_8_eq line 1250
  814. def OAI.SharpPlanar.CachedData.trans34_r5_9 line 1251
  815. lemma OAI.SharpPlanar.CachedData.trans34_r5_9_eq line 1252
  816. def OAI.SharpPlanar.CachedData.trans34_r5_10 line 1253
  817. lemma OAI.SharpPlanar.CachedData.trans34_r5_10_eq line 1254
  818. def OAI.SharpPlanar.CachedData.trans34_r5_11 line 1255
  819. lemma OAI.SharpPlanar.CachedData.trans34_r5_11_eq line 1256
  820. def OAI.SharpPlanar.CachedData.trans34_r5_12 line 1257
  821. lemma OAI.SharpPlanar.CachedData.trans34_r5_12_eq line 1258
  822. def OAI.SharpPlanar.CachedData.trans34_r5_13 line 1259
  823. lemma OAI.SharpPlanar.CachedData.trans34_r5_13_eq line 1260
  824. def OAI.SharpPlanar.CachedData.trans34_r5_14 line 1261
  825. lemma OAI.SharpPlanar.CachedData.trans34_r5_14_eq line 1262
  826. def OAI.SharpPlanar.CachedData.trans34_r5_15 line 1263
  827. lemma OAI.SharpPlanar.CachedData.trans34_r5_15_eq line 1264
  828. def OAI.SharpPlanar.CachedData.trans34_r5 line 1265
  829. lemma OAI.SharpPlanar.CachedData.trans34_r5_eq line 1266
  830. def OAI.SharpPlanar.CachedData.trans34 line 1284
  831. lemma OAI.SharpPlanar.CachedData.trans34_eq line 1285
  832. lemma OAI.SharpPlanar.CachedData.trans34_contains line 1293
  833. def OAI.SharpPlanar.CachedData.trans35Expr line 1298
  834. def OAI.SharpPlanar.CachedData.trans35_r0_0 line 1299
  835. lemma OAI.SharpPlanar.CachedData.trans35_r0_0_eq line 1300
  836. def OAI.SharpPlanar.CachedData.trans35_r0_1 line 1301
  837. lemma OAI.SharpPlanar.CachedData.trans35_r0_1_eq line 1302
  838. def OAI.SharpPlanar.CachedData.trans35_r0_2 line 1303
  839. lemma OAI.SharpPlanar.CachedData.trans35_r0_2_eq line 1304
  840. def OAI.SharpPlanar.CachedData.trans35_r0_3 line 1305
  841. lemma OAI.SharpPlanar.CachedData.trans35_r0_3_eq line 1306
  842. def OAI.SharpPlanar.CachedData.trans35_r0_4 line 1307
  843. lemma OAI.SharpPlanar.CachedData.trans35_r0_4_eq line 1308
  844. def OAI.SharpPlanar.CachedData.trans35_r0_5 line 1309
  845. lemma OAI.SharpPlanar.CachedData.trans35_r0_5_eq line 1310
  846. def OAI.SharpPlanar.CachedData.trans35_r0_6 line 1311
  847. lemma OAI.SharpPlanar.CachedData.trans35_r0_6_eq line 1312
  848. def OAI.SharpPlanar.CachedData.trans35_r0_7 line 1313
  849. lemma OAI.SharpPlanar.CachedData.trans35_r0_7_eq line 1314
  850. def OAI.SharpPlanar.CachedData.trans35_r0_8 line 1315
  851. lemma OAI.SharpPlanar.CachedData.trans35_r0_8_eq line 1316
  852. def OAI.SharpPlanar.CachedData.trans35_r0_9 line 1317
  853. lemma OAI.SharpPlanar.CachedData.trans35_r0_9_eq line 1318
  854. def OAI.SharpPlanar.CachedData.trans35_r0_10 line 1319
  855. lemma OAI.SharpPlanar.CachedData.trans35_r0_10_eq line 1320
  856. def OAI.SharpPlanar.CachedData.trans35_r0_11 line 1321
  857. lemma OAI.SharpPlanar.CachedData.trans35_r0_11_eq line 1322
  858. def OAI.SharpPlanar.CachedData.trans35_r0_12 line 1323
  859. lemma OAI.SharpPlanar.CachedData.trans35_r0_12_eq line 1324
  860. def OAI.SharpPlanar.CachedData.trans35_r0_13 line 1325
  861. lemma OAI.SharpPlanar.CachedData.trans35_r0_13_eq line 1326
  862. def OAI.SharpPlanar.CachedData.trans35_r0_14 line 1327
  863. lemma OAI.SharpPlanar.CachedData.trans35_r0_14_eq line 1328
  864. def OAI.SharpPlanar.CachedData.trans35_r0_15 line 1329
  865. lemma OAI.SharpPlanar.CachedData.trans35_r0_15_eq line 1330
  866. def OAI.SharpPlanar.CachedData.trans35_r0 line 1331
  867. lemma OAI.SharpPlanar.CachedData.trans35_r0_eq line 1332
  868. def OAI.SharpPlanar.CachedData.trans35_r1_0 line 1350
  869. lemma OAI.SharpPlanar.CachedData.trans35_r1_0_eq line 1351
  870. def OAI.SharpPlanar.CachedData.trans35_r1_1 line 1352
  871. lemma OAI.SharpPlanar.CachedData.trans35_r1_1_eq line 1353
  872. def OAI.SharpPlanar.CachedData.trans35_r1_2 line 1354
  873. lemma OAI.SharpPlanar.CachedData.trans35_r1_2_eq line 1355
  874. def OAI.SharpPlanar.CachedData.trans35_r1_3 line 1356
  875. lemma OAI.SharpPlanar.CachedData.trans35_r1_3_eq line 1357
  876. def OAI.SharpPlanar.CachedData.trans35_r1_4 line 1358
  877. lemma OAI.SharpPlanar.CachedData.trans35_r1_4_eq line 1359
  878. def OAI.SharpPlanar.CachedData.trans35_r1_5 line 1360
  879. lemma OAI.SharpPlanar.CachedData.trans35_r1_5_eq line 1361
  880. def OAI.SharpPlanar.CachedData.trans35_r1_6 line 1362
  881. lemma OAI.SharpPlanar.CachedData.trans35_r1_6_eq line 1363
  882. def OAI.SharpPlanar.CachedData.trans35_r1_7 line 1364
  883. lemma OAI.SharpPlanar.CachedData.trans35_r1_7_eq line 1365
  884. def OAI.SharpPlanar.CachedData.trans35_r1_8 line 1366
  885. lemma OAI.SharpPlanar.CachedData.trans35_r1_8_eq line 1367
  886. def OAI.SharpPlanar.CachedData.trans35_r1_9 line 1368
  887. lemma OAI.SharpPlanar.CachedData.trans35_r1_9_eq line 1369
  888. def OAI.SharpPlanar.CachedData.trans35_r1_10 line 1370
  889. lemma OAI.SharpPlanar.CachedData.trans35_r1_10_eq line 1371
  890. def OAI.SharpPlanar.CachedData.trans35_r1_11 line 1372
  891. lemma OAI.SharpPlanar.CachedData.trans35_r1_11_eq line 1373
  892. def OAI.SharpPlanar.CachedData.trans35_r1_12 line 1374
  893. lemma OAI.SharpPlanar.CachedData.trans35_r1_12_eq line 1375
  894. def OAI.SharpPlanar.CachedData.trans35_r1_13 line 1376
  895. lemma OAI.SharpPlanar.CachedData.trans35_r1_13_eq line 1377
  896. def OAI.SharpPlanar.CachedData.trans35_r1_14 line 1378
  897. lemma OAI.SharpPlanar.CachedData.trans35_r1_14_eq line 1379
  898. def OAI.SharpPlanar.CachedData.trans35_r1_15 line 1380
  899. lemma OAI.SharpPlanar.CachedData.trans35_r1_15_eq line 1381
  900. def OAI.SharpPlanar.CachedData.trans35_r1 line 1382
  901. lemma OAI.SharpPlanar.CachedData.trans35_r1_eq line 1383
  902. def OAI.SharpPlanar.CachedData.trans35_r2_0 line 1401
  903. lemma OAI.SharpPlanar.CachedData.trans35_r2_0_eq line 1402
  904. def OAI.SharpPlanar.CachedData.trans35_r2_1 line 1403
  905. lemma OAI.SharpPlanar.CachedData.trans35_r2_1_eq line 1404
  906. def OAI.SharpPlanar.CachedData.trans35_r2_2 line 1405
  907. lemma OAI.SharpPlanar.CachedData.trans35_r2_2_eq line 1406
  908. def OAI.SharpPlanar.CachedData.trans35_r2_3 line 1407
  909. lemma OAI.SharpPlanar.CachedData.trans35_r2_3_eq line 1408
  910. def OAI.SharpPlanar.CachedData.trans35_r2_4 line 1409
  911. lemma OAI.SharpPlanar.CachedData.trans35_r2_4_eq line 1410
  912. def OAI.SharpPlanar.CachedData.trans35_r2_5 line 1411
  913. lemma OAI.SharpPlanar.CachedData.trans35_r2_5_eq line 1412
  914. def OAI.SharpPlanar.CachedData.trans35_r2_6 line 1413
  915. lemma OAI.SharpPlanar.CachedData.trans35_r2_6_eq line 1414
  916. def OAI.SharpPlanar.CachedData.trans35_r2_7 line 1415
  917. lemma OAI.SharpPlanar.CachedData.trans35_r2_7_eq line 1416
  918. def OAI.SharpPlanar.CachedData.trans35_r2_8 line 1417
  919. lemma OAI.SharpPlanar.CachedData.trans35_r2_8_eq line 1418
  920. def OAI.SharpPlanar.CachedData.trans35_r2_9 line 1419
  921. lemma OAI.SharpPlanar.CachedData.trans35_r2_9_eq line 1420
  922. def OAI.SharpPlanar.CachedData.trans35_r2_10 line 1421
  923. lemma OAI.SharpPlanar.CachedData.trans35_r2_10_eq line 1422
  924. def OAI.SharpPlanar.CachedData.trans35_r2_11 line 1423
  925. lemma OAI.SharpPlanar.CachedData.trans35_r2_11_eq line 1424
  926. def OAI.SharpPlanar.CachedData.trans35_r2_12 line 1425
  927. lemma OAI.SharpPlanar.CachedData.trans35_r2_12_eq line 1426
  928. def OAI.SharpPlanar.CachedData.trans35_r2_13 line 1427
  929. lemma OAI.SharpPlanar.CachedData.trans35_r2_13_eq line 1428
  930. def OAI.SharpPlanar.CachedData.trans35_r2_14 line 1429
  931. lemma OAI.SharpPlanar.CachedData.trans35_r2_14_eq line 1430
  932. def OAI.SharpPlanar.CachedData.trans35_r2_15 line 1431
  933. lemma OAI.SharpPlanar.CachedData.trans35_r2_15_eq line 1432
  934. def OAI.SharpPlanar.CachedData.trans35_r2 line 1433
  935. lemma OAI.SharpPlanar.CachedData.trans35_r2_eq line 1434
  936. def OAI.SharpPlanar.CachedData.trans35_r3_0 line 1452
  937. lemma OAI.SharpPlanar.CachedData.trans35_r3_0_eq line 1453
  938. def OAI.SharpPlanar.CachedData.trans35_r3_1 line 1454
  939. lemma OAI.SharpPlanar.CachedData.trans35_r3_1_eq line 1455
  940. def OAI.SharpPlanar.CachedData.trans35_r3_2 line 1456
  941. lemma OAI.SharpPlanar.CachedData.trans35_r3_2_eq line 1457
  942. def OAI.SharpPlanar.CachedData.trans35_r3_3 line 1458
  943. lemma OAI.SharpPlanar.CachedData.trans35_r3_3_eq line 1459
  944. def OAI.SharpPlanar.CachedData.trans35_r3_4 line 1460
  945. lemma OAI.SharpPlanar.CachedData.trans35_r3_4_eq line 1461
  946. def OAI.SharpPlanar.CachedData.trans35_r3_5 line 1462
  947. lemma OAI.SharpPlanar.CachedData.trans35_r3_5_eq line 1463
  948. def OAI.SharpPlanar.CachedData.trans35_r3_6 line 1464
  949. lemma OAI.SharpPlanar.CachedData.trans35_r3_6_eq line 1465
  950. def OAI.SharpPlanar.CachedData.trans35_r3_7 line 1466
  951. lemma OAI.SharpPlanar.CachedData.trans35_r3_7_eq line 1467
  952. def OAI.SharpPlanar.CachedData.trans35_r3_8 line 1468
  953. lemma OAI.SharpPlanar.CachedData.trans35_r3_8_eq line 1469
  954. def OAI.SharpPlanar.CachedData.trans35_r3_9 line 1470
  955. lemma OAI.SharpPlanar.CachedData.trans35_r3_9_eq line 1471
  956. def OAI.SharpPlanar.CachedData.trans35_r3_10 line 1472
  957. lemma OAI.SharpPlanar.CachedData.trans35_r3_10_eq line 1473
  958. def OAI.SharpPlanar.CachedData.trans35_r3_11 line 1474
  959. lemma OAI.SharpPlanar.CachedData.trans35_r3_11_eq line 1475
  960. def OAI.SharpPlanar.CachedData.trans35_r3_12 line 1476
  961. lemma OAI.SharpPlanar.CachedData.trans35_r3_12_eq line 1477
  962. def OAI.SharpPlanar.CachedData.trans35_r3_13 line 1478
  963. lemma OAI.SharpPlanar.CachedData.trans35_r3_13_eq line 1479
  964. def OAI.SharpPlanar.CachedData.trans35_r3_14 line 1480
  965. lemma OAI.SharpPlanar.CachedData.trans35_r3_14_eq line 1481
  966. def OAI.SharpPlanar.CachedData.trans35_r3_15 line 1482
  967. lemma OAI.SharpPlanar.CachedData.trans35_r3_15_eq line 1483
  968. def OAI.SharpPlanar.CachedData.trans35_r3 line 1484
  969. lemma OAI.SharpPlanar.CachedData.trans35_r3_eq line 1485
  970. def OAI.SharpPlanar.CachedData.trans35_r4_0 line 1503
  971. lemma OAI.SharpPlanar.CachedData.trans35_r4_0_eq line 1504
  972. def OAI.SharpPlanar.CachedData.trans35_r4_1 line 1505
  973. lemma OAI.SharpPlanar.CachedData.trans35_r4_1_eq line 1506
  974. def OAI.SharpPlanar.CachedData.trans35_r4_2 line 1507
  975. lemma OAI.SharpPlanar.CachedData.trans35_r4_2_eq line 1508
  976. def OAI.SharpPlanar.CachedData.trans35_r4_3 line 1509
  977. lemma OAI.SharpPlanar.CachedData.trans35_r4_3_eq line 1510
  978. def OAI.SharpPlanar.CachedData.trans35_r4_4 line 1511
  979. lemma OAI.SharpPlanar.CachedData.trans35_r4_4_eq line 1512
  980. def OAI.SharpPlanar.CachedData.trans35_r4_5 line 1513
  981. lemma OAI.SharpPlanar.CachedData.trans35_r4_5_eq line 1514
  982. def OAI.SharpPlanar.CachedData.trans35_r4_6 line 1515
  983. lemma OAI.SharpPlanar.CachedData.trans35_r4_6_eq line 1516
  984. def OAI.SharpPlanar.CachedData.trans35_r4_7 line 1517
  985. lemma OAI.SharpPlanar.CachedData.trans35_r4_7_eq line 1518
  986. def OAI.SharpPlanar.CachedData.trans35_r4_8 line 1519
  987. lemma OAI.SharpPlanar.CachedData.trans35_r4_8_eq line 1520
  988. def OAI.SharpPlanar.CachedData.trans35_r4_9 line 1521
  989. lemma OAI.SharpPlanar.CachedData.trans35_r4_9_eq line 1522
  990. def OAI.SharpPlanar.CachedData.trans35_r4_10 line 1523
  991. lemma OAI.SharpPlanar.CachedData.trans35_r4_10_eq line 1524
  992. def OAI.SharpPlanar.CachedData.trans35_r4_11 line 1525
  993. lemma OAI.SharpPlanar.CachedData.trans35_r4_11_eq line 1526
  994. def OAI.SharpPlanar.CachedData.trans35_r4_12 line 1527
  995. lemma OAI.SharpPlanar.CachedData.trans35_r4_12_eq line 1528
  996. def OAI.SharpPlanar.CachedData.trans35_r4_13 line 1529
  997. lemma OAI.SharpPlanar.CachedData.trans35_r4_13_eq line 1530
  998. def OAI.SharpPlanar.CachedData.trans35_r4_14 line 1531
  999. lemma OAI.SharpPlanar.CachedData.trans35_r4_14_eq line 1532
  1000. def OAI.SharpPlanar.CachedData.trans35_r4_15 line 1533
  1001. lemma OAI.SharpPlanar.CachedData.trans35_r4_15_eq line 1534
  1002. def OAI.SharpPlanar.CachedData.trans35_r4 line 1535
  1003. lemma OAI.SharpPlanar.CachedData.trans35_r4_eq line 1536
  1004. def OAI.SharpPlanar.CachedData.trans35_r5_0 line 1554
  1005. lemma OAI.SharpPlanar.CachedData.trans35_r5_0_eq line 1555
  1006. def OAI.SharpPlanar.CachedData.trans35_r5_1 line 1556
  1007. lemma OAI.SharpPlanar.CachedData.trans35_r5_1_eq line 1557
  1008. def OAI.SharpPlanar.CachedData.trans35_r5_2 line 1558
  1009. lemma OAI.SharpPlanar.CachedData.trans35_r5_2_eq line 1559
  1010. def OAI.SharpPlanar.CachedData.trans35_r5_3 line 1560
  1011. lemma OAI.SharpPlanar.CachedData.trans35_r5_3_eq line 1561
  1012. def OAI.SharpPlanar.CachedData.trans35_r5_4 line 1562
  1013. lemma OAI.SharpPlanar.CachedData.trans35_r5_4_eq line 1563
  1014. def OAI.SharpPlanar.CachedData.trans35_r5_5 line 1564
  1015. lemma OAI.SharpPlanar.CachedData.trans35_r5_5_eq line 1565
  1016. def OAI.SharpPlanar.CachedData.trans35_r5_6 line 1566
  1017. lemma OAI.SharpPlanar.CachedData.trans35_r5_6_eq line 1567
  1018. def OAI.SharpPlanar.CachedData.trans35_r5_7 line 1568
  1019. lemma OAI.SharpPlanar.CachedData.trans35_r5_7_eq line 1569
  1020. def OAI.SharpPlanar.CachedData.trans35_r5_8 line 1570
  1021. lemma OAI.SharpPlanar.CachedData.trans35_r5_8_eq line 1571
  1022. def OAI.SharpPlanar.CachedData.trans35_r5_9 line 1572
  1023. lemma OAI.SharpPlanar.CachedData.trans35_r5_9_eq line 1573
  1024. def OAI.SharpPlanar.CachedData.trans35_r5_10 line 1574
  1025. lemma OAI.SharpPlanar.CachedData.trans35_r5_10_eq line 1575
  1026. def OAI.SharpPlanar.CachedData.trans35_r5_11 line 1576
  1027. lemma OAI.SharpPlanar.CachedData.trans35_r5_11_eq line 1577
  1028. def OAI.SharpPlanar.CachedData.trans35_r5_12 line 1578
  1029. lemma OAI.SharpPlanar.CachedData.trans35_r5_12_eq line 1579
  1030. def OAI.SharpPlanar.CachedData.trans35_r5_13 line 1580
  1031. lemma OAI.SharpPlanar.CachedData.trans35_r5_13_eq line 1581
  1032. def OAI.SharpPlanar.CachedData.trans35_r5_14 line 1582
  1033. lemma OAI.SharpPlanar.CachedData.trans35_r5_14_eq line 1583
  1034. def OAI.SharpPlanar.CachedData.trans35_r5_15 line 1584
  1035. lemma OAI.SharpPlanar.CachedData.trans35_r5_15_eq line 1585
  1036. def OAI.SharpPlanar.CachedData.trans35_r5 line 1586
  1037. lemma OAI.SharpPlanar.CachedData.trans35_r5_eq line 1587
  1038. def OAI.SharpPlanar.CachedData.trans35 line 1605
  1039. lemma OAI.SharpPlanar.CachedData.trans35_eq line 1606
  1040. lemma OAI.SharpPlanar.CachedData.trans35_contains line 1614
  1041. def OAI.SharpPlanar.CachedData.trans36Expr line 1619
  1042. def OAI.SharpPlanar.CachedData.trans36_r0_0 line 1620
  1043. lemma OAI.SharpPlanar.CachedData.trans36_r0_0_eq line 1621
  1044. def OAI.SharpPlanar.CachedData.trans36_r0_1 line 1622
  1045. lemma OAI.SharpPlanar.CachedData.trans36_r0_1_eq line 1623
  1046. def OAI.SharpPlanar.CachedData.trans36_r0_2 line 1624
  1047. lemma OAI.SharpPlanar.CachedData.trans36_r0_2_eq line 1625
  1048. def OAI.SharpPlanar.CachedData.trans36_r0_3 line 1626
  1049. lemma OAI.SharpPlanar.CachedData.trans36_r0_3_eq line 1627
  1050. def OAI.SharpPlanar.CachedData.trans36_r0_4 line 1628
  1051. lemma OAI.SharpPlanar.CachedData.trans36_r0_4_eq line 1629
  1052. def OAI.SharpPlanar.CachedData.trans36_r0_5 line 1630
  1053. lemma OAI.SharpPlanar.CachedData.trans36_r0_5_eq line 1631
  1054. def OAI.SharpPlanar.CachedData.trans36_r0_6 line 1632
  1055. lemma OAI.SharpPlanar.CachedData.trans36_r0_6_eq line 1633
  1056. def OAI.SharpPlanar.CachedData.trans36_r0_7 line 1634
  1057. lemma OAI.SharpPlanar.CachedData.trans36_r0_7_eq line 1635
  1058. def OAI.SharpPlanar.CachedData.trans36_r0_8 line 1636
  1059. lemma OAI.SharpPlanar.CachedData.trans36_r0_8_eq line 1637
  1060. def OAI.SharpPlanar.CachedData.trans36_r0_9 line 1638
  1061. lemma OAI.SharpPlanar.CachedData.trans36_r0_9_eq line 1639
  1062. def OAI.SharpPlanar.CachedData.trans36_r0_10 line 1640
  1063. lemma OAI.SharpPlanar.CachedData.trans36_r0_10_eq line 1641
  1064. def OAI.SharpPlanar.CachedData.trans36_r0_11 line 1642
  1065. lemma OAI.SharpPlanar.CachedData.trans36_r0_11_eq line 1643
  1066. def OAI.SharpPlanar.CachedData.trans36_r0_12 line 1644
  1067. lemma OAI.SharpPlanar.CachedData.trans36_r0_12_eq line 1645
  1068. def OAI.SharpPlanar.CachedData.trans36_r0_13 line 1646
  1069. lemma OAI.SharpPlanar.CachedData.trans36_r0_13_eq line 1647
  1070. def OAI.SharpPlanar.CachedData.trans36_r0_14 line 1648
  1071. lemma OAI.SharpPlanar.CachedData.trans36_r0_14_eq line 1649
  1072. def OAI.SharpPlanar.CachedData.trans36_r0_15 line 1650
  1073. lemma OAI.SharpPlanar.CachedData.trans36_r0_15_eq line 1651
  1074. def OAI.SharpPlanar.CachedData.trans36_r0 line 1652
  1075. lemma OAI.SharpPlanar.CachedData.trans36_r0_eq line 1653
  1076. def OAI.SharpPlanar.CachedData.trans36_r1_0 line 1671
  1077. lemma OAI.SharpPlanar.CachedData.trans36_r1_0_eq line 1672
  1078. def OAI.SharpPlanar.CachedData.trans36_r1_1 line 1673
  1079. lemma OAI.SharpPlanar.CachedData.trans36_r1_1_eq line 1674
  1080. def OAI.SharpPlanar.CachedData.trans36_r1_2 line 1675
  1081. lemma OAI.SharpPlanar.CachedData.trans36_r1_2_eq line 1676
  1082. def OAI.SharpPlanar.CachedData.trans36_r1_3 line 1677
  1083. lemma OAI.SharpPlanar.CachedData.trans36_r1_3_eq line 1678
  1084. def OAI.SharpPlanar.CachedData.trans36_r1_4 line 1679
  1085. lemma OAI.SharpPlanar.CachedData.trans36_r1_4_eq line 1680
  1086. def OAI.SharpPlanar.CachedData.trans36_r1_5 line 1681
  1087. lemma OAI.SharpPlanar.CachedData.trans36_r1_5_eq line 1682
  1088. def OAI.SharpPlanar.CachedData.trans36_r1_6 line 1683
  1089. lemma OAI.SharpPlanar.CachedData.trans36_r1_6_eq line 1684
  1090. def OAI.SharpPlanar.CachedData.trans36_r1_7 line 1685
  1091. lemma OAI.SharpPlanar.CachedData.trans36_r1_7_eq line 1686
  1092. def OAI.SharpPlanar.CachedData.trans36_r1_8 line 1687
  1093. lemma OAI.SharpPlanar.CachedData.trans36_r1_8_eq line 1688
  1094. def OAI.SharpPlanar.CachedData.trans36_r1_9 line 1689
  1095. lemma OAI.SharpPlanar.CachedData.trans36_r1_9_eq line 1690
  1096. def OAI.SharpPlanar.CachedData.trans36_r1_10 line 1691
  1097. lemma OAI.SharpPlanar.CachedData.trans36_r1_10_eq line 1692
  1098. def OAI.SharpPlanar.CachedData.trans36_r1_11 line 1693
  1099. lemma OAI.SharpPlanar.CachedData.trans36_r1_11_eq line 1694
  1100. def OAI.SharpPlanar.CachedData.trans36_r1_12 line 1695
  1101. lemma OAI.SharpPlanar.CachedData.trans36_r1_12_eq line 1696
  1102. def OAI.SharpPlanar.CachedData.trans36_r1_13 line 1697
  1103. lemma OAI.SharpPlanar.CachedData.trans36_r1_13_eq line 1698
  1104. def OAI.SharpPlanar.CachedData.trans36_r1_14 line 1699
  1105. lemma OAI.SharpPlanar.CachedData.trans36_r1_14_eq line 1700
  1106. def OAI.SharpPlanar.CachedData.trans36_r1_15 line 1701
  1107. lemma OAI.SharpPlanar.CachedData.trans36_r1_15_eq line 1702
  1108. def OAI.SharpPlanar.CachedData.trans36_r1 line 1703
  1109. lemma OAI.SharpPlanar.CachedData.trans36_r1_eq line 1704
  1110. def OAI.SharpPlanar.CachedData.trans36_r2_0 line 1722
  1111. lemma OAI.SharpPlanar.CachedData.trans36_r2_0_eq line 1723
  1112. def OAI.SharpPlanar.CachedData.trans36_r2_1 line 1724
  1113. lemma OAI.SharpPlanar.CachedData.trans36_r2_1_eq line 1725
  1114. def OAI.SharpPlanar.CachedData.trans36_r2_2 line 1726
  1115. lemma OAI.SharpPlanar.CachedData.trans36_r2_2_eq line 1727
  1116. def OAI.SharpPlanar.CachedData.trans36_r2_3 line 1728
  1117. lemma OAI.SharpPlanar.CachedData.trans36_r2_3_eq line 1729
  1118. def OAI.SharpPlanar.CachedData.trans36_r2_4 line 1730
  1119. lemma OAI.SharpPlanar.CachedData.trans36_r2_4_eq line 1731
  1120. def OAI.SharpPlanar.CachedData.trans36_r2_5 line 1732
  1121. lemma OAI.SharpPlanar.CachedData.trans36_r2_5_eq line 1733
  1122. def OAI.SharpPlanar.CachedData.trans36_r2_6 line 1734
  1123. lemma OAI.SharpPlanar.CachedData.trans36_r2_6_eq line 1735
  1124. def OAI.SharpPlanar.CachedData.trans36_r2_7 line 1736
  1125. lemma OAI.SharpPlanar.CachedData.trans36_r2_7_eq line 1737
  1126. def OAI.SharpPlanar.CachedData.trans36_r2_8 line 1738
  1127. lemma OAI.SharpPlanar.CachedData.trans36_r2_8_eq line 1739
  1128. def OAI.SharpPlanar.CachedData.trans36_r2_9 line 1740
  1129. lemma OAI.SharpPlanar.CachedData.trans36_r2_9_eq line 1741
  1130. def OAI.SharpPlanar.CachedData.trans36_r2_10 line 1742
  1131. lemma OAI.SharpPlanar.CachedData.trans36_r2_10_eq line 1743
  1132. def OAI.SharpPlanar.CachedData.trans36_r2_11 line 1744
  1133. lemma OAI.SharpPlanar.CachedData.trans36_r2_11_eq line 1745
  1134. def OAI.SharpPlanar.CachedData.trans36_r2_12 line 1746
  1135. lemma OAI.SharpPlanar.CachedData.trans36_r2_12_eq line 1747
  1136. def OAI.SharpPlanar.CachedData.trans36_r2_13 line 1748
  1137. lemma OAI.SharpPlanar.CachedData.trans36_r2_13_eq line 1749
  1138. def OAI.SharpPlanar.CachedData.trans36_r2_14 line 1750
  1139. lemma OAI.SharpPlanar.CachedData.trans36_r2_14_eq line 1751
  1140. def OAI.SharpPlanar.CachedData.trans36_r2_15 line 1752
  1141. lemma OAI.SharpPlanar.CachedData.trans36_r2_15_eq line 1753
  1142. def OAI.SharpPlanar.CachedData.trans36_r2 line 1754
  1143. lemma OAI.SharpPlanar.CachedData.trans36_r2_eq line 1755
  1144. def OAI.SharpPlanar.CachedData.trans36_r3_0 line 1773
  1145. lemma OAI.SharpPlanar.CachedData.trans36_r3_0_eq line 1774
  1146. def OAI.SharpPlanar.CachedData.trans36_r3_1 line 1775
  1147. lemma OAI.SharpPlanar.CachedData.trans36_r3_1_eq line 1776
  1148. def OAI.SharpPlanar.CachedData.trans36_r3_2 line 1777
  1149. lemma OAI.SharpPlanar.CachedData.trans36_r3_2_eq line 1778
  1150. def OAI.SharpPlanar.CachedData.trans36_r3_3 line 1779
  1151. lemma OAI.SharpPlanar.CachedData.trans36_r3_3_eq line 1780
  1152. def OAI.SharpPlanar.CachedData.trans36_r3_4 line 1781
  1153. lemma OAI.SharpPlanar.CachedData.trans36_r3_4_eq line 1782
  1154. def OAI.SharpPlanar.CachedData.trans36_r3_5 line 1783
  1155. lemma OAI.SharpPlanar.CachedData.trans36_r3_5_eq line 1784
  1156. def OAI.SharpPlanar.CachedData.trans36_r3_6 line 1785
  1157. lemma OAI.SharpPlanar.CachedData.trans36_r3_6_eq line 1786
  1158. def OAI.SharpPlanar.CachedData.trans36_r3_7 line 1787
  1159. lemma OAI.SharpPlanar.CachedData.trans36_r3_7_eq line 1788
  1160. def OAI.SharpPlanar.CachedData.trans36_r3_8 line 1789
  1161. lemma OAI.SharpPlanar.CachedData.trans36_r3_8_eq line 1790
  1162. def OAI.SharpPlanar.CachedData.trans36_r3_9 line 1791
  1163. lemma OAI.SharpPlanar.CachedData.trans36_r3_9_eq line 1792
  1164. def OAI.SharpPlanar.CachedData.trans36_r3_10 line 1793
  1165. lemma OAI.SharpPlanar.CachedData.trans36_r3_10_eq line 1794
  1166. def OAI.SharpPlanar.CachedData.trans36_r3_11 line 1795
  1167. lemma OAI.SharpPlanar.CachedData.trans36_r3_11_eq line 1796
  1168. def OAI.SharpPlanar.CachedData.trans36_r3_12 line 1797
  1169. lemma OAI.SharpPlanar.CachedData.trans36_r3_12_eq line 1798
  1170. def OAI.SharpPlanar.CachedData.trans36_r3_13 line 1799
  1171. lemma OAI.SharpPlanar.CachedData.trans36_r3_13_eq line 1800
  1172. def OAI.SharpPlanar.CachedData.trans36_r3_14 line 1801
  1173. lemma OAI.SharpPlanar.CachedData.trans36_r3_14_eq line 1802
  1174. def OAI.SharpPlanar.CachedData.trans36_r3_15 line 1803
  1175. lemma OAI.SharpPlanar.CachedData.trans36_r3_15_eq line 1804
  1176. def OAI.SharpPlanar.CachedData.trans36_r3 line 1805
  1177. lemma OAI.SharpPlanar.CachedData.trans36_r3_eq line 1806
  1178. def OAI.SharpPlanar.CachedData.trans36_r4_0 line 1824
  1179. lemma OAI.SharpPlanar.CachedData.trans36_r4_0_eq line 1825
  1180. def OAI.SharpPlanar.CachedData.trans36_r4_1 line 1826
  1181. lemma OAI.SharpPlanar.CachedData.trans36_r4_1_eq line 1827
  1182. def OAI.SharpPlanar.CachedData.trans36_r4_2 line 1828
  1183. lemma OAI.SharpPlanar.CachedData.trans36_r4_2_eq line 1829
  1184. def OAI.SharpPlanar.CachedData.trans36_r4_3 line 1830
  1185. lemma OAI.SharpPlanar.CachedData.trans36_r4_3_eq line 1831
  1186. def OAI.SharpPlanar.CachedData.trans36_r4_4 line 1832
  1187. lemma OAI.SharpPlanar.CachedData.trans36_r4_4_eq line 1833
  1188. def OAI.SharpPlanar.CachedData.trans36_r4_5 line 1834
  1189. lemma OAI.SharpPlanar.CachedData.trans36_r4_5_eq line 1835
  1190. def OAI.SharpPlanar.CachedData.trans36_r4_6 line 1836
  1191. lemma OAI.SharpPlanar.CachedData.trans36_r4_6_eq line 1837
  1192. def OAI.SharpPlanar.CachedData.trans36_r4_7 line 1838
  1193. lemma OAI.SharpPlanar.CachedData.trans36_r4_7_eq line 1839
  1194. def OAI.SharpPlanar.CachedData.trans36_r4_8 line 1840
  1195. lemma OAI.SharpPlanar.CachedData.trans36_r4_8_eq line 1841
  1196. def OAI.SharpPlanar.CachedData.trans36_r4_9 line 1842
  1197. lemma OAI.SharpPlanar.CachedData.trans36_r4_9_eq line 1843
  1198. def OAI.SharpPlanar.CachedData.trans36_r4_10 line 1844
  1199. lemma OAI.SharpPlanar.CachedData.trans36_r4_10_eq line 1845
  1200. def OAI.SharpPlanar.CachedData.trans36_r4_11 line 1846
  1201. lemma OAI.SharpPlanar.CachedData.trans36_r4_11_eq line 1847
  1202. def OAI.SharpPlanar.CachedData.trans36_r4_12 line 1848
  1203. lemma OAI.SharpPlanar.CachedData.trans36_r4_12_eq line 1849
  1204. def OAI.SharpPlanar.CachedData.trans36_r4_13 line 1850
  1205. lemma OAI.SharpPlanar.CachedData.trans36_r4_13_eq line 1851
  1206. def OAI.SharpPlanar.CachedData.trans36_r4_14 line 1852
  1207. lemma OAI.SharpPlanar.CachedData.trans36_r4_14_eq line 1853
  1208. def OAI.SharpPlanar.CachedData.trans36_r4_15 line 1854
  1209. lemma OAI.SharpPlanar.CachedData.trans36_r4_15_eq line 1855
  1210. def OAI.SharpPlanar.CachedData.trans36_r4 line 1856
  1211. lemma OAI.SharpPlanar.CachedData.trans36_r4_eq line 1857
  1212. def OAI.SharpPlanar.CachedData.trans36_r5_0 line 1875
  1213. lemma OAI.SharpPlanar.CachedData.trans36_r5_0_eq line 1876
  1214. def OAI.SharpPlanar.CachedData.trans36_r5_1 line 1877
  1215. lemma OAI.SharpPlanar.CachedData.trans36_r5_1_eq line 1878
  1216. def OAI.SharpPlanar.CachedData.trans36_r5_2 line 1879
  1217. lemma OAI.SharpPlanar.CachedData.trans36_r5_2_eq line 1880
  1218. def OAI.SharpPlanar.CachedData.trans36_r5_3 line 1881
  1219. lemma OAI.SharpPlanar.CachedData.trans36_r5_3_eq line 1882
  1220. def OAI.SharpPlanar.CachedData.trans36_r5_4 line 1883
  1221. lemma OAI.SharpPlanar.CachedData.trans36_r5_4_eq line 1884
  1222. def OAI.SharpPlanar.CachedData.trans36_r5_5 line 1885
  1223. lemma OAI.SharpPlanar.CachedData.trans36_r5_5_eq line 1886
  1224. def OAI.SharpPlanar.CachedData.trans36_r5_6 line 1887
  1225. lemma OAI.SharpPlanar.CachedData.trans36_r5_6_eq line 1888
  1226. def OAI.SharpPlanar.CachedData.trans36_r5_7 line 1889
  1227. lemma OAI.SharpPlanar.CachedData.trans36_r5_7_eq line 1890
  1228. def OAI.SharpPlanar.CachedData.trans36_r5_8 line 1891
  1229. lemma OAI.SharpPlanar.CachedData.trans36_r5_8_eq line 1892
  1230. def OAI.SharpPlanar.CachedData.trans36_r5_9 line 1893
  1231. lemma OAI.SharpPlanar.CachedData.trans36_r5_9_eq line 1894
  1232. def OAI.SharpPlanar.CachedData.trans36_r5_10 line 1895
  1233. lemma OAI.SharpPlanar.CachedData.trans36_r5_10_eq line 1896
  1234. def OAI.SharpPlanar.CachedData.trans36_r5_11 line 1897
  1235. lemma OAI.SharpPlanar.CachedData.trans36_r5_11_eq line 1898
  1236. def OAI.SharpPlanar.CachedData.trans36_r5_12 line 1899
  1237. lemma OAI.SharpPlanar.CachedData.trans36_r5_12_eq line 1900
  1238. def OAI.SharpPlanar.CachedData.trans36_r5_13 line 1901
  1239. lemma OAI.SharpPlanar.CachedData.trans36_r5_13_eq line 1902
  1240. def OAI.SharpPlanar.CachedData.trans36_r5_14 line 1903
  1241. lemma OAI.SharpPlanar.CachedData.trans36_r5_14_eq line 1904
  1242. def OAI.SharpPlanar.CachedData.trans36_r5_15 line 1905
  1243. lemma OAI.SharpPlanar.CachedData.trans36_r5_15_eq line 1906
  1244. def OAI.SharpPlanar.CachedData.trans36_r5 line 1907
  1245. lemma OAI.SharpPlanar.CachedData.trans36_r5_eq line 1908
  1246. def OAI.SharpPlanar.CachedData.trans36 line 1926
  1247. lemma OAI.SharpPlanar.CachedData.trans36_eq line 1927
  1248. lemma OAI.SharpPlanar.CachedData.trans36_contains line 1935
  1249. def OAI.SharpPlanar.CachedData.trans37Expr line 1940
  1250. def OAI.SharpPlanar.CachedData.trans37_r0_0 line 1941
  1251. lemma OAI.SharpPlanar.CachedData.trans37_r0_0_eq line 1942
  1252. def OAI.SharpPlanar.CachedData.trans37_r0_1 line 1943
  1253. lemma OAI.SharpPlanar.CachedData.trans37_r0_1_eq line 1944
  1254. def OAI.SharpPlanar.CachedData.trans37_r0_2 line 1945
  1255. lemma OAI.SharpPlanar.CachedData.trans37_r0_2_eq line 1946
  1256. def OAI.SharpPlanar.CachedData.trans37_r0_3 line 1947
  1257. lemma OAI.SharpPlanar.CachedData.trans37_r0_3_eq line 1948
  1258. def OAI.SharpPlanar.CachedData.trans37_r0_4 line 1949
  1259. lemma OAI.SharpPlanar.CachedData.trans37_r0_4_eq line 1950
  1260. def OAI.SharpPlanar.CachedData.trans37_r0_5 line 1951
  1261. lemma OAI.SharpPlanar.CachedData.trans37_r0_5_eq line 1952
  1262. def OAI.SharpPlanar.CachedData.trans37_r0_6 line 1953
  1263. lemma OAI.SharpPlanar.CachedData.trans37_r0_6_eq line 1954
  1264. def OAI.SharpPlanar.CachedData.trans37_r0_7 line 1955
  1265. lemma OAI.SharpPlanar.CachedData.trans37_r0_7_eq line 1956
  1266. def OAI.SharpPlanar.CachedData.trans37_r0_8 line 1957
  1267. lemma OAI.SharpPlanar.CachedData.trans37_r0_8_eq line 1958
  1268. def OAI.SharpPlanar.CachedData.trans37_r0_9 line 1959
  1269. lemma OAI.SharpPlanar.CachedData.trans37_r0_9_eq line 1960
  1270. def OAI.SharpPlanar.CachedData.trans37_r0_10 line 1961
  1271. lemma OAI.SharpPlanar.CachedData.trans37_r0_10_eq line 1962
  1272. def OAI.SharpPlanar.CachedData.trans37_r0_11 line 1963
  1273. lemma OAI.SharpPlanar.CachedData.trans37_r0_11_eq line 1964
  1274. def OAI.SharpPlanar.CachedData.trans37_r0_12 line 1965
  1275. lemma OAI.SharpPlanar.CachedData.trans37_r0_12_eq line 1966
  1276. def OAI.SharpPlanar.CachedData.trans37_r0_13 line 1967
  1277. lemma OAI.SharpPlanar.CachedData.trans37_r0_13_eq line 1968
  1278. def OAI.SharpPlanar.CachedData.trans37_r0_14 line 1969
  1279. lemma OAI.SharpPlanar.CachedData.trans37_r0_14_eq line 1970
  1280. def OAI.SharpPlanar.CachedData.trans37_r0_15 line 1971
  1281. lemma OAI.SharpPlanar.CachedData.trans37_r0_15_eq line 1972
  1282. def OAI.SharpPlanar.CachedData.trans37_r0 line 1973
  1283. lemma OAI.SharpPlanar.CachedData.trans37_r0_eq line 1974
  1284. def OAI.SharpPlanar.CachedData.trans37_r1_0 line 1992
  1285. lemma OAI.SharpPlanar.CachedData.trans37_r1_0_eq line 1993
  1286. def OAI.SharpPlanar.CachedData.trans37_r1_1 line 1994
  1287. lemma OAI.SharpPlanar.CachedData.trans37_r1_1_eq line 1995
  1288. def OAI.SharpPlanar.CachedData.trans37_r1_2 line 1996
  1289. lemma OAI.SharpPlanar.CachedData.trans37_r1_2_eq line 1997
  1290. def OAI.SharpPlanar.CachedData.trans37_r1_3 line 1998
  1291. lemma OAI.SharpPlanar.CachedData.trans37_r1_3_eq line 1999
  1292. def OAI.SharpPlanar.CachedData.trans37_r1_4 line 2000
  1293. lemma OAI.SharpPlanar.CachedData.trans37_r1_4_eq line 2001
  1294. def OAI.SharpPlanar.CachedData.trans37_r1_5 line 2002
  1295. lemma OAI.SharpPlanar.CachedData.trans37_r1_5_eq line 2003
  1296. def OAI.SharpPlanar.CachedData.trans37_r1_6 line 2004
  1297. lemma OAI.SharpPlanar.CachedData.trans37_r1_6_eq line 2005
  1298. def OAI.SharpPlanar.CachedData.trans37_r1_7 line 2006
  1299. lemma OAI.SharpPlanar.CachedData.trans37_r1_7_eq line 2007
  1300. def OAI.SharpPlanar.CachedData.trans37_r1_8 line 2008
  1301. lemma OAI.SharpPlanar.CachedData.trans37_r1_8_eq line 2009
  1302. def OAI.SharpPlanar.CachedData.trans37_r1_9 line 2010
  1303. lemma OAI.SharpPlanar.CachedData.trans37_r1_9_eq line 2011
  1304. def OAI.SharpPlanar.CachedData.trans37_r1_10 line 2012
  1305. lemma OAI.SharpPlanar.CachedData.trans37_r1_10_eq line 2013
  1306. def OAI.SharpPlanar.CachedData.trans37_r1_11 line 2014
  1307. lemma OAI.SharpPlanar.CachedData.trans37_r1_11_eq line 2015
  1308. def OAI.SharpPlanar.CachedData.trans37_r1_12 line 2016
  1309. lemma OAI.SharpPlanar.CachedData.trans37_r1_12_eq line 2017
  1310. def OAI.SharpPlanar.CachedData.trans37_r1_13 line 2018
  1311. lemma OAI.SharpPlanar.CachedData.trans37_r1_13_eq line 2019
  1312. def OAI.SharpPlanar.CachedData.trans37_r1_14 line 2020
  1313. lemma OAI.SharpPlanar.CachedData.trans37_r1_14_eq line 2021
  1314. def OAI.SharpPlanar.CachedData.trans37_r1_15 line 2022
  1315. lemma OAI.SharpPlanar.CachedData.trans37_r1_15_eq line 2023
  1316. def OAI.SharpPlanar.CachedData.trans37_r1 line 2024
  1317. lemma OAI.SharpPlanar.CachedData.trans37_r1_eq line 2025
  1318. def OAI.SharpPlanar.CachedData.trans37_r2_0 line 2043
  1319. lemma OAI.SharpPlanar.CachedData.trans37_r2_0_eq line 2044
  1320. def OAI.SharpPlanar.CachedData.trans37_r2_1 line 2045
  1321. lemma OAI.SharpPlanar.CachedData.trans37_r2_1_eq line 2046
  1322. def OAI.SharpPlanar.CachedData.trans37_r2_2 line 2047
  1323. lemma OAI.SharpPlanar.CachedData.trans37_r2_2_eq line 2048
  1324. def OAI.SharpPlanar.CachedData.trans37_r2_3 line 2049
  1325. lemma OAI.SharpPlanar.CachedData.trans37_r2_3_eq line 2050
  1326. def OAI.SharpPlanar.CachedData.trans37_r2_4 line 2051
  1327. lemma OAI.SharpPlanar.CachedData.trans37_r2_4_eq line 2052
  1328. def OAI.SharpPlanar.CachedData.trans37_r2_5 line 2053
  1329. lemma OAI.SharpPlanar.CachedData.trans37_r2_5_eq line 2054
  1330. def OAI.SharpPlanar.CachedData.trans37_r2_6 line 2055
  1331. lemma OAI.SharpPlanar.CachedData.trans37_r2_6_eq line 2056
  1332. def OAI.SharpPlanar.CachedData.trans37_r2_7 line 2057
  1333. lemma OAI.SharpPlanar.CachedData.trans37_r2_7_eq line 2058
  1334. def OAI.SharpPlanar.CachedData.trans37_r2_8 line 2059
  1335. lemma OAI.SharpPlanar.CachedData.trans37_r2_8_eq line 2060
  1336. def OAI.SharpPlanar.CachedData.trans37_r2_9 line 2061
  1337. lemma OAI.SharpPlanar.CachedData.trans37_r2_9_eq line 2062
  1338. def OAI.SharpPlanar.CachedData.trans37_r2_10 line 2063
  1339. lemma OAI.SharpPlanar.CachedData.trans37_r2_10_eq line 2064
  1340. def OAI.SharpPlanar.CachedData.trans37_r2_11 line 2065
  1341. lemma OAI.SharpPlanar.CachedData.trans37_r2_11_eq line 2066
  1342. def OAI.SharpPlanar.CachedData.trans37_r2_12 line 2067
  1343. lemma OAI.SharpPlanar.CachedData.trans37_r2_12_eq line 2068
  1344. def OAI.SharpPlanar.CachedData.trans37_r2_13 line 2069
  1345. lemma OAI.SharpPlanar.CachedData.trans37_r2_13_eq line 2070
  1346. def OAI.SharpPlanar.CachedData.trans37_r2_14 line 2071
  1347. lemma OAI.SharpPlanar.CachedData.trans37_r2_14_eq line 2072
  1348. def OAI.SharpPlanar.CachedData.trans37_r2_15 line 2073
  1349. lemma OAI.SharpPlanar.CachedData.trans37_r2_15_eq line 2074
  1350. def OAI.SharpPlanar.CachedData.trans37_r2 line 2075
  1351. lemma OAI.SharpPlanar.CachedData.trans37_r2_eq line 2076
  1352. def OAI.SharpPlanar.CachedData.trans37_r3_0 line 2094
  1353. lemma OAI.SharpPlanar.CachedData.trans37_r3_0_eq line 2095
  1354. def OAI.SharpPlanar.CachedData.trans37_r3_1 line 2096
  1355. lemma OAI.SharpPlanar.CachedData.trans37_r3_1_eq line 2097
  1356. def OAI.SharpPlanar.CachedData.trans37_r3_2 line 2098
  1357. lemma OAI.SharpPlanar.CachedData.trans37_r3_2_eq line 2099
  1358. def OAI.SharpPlanar.CachedData.trans37_r3_3 line 2100
  1359. lemma OAI.SharpPlanar.CachedData.trans37_r3_3_eq line 2101
  1360. def OAI.SharpPlanar.CachedData.trans37_r3_4 line 2102
  1361. lemma OAI.SharpPlanar.CachedData.trans37_r3_4_eq line 2103
  1362. def OAI.SharpPlanar.CachedData.trans37_r3_5 line 2104
  1363. lemma OAI.SharpPlanar.CachedData.trans37_r3_5_eq line 2105
  1364. def OAI.SharpPlanar.CachedData.trans37_r3_6 line 2106
  1365. lemma OAI.SharpPlanar.CachedData.trans37_r3_6_eq line 2107
  1366. def OAI.SharpPlanar.CachedData.trans37_r3_7 line 2108
  1367. lemma OAI.SharpPlanar.CachedData.trans37_r3_7_eq line 2109
  1368. def OAI.SharpPlanar.CachedData.trans37_r3_8 line 2110
  1369. lemma OAI.SharpPlanar.CachedData.trans37_r3_8_eq line 2111
  1370. def OAI.SharpPlanar.CachedData.trans37_r3_9 line 2112
  1371. lemma OAI.SharpPlanar.CachedData.trans37_r3_9_eq line 2113
  1372. def OAI.SharpPlanar.CachedData.trans37_r3_10 line 2114
  1373. lemma OAI.SharpPlanar.CachedData.trans37_r3_10_eq line 2115
  1374. def OAI.SharpPlanar.CachedData.trans37_r3_11 line 2116
  1375. lemma OAI.SharpPlanar.CachedData.trans37_r3_11_eq line 2117
  1376. def OAI.SharpPlanar.CachedData.trans37_r3_12 line 2118
  1377. lemma OAI.SharpPlanar.CachedData.trans37_r3_12_eq line 2119
  1378. def OAI.SharpPlanar.CachedData.trans37_r3_13 line 2120
  1379. lemma OAI.SharpPlanar.CachedData.trans37_r3_13_eq line 2121
  1380. def OAI.SharpPlanar.CachedData.trans37_r3_14 line 2122
  1381. lemma OAI.SharpPlanar.CachedData.trans37_r3_14_eq line 2123
  1382. def OAI.SharpPlanar.CachedData.trans37_r3_15 line 2124
  1383. lemma OAI.SharpPlanar.CachedData.trans37_r3_15_eq line 2125
  1384. def OAI.SharpPlanar.CachedData.trans37_r3 line 2126
  1385. lemma OAI.SharpPlanar.CachedData.trans37_r3_eq line 2127
  1386. def OAI.SharpPlanar.CachedData.trans37_r4_0 line 2145
  1387. lemma OAI.SharpPlanar.CachedData.trans37_r4_0_eq line 2146
  1388. def OAI.SharpPlanar.CachedData.trans37_r4_1 line 2147
  1389. lemma OAI.SharpPlanar.CachedData.trans37_r4_1_eq line 2148
  1390. def OAI.SharpPlanar.CachedData.trans37_r4_2 line 2149
  1391. lemma OAI.SharpPlanar.CachedData.trans37_r4_2_eq line 2150
  1392. def OAI.SharpPlanar.CachedData.trans37_r4_3 line 2151
  1393. lemma OAI.SharpPlanar.CachedData.trans37_r4_3_eq line 2152
  1394. def OAI.SharpPlanar.CachedData.trans37_r4_4 line 2153
  1395. lemma OAI.SharpPlanar.CachedData.trans37_r4_4_eq line 2154
  1396. def OAI.SharpPlanar.CachedData.trans37_r4_5 line 2155
  1397. lemma OAI.SharpPlanar.CachedData.trans37_r4_5_eq line 2156
  1398. def OAI.SharpPlanar.CachedData.trans37_r4_6 line 2157
  1399. lemma OAI.SharpPlanar.CachedData.trans37_r4_6_eq line 2158
  1400. def OAI.SharpPlanar.CachedData.trans37_r4_7 line 2159
  1401. lemma OAI.SharpPlanar.CachedData.trans37_r4_7_eq line 2160
  1402. def OAI.SharpPlanar.CachedData.trans37_r4_8 line 2161
  1403. lemma OAI.SharpPlanar.CachedData.trans37_r4_8_eq line 2162
  1404. def OAI.SharpPlanar.CachedData.trans37_r4_9 line 2163
  1405. lemma OAI.SharpPlanar.CachedData.trans37_r4_9_eq line 2164
  1406. def OAI.SharpPlanar.CachedData.trans37_r4_10 line 2165
  1407. lemma OAI.SharpPlanar.CachedData.trans37_r4_10_eq line 2166
  1408. def OAI.SharpPlanar.CachedData.trans37_r4_11 line 2167
  1409. lemma OAI.SharpPlanar.CachedData.trans37_r4_11_eq line 2168
  1410. def OAI.SharpPlanar.CachedData.trans37_r4_12 line 2169
  1411. lemma OAI.SharpPlanar.CachedData.trans37_r4_12_eq line 2170
  1412. def OAI.SharpPlanar.CachedData.trans37_r4_13 line 2171
  1413. lemma OAI.SharpPlanar.CachedData.trans37_r4_13_eq line 2172
  1414. def OAI.SharpPlanar.CachedData.trans37_r4_14 line 2173
  1415. lemma OAI.SharpPlanar.CachedData.trans37_r4_14_eq line 2174
  1416. def OAI.SharpPlanar.CachedData.trans37_r4_15 line 2175
  1417. lemma OAI.SharpPlanar.CachedData.trans37_r4_15_eq line 2176
  1418. def OAI.SharpPlanar.CachedData.trans37_r4 line 2177
  1419. lemma OAI.SharpPlanar.CachedData.trans37_r4_eq line 2178
  1420. def OAI.SharpPlanar.CachedData.trans37_r5_0 line 2196
  1421. lemma OAI.SharpPlanar.CachedData.trans37_r5_0_eq line 2197
  1422. def OAI.SharpPlanar.CachedData.trans37_r5_1 line 2198
  1423. lemma OAI.SharpPlanar.CachedData.trans37_r5_1_eq line 2199
  1424. def OAI.SharpPlanar.CachedData.trans37_r5_2 line 2200
  1425. lemma OAI.SharpPlanar.CachedData.trans37_r5_2_eq line 2201
  1426. def OAI.SharpPlanar.CachedData.trans37_r5_3 line 2202
  1427. lemma OAI.SharpPlanar.CachedData.trans37_r5_3_eq line 2203
  1428. def OAI.SharpPlanar.CachedData.trans37_r5_4 line 2204
  1429. lemma OAI.SharpPlanar.CachedData.trans37_r5_4_eq line 2205
  1430. def OAI.SharpPlanar.CachedData.trans37_r5_5 line 2206
  1431. lemma OAI.SharpPlanar.CachedData.trans37_r5_5_eq line 2207
  1432. def OAI.SharpPlanar.CachedData.trans37_r5_6 line 2208
  1433. lemma OAI.SharpPlanar.CachedData.trans37_r5_6_eq line 2209
  1434. def OAI.SharpPlanar.CachedData.trans37_r5_7 line 2210
  1435. lemma OAI.SharpPlanar.CachedData.trans37_r5_7_eq line 2211
  1436. def OAI.SharpPlanar.CachedData.trans37_r5_8 line 2212
  1437. lemma OAI.SharpPlanar.CachedData.trans37_r5_8_eq line 2213
  1438. def OAI.SharpPlanar.CachedData.trans37_r5_9 line 2214
  1439. lemma OAI.SharpPlanar.CachedData.trans37_r5_9_eq line 2215
  1440. def OAI.SharpPlanar.CachedData.trans37_r5_10 line 2216
  1441. lemma OAI.SharpPlanar.CachedData.trans37_r5_10_eq line 2217
  1442. def OAI.SharpPlanar.CachedData.trans37_r5_11 line 2218
  1443. lemma OAI.SharpPlanar.CachedData.trans37_r5_11_eq line 2219
  1444. def OAI.SharpPlanar.CachedData.trans37_r5_12 line 2220
  1445. lemma OAI.SharpPlanar.CachedData.trans37_r5_12_eq line 2221
  1446. def OAI.SharpPlanar.CachedData.trans37_r5_13 line 2222
  1447. lemma OAI.SharpPlanar.CachedData.trans37_r5_13_eq line 2223
  1448. def OAI.SharpPlanar.CachedData.trans37_r5_14 line 2224
  1449. lemma OAI.SharpPlanar.CachedData.trans37_r5_14_eq line 2225
  1450. def OAI.SharpPlanar.CachedData.trans37_r5_15 line 2226
  1451. lemma OAI.SharpPlanar.CachedData.trans37_r5_15_eq line 2227
  1452. def OAI.SharpPlanar.CachedData.trans37_r5 line 2228
  1453. lemma OAI.SharpPlanar.CachedData.trans37_r5_eq line 2229
  1454. def OAI.SharpPlanar.CachedData.trans37 line 2247
  1455. lemma OAI.SharpPlanar.CachedData.trans37_eq line 2248
  1456. lemma OAI.SharpPlanar.CachedData.trans37_contains line 2256
  1457. def OAI.SharpPlanar.CachedData.trans38Expr line 2261
  1458. def OAI.SharpPlanar.CachedData.trans38_r0_0 line 2262
  1459. lemma OAI.SharpPlanar.CachedData.trans38_r0_0_eq line 2263
  1460. def OAI.SharpPlanar.CachedData.trans38_r0_1 line 2264
  1461. lemma OAI.SharpPlanar.CachedData.trans38_r0_1_eq line 2265
  1462. def OAI.SharpPlanar.CachedData.trans38_r0_2 line 2266
  1463. lemma OAI.SharpPlanar.CachedData.trans38_r0_2_eq line 2267
  1464. def OAI.SharpPlanar.CachedData.trans38_r0_3 line 2268
  1465. lemma OAI.SharpPlanar.CachedData.trans38_r0_3_eq line 2269
  1466. def OAI.SharpPlanar.CachedData.trans38_r0_4 line 2270
  1467. lemma OAI.SharpPlanar.CachedData.trans38_r0_4_eq line 2271
  1468. def OAI.SharpPlanar.CachedData.trans38_r0_5 line 2272
  1469. lemma OAI.SharpPlanar.CachedData.trans38_r0_5_eq line 2273
  1470. def OAI.SharpPlanar.CachedData.trans38_r0_6 line 2274
  1471. lemma OAI.SharpPlanar.CachedData.trans38_r0_6_eq line 2275
  1472. def OAI.SharpPlanar.CachedData.trans38_r0_7 line 2276
  1473. lemma OAI.SharpPlanar.CachedData.trans38_r0_7_eq line 2277
  1474. def OAI.SharpPlanar.CachedData.trans38_r0_8 line 2278
  1475. lemma OAI.SharpPlanar.CachedData.trans38_r0_8_eq line 2279
  1476. def OAI.SharpPlanar.CachedData.trans38_r0_9 line 2280
  1477. lemma OAI.SharpPlanar.CachedData.trans38_r0_9_eq line 2281
  1478. def OAI.SharpPlanar.CachedData.trans38_r0_10 line 2282
  1479. lemma OAI.SharpPlanar.CachedData.trans38_r0_10_eq line 2283
  1480. def OAI.SharpPlanar.CachedData.trans38_r0_11 line 2284
  1481. lemma OAI.SharpPlanar.CachedData.trans38_r0_11_eq line 2285
  1482. def OAI.SharpPlanar.CachedData.trans38_r0_12 line 2286
  1483. lemma OAI.SharpPlanar.CachedData.trans38_r0_12_eq line 2287
  1484. def OAI.SharpPlanar.CachedData.trans38_r0_13 line 2288
  1485. lemma OAI.SharpPlanar.CachedData.trans38_r0_13_eq line 2289
  1486. def OAI.SharpPlanar.CachedData.trans38_r0_14 line 2290
  1487. lemma OAI.SharpPlanar.CachedData.trans38_r0_14_eq line 2291
  1488. def OAI.SharpPlanar.CachedData.trans38_r0_15 line 2292
  1489. lemma OAI.SharpPlanar.CachedData.trans38_r0_15_eq line 2293
  1490. def OAI.SharpPlanar.CachedData.trans38_r0 line 2294
  1491. lemma OAI.SharpPlanar.CachedData.trans38_r0_eq line 2295
  1492. def OAI.SharpPlanar.CachedData.trans38_r1_0 line 2313
  1493. lemma OAI.SharpPlanar.CachedData.trans38_r1_0_eq line 2314
  1494. def OAI.SharpPlanar.CachedData.trans38_r1_1 line 2315
  1495. lemma OAI.SharpPlanar.CachedData.trans38_r1_1_eq line 2316
  1496. def OAI.SharpPlanar.CachedData.trans38_r1_2 line 2317
  1497. lemma OAI.SharpPlanar.CachedData.trans38_r1_2_eq line 2318
  1498. def OAI.SharpPlanar.CachedData.trans38_r1_3 line 2319
  1499. lemma OAI.SharpPlanar.CachedData.trans38_r1_3_eq line 2320
  1500. def OAI.SharpPlanar.CachedData.trans38_r1_4 line 2321
  1501. lemma OAI.SharpPlanar.CachedData.trans38_r1_4_eq line 2322
  1502. def OAI.SharpPlanar.CachedData.trans38_r1_5 line 2323
  1503. lemma OAI.SharpPlanar.CachedData.trans38_r1_5_eq line 2324
  1504. def OAI.SharpPlanar.CachedData.trans38_r1_6 line 2325
  1505. lemma OAI.SharpPlanar.CachedData.trans38_r1_6_eq line 2326
  1506. def OAI.SharpPlanar.CachedData.trans38_r1_7 line 2327
  1507. lemma OAI.SharpPlanar.CachedData.trans38_r1_7_eq line 2328
  1508. def OAI.SharpPlanar.CachedData.trans38_r1_8 line 2329
  1509. lemma OAI.SharpPlanar.CachedData.trans38_r1_8_eq line 2330
  1510. def OAI.SharpPlanar.CachedData.trans38_r1_9 line 2331
  1511. lemma OAI.SharpPlanar.CachedData.trans38_r1_9_eq line 2332
  1512. def OAI.SharpPlanar.CachedData.trans38_r1_10 line 2333
  1513. lemma OAI.SharpPlanar.CachedData.trans38_r1_10_eq line 2334
  1514. def OAI.SharpPlanar.CachedData.trans38_r1_11 line 2335
  1515. lemma OAI.SharpPlanar.CachedData.trans38_r1_11_eq line 2336
  1516. def OAI.SharpPlanar.CachedData.trans38_r1_12 line 2337
  1517. lemma OAI.SharpPlanar.CachedData.trans38_r1_12_eq line 2338
  1518. def OAI.SharpPlanar.CachedData.trans38_r1_13 line 2339
  1519. lemma OAI.SharpPlanar.CachedData.trans38_r1_13_eq line 2340
  1520. def OAI.SharpPlanar.CachedData.trans38_r1_14 line 2341
  1521. lemma OAI.SharpPlanar.CachedData.trans38_r1_14_eq line 2342
  1522. def OAI.SharpPlanar.CachedData.trans38_r1_15 line 2343
  1523. lemma OAI.SharpPlanar.CachedData.trans38_r1_15_eq line 2344
  1524. def OAI.SharpPlanar.CachedData.trans38_r1 line 2345
  1525. lemma OAI.SharpPlanar.CachedData.trans38_r1_eq line 2346
  1526. def OAI.SharpPlanar.CachedData.trans38_r2_0 line 2364
  1527. lemma OAI.SharpPlanar.CachedData.trans38_r2_0_eq line 2365
  1528. def OAI.SharpPlanar.CachedData.trans38_r2_1 line 2366
  1529. lemma OAI.SharpPlanar.CachedData.trans38_r2_1_eq line 2367
  1530. def OAI.SharpPlanar.CachedData.trans38_r2_2 line 2368
  1531. lemma OAI.SharpPlanar.CachedData.trans38_r2_2_eq line 2369
  1532. def OAI.SharpPlanar.CachedData.trans38_r2_3 line 2370
  1533. lemma OAI.SharpPlanar.CachedData.trans38_r2_3_eq line 2371
  1534. def OAI.SharpPlanar.CachedData.trans38_r2_4 line 2372
  1535. lemma OAI.SharpPlanar.CachedData.trans38_r2_4_eq line 2373
  1536. def OAI.SharpPlanar.CachedData.trans38_r2_5 line 2374
  1537. lemma OAI.SharpPlanar.CachedData.trans38_r2_5_eq line 2375
  1538. def OAI.SharpPlanar.CachedData.trans38_r2_6 line 2376
  1539. lemma OAI.SharpPlanar.CachedData.trans38_r2_6_eq line 2377
  1540. def OAI.SharpPlanar.CachedData.trans38_r2_7 line 2378
  1541. lemma OAI.SharpPlanar.CachedData.trans38_r2_7_eq line 2379
  1542. def OAI.SharpPlanar.CachedData.trans38_r2_8 line 2380
  1543. lemma OAI.SharpPlanar.CachedData.trans38_r2_8_eq line 2381
  1544. def OAI.SharpPlanar.CachedData.trans38_r2_9 line 2382
  1545. lemma OAI.SharpPlanar.CachedData.trans38_r2_9_eq line 2383
  1546. def OAI.SharpPlanar.CachedData.trans38_r2_10 line 2384
  1547. lemma OAI.SharpPlanar.CachedData.trans38_r2_10_eq line 2385
  1548. def OAI.SharpPlanar.CachedData.trans38_r2_11 line 2386
  1549. lemma OAI.SharpPlanar.CachedData.trans38_r2_11_eq line 2387
  1550. def OAI.SharpPlanar.CachedData.trans38_r2_12 line 2388
  1551. lemma OAI.SharpPlanar.CachedData.trans38_r2_12_eq line 2389
  1552. def OAI.SharpPlanar.CachedData.trans38_r2_13 line 2390
  1553. lemma OAI.SharpPlanar.CachedData.trans38_r2_13_eq line 2391
  1554. def OAI.SharpPlanar.CachedData.trans38_r2_14 line 2392
  1555. lemma OAI.SharpPlanar.CachedData.trans38_r2_14_eq line 2393
  1556. def OAI.SharpPlanar.CachedData.trans38_r2_15 line 2394
  1557. lemma OAI.SharpPlanar.CachedData.trans38_r2_15_eq line 2395
  1558. def OAI.SharpPlanar.CachedData.trans38_r2 line 2396
  1559. lemma OAI.SharpPlanar.CachedData.trans38_r2_eq line 2397
  1560. def OAI.SharpPlanar.CachedData.trans38_r3_0 line 2415
  1561. lemma OAI.SharpPlanar.CachedData.trans38_r3_0_eq line 2416
  1562. def OAI.SharpPlanar.CachedData.trans38_r3_1 line 2417
  1563. lemma OAI.SharpPlanar.CachedData.trans38_r3_1_eq line 2418
  1564. def OAI.SharpPlanar.CachedData.trans38_r3_2 line 2419
  1565. lemma OAI.SharpPlanar.CachedData.trans38_r3_2_eq line 2420
  1566. def OAI.SharpPlanar.CachedData.trans38_r3_3 line 2421
  1567. lemma OAI.SharpPlanar.CachedData.trans38_r3_3_eq line 2422
  1568. def OAI.SharpPlanar.CachedData.trans38_r3_4 line 2423
  1569. lemma OAI.SharpPlanar.CachedData.trans38_r3_4_eq line 2424
  1570. def OAI.SharpPlanar.CachedData.trans38_r3_5 line 2425
  1571. lemma OAI.SharpPlanar.CachedData.trans38_r3_5_eq line 2426
  1572. def OAI.SharpPlanar.CachedData.trans38_r3_6 line 2427
  1573. lemma OAI.SharpPlanar.CachedData.trans38_r3_6_eq line 2428
  1574. def OAI.SharpPlanar.CachedData.trans38_r3_7 line 2429
  1575. lemma OAI.SharpPlanar.CachedData.trans38_r3_7_eq line 2430
  1576. def OAI.SharpPlanar.CachedData.trans38_r3_8 line 2431
  1577. lemma OAI.SharpPlanar.CachedData.trans38_r3_8_eq line 2432
  1578. def OAI.SharpPlanar.CachedData.trans38_r3_9 line 2433
  1579. lemma OAI.SharpPlanar.CachedData.trans38_r3_9_eq line 2434
  1580. def OAI.SharpPlanar.CachedData.trans38_r3_10 line 2435
  1581. lemma OAI.SharpPlanar.CachedData.trans38_r3_10_eq line 2436
  1582. def OAI.SharpPlanar.CachedData.trans38_r3_11 line 2437
  1583. lemma OAI.SharpPlanar.CachedData.trans38_r3_11_eq line 2438
  1584. def OAI.SharpPlanar.CachedData.trans38_r3_12 line 2439
  1585. lemma OAI.SharpPlanar.CachedData.trans38_r3_12_eq line 2440
  1586. def OAI.SharpPlanar.CachedData.trans38_r3_13 line 2441
  1587. lemma OAI.SharpPlanar.CachedData.trans38_r3_13_eq line 2442
  1588. def OAI.SharpPlanar.CachedData.trans38_r3_14 line 2443
  1589. lemma OAI.SharpPlanar.CachedData.trans38_r3_14_eq line 2444
  1590. def OAI.SharpPlanar.CachedData.trans38_r3_15 line 2445
  1591. lemma OAI.SharpPlanar.CachedData.trans38_r3_15_eq line 2446
  1592. def OAI.SharpPlanar.CachedData.trans38_r3 line 2447
  1593. lemma OAI.SharpPlanar.CachedData.trans38_r3_eq line 2448
  1594. def OAI.SharpPlanar.CachedData.trans38_r4_0 line 2466
  1595. lemma OAI.SharpPlanar.CachedData.trans38_r4_0_eq line 2467
  1596. def OAI.SharpPlanar.CachedData.trans38_r4_1 line 2468
  1597. lemma OAI.SharpPlanar.CachedData.trans38_r4_1_eq line 2469
  1598. def OAI.SharpPlanar.CachedData.trans38_r4_2 line 2470
  1599. lemma OAI.SharpPlanar.CachedData.trans38_r4_2_eq line 2471
  1600. def OAI.SharpPlanar.CachedData.trans38_r4_3 line 2472
  1601. lemma OAI.SharpPlanar.CachedData.trans38_r4_3_eq line 2473
  1602. def OAI.SharpPlanar.CachedData.trans38_r4_4 line 2474
  1603. lemma OAI.SharpPlanar.CachedData.trans38_r4_4_eq line 2475
  1604. def OAI.SharpPlanar.CachedData.trans38_r4_5 line 2476
  1605. lemma OAI.SharpPlanar.CachedData.trans38_r4_5_eq line 2477
  1606. def OAI.SharpPlanar.CachedData.trans38_r4_6 line 2478
  1607. lemma OAI.SharpPlanar.CachedData.trans38_r4_6_eq line 2479
  1608. def OAI.SharpPlanar.CachedData.trans38_r4_7 line 2480
  1609. lemma OAI.SharpPlanar.CachedData.trans38_r4_7_eq line 2481
  1610. def OAI.SharpPlanar.CachedData.trans38_r4_8 line 2482
  1611. lemma OAI.SharpPlanar.CachedData.trans38_r4_8_eq line 2483
  1612. def OAI.SharpPlanar.CachedData.trans38_r4_9 line 2484
  1613. lemma OAI.SharpPlanar.CachedData.trans38_r4_9_eq line 2485
  1614. def OAI.SharpPlanar.CachedData.trans38_r4_10 line 2486
  1615. lemma OAI.SharpPlanar.CachedData.trans38_r4_10_eq line 2487
  1616. def OAI.SharpPlanar.CachedData.trans38_r4_11 line 2488
  1617. lemma OAI.SharpPlanar.CachedData.trans38_r4_11_eq line 2489
  1618. def OAI.SharpPlanar.CachedData.trans38_r4_12 line 2490
  1619. lemma OAI.SharpPlanar.CachedData.trans38_r4_12_eq line 2491
  1620. def OAI.SharpPlanar.CachedData.trans38_r4_13 line 2492
  1621. lemma OAI.SharpPlanar.CachedData.trans38_r4_13_eq line 2493
  1622. def OAI.SharpPlanar.CachedData.trans38_r4_14 line 2494
  1623. lemma OAI.SharpPlanar.CachedData.trans38_r4_14_eq line 2495
  1624. def OAI.SharpPlanar.CachedData.trans38_r4_15 line 2496
  1625. lemma OAI.SharpPlanar.CachedData.trans38_r4_15_eq line 2497
  1626. def OAI.SharpPlanar.CachedData.trans38_r4 line 2498
  1627. lemma OAI.SharpPlanar.CachedData.trans38_r4_eq line 2499
  1628. def OAI.SharpPlanar.CachedData.trans38_r5_0 line 2517
  1629. lemma OAI.SharpPlanar.CachedData.trans38_r5_0_eq line 2518
  1630. def OAI.SharpPlanar.CachedData.trans38_r5_1 line 2519
  1631. lemma OAI.SharpPlanar.CachedData.trans38_r5_1_eq line 2520
  1632. def OAI.SharpPlanar.CachedData.trans38_r5_2 line 2521
  1633. lemma OAI.SharpPlanar.CachedData.trans38_r5_2_eq line 2522
  1634. def OAI.SharpPlanar.CachedData.trans38_r5_3 line 2523
  1635. lemma OAI.SharpPlanar.CachedData.trans38_r5_3_eq line 2524
  1636. def OAI.SharpPlanar.CachedData.trans38_r5_4 line 2525
  1637. lemma OAI.SharpPlanar.CachedData.trans38_r5_4_eq line 2526
  1638. def OAI.SharpPlanar.CachedData.trans38_r5_5 line 2527
  1639. lemma OAI.SharpPlanar.CachedData.trans38_r5_5_eq line 2528
  1640. def OAI.SharpPlanar.CachedData.trans38_r5_6 line 2529
  1641. lemma OAI.SharpPlanar.CachedData.trans38_r5_6_eq line 2530
  1642. def OAI.SharpPlanar.CachedData.trans38_r5_7 line 2531
  1643. lemma OAI.SharpPlanar.CachedData.trans38_r5_7_eq line 2532
  1644. def OAI.SharpPlanar.CachedData.trans38_r5_8 line 2533
  1645. lemma OAI.SharpPlanar.CachedData.trans38_r5_8_eq line 2534
  1646. def OAI.SharpPlanar.CachedData.trans38_r5_9 line 2535
  1647. lemma OAI.SharpPlanar.CachedData.trans38_r5_9_eq line 2536
  1648. def OAI.SharpPlanar.CachedData.trans38_r5_10 line 2537
  1649. lemma OAI.SharpPlanar.CachedData.trans38_r5_10_eq line 2538
  1650. def OAI.SharpPlanar.CachedData.trans38_r5_11 line 2539
  1651. lemma OAI.SharpPlanar.CachedData.trans38_r5_11_eq line 2540
  1652. def OAI.SharpPlanar.CachedData.trans38_r5_12 line 2541
  1653. lemma OAI.SharpPlanar.CachedData.trans38_r5_12_eq line 2542
  1654. def OAI.SharpPlanar.CachedData.trans38_r5_13 line 2543
  1655. lemma OAI.SharpPlanar.CachedData.trans38_r5_13_eq line 2544
  1656. def OAI.SharpPlanar.CachedData.trans38_r5_14 line 2545
  1657. lemma OAI.SharpPlanar.CachedData.trans38_r5_14_eq line 2546
  1658. def OAI.SharpPlanar.CachedData.trans38_r5_15 line 2547
  1659. lemma OAI.SharpPlanar.CachedData.trans38_r5_15_eq line 2548
  1660. def OAI.SharpPlanar.CachedData.trans38_r5 line 2549
  1661. lemma OAI.SharpPlanar.CachedData.trans38_r5_eq line 2550
  1662. def OAI.SharpPlanar.CachedData.trans38 line 2568
  1663. lemma OAI.SharpPlanar.CachedData.trans38_eq line 2569
  1664. lemma OAI.SharpPlanar.CachedData.trans38_contains line 2577
  1665. def OAI.SharpPlanar.CachedData.trans39Expr line 2582
  1666. def OAI.SharpPlanar.CachedData.trans39_r0_0 line 2583
  1667. lemma OAI.SharpPlanar.CachedData.trans39_r0_0_eq line 2584
  1668. def OAI.SharpPlanar.CachedData.trans39_r0_1 line 2585
  1669. lemma OAI.SharpPlanar.CachedData.trans39_r0_1_eq line 2586
  1670. def OAI.SharpPlanar.CachedData.trans39_r0_2 line 2587
  1671. lemma OAI.SharpPlanar.CachedData.trans39_r0_2_eq line 2588
  1672. def OAI.SharpPlanar.CachedData.trans39_r0_3 line 2589
  1673. lemma OAI.SharpPlanar.CachedData.trans39_r0_3_eq line 2590
  1674. def OAI.SharpPlanar.CachedData.trans39_r0_4 line 2591
  1675. lemma OAI.SharpPlanar.CachedData.trans39_r0_4_eq line 2592
  1676. def OAI.SharpPlanar.CachedData.trans39_r0_5 line 2593
  1677. lemma OAI.SharpPlanar.CachedData.trans39_r0_5_eq line 2594
  1678. def OAI.SharpPlanar.CachedData.trans39_r0_6 line 2595
  1679. lemma OAI.SharpPlanar.CachedData.trans39_r0_6_eq line 2596
  1680. def OAI.SharpPlanar.CachedData.trans39_r0_7 line 2597
  1681. lemma OAI.SharpPlanar.CachedData.trans39_r0_7_eq line 2598
  1682. def OAI.SharpPlanar.CachedData.trans39_r0_8 line 2599
  1683. lemma OAI.SharpPlanar.CachedData.trans39_r0_8_eq line 2600
  1684. def OAI.SharpPlanar.CachedData.trans39_r0_9 line 2601
  1685. lemma OAI.SharpPlanar.CachedData.trans39_r0_9_eq line 2602
  1686. def OAI.SharpPlanar.CachedData.trans39_r0_10 line 2603
  1687. lemma OAI.SharpPlanar.CachedData.trans39_r0_10_eq line 2604
  1688. def OAI.SharpPlanar.CachedData.trans39_r0_11 line 2605
  1689. lemma OAI.SharpPlanar.CachedData.trans39_r0_11_eq line 2606
  1690. def OAI.SharpPlanar.CachedData.trans39_r0_12 line 2607
  1691. lemma OAI.SharpPlanar.CachedData.trans39_r0_12_eq line 2608
  1692. def OAI.SharpPlanar.CachedData.trans39_r0_13 line 2609
  1693. lemma OAI.SharpPlanar.CachedData.trans39_r0_13_eq line 2610
  1694. def OAI.SharpPlanar.CachedData.trans39_r0_14 line 2611
  1695. lemma OAI.SharpPlanar.CachedData.trans39_r0_14_eq line 2612
  1696. def OAI.SharpPlanar.CachedData.trans39_r0_15 line 2613
  1697. lemma OAI.SharpPlanar.CachedData.trans39_r0_15_eq line 2614
  1698. def OAI.SharpPlanar.CachedData.trans39_r0 line 2615
  1699. lemma OAI.SharpPlanar.CachedData.trans39_r0_eq line 2616
  1700. def OAI.SharpPlanar.CachedData.trans39_r1_0 line 2634
  1701. lemma OAI.SharpPlanar.CachedData.trans39_r1_0_eq line 2635
  1702. def OAI.SharpPlanar.CachedData.trans39_r1_1 line 2636
  1703. lemma OAI.SharpPlanar.CachedData.trans39_r1_1_eq line 2637
  1704. def OAI.SharpPlanar.CachedData.trans39_r1_2 line 2638
  1705. lemma OAI.SharpPlanar.CachedData.trans39_r1_2_eq line 2639
  1706. def OAI.SharpPlanar.CachedData.trans39_r1_3 line 2640
  1707. lemma OAI.SharpPlanar.CachedData.trans39_r1_3_eq line 2641
  1708. def OAI.SharpPlanar.CachedData.trans39_r1_4 line 2642
  1709. lemma OAI.SharpPlanar.CachedData.trans39_r1_4_eq line 2643
  1710. def OAI.SharpPlanar.CachedData.trans39_r1_5 line 2644
  1711. lemma OAI.SharpPlanar.CachedData.trans39_r1_5_eq line 2645
  1712. def OAI.SharpPlanar.CachedData.trans39_r1_6 line 2646
  1713. lemma OAI.SharpPlanar.CachedData.trans39_r1_6_eq line 2647
  1714. def OAI.SharpPlanar.CachedData.trans39_r1_7 line 2648
  1715. lemma OAI.SharpPlanar.CachedData.trans39_r1_7_eq line 2649
  1716. def OAI.SharpPlanar.CachedData.trans39_r1_8 line 2650
  1717. lemma OAI.SharpPlanar.CachedData.trans39_r1_8_eq line 2651
  1718. def OAI.SharpPlanar.CachedData.trans39_r1_9 line 2652
  1719. lemma OAI.SharpPlanar.CachedData.trans39_r1_9_eq line 2653
  1720. def OAI.SharpPlanar.CachedData.trans39_r1_10 line 2654
  1721. lemma OAI.SharpPlanar.CachedData.trans39_r1_10_eq line 2655
  1722. def OAI.SharpPlanar.CachedData.trans39_r1_11 line 2656
  1723. lemma OAI.SharpPlanar.CachedData.trans39_r1_11_eq line 2657
  1724. def OAI.SharpPlanar.CachedData.trans39_r1_12 line 2658
  1725. lemma OAI.SharpPlanar.CachedData.trans39_r1_12_eq line 2659
  1726. def OAI.SharpPlanar.CachedData.trans39_r1_13 line 2660
  1727. lemma OAI.SharpPlanar.CachedData.trans39_r1_13_eq line 2661
  1728. def OAI.SharpPlanar.CachedData.trans39_r1_14 line 2662
  1729. lemma OAI.SharpPlanar.CachedData.trans39_r1_14_eq line 2663
  1730. def OAI.SharpPlanar.CachedData.trans39_r1_15 line 2664
  1731. lemma OAI.SharpPlanar.CachedData.trans39_r1_15_eq line 2665
  1732. def OAI.SharpPlanar.CachedData.trans39_r1 line 2666
  1733. lemma OAI.SharpPlanar.CachedData.trans39_r1_eq line 2667
  1734. def OAI.SharpPlanar.CachedData.trans39_r2_0 line 2685
  1735. lemma OAI.SharpPlanar.CachedData.trans39_r2_0_eq line 2686
  1736. def OAI.SharpPlanar.CachedData.trans39_r2_1 line 2687
  1737. lemma OAI.SharpPlanar.CachedData.trans39_r2_1_eq line 2688
  1738. def OAI.SharpPlanar.CachedData.trans39_r2_2 line 2689
  1739. lemma OAI.SharpPlanar.CachedData.trans39_r2_2_eq line 2690
  1740. def OAI.SharpPlanar.CachedData.trans39_r2_3 line 2691
  1741. lemma OAI.SharpPlanar.CachedData.trans39_r2_3_eq line 2692
  1742. def OAI.SharpPlanar.CachedData.trans39_r2_4 line 2693
  1743. lemma OAI.SharpPlanar.CachedData.trans39_r2_4_eq line 2694
  1744. def OAI.SharpPlanar.CachedData.trans39_r2_5 line 2695
  1745. lemma OAI.SharpPlanar.CachedData.trans39_r2_5_eq line 2696
  1746. def OAI.SharpPlanar.CachedData.trans39_r2_6 line 2697
  1747. lemma OAI.SharpPlanar.CachedData.trans39_r2_6_eq line 2698
  1748. def OAI.SharpPlanar.CachedData.trans39_r2_7 line 2699
  1749. lemma OAI.SharpPlanar.CachedData.trans39_r2_7_eq line 2700
  1750. def OAI.SharpPlanar.CachedData.trans39_r2_8 line 2701
  1751. lemma OAI.SharpPlanar.CachedData.trans39_r2_8_eq line 2702
  1752. def OAI.SharpPlanar.CachedData.trans39_r2_9 line 2703
  1753. lemma OAI.SharpPlanar.CachedData.trans39_r2_9_eq line 2704
  1754. def OAI.SharpPlanar.CachedData.trans39_r2_10 line 2705
  1755. lemma OAI.SharpPlanar.CachedData.trans39_r2_10_eq line 2706
  1756. def OAI.SharpPlanar.CachedData.trans39_r2_11 line 2707
  1757. lemma OAI.SharpPlanar.CachedData.trans39_r2_11_eq line 2708
  1758. def OAI.SharpPlanar.CachedData.trans39_r2_12 line 2709
  1759. lemma OAI.SharpPlanar.CachedData.trans39_r2_12_eq line 2710
  1760. def OAI.SharpPlanar.CachedData.trans39_r2_13 line 2711
  1761. lemma OAI.SharpPlanar.CachedData.trans39_r2_13_eq line 2712
  1762. def OAI.SharpPlanar.CachedData.trans39_r2_14 line 2713
  1763. lemma OAI.SharpPlanar.CachedData.trans39_r2_14_eq line 2714
  1764. def OAI.SharpPlanar.CachedData.trans39_r2_15 line 2715
  1765. lemma OAI.SharpPlanar.CachedData.trans39_r2_15_eq line 2716
  1766. def OAI.SharpPlanar.CachedData.trans39_r2 line 2717
  1767. lemma OAI.SharpPlanar.CachedData.trans39_r2_eq line 2718
  1768. def OAI.SharpPlanar.CachedData.trans39_r3_0 line 2736
  1769. lemma OAI.SharpPlanar.CachedData.trans39_r3_0_eq line 2737
  1770. def OAI.SharpPlanar.CachedData.trans39_r3_1 line 2738
  1771. lemma OAI.SharpPlanar.CachedData.trans39_r3_1_eq line 2739
  1772. def OAI.SharpPlanar.CachedData.trans39_r3_2 line 2740
  1773. lemma OAI.SharpPlanar.CachedData.trans39_r3_2_eq line 2741
  1774. def OAI.SharpPlanar.CachedData.trans39_r3_3 line 2742
  1775. lemma OAI.SharpPlanar.CachedData.trans39_r3_3_eq line 2743
  1776. def OAI.SharpPlanar.CachedData.trans39_r3_4 line 2744
  1777. lemma OAI.SharpPlanar.CachedData.trans39_r3_4_eq line 2745
  1778. def OAI.SharpPlanar.CachedData.trans39_r3_5 line 2746
  1779. lemma OAI.SharpPlanar.CachedData.trans39_r3_5_eq line 2747
  1780. def OAI.SharpPlanar.CachedData.trans39_r3_6 line 2748
  1781. lemma OAI.SharpPlanar.CachedData.trans39_r3_6_eq line 2749
  1782. def OAI.SharpPlanar.CachedData.trans39_r3_7 line 2750
  1783. lemma OAI.SharpPlanar.CachedData.trans39_r3_7_eq line 2751
  1784. def OAI.SharpPlanar.CachedData.trans39_r3_8 line 2752
  1785. lemma OAI.SharpPlanar.CachedData.trans39_r3_8_eq line 2753
  1786. def OAI.SharpPlanar.CachedData.trans39_r3_9 line 2754
  1787. lemma OAI.SharpPlanar.CachedData.trans39_r3_9_eq line 2755
  1788. def OAI.SharpPlanar.CachedData.trans39_r3_10 line 2756
  1789. lemma OAI.SharpPlanar.CachedData.trans39_r3_10_eq line 2757
  1790. def OAI.SharpPlanar.CachedData.trans39_r3_11 line 2758
  1791. lemma OAI.SharpPlanar.CachedData.trans39_r3_11_eq line 2759
  1792. def OAI.SharpPlanar.CachedData.trans39_r3_12 line 2760
  1793. lemma OAI.SharpPlanar.CachedData.trans39_r3_12_eq line 2761
  1794. def OAI.SharpPlanar.CachedData.trans39_r3_13 line 2762
  1795. lemma OAI.SharpPlanar.CachedData.trans39_r3_13_eq line 2763
  1796. def OAI.SharpPlanar.CachedData.trans39_r3_14 line 2764
  1797. lemma OAI.SharpPlanar.CachedData.trans39_r3_14_eq line 2765
  1798. def OAI.SharpPlanar.CachedData.trans39_r3_15 line 2766
  1799. lemma OAI.SharpPlanar.CachedData.trans39_r3_15_eq line 2767
  1800. def OAI.SharpPlanar.CachedData.trans39_r3 line 2768
  1801. lemma OAI.SharpPlanar.CachedData.trans39_r3_eq line 2769
  1802. def OAI.SharpPlanar.CachedData.trans39_r4_0 line 2787
  1803. lemma OAI.SharpPlanar.CachedData.trans39_r4_0_eq line 2788
  1804. def OAI.SharpPlanar.CachedData.trans39_r4_1 line 2789
  1805. lemma OAI.SharpPlanar.CachedData.trans39_r4_1_eq line 2790
  1806. def OAI.SharpPlanar.CachedData.trans39_r4_2 line 2791
  1807. lemma OAI.SharpPlanar.CachedData.trans39_r4_2_eq line 2792
  1808. def OAI.SharpPlanar.CachedData.trans39_r4_3 line 2793
  1809. lemma OAI.SharpPlanar.CachedData.trans39_r4_3_eq line 2794
  1810. def OAI.SharpPlanar.CachedData.trans39_r4_4 line 2795
  1811. lemma OAI.SharpPlanar.CachedData.trans39_r4_4_eq line 2796
  1812. def OAI.SharpPlanar.CachedData.trans39_r4_5 line 2797
  1813. lemma OAI.SharpPlanar.CachedData.trans39_r4_5_eq line 2798
  1814. def OAI.SharpPlanar.CachedData.trans39_r4_6 line 2799
  1815. lemma OAI.SharpPlanar.CachedData.trans39_r4_6_eq line 2800
  1816. def OAI.SharpPlanar.CachedData.trans39_r4_7 line 2801
  1817. lemma OAI.SharpPlanar.CachedData.trans39_r4_7_eq line 2802
  1818. def OAI.SharpPlanar.CachedData.trans39_r4_8 line 2803
  1819. lemma OAI.SharpPlanar.CachedData.trans39_r4_8_eq line 2804
  1820. def OAI.SharpPlanar.CachedData.trans39_r4_9 line 2805
  1821. lemma OAI.SharpPlanar.CachedData.trans39_r4_9_eq line 2806
  1822. def OAI.SharpPlanar.CachedData.trans39_r4_10 line 2807
  1823. lemma OAI.SharpPlanar.CachedData.trans39_r4_10_eq line 2808
  1824. def OAI.SharpPlanar.CachedData.trans39_r4_11 line 2809
  1825. lemma OAI.SharpPlanar.CachedData.trans39_r4_11_eq line 2810
  1826. def OAI.SharpPlanar.CachedData.trans39_r4_12 line 2811
  1827. lemma OAI.SharpPlanar.CachedData.trans39_r4_12_eq line 2812
  1828. def OAI.SharpPlanar.CachedData.trans39_r4_13 line 2813
  1829. lemma OAI.SharpPlanar.CachedData.trans39_r4_13_eq line 2814
  1830. def OAI.SharpPlanar.CachedData.trans39_r4_14 line 2815
  1831. lemma OAI.SharpPlanar.CachedData.trans39_r4_14_eq line 2816
  1832. def OAI.SharpPlanar.CachedData.trans39_r4_15 line 2817
  1833. lemma OAI.SharpPlanar.CachedData.trans39_r4_15_eq line 2818
  1834. def OAI.SharpPlanar.CachedData.trans39_r4 line 2819
  1835. lemma OAI.SharpPlanar.CachedData.trans39_r4_eq line 2820
  1836. def OAI.SharpPlanar.CachedData.trans39_r5_0 line 2838
  1837. lemma OAI.SharpPlanar.CachedData.trans39_r5_0_eq line 2839
  1838. def OAI.SharpPlanar.CachedData.trans39_r5_1 line 2840
  1839. lemma OAI.SharpPlanar.CachedData.trans39_r5_1_eq line 2841
  1840. def OAI.SharpPlanar.CachedData.trans39_r5_2 line 2842
  1841. lemma OAI.SharpPlanar.CachedData.trans39_r5_2_eq line 2843
  1842. def OAI.SharpPlanar.CachedData.trans39_r5_3 line 2844
  1843. lemma OAI.SharpPlanar.CachedData.trans39_r5_3_eq line 2845
  1844. def OAI.SharpPlanar.CachedData.trans39_r5_4 line 2846
  1845. lemma OAI.SharpPlanar.CachedData.trans39_r5_4_eq line 2847
  1846. def OAI.SharpPlanar.CachedData.trans39_r5_5 line 2848
  1847. lemma OAI.SharpPlanar.CachedData.trans39_r5_5_eq line 2849
  1848. def OAI.SharpPlanar.CachedData.trans39_r5_6 line 2850
  1849. lemma OAI.SharpPlanar.CachedData.trans39_r5_6_eq line 2851
  1850. def OAI.SharpPlanar.CachedData.trans39_r5_7 line 2852
  1851. lemma OAI.SharpPlanar.CachedData.trans39_r5_7_eq line 2853
  1852. def OAI.SharpPlanar.CachedData.trans39_r5_8 line 2854
  1853. lemma OAI.SharpPlanar.CachedData.trans39_r5_8_eq line 2855
  1854. def OAI.SharpPlanar.CachedData.trans39_r5_9 line 2856
  1855. lemma OAI.SharpPlanar.CachedData.trans39_r5_9_eq line 2857
  1856. def OAI.SharpPlanar.CachedData.trans39_r5_10 line 2858
  1857. lemma OAI.SharpPlanar.CachedData.trans39_r5_10_eq line 2859
  1858. def OAI.SharpPlanar.CachedData.trans39_r5_11 line 2860
  1859. lemma OAI.SharpPlanar.CachedData.trans39_r5_11_eq line 2861
  1860. def OAI.SharpPlanar.CachedData.trans39_r5_12 line 2862
  1861. lemma OAI.SharpPlanar.CachedData.trans39_r5_12_eq line 2863
  1862. def OAI.SharpPlanar.CachedData.trans39_r5_13 line 2864
  1863. lemma OAI.SharpPlanar.CachedData.trans39_r5_13_eq line 2865
  1864. def OAI.SharpPlanar.CachedData.trans39_r5_14 line 2866
  1865. lemma OAI.SharpPlanar.CachedData.trans39_r5_14_eq line 2867
  1866. def OAI.SharpPlanar.CachedData.trans39_r5_15 line 2868
  1867. lemma OAI.SharpPlanar.CachedData.trans39_r5_15_eq line 2869
  1868. def OAI.SharpPlanar.CachedData.trans39_r5 line 2870
  1869. lemma OAI.SharpPlanar.CachedData.trans39_r5_eq line 2871
  1870. def OAI.SharpPlanar.CachedData.trans39 line 2889
  1871. lemma OAI.SharpPlanar.CachedData.trans39_eq line 2890
  1872. lemma OAI.SharpPlanar.CachedData.trans39_contains line 2898
  1873. def OAI.SharpPlanar.CachedData.trans40Expr line 2903
  1874. def OAI.SharpPlanar.CachedData.trans40_r0_0 line 2904
  1875. lemma OAI.SharpPlanar.CachedData.trans40_r0_0_eq line 2905
  1876. def OAI.SharpPlanar.CachedData.trans40_r0_1 line 2906
  1877. lemma OAI.SharpPlanar.CachedData.trans40_r0_1_eq line 2907
  1878. def OAI.SharpPlanar.CachedData.trans40_r0_2 line 2908
  1879. lemma OAI.SharpPlanar.CachedData.trans40_r0_2_eq line 2909
  1880. def OAI.SharpPlanar.CachedData.trans40_r0_3 line 2910
  1881. lemma OAI.SharpPlanar.CachedData.trans40_r0_3_eq line 2911
  1882. def OAI.SharpPlanar.CachedData.trans40_r0_4 line 2912
  1883. lemma OAI.SharpPlanar.CachedData.trans40_r0_4_eq line 2913
  1884. def OAI.SharpPlanar.CachedData.trans40_r0_5 line 2914
  1885. lemma OAI.SharpPlanar.CachedData.trans40_r0_5_eq line 2915
  1886. def OAI.SharpPlanar.CachedData.trans40_r0_6 line 2916
  1887. lemma OAI.SharpPlanar.CachedData.trans40_r0_6_eq line 2917
  1888. def OAI.SharpPlanar.CachedData.trans40_r0_7 line 2918
  1889. lemma OAI.SharpPlanar.CachedData.trans40_r0_7_eq line 2919
  1890. def OAI.SharpPlanar.CachedData.trans40_r0_8 line 2920
  1891. lemma OAI.SharpPlanar.CachedData.trans40_r0_8_eq line 2921
  1892. def OAI.SharpPlanar.CachedData.trans40_r0_9 line 2922
  1893. lemma OAI.SharpPlanar.CachedData.trans40_r0_9_eq line 2923
  1894. def OAI.SharpPlanar.CachedData.trans40_r0_10 line 2924
  1895. lemma OAI.SharpPlanar.CachedData.trans40_r0_10_eq line 2925
  1896. def OAI.SharpPlanar.CachedData.trans40_r0_11 line 2926
  1897. lemma OAI.SharpPlanar.CachedData.trans40_r0_11_eq line 2927
  1898. def OAI.SharpPlanar.CachedData.trans40_r0_12 line 2928
  1899. lemma OAI.SharpPlanar.CachedData.trans40_r0_12_eq line 2929
  1900. def OAI.SharpPlanar.CachedData.trans40_r0_13 line 2930
  1901. lemma OAI.SharpPlanar.CachedData.trans40_r0_13_eq line 2931
  1902. def OAI.SharpPlanar.CachedData.trans40_r0_14 line 2932
  1903. lemma OAI.SharpPlanar.CachedData.trans40_r0_14_eq line 2933
  1904. def OAI.SharpPlanar.CachedData.trans40_r0_15 line 2934
  1905. lemma OAI.SharpPlanar.CachedData.trans40_r0_15_eq line 2935
  1906. def OAI.SharpPlanar.CachedData.trans40_r0 line 2936
  1907. lemma OAI.SharpPlanar.CachedData.trans40_r0_eq line 2937
  1908. def OAI.SharpPlanar.CachedData.trans40_r1_0 line 2955
  1909. lemma OAI.SharpPlanar.CachedData.trans40_r1_0_eq line 2956
  1910. def OAI.SharpPlanar.CachedData.trans40_r1_1 line 2957
  1911. lemma OAI.SharpPlanar.CachedData.trans40_r1_1_eq line 2958
  1912. def OAI.SharpPlanar.CachedData.trans40_r1_2 line 2959
  1913. lemma OAI.SharpPlanar.CachedData.trans40_r1_2_eq line 2960
  1914. def OAI.SharpPlanar.CachedData.trans40_r1_3 line 2961
  1915. lemma OAI.SharpPlanar.CachedData.trans40_r1_3_eq line 2962
  1916. def OAI.SharpPlanar.CachedData.trans40_r1_4 line 2963
  1917. lemma OAI.SharpPlanar.CachedData.trans40_r1_4_eq line 2964
  1918. def OAI.SharpPlanar.CachedData.trans40_r1_5 line 2965
  1919. lemma OAI.SharpPlanar.CachedData.trans40_r1_5_eq line 2966
  1920. def OAI.SharpPlanar.CachedData.trans40_r1_6 line 2967
  1921. lemma OAI.SharpPlanar.CachedData.trans40_r1_6_eq line 2968
  1922. def OAI.SharpPlanar.CachedData.trans40_r1_7 line 2969
  1923. lemma OAI.SharpPlanar.CachedData.trans40_r1_7_eq line 2970
  1924. def OAI.SharpPlanar.CachedData.trans40_r1_8 line 2971
  1925. lemma OAI.SharpPlanar.CachedData.trans40_r1_8_eq line 2972
  1926. def OAI.SharpPlanar.CachedData.trans40_r1_9 line 2973
  1927. lemma OAI.SharpPlanar.CachedData.trans40_r1_9_eq line 2974
  1928. def OAI.SharpPlanar.CachedData.trans40_r1_10 line 2975
  1929. lemma OAI.SharpPlanar.CachedData.trans40_r1_10_eq line 2976
  1930. def OAI.SharpPlanar.CachedData.trans40_r1_11 line 2977
  1931. lemma OAI.SharpPlanar.CachedData.trans40_r1_11_eq line 2978
  1932. def OAI.SharpPlanar.CachedData.trans40_r1_12 line 2979
  1933. lemma OAI.SharpPlanar.CachedData.trans40_r1_12_eq line 2980
  1934. def OAI.SharpPlanar.CachedData.trans40_r1_13 line 2981
  1935. lemma OAI.SharpPlanar.CachedData.trans40_r1_13_eq line 2982
  1936. def OAI.SharpPlanar.CachedData.trans40_r1_14 line 2983
  1937. lemma OAI.SharpPlanar.CachedData.trans40_r1_14_eq line 2984
  1938. def OAI.SharpPlanar.CachedData.trans40_r1_15 line 2985
  1939. lemma OAI.SharpPlanar.CachedData.trans40_r1_15_eq line 2986
  1940. def OAI.SharpPlanar.CachedData.trans40_r1 line 2987
  1941. lemma OAI.SharpPlanar.CachedData.trans40_r1_eq line 2988
  1942. def OAI.SharpPlanar.CachedData.trans40_r2_0 line 3006
  1943. lemma OAI.SharpPlanar.CachedData.trans40_r2_0_eq line 3007
  1944. def OAI.SharpPlanar.CachedData.trans40_r2_1 line 3008
  1945. lemma OAI.SharpPlanar.CachedData.trans40_r2_1_eq line 3009
  1946. def OAI.SharpPlanar.CachedData.trans40_r2_2 line 3010
  1947. lemma OAI.SharpPlanar.CachedData.trans40_r2_2_eq line 3011
  1948. def OAI.SharpPlanar.CachedData.trans40_r2_3 line 3012
  1949. lemma OAI.SharpPlanar.CachedData.trans40_r2_3_eq line 3013
  1950. def OAI.SharpPlanar.CachedData.trans40_r2_4 line 3014
  1951. lemma OAI.SharpPlanar.CachedData.trans40_r2_4_eq line 3015
  1952. def OAI.SharpPlanar.CachedData.trans40_r2_5 line 3016
  1953. lemma OAI.SharpPlanar.CachedData.trans40_r2_5_eq line 3017
  1954. def OAI.SharpPlanar.CachedData.trans40_r2_6 line 3018
  1955. lemma OAI.SharpPlanar.CachedData.trans40_r2_6_eq line 3019
  1956. def OAI.SharpPlanar.CachedData.trans40_r2_7 line 3020
  1957. lemma OAI.SharpPlanar.CachedData.trans40_r2_7_eq line 3021
  1958. def OAI.SharpPlanar.CachedData.trans40_r2_8 line 3022
  1959. lemma OAI.SharpPlanar.CachedData.trans40_r2_8_eq line 3023
  1960. def OAI.SharpPlanar.CachedData.trans40_r2_9 line 3024
  1961. lemma OAI.SharpPlanar.CachedData.trans40_r2_9_eq line 3025
  1962. def OAI.SharpPlanar.CachedData.trans40_r2_10 line 3026
  1963. lemma OAI.SharpPlanar.CachedData.trans40_r2_10_eq line 3027
  1964. def OAI.SharpPlanar.CachedData.trans40_r2_11 line 3028
  1965. lemma OAI.SharpPlanar.CachedData.trans40_r2_11_eq line 3029
  1966. def OAI.SharpPlanar.CachedData.trans40_r2_12 line 3030
  1967. lemma OAI.SharpPlanar.CachedData.trans40_r2_12_eq line 3031
  1968. def OAI.SharpPlanar.CachedData.trans40_r2_13 line 3032
  1969. lemma OAI.SharpPlanar.CachedData.trans40_r2_13_eq line 3033
  1970. def OAI.SharpPlanar.CachedData.trans40_r2_14 line 3034
  1971. lemma OAI.SharpPlanar.CachedData.trans40_r2_14_eq line 3035
  1972. def OAI.SharpPlanar.CachedData.trans40_r2_15 line 3036
  1973. lemma OAI.SharpPlanar.CachedData.trans40_r2_15_eq line 3037
  1974. def OAI.SharpPlanar.CachedData.trans40_r2 line 3038
  1975. lemma OAI.SharpPlanar.CachedData.trans40_r2_eq line 3039
  1976. def OAI.SharpPlanar.CachedData.trans40_r3_0 line 3057
  1977. lemma OAI.SharpPlanar.CachedData.trans40_r3_0_eq line 3058
  1978. def OAI.SharpPlanar.CachedData.trans40_r3_1 line 3059
  1979. lemma OAI.SharpPlanar.CachedData.trans40_r3_1_eq line 3060
  1980. def OAI.SharpPlanar.CachedData.trans40_r3_2 line 3061
  1981. lemma OAI.SharpPlanar.CachedData.trans40_r3_2_eq line 3062
  1982. def OAI.SharpPlanar.CachedData.trans40_r3_3 line 3063
  1983. lemma OAI.SharpPlanar.CachedData.trans40_r3_3_eq line 3064
  1984. def OAI.SharpPlanar.CachedData.trans40_r3_4 line 3065
  1985. lemma OAI.SharpPlanar.CachedData.trans40_r3_4_eq line 3066
  1986. def OAI.SharpPlanar.CachedData.trans40_r3_5 line 3067
  1987. lemma OAI.SharpPlanar.CachedData.trans40_r3_5_eq line 3068
  1988. def OAI.SharpPlanar.CachedData.trans40_r3_6 line 3069
  1989. lemma OAI.SharpPlanar.CachedData.trans40_r3_6_eq line 3070
  1990. def OAI.SharpPlanar.CachedData.trans40_r3_7 line 3071
  1991. lemma OAI.SharpPlanar.CachedData.trans40_r3_7_eq line 3072
  1992. def OAI.SharpPlanar.CachedData.trans40_r3_8 line 3073
  1993. lemma OAI.SharpPlanar.CachedData.trans40_r3_8_eq line 3074
  1994. def OAI.SharpPlanar.CachedData.trans40_r3_9 line 3075
  1995. lemma OAI.SharpPlanar.CachedData.trans40_r3_9_eq line 3076
  1996. def OAI.SharpPlanar.CachedData.trans40_r3_10 line 3077
  1997. lemma OAI.SharpPlanar.CachedData.trans40_r3_10_eq line 3078
  1998. def OAI.SharpPlanar.CachedData.trans40_r3_11 line 3079
  1999. lemma OAI.SharpPlanar.CachedData.trans40_r3_11_eq line 3080
  2000. def OAI.SharpPlanar.CachedData.trans40_r3_12 line 3081
  2001. lemma OAI.SharpPlanar.CachedData.trans40_r3_12_eq line 3082
  2002. def OAI.SharpPlanar.CachedData.trans40_r3_13 line 3083
  2003. lemma OAI.SharpPlanar.CachedData.trans40_r3_13_eq line 3084
  2004. def OAI.SharpPlanar.CachedData.trans40_r3_14 line 3085
  2005. lemma OAI.SharpPlanar.CachedData.trans40_r3_14_eq line 3086
  2006. def OAI.SharpPlanar.CachedData.trans40_r3_15 line 3087
  2007. lemma OAI.SharpPlanar.CachedData.trans40_r3_15_eq line 3088
  2008. def OAI.SharpPlanar.CachedData.trans40_r3 line 3089
  2009. lemma OAI.SharpPlanar.CachedData.trans40_r3_eq line 3090
  2010. def OAI.SharpPlanar.CachedData.trans40_r4_0 line 3108
  2011. lemma OAI.SharpPlanar.CachedData.trans40_r4_0_eq line 3109
  2012. def OAI.SharpPlanar.CachedData.trans40_r4_1 line 3110
  2013. lemma OAI.SharpPlanar.CachedData.trans40_r4_1_eq line 3111
  2014. def OAI.SharpPlanar.CachedData.trans40_r4_2 line 3112
  2015. lemma OAI.SharpPlanar.CachedData.trans40_r4_2_eq line 3113
  2016. def OAI.SharpPlanar.CachedData.trans40_r4_3 line 3114
  2017. lemma OAI.SharpPlanar.CachedData.trans40_r4_3_eq line 3115
  2018. def OAI.SharpPlanar.CachedData.trans40_r4_4 line 3116
  2019. lemma OAI.SharpPlanar.CachedData.trans40_r4_4_eq line 3117
  2020. def OAI.SharpPlanar.CachedData.trans40_r4_5 line 3118
  2021. lemma OAI.SharpPlanar.CachedData.trans40_r4_5_eq line 3119
  2022. def OAI.SharpPlanar.CachedData.trans40_r4_6 line 3120
  2023. lemma OAI.SharpPlanar.CachedData.trans40_r4_6_eq line 3121
  2024. def OAI.SharpPlanar.CachedData.trans40_r4_7 line 3122
  2025. lemma OAI.SharpPlanar.CachedData.trans40_r4_7_eq line 3123
  2026. def OAI.SharpPlanar.CachedData.trans40_r4_8 line 3124
  2027. lemma OAI.SharpPlanar.CachedData.trans40_r4_8_eq line 3125
  2028. def OAI.SharpPlanar.CachedData.trans40_r4_9 line 3126
  2029. lemma OAI.SharpPlanar.CachedData.trans40_r4_9_eq line 3127
  2030. def OAI.SharpPlanar.CachedData.trans40_r4_10 line 3128
  2031. lemma OAI.SharpPlanar.CachedData.trans40_r4_10_eq line 3129
  2032. def OAI.SharpPlanar.CachedData.trans40_r4_11 line 3130
  2033. lemma OAI.SharpPlanar.CachedData.trans40_r4_11_eq line 3131
  2034. def OAI.SharpPlanar.CachedData.trans40_r4_12 line 3132
  2035. lemma OAI.SharpPlanar.CachedData.trans40_r4_12_eq line 3133
  2036. def OAI.SharpPlanar.CachedData.trans40_r4_13 line 3134
  2037. lemma OAI.SharpPlanar.CachedData.trans40_r4_13_eq line 3135
  2038. def OAI.SharpPlanar.CachedData.trans40_r4_14 line 3136
  2039. lemma OAI.SharpPlanar.CachedData.trans40_r4_14_eq line 3137
  2040. def OAI.SharpPlanar.CachedData.trans40_r4_15 line 3138
  2041. lemma OAI.SharpPlanar.CachedData.trans40_r4_15_eq line 3139
  2042. def OAI.SharpPlanar.CachedData.trans40_r4 line 3140
  2043. lemma OAI.SharpPlanar.CachedData.trans40_r4_eq line 3141
  2044. def OAI.SharpPlanar.CachedData.trans40_r5_0 line 3159
  2045. lemma OAI.SharpPlanar.CachedData.trans40_r5_0_eq line 3160
  2046. def OAI.SharpPlanar.CachedData.trans40_r5_1 line 3161
  2047. lemma OAI.SharpPlanar.CachedData.trans40_r5_1_eq line 3162
  2048. def OAI.SharpPlanar.CachedData.trans40_r5_2 line 3163
  2049. lemma OAI.SharpPlanar.CachedData.trans40_r5_2_eq line 3164
  2050. def OAI.SharpPlanar.CachedData.trans40_r5_3 line 3165
  2051. lemma OAI.SharpPlanar.CachedData.trans40_r5_3_eq line 3166
  2052. def OAI.SharpPlanar.CachedData.trans40_r5_4 line 3167
  2053. lemma OAI.SharpPlanar.CachedData.trans40_r5_4_eq line 3168
  2054. def OAI.SharpPlanar.CachedData.trans40_r5_5 line 3169
  2055. lemma OAI.SharpPlanar.CachedData.trans40_r5_5_eq line 3170
  2056. def OAI.SharpPlanar.CachedData.trans40_r5_6 line 3171
  2057. lemma OAI.SharpPlanar.CachedData.trans40_r5_6_eq line 3172
  2058. def OAI.SharpPlanar.CachedData.trans40_r5_7 line 3173
  2059. lemma OAI.SharpPlanar.CachedData.trans40_r5_7_eq line 3174
  2060. def OAI.SharpPlanar.CachedData.trans40_r5_8 line 3175
  2061. lemma OAI.SharpPlanar.CachedData.trans40_r5_8_eq line 3176
  2062. def OAI.SharpPlanar.CachedData.trans40_r5_9 line 3177
  2063. lemma OAI.SharpPlanar.CachedData.trans40_r5_9_eq line 3178
  2064. def OAI.SharpPlanar.CachedData.trans40_r5_10 line 3179
  2065. lemma OAI.SharpPlanar.CachedData.trans40_r5_10_eq line 3180
  2066. def OAI.SharpPlanar.CachedData.trans40_r5_11 line 3181
  2067. lemma OAI.SharpPlanar.CachedData.trans40_r5_11_eq line 3182
  2068. def OAI.SharpPlanar.CachedData.trans40_r5_12 line 3183
  2069. lemma OAI.SharpPlanar.CachedData.trans40_r5_12_eq line 3184
  2070. def OAI.SharpPlanar.CachedData.trans40_r5_13 line 3185
  2071. lemma OAI.SharpPlanar.CachedData.trans40_r5_13_eq line 3186
  2072. def OAI.SharpPlanar.CachedData.trans40_r5_14 line 3187
  2073. lemma OAI.SharpPlanar.CachedData.trans40_r5_14_eq line 3188
  2074. def OAI.SharpPlanar.CachedData.trans40_r5_15 line 3189
  2075. lemma OAI.SharpPlanar.CachedData.trans40_r5_15_eq line 3190
  2076. def OAI.SharpPlanar.CachedData.trans40_r5 line 3191
  2077. lemma OAI.SharpPlanar.CachedData.trans40_r5_eq line 3192
  2078. def OAI.SharpPlanar.CachedData.trans40 line 3210
  2079. lemma OAI.SharpPlanar.CachedData.trans40_eq line 3211
  2080. lemma OAI.SharpPlanar.CachedData.trans40_contains line 3219