MomentPowers5.lean`

2084 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.

def OAI.SharpPlanar.CachedData.mpower0_0 line 15
lemma OAI.SharpPlanar.CachedData.mpower0_0_contains line 16
def OAI.SharpPlanar.CachedData.mpower1_0 line 18
lemma OAI.SharpPlanar.CachedData.mpower1_0_contains line 19
def OAI.SharpPlanar.CachedData.mpower0_1Expr line 21
def OAI.SharpPlanar.CachedData.mpower0_1_r0_0 line 22
lemma OAI.SharpPlanar.CachedData.mpower0_1_r0_0_eq line 23
def OAI.SharpPlanar.CachedData.mpower0_1_r0_1 line 24
lemma OAI.SharpPlanar.CachedData.mpower0_1_r0_1_eq line 25
def OAI.SharpPlanar.CachedData.mpower0_1_r0_2 line 26
lemma OAI.SharpPlanar.CachedData.mpower0_1_r0_2_eq line 27
def OAI.SharpPlanar.CachedData.mpower0_1_r0_3 line 28
lemma OAI.SharpPlanar.CachedData.mpower0_1_r0_3_eq line 29
def OAI.SharpPlanar.CachedData.mpower0_1_r0_4 line 30
lemma OAI.SharpPlanar.CachedData.mpower0_1_r0_4_eq line 31
def OAI.SharpPlanar.CachedData.mpower0_1_r0_5 line 32
lemma OAI.SharpPlanar.CachedData.mpower0_1_r0_5_eq line 33
def OAI.SharpPlanar.CachedData.mpower0_1_r0_6 line 34
lemma OAI.SharpPlanar.CachedData.mpower0_1_r0_6_eq line 35
def OAI.SharpPlanar.CachedData.mpower0_1_r0_7 line 36
lemma OAI.SharpPlanar.CachedData.mpower0_1_r0_7_eq line 37
def OAI.SharpPlanar.CachedData.mpower0_1_r0_8 line 38
lemma OAI.SharpPlanar.CachedData.mpower0_1_r0_8_eq line 39
def OAI.SharpPlanar.CachedData.mpower0_1_r0_9 line 40
lemma OAI.SharpPlanar.CachedData.mpower0_1_r0_9_eq line 41
def OAI.SharpPlanar.CachedData.mpower0_1_r0_10 line 42
lemma OAI.SharpPlanar.CachedData.mpower0_1_r0_10_eq line 43
def OAI.SharpPlanar.CachedData.mpower0_1_r0_11 line 44
lemma OAI.SharpPlanar.CachedData.mpower0_1_r0_11_eq line 45
def OAI.SharpPlanar.CachedData.mpower0_1_r0_12 line 46
lemma OAI.SharpPlanar.CachedData.mpower0_1_r0_12_eq line 47
def OAI.SharpPlanar.CachedData.mpower0_1_r0_13 line 48
lemma OAI.SharpPlanar.CachedData.mpower0_1_r0_13_eq line 49
def OAI.SharpPlanar.CachedData.mpower0_1_r0_14 line 50
lemma OAI.SharpPlanar.CachedData.mpower0_1_r0_14_eq line 51
def OAI.SharpPlanar.CachedData.mpower0_1_r0_15 line 52
lemma OAI.SharpPlanar.CachedData.mpower0_1_r0_15_eq line 53
def OAI.SharpPlanar.CachedData.mpower0_1_r0 line 54
lemma OAI.SharpPlanar.CachedData.mpower0_1_r0_eq line 55
def OAI.SharpPlanar.CachedData.mpower0_1_r1_0 line 73
lemma OAI.SharpPlanar.CachedData.mpower0_1_r1_0_eq line 74
def OAI.SharpPlanar.CachedData.mpower0_1_r1_1 line 75
lemma OAI.SharpPlanar.CachedData.mpower0_1_r1_1_eq line 76
def OAI.SharpPlanar.CachedData.mpower0_1_r1_2 line 77
lemma OAI.SharpPlanar.CachedData.mpower0_1_r1_2_eq line 78
def OAI.SharpPlanar.CachedData.mpower0_1_r1_3 line 79
lemma OAI.SharpPlanar.CachedData.mpower0_1_r1_3_eq line 80
def OAI.SharpPlanar.CachedData.mpower0_1_r1_4 line 81
lemma OAI.SharpPlanar.CachedData.mpower0_1_r1_4_eq line 82
def OAI.SharpPlanar.CachedData.mpower0_1_r1_5 line 83
lemma OAI.SharpPlanar.CachedData.mpower0_1_r1_5_eq line 84
def OAI.SharpPlanar.CachedData.mpower0_1_r1_6 line 85
lemma OAI.SharpPlanar.CachedData.mpower0_1_r1_6_eq line 86
def OAI.SharpPlanar.CachedData.mpower0_1_r1_7 line 87
lemma OAI.SharpPlanar.CachedData.mpower0_1_r1_7_eq line 88
def OAI.SharpPlanar.CachedData.mpower0_1_r1_8 line 89
lemma OAI.SharpPlanar.CachedData.mpower0_1_r1_8_eq line 90
def OAI.SharpPlanar.CachedData.mpower0_1_r1_9 line 91
lemma OAI.SharpPlanar.CachedData.mpower0_1_r1_9_eq line 92
def OAI.SharpPlanar.CachedData.mpower0_1_r1_10 line 93
lemma OAI.SharpPlanar.CachedData.mpower0_1_r1_10_eq line 94
def OAI.SharpPlanar.CachedData.mpower0_1_r1_11 line 95
lemma OAI.SharpPlanar.CachedData.mpower0_1_r1_11_eq line 96
def OAI.SharpPlanar.CachedData.mpower0_1_r1_12 line 97
lemma OAI.SharpPlanar.CachedData.mpower0_1_r1_12_eq line 98
def OAI.SharpPlanar.CachedData.mpower0_1_r1_13 line 99
lemma OAI.SharpPlanar.CachedData.mpower0_1_r1_13_eq line 100
def OAI.SharpPlanar.CachedData.mpower0_1_r1_14 line 101
lemma OAI.SharpPlanar.CachedData.mpower0_1_r1_14_eq line 102
def OAI.SharpPlanar.CachedData.mpower0_1_r1_15 line 103
lemma OAI.SharpPlanar.CachedData.mpower0_1_r1_15_eq line 104
def OAI.SharpPlanar.CachedData.mpower0_1_r1 line 105
lemma OAI.SharpPlanar.CachedData.mpower0_1_r1_eq line 106
def OAI.SharpPlanar.CachedData.mpower0_1_r2_0 line 124
lemma OAI.SharpPlanar.CachedData.mpower0_1_r2_0_eq line 125
def OAI.SharpPlanar.CachedData.mpower0_1_r2_1 line 126
lemma OAI.SharpPlanar.CachedData.mpower0_1_r2_1_eq line 127
def OAI.SharpPlanar.CachedData.mpower0_1_r2_2 line 128
lemma OAI.SharpPlanar.CachedData.mpower0_1_r2_2_eq line 129
def OAI.SharpPlanar.CachedData.mpower0_1_r2_3 line 130
lemma OAI.SharpPlanar.CachedData.mpower0_1_r2_3_eq line 131
def OAI.SharpPlanar.CachedData.mpower0_1_r2_4 line 132
lemma OAI.SharpPlanar.CachedData.mpower0_1_r2_4_eq line 133
def OAI.SharpPlanar.CachedData.mpower0_1_r2_5 line 134
lemma OAI.SharpPlanar.CachedData.mpower0_1_r2_5_eq line 135
def OAI.SharpPlanar.CachedData.mpower0_1_r2_6 line 136
lemma OAI.SharpPlanar.CachedData.mpower0_1_r2_6_eq line 137
def OAI.SharpPlanar.CachedData.mpower0_1_r2_7 line 138
lemma OAI.SharpPlanar.CachedData.mpower0_1_r2_7_eq line 139
def OAI.SharpPlanar.CachedData.mpower0_1_r2_8 line 140
lemma OAI.SharpPlanar.CachedData.mpower0_1_r2_8_eq line 141
def OAI.SharpPlanar.CachedData.mpower0_1_r2_9 line 142
lemma OAI.SharpPlanar.CachedData.mpower0_1_r2_9_eq line 143
def OAI.SharpPlanar.CachedData.mpower0_1_r2_10 line 144
lemma OAI.SharpPlanar.CachedData.mpower0_1_r2_10_eq line 145
def OAI.SharpPlanar.CachedData.mpower0_1_r2_11 line 146
lemma OAI.SharpPlanar.CachedData.mpower0_1_r2_11_eq line 147
def OAI.SharpPlanar.CachedData.mpower0_1_r2_12 line 148
lemma OAI.SharpPlanar.CachedData.mpower0_1_r2_12_eq line 149
def OAI.SharpPlanar.CachedData.mpower0_1_r2_13 line 150
lemma OAI.SharpPlanar.CachedData.mpower0_1_r2_13_eq line 151
def OAI.SharpPlanar.CachedData.mpower0_1_r2_14 line 152
lemma OAI.SharpPlanar.CachedData.mpower0_1_r2_14_eq line 153
def OAI.SharpPlanar.CachedData.mpower0_1_r2_15 line 154
lemma OAI.SharpPlanar.CachedData.mpower0_1_r2_15_eq line 155
def OAI.SharpPlanar.CachedData.mpower0_1_r2 line 156
lemma OAI.SharpPlanar.CachedData.mpower0_1_r2_eq line 157
def OAI.SharpPlanar.CachedData.mpower0_1_r3_0 line 175
lemma OAI.SharpPlanar.CachedData.mpower0_1_r3_0_eq line 176
def OAI.SharpPlanar.CachedData.mpower0_1_r3_1 line 177
lemma OAI.SharpPlanar.CachedData.mpower0_1_r3_1_eq line 178
def OAI.SharpPlanar.CachedData.mpower0_1_r3_2 line 179
lemma OAI.SharpPlanar.CachedData.mpower0_1_r3_2_eq line 180
def OAI.SharpPlanar.CachedData.mpower0_1_r3_3 line 181
lemma OAI.SharpPlanar.CachedData.mpower0_1_r3_3_eq line 182
def OAI.SharpPlanar.CachedData.mpower0_1_r3_4 line 183
lemma OAI.SharpPlanar.CachedData.mpower0_1_r3_4_eq line 184
def OAI.SharpPlanar.CachedData.mpower0_1_r3_5 line 185
lemma OAI.SharpPlanar.CachedData.mpower0_1_r3_5_eq line 186
def OAI.SharpPlanar.CachedData.mpower0_1_r3_6 line 187
lemma OAI.SharpPlanar.CachedData.mpower0_1_r3_6_eq line 188
def OAI.SharpPlanar.CachedData.mpower0_1_r3_7 line 189
lemma OAI.SharpPlanar.CachedData.mpower0_1_r3_7_eq line 190
def OAI.SharpPlanar.CachedData.mpower0_1_r3_8 line 191
lemma OAI.SharpPlanar.CachedData.mpower0_1_r3_8_eq line 192
def OAI.SharpPlanar.CachedData.mpower0_1_r3_9 line 193
lemma OAI.SharpPlanar.CachedData.mpower0_1_r3_9_eq line 194
def OAI.SharpPlanar.CachedData.mpower0_1_r3_10 line 195
lemma OAI.SharpPlanar.CachedData.mpower0_1_r3_10_eq line 196
def OAI.SharpPlanar.CachedData.mpower0_1_r3_11 line 197
lemma OAI.SharpPlanar.CachedData.mpower0_1_r3_11_eq line 198
def OAI.SharpPlanar.CachedData.mpower0_1_r3_12 line 199
lemma OAI.SharpPlanar.CachedData.mpower0_1_r3_12_eq line 200
def OAI.SharpPlanar.CachedData.mpower0_1_r3_13 line 201
lemma OAI.SharpPlanar.CachedData.mpower0_1_r3_13_eq line 202
def OAI.SharpPlanar.CachedData.mpower0_1_r3_14 line 203
lemma OAI.SharpPlanar.CachedData.mpower0_1_r3_14_eq line 204
def OAI.SharpPlanar.CachedData.mpower0_1_r3_15 line 205
lemma OAI.SharpPlanar.CachedData.mpower0_1_r3_15_eq line 206
def OAI.SharpPlanar.CachedData.mpower0_1_r3 line 207
lemma OAI.SharpPlanar.CachedData.mpower0_1_r3_eq line 208
def OAI.SharpPlanar.CachedData.mpower0_1_r4_0 line 226
lemma OAI.SharpPlanar.CachedData.mpower0_1_r4_0_eq line 227
def OAI.SharpPlanar.CachedData.mpower0_1_r4_1 line 228
lemma OAI.SharpPlanar.CachedData.mpower0_1_r4_1_eq line 229
def OAI.SharpPlanar.CachedData.mpower0_1_r4_2 line 230
lemma OAI.SharpPlanar.CachedData.mpower0_1_r4_2_eq line 231
def OAI.SharpPlanar.CachedData.mpower0_1_r4_3 line 232
lemma OAI.SharpPlanar.CachedData.mpower0_1_r4_3_eq line 233
def OAI.SharpPlanar.CachedData.mpower0_1_r4_4 line 234
lemma OAI.SharpPlanar.CachedData.mpower0_1_r4_4_eq line 235
def OAI.SharpPlanar.CachedData.mpower0_1_r4_5 line 236
lemma OAI.SharpPlanar.CachedData.mpower0_1_r4_5_eq line 237
def OAI.SharpPlanar.CachedData.mpower0_1_r4_6 line 238
lemma OAI.SharpPlanar.CachedData.mpower0_1_r4_6_eq line 239
def OAI.SharpPlanar.CachedData.mpower0_1_r4_7 line 240
lemma OAI.SharpPlanar.CachedData.mpower0_1_r4_7_eq line 241
def OAI.SharpPlanar.CachedData.mpower0_1_r4_8 line 242
lemma OAI.SharpPlanar.CachedData.mpower0_1_r4_8_eq line 243
def OAI.SharpPlanar.CachedData.mpower0_1_r4_9 line 244
lemma OAI.SharpPlanar.CachedData.mpower0_1_r4_9_eq line 245
def OAI.SharpPlanar.CachedData.mpower0_1_r4_10 line 246
lemma OAI.SharpPlanar.CachedData.mpower0_1_r4_10_eq line 247
def OAI.SharpPlanar.CachedData.mpower0_1_r4_11 line 248
lemma OAI.SharpPlanar.CachedData.mpower0_1_r4_11_eq line 249
def OAI.SharpPlanar.CachedData.mpower0_1_r4_12 line 250
lemma OAI.SharpPlanar.CachedData.mpower0_1_r4_12_eq line 251
def OAI.SharpPlanar.CachedData.mpower0_1_r4_13 line 252
lemma OAI.SharpPlanar.CachedData.mpower0_1_r4_13_eq line 253
def OAI.SharpPlanar.CachedData.mpower0_1_r4_14 line 254
lemma OAI.SharpPlanar.CachedData.mpower0_1_r4_14_eq line 255
def OAI.SharpPlanar.CachedData.mpower0_1_r4_15 line 256
lemma OAI.SharpPlanar.CachedData.mpower0_1_r4_15_eq line 257
def OAI.SharpPlanar.CachedData.mpower0_1_r4 line 258
lemma OAI.SharpPlanar.CachedData.mpower0_1_r4_eq line 259
def OAI.SharpPlanar.CachedData.mpower0_1_r5_0 line 277
lemma OAI.SharpPlanar.CachedData.mpower0_1_r5_0_eq line 278
def OAI.SharpPlanar.CachedData.mpower0_1_r5_1 line 279
lemma OAI.SharpPlanar.CachedData.mpower0_1_r5_1_eq line 280
def OAI.SharpPlanar.CachedData.mpower0_1_r5_2 line 281
lemma OAI.SharpPlanar.CachedData.mpower0_1_r5_2_eq line 282
def OAI.SharpPlanar.CachedData.mpower0_1_r5_3 line 283
lemma OAI.SharpPlanar.CachedData.mpower0_1_r5_3_eq line 284
def OAI.SharpPlanar.CachedData.mpower0_1_r5_4 line 285
lemma OAI.SharpPlanar.CachedData.mpower0_1_r5_4_eq line 286
def OAI.SharpPlanar.CachedData.mpower0_1_r5_5 line 287
lemma OAI.SharpPlanar.CachedData.mpower0_1_r5_5_eq line 288
def OAI.SharpPlanar.CachedData.mpower0_1_r5_6 line 289
lemma OAI.SharpPlanar.CachedData.mpower0_1_r5_6_eq line 290
def OAI.SharpPlanar.CachedData.mpower0_1_r5_7 line 291
lemma OAI.SharpPlanar.CachedData.mpower0_1_r5_7_eq line 292
def OAI.SharpPlanar.CachedData.mpower0_1_r5_8 line 293
lemma OAI.SharpPlanar.CachedData.mpower0_1_r5_8_eq line 294
def OAI.SharpPlanar.CachedData.mpower0_1_r5_9 line 295
lemma OAI.SharpPlanar.CachedData.mpower0_1_r5_9_eq line 296
def OAI.SharpPlanar.CachedData.mpower0_1_r5_10 line 297
lemma OAI.SharpPlanar.CachedData.mpower0_1_r5_10_eq line 298
def OAI.SharpPlanar.CachedData.mpower0_1_r5_11 line 299
lemma OAI.SharpPlanar.CachedData.mpower0_1_r5_11_eq line 300
def OAI.SharpPlanar.CachedData.mpower0_1_r5_12 line 301
lemma OAI.SharpPlanar.CachedData.mpower0_1_r5_12_eq line 302
def OAI.SharpPlanar.CachedData.mpower0_1_r5_13 line 303
lemma OAI.SharpPlanar.CachedData.mpower0_1_r5_13_eq line 304
def OAI.SharpPlanar.CachedData.mpower0_1_r5_14 line 305
lemma OAI.SharpPlanar.CachedData.mpower0_1_r5_14_eq line 306
def OAI.SharpPlanar.CachedData.mpower0_1_r5_15 line 307
lemma OAI.SharpPlanar.CachedData.mpower0_1_r5_15_eq line 308
def OAI.SharpPlanar.CachedData.mpower0_1_r5 line 309
lemma OAI.SharpPlanar.CachedData.mpower0_1_r5_eq line 310
def OAI.SharpPlanar.CachedData.mpower0_1 line 328
lemma OAI.SharpPlanar.CachedData.mpower0_1_eq line 329
lemma OAI.SharpPlanar.CachedData.mpower0_1_contains line 337
def OAI.SharpPlanar.CachedData.mpower1_1Expr line 341
def OAI.SharpPlanar.CachedData.mpower1_1_r0_0 line 342
lemma OAI.SharpPlanar.CachedData.mpower1_1_r0_0_eq line 343
def OAI.SharpPlanar.CachedData.mpower1_1_r0_1 line 344
lemma OAI.SharpPlanar.CachedData.mpower1_1_r0_1_eq line 345
def OAI.SharpPlanar.CachedData.mpower1_1_r0_2 line 346
lemma OAI.SharpPlanar.CachedData.mpower1_1_r0_2_eq line 347
def OAI.SharpPlanar.CachedData.mpower1_1_r0_3 line 348
lemma OAI.SharpPlanar.CachedData.mpower1_1_r0_3_eq line 349
def OAI.SharpPlanar.CachedData.mpower1_1_r0_4 line 350
lemma OAI.SharpPlanar.CachedData.mpower1_1_r0_4_eq line 351
def OAI.SharpPlanar.CachedData.mpower1_1_r0_5 line 352
lemma OAI.SharpPlanar.CachedData.mpower1_1_r0_5_eq line 353
def OAI.SharpPlanar.CachedData.mpower1_1_r0_6 line 354
lemma OAI.SharpPlanar.CachedData.mpower1_1_r0_6_eq line 355
def OAI.SharpPlanar.CachedData.mpower1_1_r0_7 line 356
lemma OAI.SharpPlanar.CachedData.mpower1_1_r0_7_eq line 357
def OAI.SharpPlanar.CachedData.mpower1_1_r0_8 line 358
lemma OAI.SharpPlanar.CachedData.mpower1_1_r0_8_eq line 359
def OAI.SharpPlanar.CachedData.mpower1_1_r0_9 line 360
lemma OAI.SharpPlanar.CachedData.mpower1_1_r0_9_eq line 361
def OAI.SharpPlanar.CachedData.mpower1_1_r0_10 line 362
lemma OAI.SharpPlanar.CachedData.mpower1_1_r0_10_eq line 363
def OAI.SharpPlanar.CachedData.mpower1_1_r0_11 line 364
lemma OAI.SharpPlanar.CachedData.mpower1_1_r0_11_eq line 365
def OAI.SharpPlanar.CachedData.mpower1_1_r0_12 line 366
lemma OAI.SharpPlanar.CachedData.mpower1_1_r0_12_eq line 367
def OAI.SharpPlanar.CachedData.mpower1_1_r0_13 line 368
lemma OAI.SharpPlanar.CachedData.mpower1_1_r0_13_eq line 369
def OAI.SharpPlanar.CachedData.mpower1_1_r0_14 line 370
lemma OAI.SharpPlanar.CachedData.mpower1_1_r0_14_eq line 371
def OAI.SharpPlanar.CachedData.mpower1_1_r0_15 line 372
lemma OAI.SharpPlanar.CachedData.mpower1_1_r0_15_eq line 373
def OAI.SharpPlanar.CachedData.mpower1_1_r0 line 374
lemma OAI.SharpPlanar.CachedData.mpower1_1_r0_eq line 375
def OAI.SharpPlanar.CachedData.mpower1_1_r1_0 line 393
lemma OAI.SharpPlanar.CachedData.mpower1_1_r1_0_eq line 394
def OAI.SharpPlanar.CachedData.mpower1_1_r1_1 line 395
lemma OAI.SharpPlanar.CachedData.mpower1_1_r1_1_eq line 396
def OAI.SharpPlanar.CachedData.mpower1_1_r1_2 line 397
lemma OAI.SharpPlanar.CachedData.mpower1_1_r1_2_eq line 398
def OAI.SharpPlanar.CachedData.mpower1_1_r1_3 line 399
lemma OAI.SharpPlanar.CachedData.mpower1_1_r1_3_eq line 400
def OAI.SharpPlanar.CachedData.mpower1_1_r1_4 line 401
lemma OAI.SharpPlanar.CachedData.mpower1_1_r1_4_eq line 402
def OAI.SharpPlanar.CachedData.mpower1_1_r1_5 line 403
lemma OAI.SharpPlanar.CachedData.mpower1_1_r1_5_eq line 404
def OAI.SharpPlanar.CachedData.mpower1_1_r1_6 line 405
lemma OAI.SharpPlanar.CachedData.mpower1_1_r1_6_eq line 406
def OAI.SharpPlanar.CachedData.mpower1_1_r1_7 line 407
lemma OAI.SharpPlanar.CachedData.mpower1_1_r1_7_eq line 408
def OAI.SharpPlanar.CachedData.mpower1_1_r1_8 line 409
lemma OAI.SharpPlanar.CachedData.mpower1_1_r1_8_eq line 410
def OAI.SharpPlanar.CachedData.mpower1_1_r1_9 line 411
lemma OAI.SharpPlanar.CachedData.mpower1_1_r1_9_eq line 412
def OAI.SharpPlanar.CachedData.mpower1_1_r1_10 line 413
lemma OAI.SharpPlanar.CachedData.mpower1_1_r1_10_eq line 414
def OAI.SharpPlanar.CachedData.mpower1_1_r1_11 line 415
lemma OAI.SharpPlanar.CachedData.mpower1_1_r1_11_eq line 416
def OAI.SharpPlanar.CachedData.mpower1_1_r1_12 line 417
lemma OAI.SharpPlanar.CachedData.mpower1_1_r1_12_eq line 418
def OAI.SharpPlanar.CachedData.mpower1_1_r1_13 line 419
lemma OAI.SharpPlanar.CachedData.mpower1_1_r1_13_eq line 420
def OAI.SharpPlanar.CachedData.mpower1_1_r1_14 line 421
lemma OAI.SharpPlanar.CachedData.mpower1_1_r1_14_eq line 422
def OAI.SharpPlanar.CachedData.mpower1_1_r1_15 line 423
lemma OAI.SharpPlanar.CachedData.mpower1_1_r1_15_eq line 424
def OAI.SharpPlanar.CachedData.mpower1_1_r1 line 425
lemma OAI.SharpPlanar.CachedData.mpower1_1_r1_eq line 426
def OAI.SharpPlanar.CachedData.mpower1_1_r2_0 line 444
lemma OAI.SharpPlanar.CachedData.mpower1_1_r2_0_eq line 445
def OAI.SharpPlanar.CachedData.mpower1_1_r2_1 line 446
lemma OAI.SharpPlanar.CachedData.mpower1_1_r2_1_eq line 447
def OAI.SharpPlanar.CachedData.mpower1_1_r2_2 line 448
lemma OAI.SharpPlanar.CachedData.mpower1_1_r2_2_eq line 449
def OAI.SharpPlanar.CachedData.mpower1_1_r2_3 line 450
lemma OAI.SharpPlanar.CachedData.mpower1_1_r2_3_eq line 451
def OAI.SharpPlanar.CachedData.mpower1_1_r2_4 line 452
lemma OAI.SharpPlanar.CachedData.mpower1_1_r2_4_eq line 453
def OAI.SharpPlanar.CachedData.mpower1_1_r2_5 line 454
lemma OAI.SharpPlanar.CachedData.mpower1_1_r2_5_eq line 455
def OAI.SharpPlanar.CachedData.mpower1_1_r2_6 line 456
lemma OAI.SharpPlanar.CachedData.mpower1_1_r2_6_eq line 457
def OAI.SharpPlanar.CachedData.mpower1_1_r2_7 line 458
lemma OAI.SharpPlanar.CachedData.mpower1_1_r2_7_eq line 459
def OAI.SharpPlanar.CachedData.mpower1_1_r2_8 line 460
lemma OAI.SharpPlanar.CachedData.mpower1_1_r2_8_eq line 461
def OAI.SharpPlanar.CachedData.mpower1_1_r2_9 line 462
lemma OAI.SharpPlanar.CachedData.mpower1_1_r2_9_eq line 463
def OAI.SharpPlanar.CachedData.mpower1_1_r2_10 line 464
lemma OAI.SharpPlanar.CachedData.mpower1_1_r2_10_eq line 465
def OAI.SharpPlanar.CachedData.mpower1_1_r2_11 line 466
lemma OAI.SharpPlanar.CachedData.mpower1_1_r2_11_eq line 467
def OAI.SharpPlanar.CachedData.mpower1_1_r2_12 line 468
lemma OAI.SharpPlanar.CachedData.mpower1_1_r2_12_eq line 469
def OAI.SharpPlanar.CachedData.mpower1_1_r2_13 line 470
lemma OAI.SharpPlanar.CachedData.mpower1_1_r2_13_eq line 471
def OAI.SharpPlanar.CachedData.mpower1_1_r2_14 line 472
lemma OAI.SharpPlanar.CachedData.mpower1_1_r2_14_eq line 473
def OAI.SharpPlanar.CachedData.mpower1_1_r2_15 line 474
lemma OAI.SharpPlanar.CachedData.mpower1_1_r2_15_eq line 475
def OAI.SharpPlanar.CachedData.mpower1_1_r2 line 476
lemma OAI.SharpPlanar.CachedData.mpower1_1_r2_eq line 477
def OAI.SharpPlanar.CachedData.mpower1_1_r3_0 line 495
lemma OAI.SharpPlanar.CachedData.mpower1_1_r3_0_eq line 496
def OAI.SharpPlanar.CachedData.mpower1_1_r3_1 line 497
lemma OAI.SharpPlanar.CachedData.mpower1_1_r3_1_eq line 498
def OAI.SharpPlanar.CachedData.mpower1_1_r3_2 line 499
lemma OAI.SharpPlanar.CachedData.mpower1_1_r3_2_eq line 500
def OAI.SharpPlanar.CachedData.mpower1_1_r3_3 line 501
lemma OAI.SharpPlanar.CachedData.mpower1_1_r3_3_eq line 502
def OAI.SharpPlanar.CachedData.mpower1_1_r3_4 line 503
lemma OAI.SharpPlanar.CachedData.mpower1_1_r3_4_eq line 504
def OAI.SharpPlanar.CachedData.mpower1_1_r3_5 line 505
lemma OAI.SharpPlanar.CachedData.mpower1_1_r3_5_eq line 506
def OAI.SharpPlanar.CachedData.mpower1_1_r3_6 line 507
lemma OAI.SharpPlanar.CachedData.mpower1_1_r3_6_eq line 508
def OAI.SharpPlanar.CachedData.mpower1_1_r3_7 line 509
lemma OAI.SharpPlanar.CachedData.mpower1_1_r3_7_eq line 510
def OAI.SharpPlanar.CachedData.mpower1_1_r3_8 line 511
lemma OAI.SharpPlanar.CachedData.mpower1_1_r3_8_eq line 512
def OAI.SharpPlanar.CachedData.mpower1_1_r3_9 line 513
lemma OAI.SharpPlanar.CachedData.mpower1_1_r3_9_eq line 514
def OAI.SharpPlanar.CachedData.mpower1_1_r3_10 line 515
lemma OAI.SharpPlanar.CachedData.mpower1_1_r3_10_eq line 516
def OAI.SharpPlanar.CachedData.mpower1_1_r3_11 line 517
lemma OAI.SharpPlanar.CachedData.mpower1_1_r3_11_eq line 518
def OAI.SharpPlanar.CachedData.mpower1_1_r3_12 line 519
lemma OAI.SharpPlanar.CachedData.mpower1_1_r3_12_eq line 520
def OAI.SharpPlanar.CachedData.mpower1_1_r3_13 line 521
lemma OAI.SharpPlanar.CachedData.mpower1_1_r3_13_eq line 522
def OAI.SharpPlanar.CachedData.mpower1_1_r3_14 line 523
lemma OAI.SharpPlanar.CachedData.mpower1_1_r3_14_eq line 524
def OAI.SharpPlanar.CachedData.mpower1_1_r3_15 line 525
lemma OAI.SharpPlanar.CachedData.mpower1_1_r3_15_eq line 526
def OAI.SharpPlanar.CachedData.mpower1_1_r3 line 527
lemma OAI.SharpPlanar.CachedData.mpower1_1_r3_eq line 528
def OAI.SharpPlanar.CachedData.mpower1_1_r4_0 line 546
lemma OAI.SharpPlanar.CachedData.mpower1_1_r4_0_eq line 547
def OAI.SharpPlanar.CachedData.mpower1_1_r4_1 line 548
lemma OAI.SharpPlanar.CachedData.mpower1_1_r4_1_eq line 549
def OAI.SharpPlanar.CachedData.mpower1_1_r4_2 line 550
lemma OAI.SharpPlanar.CachedData.mpower1_1_r4_2_eq line 551
def OAI.SharpPlanar.CachedData.mpower1_1_r4_3 line 552
lemma OAI.SharpPlanar.CachedData.mpower1_1_r4_3_eq line 553
def OAI.SharpPlanar.CachedData.mpower1_1_r4_4 line 554
lemma OAI.SharpPlanar.CachedData.mpower1_1_r4_4_eq line 555
def OAI.SharpPlanar.CachedData.mpower1_1_r4_5 line 556
lemma OAI.SharpPlanar.CachedData.mpower1_1_r4_5_eq line 557
def OAI.SharpPlanar.CachedData.mpower1_1_r4_6 line 558
lemma OAI.SharpPlanar.CachedData.mpower1_1_r4_6_eq line 559
def OAI.SharpPlanar.CachedData.mpower1_1_r4_7 line 560
lemma OAI.SharpPlanar.CachedData.mpower1_1_r4_7_eq line 561
def OAI.SharpPlanar.CachedData.mpower1_1_r4_8 line 562
lemma OAI.SharpPlanar.CachedData.mpower1_1_r4_8_eq line 563
def OAI.SharpPlanar.CachedData.mpower1_1_r4_9 line 564
lemma OAI.SharpPlanar.CachedData.mpower1_1_r4_9_eq line 565
def OAI.SharpPlanar.CachedData.mpower1_1_r4_10 line 566
lemma OAI.SharpPlanar.CachedData.mpower1_1_r4_10_eq line 567
def OAI.SharpPlanar.CachedData.mpower1_1_r4_11 line 568
lemma OAI.SharpPlanar.CachedData.mpower1_1_r4_11_eq line 569
def OAI.SharpPlanar.CachedData.mpower1_1_r4_12 line 570
lemma OAI.SharpPlanar.CachedData.mpower1_1_r4_12_eq line 571
def OAI.SharpPlanar.CachedData.mpower1_1_r4_13 line 572
lemma OAI.SharpPlanar.CachedData.mpower1_1_r4_13_eq line 573
def OAI.SharpPlanar.CachedData.mpower1_1_r4_14 line 574
lemma OAI.SharpPlanar.CachedData.mpower1_1_r4_14_eq line 575
def OAI.SharpPlanar.CachedData.mpower1_1_r4_15 line 576
lemma OAI.SharpPlanar.CachedData.mpower1_1_r4_15_eq line 577
def OAI.SharpPlanar.CachedData.mpower1_1_r4 line 578
lemma OAI.SharpPlanar.CachedData.mpower1_1_r4_eq line 579
def OAI.SharpPlanar.CachedData.mpower1_1_r5_0 line 597
lemma OAI.SharpPlanar.CachedData.mpower1_1_r5_0_eq line 598
def OAI.SharpPlanar.CachedData.mpower1_1_r5_1 line 599
lemma OAI.SharpPlanar.CachedData.mpower1_1_r5_1_eq line 600
def OAI.SharpPlanar.CachedData.mpower1_1_r5_2 line 601
lemma OAI.SharpPlanar.CachedData.mpower1_1_r5_2_eq line 602
def OAI.SharpPlanar.CachedData.mpower1_1_r5_3 line 603
lemma OAI.SharpPlanar.CachedData.mpower1_1_r5_3_eq line 604
def OAI.SharpPlanar.CachedData.mpower1_1_r5_4 line 605
lemma OAI.SharpPlanar.CachedData.mpower1_1_r5_4_eq line 606
def OAI.SharpPlanar.CachedData.mpower1_1_r5_5 line 607
lemma OAI.SharpPlanar.CachedData.mpower1_1_r5_5_eq line 608
def OAI.SharpPlanar.CachedData.mpower1_1_r5_6 line 609
lemma OAI.SharpPlanar.CachedData.mpower1_1_r5_6_eq line 610
def OAI.SharpPlanar.CachedData.mpower1_1_r5_7 line 611
lemma OAI.SharpPlanar.CachedData.mpower1_1_r5_7_eq line 612
def OAI.SharpPlanar.CachedData.mpower1_1_r5_8 line 613
lemma OAI.SharpPlanar.CachedData.mpower1_1_r5_8_eq line 614
def OAI.SharpPlanar.CachedData.mpower1_1_r5_9 line 615
lemma OAI.SharpPlanar.CachedData.mpower1_1_r5_9_eq line 616
def OAI.SharpPlanar.CachedData.mpower1_1_r5_10 line 617
lemma OAI.SharpPlanar.CachedData.mpower1_1_r5_10_eq line 618
def OAI.SharpPlanar.CachedData.mpower1_1_r5_11 line 619
lemma OAI.SharpPlanar.CachedData.mpower1_1_r5_11_eq line 620
def OAI.SharpPlanar.CachedData.mpower1_1_r5_12 line 621
lemma OAI.SharpPlanar.CachedData.mpower1_1_r5_12_eq line 622
def OAI.SharpPlanar.CachedData.mpower1_1_r5_13 line 623
lemma OAI.SharpPlanar.CachedData.mpower1_1_r5_13_eq line 624
def OAI.SharpPlanar.CachedData.mpower1_1_r5_14 line 625
lemma OAI.SharpPlanar.CachedData.mpower1_1_r5_14_eq line 626
def OAI.SharpPlanar.CachedData.mpower1_1_r5_15 line 627
lemma OAI.SharpPlanar.CachedData.mpower1_1_r5_15_eq line 628
def OAI.SharpPlanar.CachedData.mpower1_1_r5 line 629
lemma OAI.SharpPlanar.CachedData.mpower1_1_r5_eq line 630
def OAI.SharpPlanar.CachedData.mpower1_1 line 648
lemma OAI.SharpPlanar.CachedData.mpower1_1_eq line 649
lemma OAI.SharpPlanar.CachedData.mpower1_1_contains line 657
def OAI.SharpPlanar.CachedData.mpower0_2Expr line 661
def OAI.SharpPlanar.CachedData.mpower0_2_r0_0 line 662
lemma OAI.SharpPlanar.CachedData.mpower0_2_r0_0_eq line 663
def OAI.SharpPlanar.CachedData.mpower0_2_r0_1 line 664
lemma OAI.SharpPlanar.CachedData.mpower0_2_r0_1_eq line 665
def OAI.SharpPlanar.CachedData.mpower0_2_r0_2 line 666
lemma OAI.SharpPlanar.CachedData.mpower0_2_r0_2_eq line 667
def OAI.SharpPlanar.CachedData.mpower0_2_r0_3 line 668
lemma OAI.SharpPlanar.CachedData.mpower0_2_r0_3_eq line 669
def OAI.SharpPlanar.CachedData.mpower0_2_r0_4 line 670
lemma OAI.SharpPlanar.CachedData.mpower0_2_r0_4_eq line 671
def OAI.SharpPlanar.CachedData.mpower0_2_r0_5 line 672
lemma OAI.SharpPlanar.CachedData.mpower0_2_r0_5_eq line 673
def OAI.SharpPlanar.CachedData.mpower0_2_r0_6 line 674
lemma OAI.SharpPlanar.CachedData.mpower0_2_r0_6_eq line 675
def OAI.SharpPlanar.CachedData.mpower0_2_r0_7 line 676
lemma OAI.SharpPlanar.CachedData.mpower0_2_r0_7_eq line 677
def OAI.SharpPlanar.CachedData.mpower0_2_r0_8 line 678
lemma OAI.SharpPlanar.CachedData.mpower0_2_r0_8_eq line 679
def OAI.SharpPlanar.CachedData.mpower0_2_r0_9 line 680
lemma OAI.SharpPlanar.CachedData.mpower0_2_r0_9_eq line 681
def OAI.SharpPlanar.CachedData.mpower0_2_r0_10 line 682
lemma OAI.SharpPlanar.CachedData.mpower0_2_r0_10_eq line 683
def OAI.SharpPlanar.CachedData.mpower0_2_r0_11 line 684
lemma OAI.SharpPlanar.CachedData.mpower0_2_r0_11_eq line 685
def OAI.SharpPlanar.CachedData.mpower0_2_r0_12 line 686
lemma OAI.SharpPlanar.CachedData.mpower0_2_r0_12_eq line 687
def OAI.SharpPlanar.CachedData.mpower0_2_r0_13 line 688
lemma OAI.SharpPlanar.CachedData.mpower0_2_r0_13_eq line 689
def OAI.SharpPlanar.CachedData.mpower0_2_r0_14 line 690
lemma OAI.SharpPlanar.CachedData.mpower0_2_r0_14_eq line 691
def OAI.SharpPlanar.CachedData.mpower0_2_r0_15 line 692
lemma OAI.SharpPlanar.CachedData.mpower0_2_r0_15_eq line 693
def OAI.SharpPlanar.CachedData.mpower0_2_r0 line 694
lemma OAI.SharpPlanar.CachedData.mpower0_2_r0_eq line 695
def OAI.SharpPlanar.CachedData.mpower0_2_r1_0 line 713
lemma OAI.SharpPlanar.CachedData.mpower0_2_r1_0_eq line 714
def OAI.SharpPlanar.CachedData.mpower0_2_r1_1 line 715
lemma OAI.SharpPlanar.CachedData.mpower0_2_r1_1_eq line 716
def OAI.SharpPlanar.CachedData.mpower0_2_r1_2 line 717
lemma OAI.SharpPlanar.CachedData.mpower0_2_r1_2_eq line 718
def OAI.SharpPlanar.CachedData.mpower0_2_r1_3 line 719
lemma OAI.SharpPlanar.CachedData.mpower0_2_r1_3_eq line 720
def OAI.SharpPlanar.CachedData.mpower0_2_r1_4 line 721
lemma OAI.SharpPlanar.CachedData.mpower0_2_r1_4_eq line 722
def OAI.SharpPlanar.CachedData.mpower0_2_r1_5 line 723
lemma OAI.SharpPlanar.CachedData.mpower0_2_r1_5_eq line 724
def OAI.SharpPlanar.CachedData.mpower0_2_r1_6 line 725
lemma OAI.SharpPlanar.CachedData.mpower0_2_r1_6_eq line 726
def OAI.SharpPlanar.CachedData.mpower0_2_r1_7 line 727
lemma OAI.SharpPlanar.CachedData.mpower0_2_r1_7_eq line 728
def OAI.SharpPlanar.CachedData.mpower0_2_r1_8 line 729
lemma OAI.SharpPlanar.CachedData.mpower0_2_r1_8_eq line 730
def OAI.SharpPlanar.CachedData.mpower0_2_r1_9 line 731
lemma OAI.SharpPlanar.CachedData.mpower0_2_r1_9_eq line 732
def OAI.SharpPlanar.CachedData.mpower0_2_r1_10 line 733
lemma OAI.SharpPlanar.CachedData.mpower0_2_r1_10_eq line 734
def OAI.SharpPlanar.CachedData.mpower0_2_r1_11 line 735
lemma OAI.SharpPlanar.CachedData.mpower0_2_r1_11_eq line 736
def OAI.SharpPlanar.CachedData.mpower0_2_r1_12 line 737
lemma OAI.SharpPlanar.CachedData.mpower0_2_r1_12_eq line 738
def OAI.SharpPlanar.CachedData.mpower0_2_r1_13 line 739
lemma OAI.SharpPlanar.CachedData.mpower0_2_r1_13_eq line 740
def OAI.SharpPlanar.CachedData.mpower0_2_r1_14 line 741
lemma OAI.SharpPlanar.CachedData.mpower0_2_r1_14_eq line 742
def OAI.SharpPlanar.CachedData.mpower0_2_r1_15 line 743
lemma OAI.SharpPlanar.CachedData.mpower0_2_r1_15_eq line 744
def OAI.SharpPlanar.CachedData.mpower0_2_r1 line 745
lemma OAI.SharpPlanar.CachedData.mpower0_2_r1_eq line 746
def OAI.SharpPlanar.CachedData.mpower0_2_r2_0 line 764
lemma OAI.SharpPlanar.CachedData.mpower0_2_r2_0_eq line 765
def OAI.SharpPlanar.CachedData.mpower0_2_r2_1 line 766
lemma OAI.SharpPlanar.CachedData.mpower0_2_r2_1_eq line 767
def OAI.SharpPlanar.CachedData.mpower0_2_r2_2 line 768
lemma OAI.SharpPlanar.CachedData.mpower0_2_r2_2_eq line 769
def OAI.SharpPlanar.CachedData.mpower0_2_r2_3 line 770
lemma OAI.SharpPlanar.CachedData.mpower0_2_r2_3_eq line 771
def OAI.SharpPlanar.CachedData.mpower0_2_r2_4 line 772
lemma OAI.SharpPlanar.CachedData.mpower0_2_r2_4_eq line 773
def OAI.SharpPlanar.CachedData.mpower0_2_r2_5 line 774
lemma OAI.SharpPlanar.CachedData.mpower0_2_r2_5_eq line 775
def OAI.SharpPlanar.CachedData.mpower0_2_r2_6 line 776
lemma OAI.SharpPlanar.CachedData.mpower0_2_r2_6_eq line 777
def OAI.SharpPlanar.CachedData.mpower0_2_r2_7 line 778
lemma OAI.SharpPlanar.CachedData.mpower0_2_r2_7_eq line 779
def OAI.SharpPlanar.CachedData.mpower0_2_r2_8 line 780
lemma OAI.SharpPlanar.CachedData.mpower0_2_r2_8_eq line 781
def OAI.SharpPlanar.CachedData.mpower0_2_r2_9 line 782
lemma OAI.SharpPlanar.CachedData.mpower0_2_r2_9_eq line 783
def OAI.SharpPlanar.CachedData.mpower0_2_r2_10 line 784
lemma OAI.SharpPlanar.CachedData.mpower0_2_r2_10_eq line 785
def OAI.SharpPlanar.CachedData.mpower0_2_r2_11 line 786
lemma OAI.SharpPlanar.CachedData.mpower0_2_r2_11_eq line 787
def OAI.SharpPlanar.CachedData.mpower0_2_r2_12 line 788
lemma OAI.SharpPlanar.CachedData.mpower0_2_r2_12_eq line 789
def OAI.SharpPlanar.CachedData.mpower0_2_r2_13 line 790
lemma OAI.SharpPlanar.CachedData.mpower0_2_r2_13_eq line 791
def OAI.SharpPlanar.CachedData.mpower0_2_r2_14 line 792
lemma OAI.SharpPlanar.CachedData.mpower0_2_r2_14_eq line 793
def OAI.SharpPlanar.CachedData.mpower0_2_r2_15 line 794
lemma OAI.SharpPlanar.CachedData.mpower0_2_r2_15_eq line 795
def OAI.SharpPlanar.CachedData.mpower0_2_r2 line 796
lemma OAI.SharpPlanar.CachedData.mpower0_2_r2_eq line 797
def OAI.SharpPlanar.CachedData.mpower0_2_r3_0 line 815
lemma OAI.SharpPlanar.CachedData.mpower0_2_r3_0_eq line 816
def OAI.SharpPlanar.CachedData.mpower0_2_r3_1 line 817
lemma OAI.SharpPlanar.CachedData.mpower0_2_r3_1_eq line 818
def OAI.SharpPlanar.CachedData.mpower0_2_r3_2 line 819
lemma OAI.SharpPlanar.CachedData.mpower0_2_r3_2_eq line 820
def OAI.SharpPlanar.CachedData.mpower0_2_r3_3 line 821
lemma OAI.SharpPlanar.CachedData.mpower0_2_r3_3_eq line 822
def OAI.SharpPlanar.CachedData.mpower0_2_r3_4 line 823
lemma OAI.SharpPlanar.CachedData.mpower0_2_r3_4_eq line 824
def OAI.SharpPlanar.CachedData.mpower0_2_r3_5 line 825
lemma OAI.SharpPlanar.CachedData.mpower0_2_r3_5_eq line 826
def OAI.SharpPlanar.CachedData.mpower0_2_r3_6 line 827
lemma OAI.SharpPlanar.CachedData.mpower0_2_r3_6_eq line 828
def OAI.SharpPlanar.CachedData.mpower0_2_r3_7 line 829
lemma OAI.SharpPlanar.CachedData.mpower0_2_r3_7_eq line 830
def OAI.SharpPlanar.CachedData.mpower0_2_r3_8 line 831
lemma OAI.SharpPlanar.CachedData.mpower0_2_r3_8_eq line 832
def OAI.SharpPlanar.CachedData.mpower0_2_r3_9 line 833
lemma OAI.SharpPlanar.CachedData.mpower0_2_r3_9_eq line 834
def OAI.SharpPlanar.CachedData.mpower0_2_r3_10 line 835
lemma OAI.SharpPlanar.CachedData.mpower0_2_r3_10_eq line 836
def OAI.SharpPlanar.CachedData.mpower0_2_r3_11 line 837
lemma OAI.SharpPlanar.CachedData.mpower0_2_r3_11_eq line 838
def OAI.SharpPlanar.CachedData.mpower0_2_r3_12 line 839
lemma OAI.SharpPlanar.CachedData.mpower0_2_r3_12_eq line 840
def OAI.SharpPlanar.CachedData.mpower0_2_r3_13 line 841
lemma OAI.SharpPlanar.CachedData.mpower0_2_r3_13_eq line 842
def OAI.SharpPlanar.CachedData.mpower0_2_r3_14 line 843
lemma OAI.SharpPlanar.CachedData.mpower0_2_r3_14_eq line 844
def OAI.SharpPlanar.CachedData.mpower0_2_r3_15 line 845
lemma OAI.SharpPlanar.CachedData.mpower0_2_r3_15_eq line 846
def OAI.SharpPlanar.CachedData.mpower0_2_r3 line 847
lemma OAI.SharpPlanar.CachedData.mpower0_2_r3_eq line 848
def OAI.SharpPlanar.CachedData.mpower0_2_r4_0 line 866
lemma OAI.SharpPlanar.CachedData.mpower0_2_r4_0_eq line 867
def OAI.SharpPlanar.CachedData.mpower0_2_r4_1 line 868
lemma OAI.SharpPlanar.CachedData.mpower0_2_r4_1_eq line 869
def OAI.SharpPlanar.CachedData.mpower0_2_r4_2 line 870
lemma OAI.SharpPlanar.CachedData.mpower0_2_r4_2_eq line 871
def OAI.SharpPlanar.CachedData.mpower0_2_r4_3 line 872
lemma OAI.SharpPlanar.CachedData.mpower0_2_r4_3_eq line 873
def OAI.SharpPlanar.CachedData.mpower0_2_r4_4 line 874
lemma OAI.SharpPlanar.CachedData.mpower0_2_r4_4_eq line 875
def OAI.SharpPlanar.CachedData.mpower0_2_r4_5 line 876
lemma OAI.SharpPlanar.CachedData.mpower0_2_r4_5_eq line 877
def OAI.SharpPlanar.CachedData.mpower0_2_r4_6 line 878
lemma OAI.SharpPlanar.CachedData.mpower0_2_r4_6_eq line 879
def OAI.SharpPlanar.CachedData.mpower0_2_r4_7 line 880
lemma OAI.SharpPlanar.CachedData.mpower0_2_r4_7_eq line 881
def OAI.SharpPlanar.CachedData.mpower0_2_r4_8 line 882
lemma OAI.SharpPlanar.CachedData.mpower0_2_r4_8_eq line 883
def OAI.SharpPlanar.CachedData.mpower0_2_r4_9 line 884
lemma OAI.SharpPlanar.CachedData.mpower0_2_r4_9_eq line 885
def OAI.SharpPlanar.CachedData.mpower0_2_r4_10 line 886
lemma OAI.SharpPlanar.CachedData.mpower0_2_r4_10_eq line 887
def OAI.SharpPlanar.CachedData.mpower0_2_r4_11 line 888
lemma OAI.SharpPlanar.CachedData.mpower0_2_r4_11_eq line 889
def OAI.SharpPlanar.CachedData.mpower0_2_r4_12 line 890
lemma OAI.SharpPlanar.CachedData.mpower0_2_r4_12_eq line 891
def OAI.SharpPlanar.CachedData.mpower0_2_r4_13 line 892
lemma OAI.SharpPlanar.CachedData.mpower0_2_r4_13_eq line 893
def OAI.SharpPlanar.CachedData.mpower0_2_r4_14 line 894
lemma OAI.SharpPlanar.CachedData.mpower0_2_r4_14_eq line 895
def OAI.SharpPlanar.CachedData.mpower0_2_r4_15 line 896
lemma OAI.SharpPlanar.CachedData.mpower0_2_r4_15_eq line 897
def OAI.SharpPlanar.CachedData.mpower0_2_r4 line 898
lemma OAI.SharpPlanar.CachedData.mpower0_2_r4_eq line 899
def OAI.SharpPlanar.CachedData.mpower0_2_r5_0 line 917
lemma OAI.SharpPlanar.CachedData.mpower0_2_r5_0_eq line 918
def OAI.SharpPlanar.CachedData.mpower0_2_r5_1 line 919
lemma OAI.SharpPlanar.CachedData.mpower0_2_r5_1_eq line 920
def OAI.SharpPlanar.CachedData.mpower0_2_r5_2 line 921
lemma OAI.SharpPlanar.CachedData.mpower0_2_r5_2_eq line 922
def OAI.SharpPlanar.CachedData.mpower0_2_r5_3 line 923
lemma OAI.SharpPlanar.CachedData.mpower0_2_r5_3_eq line 924
def OAI.SharpPlanar.CachedData.mpower0_2_r5_4 line 925
lemma OAI.SharpPlanar.CachedData.mpower0_2_r5_4_eq line 926
def OAI.SharpPlanar.CachedData.mpower0_2_r5_5 line 927
lemma OAI.SharpPlanar.CachedData.mpower0_2_r5_5_eq line 928
def OAI.SharpPlanar.CachedData.mpower0_2_r5_6 line 929
lemma OAI.SharpPlanar.CachedData.mpower0_2_r5_6_eq line 930
def OAI.SharpPlanar.CachedData.mpower0_2_r5_7 line 931
lemma OAI.SharpPlanar.CachedData.mpower0_2_r5_7_eq line 932
def OAI.SharpPlanar.CachedData.mpower0_2_r5_8 line 933
lemma OAI.SharpPlanar.CachedData.mpower0_2_r5_8_eq line 934
def OAI.SharpPlanar.CachedData.mpower0_2_r5_9 line 935
lemma OAI.SharpPlanar.CachedData.mpower0_2_r5_9_eq line 936
def OAI.SharpPlanar.CachedData.mpower0_2_r5_10 line 937
lemma OAI.SharpPlanar.CachedData.mpower0_2_r5_10_eq line 938
def OAI.SharpPlanar.CachedData.mpower0_2_r5_11 line 939
lemma OAI.SharpPlanar.CachedData.mpower0_2_r5_11_eq line 940
def OAI.SharpPlanar.CachedData.mpower0_2_r5_12 line 941
lemma OAI.SharpPlanar.CachedData.mpower0_2_r5_12_eq line 942
def OAI.SharpPlanar.CachedData.mpower0_2_r5_13 line 943
lemma OAI.SharpPlanar.CachedData.mpower0_2_r5_13_eq line 944
def OAI.SharpPlanar.CachedData.mpower0_2_r5_14 line 945
lemma OAI.SharpPlanar.CachedData.mpower0_2_r5_14_eq line 946
def OAI.SharpPlanar.CachedData.mpower0_2_r5_15 line 947
lemma OAI.SharpPlanar.CachedData.mpower0_2_r5_15_eq line 948
def OAI.SharpPlanar.CachedData.mpower0_2_r5 line 949
lemma OAI.SharpPlanar.CachedData.mpower0_2_r5_eq line 950
def OAI.SharpPlanar.CachedData.mpower0_2 line 968
lemma OAI.SharpPlanar.CachedData.mpower0_2_eq line 969
lemma OAI.SharpPlanar.CachedData.mpower0_2_contains line 977
def OAI.SharpPlanar.CachedData.mpower1_2Expr line 981
def OAI.SharpPlanar.CachedData.mpower1_2_r0_0 line 982
lemma OAI.SharpPlanar.CachedData.mpower1_2_r0_0_eq line 983
def OAI.SharpPlanar.CachedData.mpower1_2_r0_1 line 984
lemma OAI.SharpPlanar.CachedData.mpower1_2_r0_1_eq line 985
def OAI.SharpPlanar.CachedData.mpower1_2_r0_2 line 986
lemma OAI.SharpPlanar.CachedData.mpower1_2_r0_2_eq line 987
def OAI.SharpPlanar.CachedData.mpower1_2_r0_3 line 988
lemma OAI.SharpPlanar.CachedData.mpower1_2_r0_3_eq line 989
def OAI.SharpPlanar.CachedData.mpower1_2_r0_4 line 990
lemma OAI.SharpPlanar.CachedData.mpower1_2_r0_4_eq line 991
def OAI.SharpPlanar.CachedData.mpower1_2_r0_5 line 992
lemma OAI.SharpPlanar.CachedData.mpower1_2_r0_5_eq line 993
def OAI.SharpPlanar.CachedData.mpower1_2_r0_6 line 994
lemma OAI.SharpPlanar.CachedData.mpower1_2_r0_6_eq line 995
def OAI.SharpPlanar.CachedData.mpower1_2_r0_7 line 996
lemma OAI.SharpPlanar.CachedData.mpower1_2_r0_7_eq line 997
def OAI.SharpPlanar.CachedData.mpower1_2_r0_8 line 998
lemma OAI.SharpPlanar.CachedData.mpower1_2_r0_8_eq line 999
def OAI.SharpPlanar.CachedData.mpower1_2_r0_9 line 1000
lemma OAI.SharpPlanar.CachedData.mpower1_2_r0_9_eq line 1001
def OAI.SharpPlanar.CachedData.mpower1_2_r0_10 line 1002
lemma OAI.SharpPlanar.CachedData.mpower1_2_r0_10_eq line 1003
def OAI.SharpPlanar.CachedData.mpower1_2_r0_11 line 1004
lemma OAI.SharpPlanar.CachedData.mpower1_2_r0_11_eq line 1005
def OAI.SharpPlanar.CachedData.mpower1_2_r0_12 line 1006
lemma OAI.SharpPlanar.CachedData.mpower1_2_r0_12_eq line 1007
def OAI.SharpPlanar.CachedData.mpower1_2_r0_13 line 1008
lemma OAI.SharpPlanar.CachedData.mpower1_2_r0_13_eq line 1009
def OAI.SharpPlanar.CachedData.mpower1_2_r0_14 line 1010
lemma OAI.SharpPlanar.CachedData.mpower1_2_r0_14_eq line 1011
def OAI.SharpPlanar.CachedData.mpower1_2_r0_15 line 1012
lemma OAI.SharpPlanar.CachedData.mpower1_2_r0_15_eq line 1013
def OAI.SharpPlanar.CachedData.mpower1_2_r0 line 1014
lemma OAI.SharpPlanar.CachedData.mpower1_2_r0_eq line 1015
def OAI.SharpPlanar.CachedData.mpower1_2_r1_0 line 1033
lemma OAI.SharpPlanar.CachedData.mpower1_2_r1_0_eq line 1034
def OAI.SharpPlanar.CachedData.mpower1_2_r1_1 line 1035
lemma OAI.SharpPlanar.CachedData.mpower1_2_r1_1_eq line 1036
def OAI.SharpPlanar.CachedData.mpower1_2_r1_2 line 1037
lemma OAI.SharpPlanar.CachedData.mpower1_2_r1_2_eq line 1038
def OAI.SharpPlanar.CachedData.mpower1_2_r1_3 line 1039
lemma OAI.SharpPlanar.CachedData.mpower1_2_r1_3_eq line 1040
def OAI.SharpPlanar.CachedData.mpower1_2_r1_4 line 1041
lemma OAI.SharpPlanar.CachedData.mpower1_2_r1_4_eq line 1042
def OAI.SharpPlanar.CachedData.mpower1_2_r1_5 line 1043
lemma OAI.SharpPlanar.CachedData.mpower1_2_r1_5_eq line 1044
def OAI.SharpPlanar.CachedData.mpower1_2_r1_6 line 1045
lemma OAI.SharpPlanar.CachedData.mpower1_2_r1_6_eq line 1046
def OAI.SharpPlanar.CachedData.mpower1_2_r1_7 line 1047
lemma OAI.SharpPlanar.CachedData.mpower1_2_r1_7_eq line 1048
def OAI.SharpPlanar.CachedData.mpower1_2_r1_8 line 1049
lemma OAI.SharpPlanar.CachedData.mpower1_2_r1_8_eq line 1050
def OAI.SharpPlanar.CachedData.mpower1_2_r1_9 line 1051
lemma OAI.SharpPlanar.CachedData.mpower1_2_r1_9_eq line 1052
def OAI.SharpPlanar.CachedData.mpower1_2_r1_10 line 1053
lemma OAI.SharpPlanar.CachedData.mpower1_2_r1_10_eq line 1054
def OAI.SharpPlanar.CachedData.mpower1_2_r1_11 line 1055
lemma OAI.SharpPlanar.CachedData.mpower1_2_r1_11_eq line 1056
def OAI.SharpPlanar.CachedData.mpower1_2_r1_12 line 1057
lemma OAI.SharpPlanar.CachedData.mpower1_2_r1_12_eq line 1058
def OAI.SharpPlanar.CachedData.mpower1_2_r1_13 line 1059
lemma OAI.SharpPlanar.CachedData.mpower1_2_r1_13_eq line 1060
def OAI.SharpPlanar.CachedData.mpower1_2_r1_14 line 1061
lemma OAI.SharpPlanar.CachedData.mpower1_2_r1_14_eq line 1062
def OAI.SharpPlanar.CachedData.mpower1_2_r1_15 line 1063
lemma OAI.SharpPlanar.CachedData.mpower1_2_r1_15_eq line 1064
def OAI.SharpPlanar.CachedData.mpower1_2_r1 line 1065
lemma OAI.SharpPlanar.CachedData.mpower1_2_r1_eq line 1066
def OAI.SharpPlanar.CachedData.mpower1_2_r2_0 line 1084
lemma OAI.SharpPlanar.CachedData.mpower1_2_r2_0_eq line 1085
def OAI.SharpPlanar.CachedData.mpower1_2_r2_1 line 1086
lemma OAI.SharpPlanar.CachedData.mpower1_2_r2_1_eq line 1087
def OAI.SharpPlanar.CachedData.mpower1_2_r2_2 line 1088
lemma OAI.SharpPlanar.CachedData.mpower1_2_r2_2_eq line 1089
def OAI.SharpPlanar.CachedData.mpower1_2_r2_3 line 1090
lemma OAI.SharpPlanar.CachedData.mpower1_2_r2_3_eq line 1091
def OAI.SharpPlanar.CachedData.mpower1_2_r2_4 line 1092
lemma OAI.SharpPlanar.CachedData.mpower1_2_r2_4_eq line 1093
def OAI.SharpPlanar.CachedData.mpower1_2_r2_5 line 1094
lemma OAI.SharpPlanar.CachedData.mpower1_2_r2_5_eq line 1095
def OAI.SharpPlanar.CachedData.mpower1_2_r2_6 line 1096
lemma OAI.SharpPlanar.CachedData.mpower1_2_r2_6_eq line 1097
def OAI.SharpPlanar.CachedData.mpower1_2_r2_7 line 1098
lemma OAI.SharpPlanar.CachedData.mpower1_2_r2_7_eq line 1099
def OAI.SharpPlanar.CachedData.mpower1_2_r2_8 line 1100
lemma OAI.SharpPlanar.CachedData.mpower1_2_r2_8_eq line 1101
def OAI.SharpPlanar.CachedData.mpower1_2_r2_9 line 1102
lemma OAI.SharpPlanar.CachedData.mpower1_2_r2_9_eq line 1103
def OAI.SharpPlanar.CachedData.mpower1_2_r2_10 line 1104
lemma OAI.SharpPlanar.CachedData.mpower1_2_r2_10_eq line 1105
def OAI.SharpPlanar.CachedData.mpower1_2_r2_11 line 1106
lemma OAI.SharpPlanar.CachedData.mpower1_2_r2_11_eq line 1107
def OAI.SharpPlanar.CachedData.mpower1_2_r2_12 line 1108
lemma OAI.SharpPlanar.CachedData.mpower1_2_r2_12_eq line 1109
def OAI.SharpPlanar.CachedData.mpower1_2_r2_13 line 1110
lemma OAI.SharpPlanar.CachedData.mpower1_2_r2_13_eq line 1111
def OAI.SharpPlanar.CachedData.mpower1_2_r2_14 line 1112
lemma OAI.SharpPlanar.CachedData.mpower1_2_r2_14_eq line 1113
def OAI.SharpPlanar.CachedData.mpower1_2_r2_15 line 1114
lemma OAI.SharpPlanar.CachedData.mpower1_2_r2_15_eq line 1115
def OAI.SharpPlanar.CachedData.mpower1_2_r2 line 1116
lemma OAI.SharpPlanar.CachedData.mpower1_2_r2_eq line 1117
def OAI.SharpPlanar.CachedData.mpower1_2_r3_0 line 1135
lemma OAI.SharpPlanar.CachedData.mpower1_2_r3_0_eq line 1136
def OAI.SharpPlanar.CachedData.mpower1_2_r3_1 line 1137
lemma OAI.SharpPlanar.CachedData.mpower1_2_r3_1_eq line 1138
def OAI.SharpPlanar.CachedData.mpower1_2_r3_2 line 1139
lemma OAI.SharpPlanar.CachedData.mpower1_2_r3_2_eq line 1140
def OAI.SharpPlanar.CachedData.mpower1_2_r3_3 line 1141
lemma OAI.SharpPlanar.CachedData.mpower1_2_r3_3_eq line 1142
def OAI.SharpPlanar.CachedData.mpower1_2_r3_4 line 1143
lemma OAI.SharpPlanar.CachedData.mpower1_2_r3_4_eq line 1144
def OAI.SharpPlanar.CachedData.mpower1_2_r3_5 line 1145
lemma OAI.SharpPlanar.CachedData.mpower1_2_r3_5_eq line 1146
def OAI.SharpPlanar.CachedData.mpower1_2_r3_6 line 1147
lemma OAI.SharpPlanar.CachedData.mpower1_2_r3_6_eq line 1148
def OAI.SharpPlanar.CachedData.mpower1_2_r3_7 line 1149
lemma OAI.SharpPlanar.CachedData.mpower1_2_r3_7_eq line 1150
def OAI.SharpPlanar.CachedData.mpower1_2_r3_8 line 1151
lemma OAI.SharpPlanar.CachedData.mpower1_2_r3_8_eq line 1152
def OAI.SharpPlanar.CachedData.mpower1_2_r3_9 line 1153
lemma OAI.SharpPlanar.CachedData.mpower1_2_r3_9_eq line 1154
def OAI.SharpPlanar.CachedData.mpower1_2_r3_10 line 1155
lemma OAI.SharpPlanar.CachedData.mpower1_2_r3_10_eq line 1156
def OAI.SharpPlanar.CachedData.mpower1_2_r3_11 line 1157
lemma OAI.SharpPlanar.CachedData.mpower1_2_r3_11_eq line 1158
def OAI.SharpPlanar.CachedData.mpower1_2_r3_12 line 1159
lemma OAI.SharpPlanar.CachedData.mpower1_2_r3_12_eq line 1160
def OAI.SharpPlanar.CachedData.mpower1_2_r3_13 line 1161
lemma OAI.SharpPlanar.CachedData.mpower1_2_r3_13_eq line 1162
def OAI.SharpPlanar.CachedData.mpower1_2_r3_14 line 1163
lemma OAI.SharpPlanar.CachedData.mpower1_2_r3_14_eq line 1164
def OAI.SharpPlanar.CachedData.mpower1_2_r3_15 line 1165
lemma OAI.SharpPlanar.CachedData.mpower1_2_r3_15_eq line 1166
def OAI.SharpPlanar.CachedData.mpower1_2_r3 line 1167
lemma OAI.SharpPlanar.CachedData.mpower1_2_r3_eq line 1168
def OAI.SharpPlanar.CachedData.mpower1_2_r4_0 line 1186
lemma OAI.SharpPlanar.CachedData.mpower1_2_r4_0_eq line 1187
def OAI.SharpPlanar.CachedData.mpower1_2_r4_1 line 1188
lemma OAI.SharpPlanar.CachedData.mpower1_2_r4_1_eq line 1189
def OAI.SharpPlanar.CachedData.mpower1_2_r4_2 line 1190
lemma OAI.SharpPlanar.CachedData.mpower1_2_r4_2_eq line 1191
def OAI.SharpPlanar.CachedData.mpower1_2_r4_3 line 1192
lemma OAI.SharpPlanar.CachedData.mpower1_2_r4_3_eq line 1193
def OAI.SharpPlanar.CachedData.mpower1_2_r4_4 line 1194
lemma OAI.SharpPlanar.CachedData.mpower1_2_r4_4_eq line 1195
def OAI.SharpPlanar.CachedData.mpower1_2_r4_5 line 1196
lemma OAI.SharpPlanar.CachedData.mpower1_2_r4_5_eq line 1197
def OAI.SharpPlanar.CachedData.mpower1_2_r4_6 line 1198
lemma OAI.SharpPlanar.CachedData.mpower1_2_r4_6_eq line 1199
def OAI.SharpPlanar.CachedData.mpower1_2_r4_7 line 1200
lemma OAI.SharpPlanar.CachedData.mpower1_2_r4_7_eq line 1201
def OAI.SharpPlanar.CachedData.mpower1_2_r4_8 line 1202
lemma OAI.SharpPlanar.CachedData.mpower1_2_r4_8_eq line 1203
def OAI.SharpPlanar.CachedData.mpower1_2_r4_9 line 1204
lemma OAI.SharpPlanar.CachedData.mpower1_2_r4_9_eq line 1205
def OAI.SharpPlanar.CachedData.mpower1_2_r4_10 line 1206
lemma OAI.SharpPlanar.CachedData.mpower1_2_r4_10_eq line 1207
def OAI.SharpPlanar.CachedData.mpower1_2_r4_11 line 1208
lemma OAI.SharpPlanar.CachedData.mpower1_2_r4_11_eq line 1209
def OAI.SharpPlanar.CachedData.mpower1_2_r4_12 line 1210
lemma OAI.SharpPlanar.CachedData.mpower1_2_r4_12_eq line 1211
def OAI.SharpPlanar.CachedData.mpower1_2_r4_13 line 1212
lemma OAI.SharpPlanar.CachedData.mpower1_2_r4_13_eq line 1213
def OAI.SharpPlanar.CachedData.mpower1_2_r4_14 line 1214
lemma OAI.SharpPlanar.CachedData.mpower1_2_r4_14_eq line 1215
def OAI.SharpPlanar.CachedData.mpower1_2_r4_15 line 1216
lemma OAI.SharpPlanar.CachedData.mpower1_2_r4_15_eq line 1217
def OAI.SharpPlanar.CachedData.mpower1_2_r4 line 1218
lemma OAI.SharpPlanar.CachedData.mpower1_2_r4_eq line 1219
def OAI.SharpPlanar.CachedData.mpower1_2_r5_0 line 1237
lemma OAI.SharpPlanar.CachedData.mpower1_2_r5_0_eq line 1238
def OAI.SharpPlanar.CachedData.mpower1_2_r5_1 line 1239
lemma OAI.SharpPlanar.CachedData.mpower1_2_r5_1_eq line 1240
def OAI.SharpPlanar.CachedData.mpower1_2_r5_2 line 1241
lemma OAI.SharpPlanar.CachedData.mpower1_2_r5_2_eq line 1242
def OAI.SharpPlanar.CachedData.mpower1_2_r5_3 line 1243
lemma OAI.SharpPlanar.CachedData.mpower1_2_r5_3_eq line 1244
def OAI.SharpPlanar.CachedData.mpower1_2_r5_4 line 1245
lemma OAI.SharpPlanar.CachedData.mpower1_2_r5_4_eq line 1246
def OAI.SharpPlanar.CachedData.mpower1_2_r5_5 line 1247
lemma OAI.SharpPlanar.CachedData.mpower1_2_r5_5_eq line 1248
def OAI.SharpPlanar.CachedData.mpower1_2_r5_6 line 1249
lemma OAI.SharpPlanar.CachedData.mpower1_2_r5_6_eq line 1250
def OAI.SharpPlanar.CachedData.mpower1_2_r5_7 line 1251
lemma OAI.SharpPlanar.CachedData.mpower1_2_r5_7_eq line 1252
def OAI.SharpPlanar.CachedData.mpower1_2_r5_8 line 1253
lemma OAI.SharpPlanar.CachedData.mpower1_2_r5_8_eq line 1254
def OAI.SharpPlanar.CachedData.mpower1_2_r5_9 line 1255
lemma OAI.SharpPlanar.CachedData.mpower1_2_r5_9_eq line 1256
def OAI.SharpPlanar.CachedData.mpower1_2_r5_10 line 1257
lemma OAI.SharpPlanar.CachedData.mpower1_2_r5_10_eq line 1258
def OAI.SharpPlanar.CachedData.mpower1_2_r5_11 line 1259
lemma OAI.SharpPlanar.CachedData.mpower1_2_r5_11_eq line 1260
def OAI.SharpPlanar.CachedData.mpower1_2_r5_12 line 1261
lemma OAI.SharpPlanar.CachedData.mpower1_2_r5_12_eq line 1262
def OAI.SharpPlanar.CachedData.mpower1_2_r5_13 line 1263
lemma OAI.SharpPlanar.CachedData.mpower1_2_r5_13_eq line 1264
def OAI.SharpPlanar.CachedData.mpower1_2_r5_14 line 1265
lemma OAI.SharpPlanar.CachedData.mpower1_2_r5_14_eq line 1266
def OAI.SharpPlanar.CachedData.mpower1_2_r5_15 line 1267
lemma OAI.SharpPlanar.CachedData.mpower1_2_r5_15_eq line 1268
def OAI.SharpPlanar.CachedData.mpower1_2_r5 line 1269
lemma OAI.SharpPlanar.CachedData.mpower1_2_r5_eq line 1270
def OAI.SharpPlanar.CachedData.mpower1_2 line 1288
lemma OAI.SharpPlanar.CachedData.mpower1_2_eq line 1289
lemma OAI.SharpPlanar.CachedData.mpower1_2_contains line 1297
def OAI.SharpPlanar.CachedData.mpower0_3Expr line 1301
def OAI.SharpPlanar.CachedData.mpower0_3_r0_0 line 1302
lemma OAI.SharpPlanar.CachedData.mpower0_3_r0_0_eq line 1303
def OAI.SharpPlanar.CachedData.mpower0_3_r0_1 line 1304
lemma OAI.SharpPlanar.CachedData.mpower0_3_r0_1_eq line 1305
def OAI.SharpPlanar.CachedData.mpower0_3_r0_2 line 1306
lemma OAI.SharpPlanar.CachedData.mpower0_3_r0_2_eq line 1307
def OAI.SharpPlanar.CachedData.mpower0_3_r0_3 line 1308
lemma OAI.SharpPlanar.CachedData.mpower0_3_r0_3_eq line 1309
def OAI.SharpPlanar.CachedData.mpower0_3_r0_4 line 1310
lemma OAI.SharpPlanar.CachedData.mpower0_3_r0_4_eq line 1311
def OAI.SharpPlanar.CachedData.mpower0_3_r0_5 line 1312
lemma OAI.SharpPlanar.CachedData.mpower0_3_r0_5_eq line 1313
def OAI.SharpPlanar.CachedData.mpower0_3_r0_6 line 1314
lemma OAI.SharpPlanar.CachedData.mpower0_3_r0_6_eq line 1315
def OAI.SharpPlanar.CachedData.mpower0_3_r0_7 line 1316
lemma OAI.SharpPlanar.CachedData.mpower0_3_r0_7_eq line 1317
def OAI.SharpPlanar.CachedData.mpower0_3_r0_8 line 1318
lemma OAI.SharpPlanar.CachedData.mpower0_3_r0_8_eq line 1319
def OAI.SharpPlanar.CachedData.mpower0_3_r0_9 line 1320
lemma OAI.SharpPlanar.CachedData.mpower0_3_r0_9_eq line 1321
def OAI.SharpPlanar.CachedData.mpower0_3_r0_10 line 1322
lemma OAI.SharpPlanar.CachedData.mpower0_3_r0_10_eq line 1323
def OAI.SharpPlanar.CachedData.mpower0_3_r0_11 line 1324
lemma OAI.SharpPlanar.CachedData.mpower0_3_r0_11_eq line 1325
def OAI.SharpPlanar.CachedData.mpower0_3_r0_12 line 1326
lemma OAI.SharpPlanar.CachedData.mpower0_3_r0_12_eq line 1327
def OAI.SharpPlanar.CachedData.mpower0_3_r0_13 line 1328
lemma OAI.SharpPlanar.CachedData.mpower0_3_r0_13_eq line 1329
def OAI.SharpPlanar.CachedData.mpower0_3_r0_14 line 1330
lemma OAI.SharpPlanar.CachedData.mpower0_3_r0_14_eq line 1331
def OAI.SharpPlanar.CachedData.mpower0_3_r0_15 line 1332
lemma OAI.SharpPlanar.CachedData.mpower0_3_r0_15_eq line 1333
def OAI.SharpPlanar.CachedData.mpower0_3_r0 line 1334
lemma OAI.SharpPlanar.CachedData.mpower0_3_r0_eq line 1335
def OAI.SharpPlanar.CachedData.mpower0_3_r1_0 line 1353
lemma OAI.SharpPlanar.CachedData.mpower0_3_r1_0_eq line 1354
def OAI.SharpPlanar.CachedData.mpower0_3_r1_1 line 1355
lemma OAI.SharpPlanar.CachedData.mpower0_3_r1_1_eq line 1356
def OAI.SharpPlanar.CachedData.mpower0_3_r1_2 line 1357
lemma OAI.SharpPlanar.CachedData.mpower0_3_r1_2_eq line 1358
def OAI.SharpPlanar.CachedData.mpower0_3_r1_3 line 1359
lemma OAI.SharpPlanar.CachedData.mpower0_3_r1_3_eq line 1360
def OAI.SharpPlanar.CachedData.mpower0_3_r1_4 line 1361
lemma OAI.SharpPlanar.CachedData.mpower0_3_r1_4_eq line 1362
def OAI.SharpPlanar.CachedData.mpower0_3_r1_5 line 1363
lemma OAI.SharpPlanar.CachedData.mpower0_3_r1_5_eq line 1364
def OAI.SharpPlanar.CachedData.mpower0_3_r1_6 line 1365
lemma OAI.SharpPlanar.CachedData.mpower0_3_r1_6_eq line 1366
def OAI.SharpPlanar.CachedData.mpower0_3_r1_7 line 1367
lemma OAI.SharpPlanar.CachedData.mpower0_3_r1_7_eq line 1368
def OAI.SharpPlanar.CachedData.mpower0_3_r1_8 line 1369
lemma OAI.SharpPlanar.CachedData.mpower0_3_r1_8_eq line 1370
def OAI.SharpPlanar.CachedData.mpower0_3_r1_9 line 1371
lemma OAI.SharpPlanar.CachedData.mpower0_3_r1_9_eq line 1372
def OAI.SharpPlanar.CachedData.mpower0_3_r1_10 line 1373
lemma OAI.SharpPlanar.CachedData.mpower0_3_r1_10_eq line 1374
def OAI.SharpPlanar.CachedData.mpower0_3_r1_11 line 1375
lemma OAI.SharpPlanar.CachedData.mpower0_3_r1_11_eq line 1376
def OAI.SharpPlanar.CachedData.mpower0_3_r1_12 line 1377
lemma OAI.SharpPlanar.CachedData.mpower0_3_r1_12_eq line 1378
def OAI.SharpPlanar.CachedData.mpower0_3_r1_13 line 1379
lemma OAI.SharpPlanar.CachedData.mpower0_3_r1_13_eq line 1380
def OAI.SharpPlanar.CachedData.mpower0_3_r1_14 line 1381
lemma OAI.SharpPlanar.CachedData.mpower0_3_r1_14_eq line 1382
def OAI.SharpPlanar.CachedData.mpower0_3_r1_15 line 1383
lemma OAI.SharpPlanar.CachedData.mpower0_3_r1_15_eq line 1384
def OAI.SharpPlanar.CachedData.mpower0_3_r1 line 1385
lemma OAI.SharpPlanar.CachedData.mpower0_3_r1_eq line 1386
def OAI.SharpPlanar.CachedData.mpower0_3_r2_0 line 1404
lemma OAI.SharpPlanar.CachedData.mpower0_3_r2_0_eq line 1405
def OAI.SharpPlanar.CachedData.mpower0_3_r2_1 line 1406
lemma OAI.SharpPlanar.CachedData.mpower0_3_r2_1_eq line 1407
def OAI.SharpPlanar.CachedData.mpower0_3_r2_2 line 1408
lemma OAI.SharpPlanar.CachedData.mpower0_3_r2_2_eq line 1409
def OAI.SharpPlanar.CachedData.mpower0_3_r2_3 line 1410
lemma OAI.SharpPlanar.CachedData.mpower0_3_r2_3_eq line 1411
def OAI.SharpPlanar.CachedData.mpower0_3_r2_4 line 1412
lemma OAI.SharpPlanar.CachedData.mpower0_3_r2_4_eq line 1413
def OAI.SharpPlanar.CachedData.mpower0_3_r2_5 line 1414
lemma OAI.SharpPlanar.CachedData.mpower0_3_r2_5_eq line 1415
def OAI.SharpPlanar.CachedData.mpower0_3_r2_6 line 1416
lemma OAI.SharpPlanar.CachedData.mpower0_3_r2_6_eq line 1417
def OAI.SharpPlanar.CachedData.mpower0_3_r2_7 line 1418
lemma OAI.SharpPlanar.CachedData.mpower0_3_r2_7_eq line 1419
def OAI.SharpPlanar.CachedData.mpower0_3_r2_8 line 1420
lemma OAI.SharpPlanar.CachedData.mpower0_3_r2_8_eq line 1421
def OAI.SharpPlanar.CachedData.mpower0_3_r2_9 line 1422
lemma OAI.SharpPlanar.CachedData.mpower0_3_r2_9_eq line 1423
def OAI.SharpPlanar.CachedData.mpower0_3_r2_10 line 1424
lemma OAI.SharpPlanar.CachedData.mpower0_3_r2_10_eq line 1425
def OAI.SharpPlanar.CachedData.mpower0_3_r2_11 line 1426
lemma OAI.SharpPlanar.CachedData.mpower0_3_r2_11_eq line 1427
def OAI.SharpPlanar.CachedData.mpower0_3_r2_12 line 1428
lemma OAI.SharpPlanar.CachedData.mpower0_3_r2_12_eq line 1429
def OAI.SharpPlanar.CachedData.mpower0_3_r2_13 line 1430
lemma OAI.SharpPlanar.CachedData.mpower0_3_r2_13_eq line 1431
def OAI.SharpPlanar.CachedData.mpower0_3_r2_14 line 1432
lemma OAI.SharpPlanar.CachedData.mpower0_3_r2_14_eq line 1433
def OAI.SharpPlanar.CachedData.mpower0_3_r2_15 line 1434
lemma OAI.SharpPlanar.CachedData.mpower0_3_r2_15_eq line 1435
def OAI.SharpPlanar.CachedData.mpower0_3_r2 line 1436
lemma OAI.SharpPlanar.CachedData.mpower0_3_r2_eq line 1437
def OAI.SharpPlanar.CachedData.mpower0_3_r3_0 line 1455
lemma OAI.SharpPlanar.CachedData.mpower0_3_r3_0_eq line 1456
def OAI.SharpPlanar.CachedData.mpower0_3_r3_1 line 1457
lemma OAI.SharpPlanar.CachedData.mpower0_3_r3_1_eq line 1458
def OAI.SharpPlanar.CachedData.mpower0_3_r3_2 line 1459
lemma OAI.SharpPlanar.CachedData.mpower0_3_r3_2_eq line 1460
def OAI.SharpPlanar.CachedData.mpower0_3_r3_3 line 1461
lemma OAI.SharpPlanar.CachedData.mpower0_3_r3_3_eq line 1462
def OAI.SharpPlanar.CachedData.mpower0_3_r3_4 line 1463
lemma OAI.SharpPlanar.CachedData.mpower0_3_r3_4_eq line 1464
def OAI.SharpPlanar.CachedData.mpower0_3_r3_5 line 1465
lemma OAI.SharpPlanar.CachedData.mpower0_3_r3_5_eq line 1466
def OAI.SharpPlanar.CachedData.mpower0_3_r3_6 line 1467
lemma OAI.SharpPlanar.CachedData.mpower0_3_r3_6_eq line 1468
def OAI.SharpPlanar.CachedData.mpower0_3_r3_7 line 1469
lemma OAI.SharpPlanar.CachedData.mpower0_3_r3_7_eq line 1470
def OAI.SharpPlanar.CachedData.mpower0_3_r3_8 line 1471
lemma OAI.SharpPlanar.CachedData.mpower0_3_r3_8_eq line 1472
def OAI.SharpPlanar.CachedData.mpower0_3_r3_9 line 1473
lemma OAI.SharpPlanar.CachedData.mpower0_3_r3_9_eq line 1474
def OAI.SharpPlanar.CachedData.mpower0_3_r3_10 line 1475
lemma OAI.SharpPlanar.CachedData.mpower0_3_r3_10_eq line 1476
def OAI.SharpPlanar.CachedData.mpower0_3_r3_11 line 1477
lemma OAI.SharpPlanar.CachedData.mpower0_3_r3_11_eq line 1478
def OAI.SharpPlanar.CachedData.mpower0_3_r3_12 line 1479
lemma OAI.SharpPlanar.CachedData.mpower0_3_r3_12_eq line 1480
def OAI.SharpPlanar.CachedData.mpower0_3_r3_13 line 1481
lemma OAI.SharpPlanar.CachedData.mpower0_3_r3_13_eq line 1482
def OAI.SharpPlanar.CachedData.mpower0_3_r3_14 line 1483
lemma OAI.SharpPlanar.CachedData.mpower0_3_r3_14_eq line 1484
def OAI.SharpPlanar.CachedData.mpower0_3_r3_15 line 1485
lemma OAI.SharpPlanar.CachedData.mpower0_3_r3_15_eq line 1486
def OAI.SharpPlanar.CachedData.mpower0_3_r3 line 1487
lemma OAI.SharpPlanar.CachedData.mpower0_3_r3_eq line 1488
def OAI.SharpPlanar.CachedData.mpower0_3_r4_0 line 1506
lemma OAI.SharpPlanar.CachedData.mpower0_3_r4_0_eq line 1507
def OAI.SharpPlanar.CachedData.mpower0_3_r4_1 line 1508
lemma OAI.SharpPlanar.CachedData.mpower0_3_r4_1_eq line 1509
def OAI.SharpPlanar.CachedData.mpower0_3_r4_2 line 1510
lemma OAI.SharpPlanar.CachedData.mpower0_3_r4_2_eq line 1511
def OAI.SharpPlanar.CachedData.mpower0_3_r4_3 line 1512
lemma OAI.SharpPlanar.CachedData.mpower0_3_r4_3_eq line 1513
def OAI.SharpPlanar.CachedData.mpower0_3_r4_4 line 1514
lemma OAI.SharpPlanar.CachedData.mpower0_3_r4_4_eq line 1515
def OAI.SharpPlanar.CachedData.mpower0_3_r4_5 line 1516
lemma OAI.SharpPlanar.CachedData.mpower0_3_r4_5_eq line 1517
def OAI.SharpPlanar.CachedData.mpower0_3_r4_6 line 1518
lemma OAI.SharpPlanar.CachedData.mpower0_3_r4_6_eq line 1519
def OAI.SharpPlanar.CachedData.mpower0_3_r4_7 line 1520
lemma OAI.SharpPlanar.CachedData.mpower0_3_r4_7_eq line 1521
def OAI.SharpPlanar.CachedData.mpower0_3_r4_8 line 1522
lemma OAI.SharpPlanar.CachedData.mpower0_3_r4_8_eq line 1523
def OAI.SharpPlanar.CachedData.mpower0_3_r4_9 line 1524
lemma OAI.SharpPlanar.CachedData.mpower0_3_r4_9_eq line 1525
def OAI.SharpPlanar.CachedData.mpower0_3_r4_10 line 1526
lemma OAI.SharpPlanar.CachedData.mpower0_3_r4_10_eq line 1527
def OAI.SharpPlanar.CachedData.mpower0_3_r4_11 line 1528
lemma OAI.SharpPlanar.CachedData.mpower0_3_r4_11_eq line 1529
def OAI.SharpPlanar.CachedData.mpower0_3_r4_12 line 1530
lemma OAI.SharpPlanar.CachedData.mpower0_3_r4_12_eq line 1531
def OAI.SharpPlanar.CachedData.mpower0_3_r4_13 line 1532
lemma OAI.SharpPlanar.CachedData.mpower0_3_r4_13_eq line 1533
def OAI.SharpPlanar.CachedData.mpower0_3_r4_14 line 1534
lemma OAI.SharpPlanar.CachedData.mpower0_3_r4_14_eq line 1535
def OAI.SharpPlanar.CachedData.mpower0_3_r4_15 line 1536
lemma OAI.SharpPlanar.CachedData.mpower0_3_r4_15_eq line 1537
def OAI.SharpPlanar.CachedData.mpower0_3_r4 line 1538
lemma OAI.SharpPlanar.CachedData.mpower0_3_r4_eq line 1539
def OAI.SharpPlanar.CachedData.mpower0_3_r5_0 line 1557
lemma OAI.SharpPlanar.CachedData.mpower0_3_r5_0_eq line 1558
def OAI.SharpPlanar.CachedData.mpower0_3_r5_1 line 1559
lemma OAI.SharpPlanar.CachedData.mpower0_3_r5_1_eq line 1560
def OAI.SharpPlanar.CachedData.mpower0_3_r5_2 line 1561
lemma OAI.SharpPlanar.CachedData.mpower0_3_r5_2_eq line 1562
def OAI.SharpPlanar.CachedData.mpower0_3_r5_3 line 1563
lemma OAI.SharpPlanar.CachedData.mpower0_3_r5_3_eq line 1564
def OAI.SharpPlanar.CachedData.mpower0_3_r5_4 line 1565
lemma OAI.SharpPlanar.CachedData.mpower0_3_r5_4_eq line 1566
def OAI.SharpPlanar.CachedData.mpower0_3_r5_5 line 1567
lemma OAI.SharpPlanar.CachedData.mpower0_3_r5_5_eq line 1568
def OAI.SharpPlanar.CachedData.mpower0_3_r5_6 line 1569
lemma OAI.SharpPlanar.CachedData.mpower0_3_r5_6_eq line 1570
def OAI.SharpPlanar.CachedData.mpower0_3_r5_7 line 1571
lemma OAI.SharpPlanar.CachedData.mpower0_3_r5_7_eq line 1572
def OAI.SharpPlanar.CachedData.mpower0_3_r5_8 line 1573
lemma OAI.SharpPlanar.CachedData.mpower0_3_r5_8_eq line 1574
def OAI.SharpPlanar.CachedData.mpower0_3_r5_9 line 1575
lemma OAI.SharpPlanar.CachedData.mpower0_3_r5_9_eq line 1576
def OAI.SharpPlanar.CachedData.mpower0_3_r5_10 line 1577
lemma OAI.SharpPlanar.CachedData.mpower0_3_r5_10_eq line 1578
def OAI.SharpPlanar.CachedData.mpower0_3_r5_11 line 1579
lemma OAI.SharpPlanar.CachedData.mpower0_3_r5_11_eq line 1580
def OAI.SharpPlanar.CachedData.mpower0_3_r5_12 line 1581
lemma OAI.SharpPlanar.CachedData.mpower0_3_r5_12_eq line 1582
def OAI.SharpPlanar.CachedData.mpower0_3_r5_13 line 1583
lemma OAI.SharpPlanar.CachedData.mpower0_3_r5_13_eq line 1584
def OAI.SharpPlanar.CachedData.mpower0_3_r5_14 line 1585
lemma OAI.SharpPlanar.CachedData.mpower0_3_r5_14_eq line 1586
def OAI.SharpPlanar.CachedData.mpower0_3_r5_15 line 1587
lemma OAI.SharpPlanar.CachedData.mpower0_3_r5_15_eq line 1588
def OAI.SharpPlanar.CachedData.mpower0_3_r5 line 1589
lemma OAI.SharpPlanar.CachedData.mpower0_3_r5_eq line 1590
def OAI.SharpPlanar.CachedData.mpower0_3 line 1608
lemma OAI.SharpPlanar.CachedData.mpower0_3_eq line 1609
lemma OAI.SharpPlanar.CachedData.mpower0_3_contains line 1617
def OAI.SharpPlanar.CachedData.mpower1_3Expr line 1621
def OAI.SharpPlanar.CachedData.mpower1_3_r0_0 line 1622
lemma OAI.SharpPlanar.CachedData.mpower1_3_r0_0_eq line 1623
def OAI.SharpPlanar.CachedData.mpower1_3_r0_1 line 1624
lemma OAI.SharpPlanar.CachedData.mpower1_3_r0_1_eq line 1625
def OAI.SharpPlanar.CachedData.mpower1_3_r0_2 line 1626
lemma OAI.SharpPlanar.CachedData.mpower1_3_r0_2_eq line 1627
def OAI.SharpPlanar.CachedData.mpower1_3_r0_3 line 1628
lemma OAI.SharpPlanar.CachedData.mpower1_3_r0_3_eq line 1629
def OAI.SharpPlanar.CachedData.mpower1_3_r0_4 line 1630
lemma OAI.SharpPlanar.CachedData.mpower1_3_r0_4_eq line 1631
def OAI.SharpPlanar.CachedData.mpower1_3_r0_5 line 1632
lemma OAI.SharpPlanar.CachedData.mpower1_3_r0_5_eq line 1633
def OAI.SharpPlanar.CachedData.mpower1_3_r0_6 line 1634
lemma OAI.SharpPlanar.CachedData.mpower1_3_r0_6_eq line 1635
def OAI.SharpPlanar.CachedData.mpower1_3_r0_7 line 1636
lemma OAI.SharpPlanar.CachedData.mpower1_3_r0_7_eq line 1637
def OAI.SharpPlanar.CachedData.mpower1_3_r0_8 line 1638
lemma OAI.SharpPlanar.CachedData.mpower1_3_r0_8_eq line 1639
def OAI.SharpPlanar.CachedData.mpower1_3_r0_9 line 1640
lemma OAI.SharpPlanar.CachedData.mpower1_3_r0_9_eq line 1641
def OAI.SharpPlanar.CachedData.mpower1_3_r0_10 line 1642
lemma OAI.SharpPlanar.CachedData.mpower1_3_r0_10_eq line 1643
def OAI.SharpPlanar.CachedData.mpower1_3_r0_11 line 1644
lemma OAI.SharpPlanar.CachedData.mpower1_3_r0_11_eq line 1645
def OAI.SharpPlanar.CachedData.mpower1_3_r0_12 line 1646
lemma OAI.SharpPlanar.CachedData.mpower1_3_r0_12_eq line 1647
def OAI.SharpPlanar.CachedData.mpower1_3_r0_13 line 1648
lemma OAI.SharpPlanar.CachedData.mpower1_3_r0_13_eq line 1649
def OAI.SharpPlanar.CachedData.mpower1_3_r0_14 line 1650
lemma OAI.SharpPlanar.CachedData.mpower1_3_r0_14_eq line 1651
def OAI.SharpPlanar.CachedData.mpower1_3_r0_15 line 1652
lemma OAI.SharpPlanar.CachedData.mpower1_3_r0_15_eq line 1653
def OAI.SharpPlanar.CachedData.mpower1_3_r0 line 1654
lemma OAI.SharpPlanar.CachedData.mpower1_3_r0_eq line 1655
def OAI.SharpPlanar.CachedData.mpower1_3_r1_0 line 1673
lemma OAI.SharpPlanar.CachedData.mpower1_3_r1_0_eq line 1674
def OAI.SharpPlanar.CachedData.mpower1_3_r1_1 line 1675
lemma OAI.SharpPlanar.CachedData.mpower1_3_r1_1_eq line 1676
def OAI.SharpPlanar.CachedData.mpower1_3_r1_2 line 1677
lemma OAI.SharpPlanar.CachedData.mpower1_3_r1_2_eq line 1678
def OAI.SharpPlanar.CachedData.mpower1_3_r1_3 line 1679
lemma OAI.SharpPlanar.CachedData.mpower1_3_r1_3_eq line 1680
def OAI.SharpPlanar.CachedData.mpower1_3_r1_4 line 1681
lemma OAI.SharpPlanar.CachedData.mpower1_3_r1_4_eq line 1682
def OAI.SharpPlanar.CachedData.mpower1_3_r1_5 line 1683
lemma OAI.SharpPlanar.CachedData.mpower1_3_r1_5_eq line 1684
def OAI.SharpPlanar.CachedData.mpower1_3_r1_6 line 1685
lemma OAI.SharpPlanar.CachedData.mpower1_3_r1_6_eq line 1686
def OAI.SharpPlanar.CachedData.mpower1_3_r1_7 line 1687
lemma OAI.SharpPlanar.CachedData.mpower1_3_r1_7_eq line 1688
def OAI.SharpPlanar.CachedData.mpower1_3_r1_8 line 1689
lemma OAI.SharpPlanar.CachedData.mpower1_3_r1_8_eq line 1690
def OAI.SharpPlanar.CachedData.mpower1_3_r1_9 line 1691
lemma OAI.SharpPlanar.CachedData.mpower1_3_r1_9_eq line 1692
def OAI.SharpPlanar.CachedData.mpower1_3_r1_10 line 1693
lemma OAI.SharpPlanar.CachedData.mpower1_3_r1_10_eq line 1694
def OAI.SharpPlanar.CachedData.mpower1_3_r1_11 line 1695
lemma OAI.SharpPlanar.CachedData.mpower1_3_r1_11_eq line 1696
def OAI.SharpPlanar.CachedData.mpower1_3_r1_12 line 1697
lemma OAI.SharpPlanar.CachedData.mpower1_3_r1_12_eq line 1698
def OAI.SharpPlanar.CachedData.mpower1_3_r1_13 line 1699
lemma OAI.SharpPlanar.CachedData.mpower1_3_r1_13_eq line 1700
def OAI.SharpPlanar.CachedData.mpower1_3_r1_14 line 1701
lemma OAI.SharpPlanar.CachedData.mpower1_3_r1_14_eq line 1702
def OAI.SharpPlanar.CachedData.mpower1_3_r1_15 line 1703
lemma OAI.SharpPlanar.CachedData.mpower1_3_r1_15_eq line 1704
def OAI.SharpPlanar.CachedData.mpower1_3_r1 line 1705
lemma OAI.SharpPlanar.CachedData.mpower1_3_r1_eq line 1706
def OAI.SharpPlanar.CachedData.mpower1_3_r2_0 line 1724
lemma OAI.SharpPlanar.CachedData.mpower1_3_r2_0_eq line 1725
def OAI.SharpPlanar.CachedData.mpower1_3_r2_1 line 1726
lemma OAI.SharpPlanar.CachedData.mpower1_3_r2_1_eq line 1727
def OAI.SharpPlanar.CachedData.mpower1_3_r2_2 line 1728
lemma OAI.SharpPlanar.CachedData.mpower1_3_r2_2_eq line 1729
def OAI.SharpPlanar.CachedData.mpower1_3_r2_3 line 1730
lemma OAI.SharpPlanar.CachedData.mpower1_3_r2_3_eq line 1731
def OAI.SharpPlanar.CachedData.mpower1_3_r2_4 line 1732
lemma OAI.SharpPlanar.CachedData.mpower1_3_r2_4_eq line 1733
def OAI.SharpPlanar.CachedData.mpower1_3_r2_5 line 1734
lemma OAI.SharpPlanar.CachedData.mpower1_3_r2_5_eq line 1735
def OAI.SharpPlanar.CachedData.mpower1_3_r2_6 line 1736
lemma OAI.SharpPlanar.CachedData.mpower1_3_r2_6_eq line 1737
def OAI.SharpPlanar.CachedData.mpower1_3_r2_7 line 1738
lemma OAI.SharpPlanar.CachedData.mpower1_3_r2_7_eq line 1739
def OAI.SharpPlanar.CachedData.mpower1_3_r2_8 line 1740
lemma OAI.SharpPlanar.CachedData.mpower1_3_r2_8_eq line 1741
def OAI.SharpPlanar.CachedData.mpower1_3_r2_9 line 1742
lemma OAI.SharpPlanar.CachedData.mpower1_3_r2_9_eq line 1743
def OAI.SharpPlanar.CachedData.mpower1_3_r2_10 line 1744
lemma OAI.SharpPlanar.CachedData.mpower1_3_r2_10_eq line 1745
def OAI.SharpPlanar.CachedData.mpower1_3_r2_11 line 1746
lemma OAI.SharpPlanar.CachedData.mpower1_3_r2_11_eq line 1747
def OAI.SharpPlanar.CachedData.mpower1_3_r2_12 line 1748
lemma OAI.SharpPlanar.CachedData.mpower1_3_r2_12_eq line 1749
def OAI.SharpPlanar.CachedData.mpower1_3_r2_13 line 1750
lemma OAI.SharpPlanar.CachedData.mpower1_3_r2_13_eq line 1751
def OAI.SharpPlanar.CachedData.mpower1_3_r2_14 line 1752
lemma OAI.SharpPlanar.CachedData.mpower1_3_r2_14_eq line 1753
def OAI.SharpPlanar.CachedData.mpower1_3_r2_15 line 1754
lemma OAI.SharpPlanar.CachedData.mpower1_3_r2_15_eq line 1755
def OAI.SharpPlanar.CachedData.mpower1_3_r2 line 1756
lemma OAI.SharpPlanar.CachedData.mpower1_3_r2_eq line 1757
def OAI.SharpPlanar.CachedData.mpower1_3_r3_0 line 1775
lemma OAI.SharpPlanar.CachedData.mpower1_3_r3_0_eq line 1776
def OAI.SharpPlanar.CachedData.mpower1_3_r3_1 line 1777
lemma OAI.SharpPlanar.CachedData.mpower1_3_r3_1_eq line 1778
def OAI.SharpPlanar.CachedData.mpower1_3_r3_2 line 1779
lemma OAI.SharpPlanar.CachedData.mpower1_3_r3_2_eq line 1780
def OAI.SharpPlanar.CachedData.mpower1_3_r3_3 line 1781
lemma OAI.SharpPlanar.CachedData.mpower1_3_r3_3_eq line 1782
def OAI.SharpPlanar.CachedData.mpower1_3_r3_4 line 1783
lemma OAI.SharpPlanar.CachedData.mpower1_3_r3_4_eq line 1784
def OAI.SharpPlanar.CachedData.mpower1_3_r3_5 line 1785
lemma OAI.SharpPlanar.CachedData.mpower1_3_r3_5_eq line 1786
def OAI.SharpPlanar.CachedData.mpower1_3_r3_6 line 1787
lemma OAI.SharpPlanar.CachedData.mpower1_3_r3_6_eq line 1788
def OAI.SharpPlanar.CachedData.mpower1_3_r3_7 line 1789
lemma OAI.SharpPlanar.CachedData.mpower1_3_r3_7_eq line 1790
def OAI.SharpPlanar.CachedData.mpower1_3_r3_8 line 1791
lemma OAI.SharpPlanar.CachedData.mpower1_3_r3_8_eq line 1792
def OAI.SharpPlanar.CachedData.mpower1_3_r3_9 line 1793
lemma OAI.SharpPlanar.CachedData.mpower1_3_r3_9_eq line 1794
def OAI.SharpPlanar.CachedData.mpower1_3_r3_10 line 1795
lemma OAI.SharpPlanar.CachedData.mpower1_3_r3_10_eq line 1796
def OAI.SharpPlanar.CachedData.mpower1_3_r3_11 line 1797
lemma OAI.SharpPlanar.CachedData.mpower1_3_r3_11_eq line 1798
def OAI.SharpPlanar.CachedData.mpower1_3_r3_12 line 1799
lemma OAI.SharpPlanar.CachedData.mpower1_3_r3_12_eq line 1800
def OAI.SharpPlanar.CachedData.mpower1_3_r3_13 line 1801
lemma OAI.SharpPlanar.CachedData.mpower1_3_r3_13_eq line 1802
def OAI.SharpPlanar.CachedData.mpower1_3_r3_14 line 1803
lemma OAI.SharpPlanar.CachedData.mpower1_3_r3_14_eq line 1804
def OAI.SharpPlanar.CachedData.mpower1_3_r3_15 line 1805
lemma OAI.SharpPlanar.CachedData.mpower1_3_r3_15_eq line 1806
def OAI.SharpPlanar.CachedData.mpower1_3_r3 line 1807
lemma OAI.SharpPlanar.CachedData.mpower1_3_r3_eq line 1808
def OAI.SharpPlanar.CachedData.mpower1_3_r4_0 line 1826
lemma OAI.SharpPlanar.CachedData.mpower1_3_r4_0_eq line 1827
def OAI.SharpPlanar.CachedData.mpower1_3_r4_1 line 1828
lemma OAI.SharpPlanar.CachedData.mpower1_3_r4_1_eq line 1829
def OAI.SharpPlanar.CachedData.mpower1_3_r4_2 line 1830
lemma OAI.SharpPlanar.CachedData.mpower1_3_r4_2_eq line 1831
def OAI.SharpPlanar.CachedData.mpower1_3_r4_3 line 1832
lemma OAI.SharpPlanar.CachedData.mpower1_3_r4_3_eq line 1833
def OAI.SharpPlanar.CachedData.mpower1_3_r4_4 line 1834
lemma OAI.SharpPlanar.CachedData.mpower1_3_r4_4_eq line 1835
def OAI.SharpPlanar.CachedData.mpower1_3_r4_5 line 1836
lemma OAI.SharpPlanar.CachedData.mpower1_3_r4_5_eq line 1837
def OAI.SharpPlanar.CachedData.mpower1_3_r4_6 line 1838
lemma OAI.SharpPlanar.CachedData.mpower1_3_r4_6_eq line 1839
def OAI.SharpPlanar.CachedData.mpower1_3_r4_7 line 1840
lemma OAI.SharpPlanar.CachedData.mpower1_3_r4_7_eq line 1841
def OAI.SharpPlanar.CachedData.mpower1_3_r4_8 line 1842
lemma OAI.SharpPlanar.CachedData.mpower1_3_r4_8_eq line 1843
def OAI.SharpPlanar.CachedData.mpower1_3_r4_9 line 1844
lemma OAI.SharpPlanar.CachedData.mpower1_3_r4_9_eq line 1845
def OAI.SharpPlanar.CachedData.mpower1_3_r4_10 line 1846
lemma OAI.SharpPlanar.CachedData.mpower1_3_r4_10_eq line 1847
def OAI.SharpPlanar.CachedData.mpower1_3_r4_11 line 1848
lemma OAI.SharpPlanar.CachedData.mpower1_3_r4_11_eq line 1849
def OAI.SharpPlanar.CachedData.mpower1_3_r4_12 line 1850
lemma OAI.SharpPlanar.CachedData.mpower1_3_r4_12_eq line 1851
def OAI.SharpPlanar.CachedData.mpower1_3_r4_13 line 1852
lemma OAI.SharpPlanar.CachedData.mpower1_3_r4_13_eq line 1853
def OAI.SharpPlanar.CachedData.mpower1_3_r4_14 line 1854
lemma OAI.SharpPlanar.CachedData.mpower1_3_r4_14_eq line 1855
def OAI.SharpPlanar.CachedData.mpower1_3_r4_15 line 1856
lemma OAI.SharpPlanar.CachedData.mpower1_3_r4_15_eq line 1857
def OAI.SharpPlanar.CachedData.mpower1_3_r4 line 1858
lemma OAI.SharpPlanar.CachedData.mpower1_3_r4_eq line 1859
def OAI.SharpPlanar.CachedData.mpower1_3_r5_0 line 1877
lemma OAI.SharpPlanar.CachedData.mpower1_3_r5_0_eq line 1878
def OAI.SharpPlanar.CachedData.mpower1_3_r5_1 line 1879
lemma OAI.SharpPlanar.CachedData.mpower1_3_r5_1_eq line 1880
def OAI.SharpPlanar.CachedData.mpower1_3_r5_2 line 1881
lemma OAI.SharpPlanar.CachedData.mpower1_3_r5_2_eq line 1882
def OAI.SharpPlanar.CachedData.mpower1_3_r5_3 line 1883
lemma OAI.SharpPlanar.CachedData.mpower1_3_r5_3_eq line 1884
def OAI.SharpPlanar.CachedData.mpower1_3_r5_4 line 1885
lemma OAI.SharpPlanar.CachedData.mpower1_3_r5_4_eq line 1886
def OAI.SharpPlanar.CachedData.mpower1_3_r5_5 line 1887
lemma OAI.SharpPlanar.CachedData.mpower1_3_r5_5_eq line 1888
def OAI.SharpPlanar.CachedData.mpower1_3_r5_6 line 1889
lemma OAI.SharpPlanar.CachedData.mpower1_3_r5_6_eq line 1890
def OAI.SharpPlanar.CachedData.mpower1_3_r5_7 line 1891
lemma OAI.SharpPlanar.CachedData.mpower1_3_r5_7_eq line 1892
def OAI.SharpPlanar.CachedData.mpower1_3_r5_8 line 1893
lemma OAI.SharpPlanar.CachedData.mpower1_3_r5_8_eq line 1894
def OAI.SharpPlanar.CachedData.mpower1_3_r5_9 line 1895
lemma OAI.SharpPlanar.CachedData.mpower1_3_r5_9_eq line 1896
def OAI.SharpPlanar.CachedData.mpower1_3_r5_10 line 1897
lemma OAI.SharpPlanar.CachedData.mpower1_3_r5_10_eq line 1898
def OAI.SharpPlanar.CachedData.mpower1_3_r5_11 line 1899
lemma OAI.SharpPlanar.CachedData.mpower1_3_r5_11_eq line 1900
def OAI.SharpPlanar.CachedData.mpower1_3_r5_12 line 1901
lemma OAI.SharpPlanar.CachedData.mpower1_3_r5_12_eq line 1902
def OAI.SharpPlanar.CachedData.mpower1_3_r5_13 line 1903
lemma OAI.SharpPlanar.CachedData.mpower1_3_r5_13_eq line 1904
def OAI.SharpPlanar.CachedData.mpower1_3_r5_14 line 1905
lemma OAI.SharpPlanar.CachedData.mpower1_3_r5_14_eq line 1906
def OAI.SharpPlanar.CachedData.mpower1_3_r5_15 line 1907
lemma OAI.SharpPlanar.CachedData.mpower1_3_r5_15_eq line 1908
def OAI.SharpPlanar.CachedData.mpower1_3_r5 line 1909
lemma OAI.SharpPlanar.CachedData.mpower1_3_r5_eq line 1910
def OAI.SharpPlanar.CachedData.mpower1_3 line 1928
lemma OAI.SharpPlanar.CachedData.mpower1_3_eq line 1929
lemma OAI.SharpPlanar.CachedData.mpower1_3_contains line 1937
def OAI.SharpPlanar.CachedData.mpower0_4Expr line 1941
def OAI.SharpPlanar.CachedData.mpower0_4_r0_0 line 1942
lemma OAI.SharpPlanar.CachedData.mpower0_4_r0_0_eq line 1943
def OAI.SharpPlanar.CachedData.mpower0_4_r0_1 line 1944
lemma OAI.SharpPlanar.CachedData.mpower0_4_r0_1_eq line 1945
def OAI.SharpPlanar.CachedData.mpower0_4_r0_2 line 1946
lemma OAI.SharpPlanar.CachedData.mpower0_4_r0_2_eq line 1947
def OAI.SharpPlanar.CachedData.mpower0_4_r0_3 line 1948
lemma OAI.SharpPlanar.CachedData.mpower0_4_r0_3_eq line 1949
def OAI.SharpPlanar.CachedData.mpower0_4_r0_4 line 1950
lemma OAI.SharpPlanar.CachedData.mpower0_4_r0_4_eq line 1951
def OAI.SharpPlanar.CachedData.mpower0_4_r0_5 line 1952
lemma OAI.SharpPlanar.CachedData.mpower0_4_r0_5_eq line 1953
def OAI.SharpPlanar.CachedData.mpower0_4_r0_6 line 1954
lemma OAI.SharpPlanar.CachedData.mpower0_4_r0_6_eq line 1955
def OAI.SharpPlanar.CachedData.mpower0_4_r0_7 line 1956
lemma OAI.SharpPlanar.CachedData.mpower0_4_r0_7_eq line 1957
def OAI.SharpPlanar.CachedData.mpower0_4_r0_8 line 1958
lemma OAI.SharpPlanar.CachedData.mpower0_4_r0_8_eq line 1959
def OAI.SharpPlanar.CachedData.mpower0_4_r0_9 line 1960
lemma OAI.SharpPlanar.CachedData.mpower0_4_r0_9_eq line 1961
def OAI.SharpPlanar.CachedData.mpower0_4_r0_10 line 1962
lemma OAI.SharpPlanar.CachedData.mpower0_4_r0_10_eq line 1963
def OAI.SharpPlanar.CachedData.mpower0_4_r0_11 line 1964
lemma OAI.SharpPlanar.CachedData.mpower0_4_r0_11_eq line 1965
def OAI.SharpPlanar.CachedData.mpower0_4_r0_12 line 1966
lemma OAI.SharpPlanar.CachedData.mpower0_4_r0_12_eq line 1967
def OAI.SharpPlanar.CachedData.mpower0_4_r0_13 line 1968
lemma OAI.SharpPlanar.CachedData.mpower0_4_r0_13_eq line 1969
def OAI.SharpPlanar.CachedData.mpower0_4_r0_14 line 1970
lemma OAI.SharpPlanar.CachedData.mpower0_4_r0_14_eq line 1971
def OAI.SharpPlanar.CachedData.mpower0_4_r0_15 line 1972
lemma OAI.SharpPlanar.CachedData.mpower0_4_r0_15_eq line 1973
def OAI.SharpPlanar.CachedData.mpower0_4_r0 line 1974
lemma OAI.SharpPlanar.CachedData.mpower0_4_r0_eq line 1975
def OAI.SharpPlanar.CachedData.mpower0_4_r1_0 line 1993
lemma OAI.SharpPlanar.CachedData.mpower0_4_r1_0_eq line 1994
def OAI.SharpPlanar.CachedData.mpower0_4_r1_1 line 1995
lemma OAI.SharpPlanar.CachedData.mpower0_4_r1_1_eq line 1996
def OAI.SharpPlanar.CachedData.mpower0_4_r1_2 line 1997
lemma OAI.SharpPlanar.CachedData.mpower0_4_r1_2_eq line 1998
def OAI.SharpPlanar.CachedData.mpower0_4_r1_3 line 1999
lemma OAI.SharpPlanar.CachedData.mpower0_4_r1_3_eq line 2000
def OAI.SharpPlanar.CachedData.mpower0_4_r1_4 line 2001
lemma OAI.SharpPlanar.CachedData.mpower0_4_r1_4_eq line 2002
def OAI.SharpPlanar.CachedData.mpower0_4_r1_5 line 2003
lemma OAI.SharpPlanar.CachedData.mpower0_4_r1_5_eq line 2004
def OAI.SharpPlanar.CachedData.mpower0_4_r1_6 line 2005
lemma OAI.SharpPlanar.CachedData.mpower0_4_r1_6_eq line 2006
def OAI.SharpPlanar.CachedData.mpower0_4_r1_7 line 2007
lemma OAI.SharpPlanar.CachedData.mpower0_4_r1_7_eq line 2008
def OAI.SharpPlanar.CachedData.mpower0_4_r1_8 line 2009
lemma OAI.SharpPlanar.CachedData.mpower0_4_r1_8_eq line 2010
def OAI.SharpPlanar.CachedData.mpower0_4_r1_9 line 2011
lemma OAI.SharpPlanar.CachedData.mpower0_4_r1_9_eq line 2012
def OAI.SharpPlanar.CachedData.mpower0_4_r1_10 line 2013
lemma OAI.SharpPlanar.CachedData.mpower0_4_r1_10_eq line 2014
def OAI.SharpPlanar.CachedData.mpower0_4_r1_11 line 2015
lemma OAI.SharpPlanar.CachedData.mpower0_4_r1_11_eq line 2016
def OAI.SharpPlanar.CachedData.mpower0_4_r1_12 line 2017
lemma OAI.SharpPlanar.CachedData.mpower0_4_r1_12_eq line 2018
def OAI.SharpPlanar.CachedData.mpower0_4_r1_13 line 2019
lemma OAI.SharpPlanar.CachedData.mpower0_4_r1_13_eq line 2020
def OAI.SharpPlanar.CachedData.mpower0_4_r1_14 line 2021
lemma OAI.SharpPlanar.CachedData.mpower0_4_r1_14_eq line 2022
def OAI.SharpPlanar.CachedData.mpower0_4_r1_15 line 2023
lemma OAI.SharpPlanar.CachedData.mpower0_4_r1_15_eq line 2024
def OAI.SharpPlanar.CachedData.mpower0_4_r1 line 2025
lemma OAI.SharpPlanar.CachedData.mpower0_4_r1_eq line 2026
def OAI.SharpPlanar.CachedData.mpower0_4_r2_0 line 2044
lemma OAI.SharpPlanar.CachedData.mpower0_4_r2_0_eq line 2045
def OAI.SharpPlanar.CachedData.mpower0_4_r2_1 line 2046
lemma OAI.SharpPlanar.CachedData.mpower0_4_r2_1_eq line 2047
def OAI.SharpPlanar.CachedData.mpower0_4_r2_2 line 2048
lemma OAI.SharpPlanar.CachedData.mpower0_4_r2_2_eq line 2049
def OAI.SharpPlanar.CachedData.mpower0_4_r2_3 line 2050
lemma OAI.SharpPlanar.CachedData.mpower0_4_r2_3_eq line 2051
def OAI.SharpPlanar.CachedData.mpower0_4_r2_4 line 2052
lemma OAI.SharpPlanar.CachedData.mpower0_4_r2_4_eq line 2053
def OAI.SharpPlanar.CachedData.mpower0_4_r2_5 line 2054
lemma OAI.SharpPlanar.CachedData.mpower0_4_r2_5_eq line 2055
def OAI.SharpPlanar.CachedData.mpower0_4_r2_6 line 2056
lemma OAI.SharpPlanar.CachedData.mpower0_4_r2_6_eq line 2057
def OAI.SharpPlanar.CachedData.mpower0_4_r2_7 line 2058
lemma OAI.SharpPlanar.CachedData.mpower0_4_r2_7_eq line 2059
def OAI.SharpPlanar.CachedData.mpower0_4_r2_8 line 2060
lemma OAI.SharpPlanar.CachedData.mpower0_4_r2_8_eq line 2061
def OAI.SharpPlanar.CachedData.mpower0_4_r2_9 line 2062
lemma OAI.SharpPlanar.CachedData.mpower0_4_r2_9_eq line 2063
def OAI.SharpPlanar.CachedData.mpower0_4_r2_10 line 2064
lemma OAI.SharpPlanar.CachedData.mpower0_4_r2_10_eq line 2065
def OAI.SharpPlanar.CachedData.mpower0_4_r2_11 line 2066
lemma OAI.SharpPlanar.CachedData.mpower0_4_r2_11_eq line 2067
def OAI.SharpPlanar.CachedData.mpower0_4_r2_12 line 2068
lemma OAI.SharpPlanar.CachedData.mpower0_4_r2_12_eq line 2069
def OAI.SharpPlanar.CachedData.mpower0_4_r2_13 line 2070
lemma OAI.SharpPlanar.CachedData.mpower0_4_r2_13_eq line 2071
def OAI.SharpPlanar.CachedData.mpower0_4_r2_14 line 2072
lemma OAI.SharpPlanar.CachedData.mpower0_4_r2_14_eq line 2073
def OAI.SharpPlanar.CachedData.mpower0_4_r2_15 line 2074
lemma OAI.SharpPlanar.CachedData.mpower0_4_r2_15_eq line 2075
def OAI.SharpPlanar.CachedData.mpower0_4_r2 line 2076
lemma OAI.SharpPlanar.CachedData.mpower0_4_r2_eq line 2077
def OAI.SharpPlanar.CachedData.mpower0_4_r3_0 line 2095
lemma OAI.SharpPlanar.CachedData.mpower0_4_r3_0_eq line 2096
def OAI.SharpPlanar.CachedData.mpower0_4_r3_1 line 2097
lemma OAI.SharpPlanar.CachedData.mpower0_4_r3_1_eq line 2098
def OAI.SharpPlanar.CachedData.mpower0_4_r3_2 line 2099
lemma OAI.SharpPlanar.CachedData.mpower0_4_r3_2_eq line 2100
def OAI.SharpPlanar.CachedData.mpower0_4_r3_3 line 2101
lemma OAI.SharpPlanar.CachedData.mpower0_4_r3_3_eq line 2102
def OAI.SharpPlanar.CachedData.mpower0_4_r3_4 line 2103
lemma OAI.SharpPlanar.CachedData.mpower0_4_r3_4_eq line 2104
def OAI.SharpPlanar.CachedData.mpower0_4_r3_5 line 2105
lemma OAI.SharpPlanar.CachedData.mpower0_4_r3_5_eq line 2106
def OAI.SharpPlanar.CachedData.mpower0_4_r3_6 line 2107
lemma OAI.SharpPlanar.CachedData.mpower0_4_r3_6_eq line 2108
def OAI.SharpPlanar.CachedData.mpower0_4_r3_7 line 2109
lemma OAI.SharpPlanar.CachedData.mpower0_4_r3_7_eq line 2110
def OAI.SharpPlanar.CachedData.mpower0_4_r3_8 line 2111
lemma OAI.SharpPlanar.CachedData.mpower0_4_r3_8_eq line 2112
def OAI.SharpPlanar.CachedData.mpower0_4_r3_9 line 2113
lemma OAI.SharpPlanar.CachedData.mpower0_4_r3_9_eq line 2114
def OAI.SharpPlanar.CachedData.mpower0_4_r3_10 line 2115
lemma OAI.SharpPlanar.CachedData.mpower0_4_r3_10_eq line 2116
def OAI.SharpPlanar.CachedData.mpower0_4_r3_11 line 2117
lemma OAI.SharpPlanar.CachedData.mpower0_4_r3_11_eq line 2118
def OAI.SharpPlanar.CachedData.mpower0_4_r3_12 line 2119
lemma OAI.SharpPlanar.CachedData.mpower0_4_r3_12_eq line 2120
def OAI.SharpPlanar.CachedData.mpower0_4_r3_13 line 2121
lemma OAI.SharpPlanar.CachedData.mpower0_4_r3_13_eq line 2122
def OAI.SharpPlanar.CachedData.mpower0_4_r3_14 line 2123
lemma OAI.SharpPlanar.CachedData.mpower0_4_r3_14_eq line 2124
def OAI.SharpPlanar.CachedData.mpower0_4_r3_15 line 2125
lemma OAI.SharpPlanar.CachedData.mpower0_4_r3_15_eq line 2126
def OAI.SharpPlanar.CachedData.mpower0_4_r3 line 2127
lemma OAI.SharpPlanar.CachedData.mpower0_4_r3_eq line 2128
def OAI.SharpPlanar.CachedData.mpower0_4_r4_0 line 2146
lemma OAI.SharpPlanar.CachedData.mpower0_4_r4_0_eq line 2147
def OAI.SharpPlanar.CachedData.mpower0_4_r4_1 line 2148
lemma OAI.SharpPlanar.CachedData.mpower0_4_r4_1_eq line 2149
def OAI.SharpPlanar.CachedData.mpower0_4_r4_2 line 2150
lemma OAI.SharpPlanar.CachedData.mpower0_4_r4_2_eq line 2151
def OAI.SharpPlanar.CachedData.mpower0_4_r4_3 line 2152
lemma OAI.SharpPlanar.CachedData.mpower0_4_r4_3_eq line 2153
def OAI.SharpPlanar.CachedData.mpower0_4_r4_4 line 2154
lemma OAI.SharpPlanar.CachedData.mpower0_4_r4_4_eq line 2155
def OAI.SharpPlanar.CachedData.mpower0_4_r4_5 line 2156
lemma OAI.SharpPlanar.CachedData.mpower0_4_r4_5_eq line 2157
def OAI.SharpPlanar.CachedData.mpower0_4_r4_6 line 2158
lemma OAI.SharpPlanar.CachedData.mpower0_4_r4_6_eq line 2159
def OAI.SharpPlanar.CachedData.mpower0_4_r4_7 line 2160
lemma OAI.SharpPlanar.CachedData.mpower0_4_r4_7_eq line 2161
def OAI.SharpPlanar.CachedData.mpower0_4_r4_8 line 2162
lemma OAI.SharpPlanar.CachedData.mpower0_4_r4_8_eq line 2163
def OAI.SharpPlanar.CachedData.mpower0_4_r4_9 line 2164
lemma OAI.SharpPlanar.CachedData.mpower0_4_r4_9_eq line 2165
def OAI.SharpPlanar.CachedData.mpower0_4_r4_10 line 2166
lemma OAI.SharpPlanar.CachedData.mpower0_4_r4_10_eq line 2167
def OAI.SharpPlanar.CachedData.mpower0_4_r4_11 line 2168
lemma OAI.SharpPlanar.CachedData.mpower0_4_r4_11_eq line 2169
def OAI.SharpPlanar.CachedData.mpower0_4_r4_12 line 2170
lemma OAI.SharpPlanar.CachedData.mpower0_4_r4_12_eq line 2171
def OAI.SharpPlanar.CachedData.mpower0_4_r4_13 line 2172
lemma OAI.SharpPlanar.CachedData.mpower0_4_r4_13_eq line 2173
def OAI.SharpPlanar.CachedData.mpower0_4_r4_14 line 2174
lemma OAI.SharpPlanar.CachedData.mpower0_4_r4_14_eq line 2175
def OAI.SharpPlanar.CachedData.mpower0_4_r4_15 line 2176
lemma OAI.SharpPlanar.CachedData.mpower0_4_r4_15_eq line 2177
def OAI.SharpPlanar.CachedData.mpower0_4_r4 line 2178
lemma OAI.SharpPlanar.CachedData.mpower0_4_r4_eq line 2179
def OAI.SharpPlanar.CachedData.mpower0_4_r5_0 line 2197
lemma OAI.SharpPlanar.CachedData.mpower0_4_r5_0_eq line 2198
def OAI.SharpPlanar.CachedData.mpower0_4_r5_1 line 2199
lemma OAI.SharpPlanar.CachedData.mpower0_4_r5_1_eq line 2200
def OAI.SharpPlanar.CachedData.mpower0_4_r5_2 line 2201
lemma OAI.SharpPlanar.CachedData.mpower0_4_r5_2_eq line 2202
def OAI.SharpPlanar.CachedData.mpower0_4_r5_3 line 2203
lemma OAI.SharpPlanar.CachedData.mpower0_4_r5_3_eq line 2204
def OAI.SharpPlanar.CachedData.mpower0_4_r5_4 line 2205
lemma OAI.SharpPlanar.CachedData.mpower0_4_r5_4_eq line 2206
def OAI.SharpPlanar.CachedData.mpower0_4_r5_5 line 2207
lemma OAI.SharpPlanar.CachedData.mpower0_4_r5_5_eq line 2208
def OAI.SharpPlanar.CachedData.mpower0_4_r5_6 line 2209
lemma OAI.SharpPlanar.CachedData.mpower0_4_r5_6_eq line 2210
def OAI.SharpPlanar.CachedData.mpower0_4_r5_7 line 2211
lemma OAI.SharpPlanar.CachedData.mpower0_4_r5_7_eq line 2212
def OAI.SharpPlanar.CachedData.mpower0_4_r5_8 line 2213
lemma OAI.SharpPlanar.CachedData.mpower0_4_r5_8_eq line 2214
def OAI.SharpPlanar.CachedData.mpower0_4_r5_9 line 2215
lemma OAI.SharpPlanar.CachedData.mpower0_4_r5_9_eq line 2216
def OAI.SharpPlanar.CachedData.mpower0_4_r5_10 line 2217
lemma OAI.SharpPlanar.CachedData.mpower0_4_r5_10_eq line 2218
def OAI.SharpPlanar.CachedData.mpower0_4_r5_11 line 2219
lemma OAI.SharpPlanar.CachedData.mpower0_4_r5_11_eq line 2220
def OAI.SharpPlanar.CachedData.mpower0_4_r5_12 line 2221
lemma OAI.SharpPlanar.CachedData.mpower0_4_r5_12_eq line 2222
def OAI.SharpPlanar.CachedData.mpower0_4_r5_13 line 2223
lemma OAI.SharpPlanar.CachedData.mpower0_4_r5_13_eq line 2224
def OAI.SharpPlanar.CachedData.mpower0_4_r5_14 line 2225
lemma OAI.SharpPlanar.CachedData.mpower0_4_r5_14_eq line 2226
def OAI.SharpPlanar.CachedData.mpower0_4_r5_15 line 2227
lemma OAI.SharpPlanar.CachedData.mpower0_4_r5_15_eq line 2228
def OAI.SharpPlanar.CachedData.mpower0_4_r5 line 2229
lemma OAI.SharpPlanar.CachedData.mpower0_4_r5_eq line 2230
def OAI.SharpPlanar.CachedData.mpower0_4 line 2248
lemma OAI.SharpPlanar.CachedData.mpower0_4_eq line 2249
lemma OAI.SharpPlanar.CachedData.mpower0_4_contains line 2257
def OAI.SharpPlanar.CachedData.mpower1_4Expr line 2261
def OAI.SharpPlanar.CachedData.mpower1_4_r0_0 line 2262
lemma OAI.SharpPlanar.CachedData.mpower1_4_r0_0_eq line 2263
def OAI.SharpPlanar.CachedData.mpower1_4_r0_1 line 2264
lemma OAI.SharpPlanar.CachedData.mpower1_4_r0_1_eq line 2265
def OAI.SharpPlanar.CachedData.mpower1_4_r0_2 line 2266
lemma OAI.SharpPlanar.CachedData.mpower1_4_r0_2_eq line 2267
def OAI.SharpPlanar.CachedData.mpower1_4_r0_3 line 2268
lemma OAI.SharpPlanar.CachedData.mpower1_4_r0_3_eq line 2269
def OAI.SharpPlanar.CachedData.mpower1_4_r0_4 line 2270
lemma OAI.SharpPlanar.CachedData.mpower1_4_r0_4_eq line 2271
def OAI.SharpPlanar.CachedData.mpower1_4_r0_5 line 2272
lemma OAI.SharpPlanar.CachedData.mpower1_4_r0_5_eq line 2273
def OAI.SharpPlanar.CachedData.mpower1_4_r0_6 line 2274
lemma OAI.SharpPlanar.CachedData.mpower1_4_r0_6_eq line 2275
def OAI.SharpPlanar.CachedData.mpower1_4_r0_7 line 2276
lemma OAI.SharpPlanar.CachedData.mpower1_4_r0_7_eq line 2277
def OAI.SharpPlanar.CachedData.mpower1_4_r0_8 line 2278
lemma OAI.SharpPlanar.CachedData.mpower1_4_r0_8_eq line 2279
def OAI.SharpPlanar.CachedData.mpower1_4_r0_9 line 2280
lemma OAI.SharpPlanar.CachedData.mpower1_4_r0_9_eq line 2281
def OAI.SharpPlanar.CachedData.mpower1_4_r0_10 line 2282
lemma OAI.SharpPlanar.CachedData.mpower1_4_r0_10_eq line 2283
def OAI.SharpPlanar.CachedData.mpower1_4_r0_11 line 2284
lemma OAI.SharpPlanar.CachedData.mpower1_4_r0_11_eq line 2285
def OAI.SharpPlanar.CachedData.mpower1_4_r0_12 line 2286
lemma OAI.SharpPlanar.CachedData.mpower1_4_r0_12_eq line 2287
def OAI.SharpPlanar.CachedData.mpower1_4_r0_13 line 2288
lemma OAI.SharpPlanar.CachedData.mpower1_4_r0_13_eq line 2289
def OAI.SharpPlanar.CachedData.mpower1_4_r0_14 line 2290
lemma OAI.SharpPlanar.CachedData.mpower1_4_r0_14_eq line 2291
def OAI.SharpPlanar.CachedData.mpower1_4_r0_15 line 2292
lemma OAI.SharpPlanar.CachedData.mpower1_4_r0_15_eq line 2293
def OAI.SharpPlanar.CachedData.mpower1_4_r0 line 2294
lemma OAI.SharpPlanar.CachedData.mpower1_4_r0_eq line 2295
def OAI.SharpPlanar.CachedData.mpower1_4_r1_0 line 2313
lemma OAI.SharpPlanar.CachedData.mpower1_4_r1_0_eq line 2314
def OAI.SharpPlanar.CachedData.mpower1_4_r1_1 line 2315
lemma OAI.SharpPlanar.CachedData.mpower1_4_r1_1_eq line 2316
def OAI.SharpPlanar.CachedData.mpower1_4_r1_2 line 2317
lemma OAI.SharpPlanar.CachedData.mpower1_4_r1_2_eq line 2318
def OAI.SharpPlanar.CachedData.mpower1_4_r1_3 line 2319
lemma OAI.SharpPlanar.CachedData.mpower1_4_r1_3_eq line 2320
def OAI.SharpPlanar.CachedData.mpower1_4_r1_4 line 2321
lemma OAI.SharpPlanar.CachedData.mpower1_4_r1_4_eq line 2322
def OAI.SharpPlanar.CachedData.mpower1_4_r1_5 line 2323
lemma OAI.SharpPlanar.CachedData.mpower1_4_r1_5_eq line 2324
def OAI.SharpPlanar.CachedData.mpower1_4_r1_6 line 2325
lemma OAI.SharpPlanar.CachedData.mpower1_4_r1_6_eq line 2326
def OAI.SharpPlanar.CachedData.mpower1_4_r1_7 line 2327
lemma OAI.SharpPlanar.CachedData.mpower1_4_r1_7_eq line 2328
def OAI.SharpPlanar.CachedData.mpower1_4_r1_8 line 2329
lemma OAI.SharpPlanar.CachedData.mpower1_4_r1_8_eq line 2330
def OAI.SharpPlanar.CachedData.mpower1_4_r1_9 line 2331
lemma OAI.SharpPlanar.CachedData.mpower1_4_r1_9_eq line 2332
def OAI.SharpPlanar.CachedData.mpower1_4_r1_10 line 2333
lemma OAI.SharpPlanar.CachedData.mpower1_4_r1_10_eq line 2334
def OAI.SharpPlanar.CachedData.mpower1_4_r1_11 line 2335
lemma OAI.SharpPlanar.CachedData.mpower1_4_r1_11_eq line 2336
def OAI.SharpPlanar.CachedData.mpower1_4_r1_12 line 2337
lemma OAI.SharpPlanar.CachedData.mpower1_4_r1_12_eq line 2338
def OAI.SharpPlanar.CachedData.mpower1_4_r1_13 line 2339
lemma OAI.SharpPlanar.CachedData.mpower1_4_r1_13_eq line 2340
def OAI.SharpPlanar.CachedData.mpower1_4_r1_14 line 2341
lemma OAI.SharpPlanar.CachedData.mpower1_4_r1_14_eq line 2342
def OAI.SharpPlanar.CachedData.mpower1_4_r1_15 line 2343
lemma OAI.SharpPlanar.CachedData.mpower1_4_r1_15_eq line 2344
def OAI.SharpPlanar.CachedData.mpower1_4_r1 line 2345
lemma OAI.SharpPlanar.CachedData.mpower1_4_r1_eq line 2346
def OAI.SharpPlanar.CachedData.mpower1_4_r2_0 line 2364
lemma OAI.SharpPlanar.CachedData.mpower1_4_r2_0_eq line 2365
def OAI.SharpPlanar.CachedData.mpower1_4_r2_1 line 2366
lemma OAI.SharpPlanar.CachedData.mpower1_4_r2_1_eq line 2367
def OAI.SharpPlanar.CachedData.mpower1_4_r2_2 line 2368
lemma OAI.SharpPlanar.CachedData.mpower1_4_r2_2_eq line 2369
def OAI.SharpPlanar.CachedData.mpower1_4_r2_3 line 2370
lemma OAI.SharpPlanar.CachedData.mpower1_4_r2_3_eq line 2371
def OAI.SharpPlanar.CachedData.mpower1_4_r2_4 line 2372
lemma OAI.SharpPlanar.CachedData.mpower1_4_r2_4_eq line 2373
def OAI.SharpPlanar.CachedData.mpower1_4_r2_5 line 2374
lemma OAI.SharpPlanar.CachedData.mpower1_4_r2_5_eq line 2375
def OAI.SharpPlanar.CachedData.mpower1_4_r2_6 line 2376
lemma OAI.SharpPlanar.CachedData.mpower1_4_r2_6_eq line 2377
def OAI.SharpPlanar.CachedData.mpower1_4_r2_7 line 2378
lemma OAI.SharpPlanar.CachedData.mpower1_4_r2_7_eq line 2379
def OAI.SharpPlanar.CachedData.mpower1_4_r2_8 line 2380
lemma OAI.SharpPlanar.CachedData.mpower1_4_r2_8_eq line 2381
def OAI.SharpPlanar.CachedData.mpower1_4_r2_9 line 2382
lemma OAI.SharpPlanar.CachedData.mpower1_4_r2_9_eq line 2383
def OAI.SharpPlanar.CachedData.mpower1_4_r2_10 line 2384
lemma OAI.SharpPlanar.CachedData.mpower1_4_r2_10_eq line 2385
def OAI.SharpPlanar.CachedData.mpower1_4_r2_11 line 2386
lemma OAI.SharpPlanar.CachedData.mpower1_4_r2_11_eq line 2387
def OAI.SharpPlanar.CachedData.mpower1_4_r2_12 line 2388
lemma OAI.SharpPlanar.CachedData.mpower1_4_r2_12_eq line 2389
def OAI.SharpPlanar.CachedData.mpower1_4_r2_13 line 2390
lemma OAI.SharpPlanar.CachedData.mpower1_4_r2_13_eq line 2391
def OAI.SharpPlanar.CachedData.mpower1_4_r2_14 line 2392
lemma OAI.SharpPlanar.CachedData.mpower1_4_r2_14_eq line 2393
def OAI.SharpPlanar.CachedData.mpower1_4_r2_15 line 2394
lemma OAI.SharpPlanar.CachedData.mpower1_4_r2_15_eq line 2395
def OAI.SharpPlanar.CachedData.mpower1_4_r2 line 2396
lemma OAI.SharpPlanar.CachedData.mpower1_4_r2_eq line 2397
def OAI.SharpPlanar.CachedData.mpower1_4_r3_0 line 2415
lemma OAI.SharpPlanar.CachedData.mpower1_4_r3_0_eq line 2416
def OAI.SharpPlanar.CachedData.mpower1_4_r3_1 line 2417
lemma OAI.SharpPlanar.CachedData.mpower1_4_r3_1_eq line 2418
def OAI.SharpPlanar.CachedData.mpower1_4_r3_2 line 2419
lemma OAI.SharpPlanar.CachedData.mpower1_4_r3_2_eq line 2420
def OAI.SharpPlanar.CachedData.mpower1_4_r3_3 line 2421
lemma OAI.SharpPlanar.CachedData.mpower1_4_r3_3_eq line 2422
def OAI.SharpPlanar.CachedData.mpower1_4_r3_4 line 2423
lemma OAI.SharpPlanar.CachedData.mpower1_4_r3_4_eq line 2424
def OAI.SharpPlanar.CachedData.mpower1_4_r3_5 line 2425
lemma OAI.SharpPlanar.CachedData.mpower1_4_r3_5_eq line 2426
def OAI.SharpPlanar.CachedData.mpower1_4_r3_6 line 2427
lemma OAI.SharpPlanar.CachedData.mpower1_4_r3_6_eq line 2428
def OAI.SharpPlanar.CachedData.mpower1_4_r3_7 line 2429
lemma OAI.SharpPlanar.CachedData.mpower1_4_r3_7_eq line 2430
def OAI.SharpPlanar.CachedData.mpower1_4_r3_8 line 2431
lemma OAI.SharpPlanar.CachedData.mpower1_4_r3_8_eq line 2432
def OAI.SharpPlanar.CachedData.mpower1_4_r3_9 line 2433
lemma OAI.SharpPlanar.CachedData.mpower1_4_r3_9_eq line 2434
def OAI.SharpPlanar.CachedData.mpower1_4_r3_10 line 2435
lemma OAI.SharpPlanar.CachedData.mpower1_4_r3_10_eq line 2436
def OAI.SharpPlanar.CachedData.mpower1_4_r3_11 line 2437
lemma OAI.SharpPlanar.CachedData.mpower1_4_r3_11_eq line 2438
def OAI.SharpPlanar.CachedData.mpower1_4_r3_12 line 2439
lemma OAI.SharpPlanar.CachedData.mpower1_4_r3_12_eq line 2440
def OAI.SharpPlanar.CachedData.mpower1_4_r3_13 line 2441
lemma OAI.SharpPlanar.CachedData.mpower1_4_r3_13_eq line 2442
def OAI.SharpPlanar.CachedData.mpower1_4_r3_14 line 2443
lemma OAI.SharpPlanar.CachedData.mpower1_4_r3_14_eq line 2444
def OAI.SharpPlanar.CachedData.mpower1_4_r3_15 line 2445
lemma OAI.SharpPlanar.CachedData.mpower1_4_r3_15_eq line 2446
def OAI.SharpPlanar.CachedData.mpower1_4_r3 line 2447
lemma OAI.SharpPlanar.CachedData.mpower1_4_r3_eq line 2448
def OAI.SharpPlanar.CachedData.mpower1_4_r4_0 line 2466
lemma OAI.SharpPlanar.CachedData.mpower1_4_r4_0_eq line 2467
def OAI.SharpPlanar.CachedData.mpower1_4_r4_1 line 2468
lemma OAI.SharpPlanar.CachedData.mpower1_4_r4_1_eq line 2469
def OAI.SharpPlanar.CachedData.mpower1_4_r4_2 line 2470
lemma OAI.SharpPlanar.CachedData.mpower1_4_r4_2_eq line 2471
def OAI.SharpPlanar.CachedData.mpower1_4_r4_3 line 2472
lemma OAI.SharpPlanar.CachedData.mpower1_4_r4_3_eq line 2473
def OAI.SharpPlanar.CachedData.mpower1_4_r4_4 line 2474
lemma OAI.SharpPlanar.CachedData.mpower1_4_r4_4_eq line 2475
def OAI.SharpPlanar.CachedData.mpower1_4_r4_5 line 2476
lemma OAI.SharpPlanar.CachedData.mpower1_4_r4_5_eq line 2477
def OAI.SharpPlanar.CachedData.mpower1_4_r4_6 line 2478
lemma OAI.SharpPlanar.CachedData.mpower1_4_r4_6_eq line 2479
def OAI.SharpPlanar.CachedData.mpower1_4_r4_7 line 2480
lemma OAI.SharpPlanar.CachedData.mpower1_4_r4_7_eq line 2481
def OAI.SharpPlanar.CachedData.mpower1_4_r4_8 line 2482
lemma OAI.SharpPlanar.CachedData.mpower1_4_r4_8_eq line 2483
def OAI.SharpPlanar.CachedData.mpower1_4_r4_9 line 2484
lemma OAI.SharpPlanar.CachedData.mpower1_4_r4_9_eq line 2485
def OAI.SharpPlanar.CachedData.mpower1_4_r4_10 line 2486
lemma OAI.SharpPlanar.CachedData.mpower1_4_r4_10_eq line 2487
def OAI.SharpPlanar.CachedData.mpower1_4_r4_11 line 2488
lemma OAI.SharpPlanar.CachedData.mpower1_4_r4_11_eq line 2489
def OAI.SharpPlanar.CachedData.mpower1_4_r4_12 line 2490
lemma OAI.SharpPlanar.CachedData.mpower1_4_r4_12_eq line 2491
def OAI.SharpPlanar.CachedData.mpower1_4_r4_13 line 2492
lemma OAI.SharpPlanar.CachedData.mpower1_4_r4_13_eq line 2493
def OAI.SharpPlanar.CachedData.mpower1_4_r4_14 line 2494
lemma OAI.SharpPlanar.CachedData.mpower1_4_r4_14_eq line 2495
def OAI.SharpPlanar.CachedData.mpower1_4_r4_15 line 2496
lemma OAI.SharpPlanar.CachedData.mpower1_4_r4_15_eq line 2497
def OAI.SharpPlanar.CachedData.mpower1_4_r4 line 2498
lemma OAI.SharpPlanar.CachedData.mpower1_4_r4_eq line 2499
def OAI.SharpPlanar.CachedData.mpower1_4_r5_0 line 2517
lemma OAI.SharpPlanar.CachedData.mpower1_4_r5_0_eq line 2518
def OAI.SharpPlanar.CachedData.mpower1_4_r5_1 line 2519
lemma OAI.SharpPlanar.CachedData.mpower1_4_r5_1_eq line 2520
def OAI.SharpPlanar.CachedData.mpower1_4_r5_2 line 2521
lemma OAI.SharpPlanar.CachedData.mpower1_4_r5_2_eq line 2522
def OAI.SharpPlanar.CachedData.mpower1_4_r5_3 line 2523
lemma OAI.SharpPlanar.CachedData.mpower1_4_r5_3_eq line 2524
def OAI.SharpPlanar.CachedData.mpower1_4_r5_4 line 2525
lemma OAI.SharpPlanar.CachedData.mpower1_4_r5_4_eq line 2526
def OAI.SharpPlanar.CachedData.mpower1_4_r5_5 line 2527
lemma OAI.SharpPlanar.CachedData.mpower1_4_r5_5_eq line 2528
def OAI.SharpPlanar.CachedData.mpower1_4_r5_6 line 2529
lemma OAI.SharpPlanar.CachedData.mpower1_4_r5_6_eq line 2530
def OAI.SharpPlanar.CachedData.mpower1_4_r5_7 line 2531
lemma OAI.SharpPlanar.CachedData.mpower1_4_r5_7_eq line 2532
def OAI.SharpPlanar.CachedData.mpower1_4_r5_8 line 2533
lemma OAI.SharpPlanar.CachedData.mpower1_4_r5_8_eq line 2534
def OAI.SharpPlanar.CachedData.mpower1_4_r5_9 line 2535
lemma OAI.SharpPlanar.CachedData.mpower1_4_r5_9_eq line 2536
def OAI.SharpPlanar.CachedData.mpower1_4_r5_10 line 2537
lemma OAI.SharpPlanar.CachedData.mpower1_4_r5_10_eq line 2538
def OAI.SharpPlanar.CachedData.mpower1_4_r5_11 line 2539
lemma OAI.SharpPlanar.CachedData.mpower1_4_r5_11_eq line 2540
def OAI.SharpPlanar.CachedData.mpower1_4_r5_12 line 2541
lemma OAI.SharpPlanar.CachedData.mpower1_4_r5_12_eq line 2542
def OAI.SharpPlanar.CachedData.mpower1_4_r5_13 line 2543
lemma OAI.SharpPlanar.CachedData.mpower1_4_r5_13_eq line 2544
def OAI.SharpPlanar.CachedData.mpower1_4_r5_14 line 2545
lemma OAI.SharpPlanar.CachedData.mpower1_4_r5_14_eq line 2546
def OAI.SharpPlanar.CachedData.mpower1_4_r5_15 line 2547
lemma OAI.SharpPlanar.CachedData.mpower1_4_r5_15_eq line 2548
def OAI.SharpPlanar.CachedData.mpower1_4_r5 line 2549
lemma OAI.SharpPlanar.CachedData.mpower1_4_r5_eq line 2550
def OAI.SharpPlanar.CachedData.mpower1_4 line 2568
lemma OAI.SharpPlanar.CachedData.mpower1_4_eq line 2569
lemma OAI.SharpPlanar.CachedData.mpower1_4_contains line 2577
def OAI.SharpPlanar.CachedData.mpower0_5Expr line 2581
def OAI.SharpPlanar.CachedData.mpower0_5_r0_0 line 2582
lemma OAI.SharpPlanar.CachedData.mpower0_5_r0_0_eq line 2583
def OAI.SharpPlanar.CachedData.mpower0_5_r0_1 line 2584
lemma OAI.SharpPlanar.CachedData.mpower0_5_r0_1_eq line 2585
def OAI.SharpPlanar.CachedData.mpower0_5_r0_2 line 2586
lemma OAI.SharpPlanar.CachedData.mpower0_5_r0_2_eq line 2587
def OAI.SharpPlanar.CachedData.mpower0_5_r0_3 line 2588
lemma OAI.SharpPlanar.CachedData.mpower0_5_r0_3_eq line 2589
def OAI.SharpPlanar.CachedData.mpower0_5_r0_4 line 2590
lemma OAI.SharpPlanar.CachedData.mpower0_5_r0_4_eq line 2591
def OAI.SharpPlanar.CachedData.mpower0_5_r0_5 line 2592
lemma OAI.SharpPlanar.CachedData.mpower0_5_r0_5_eq line 2593
def OAI.SharpPlanar.CachedData.mpower0_5_r0_6 line 2594
lemma OAI.SharpPlanar.CachedData.mpower0_5_r0_6_eq line 2595
def OAI.SharpPlanar.CachedData.mpower0_5_r0_7 line 2596
lemma OAI.SharpPlanar.CachedData.mpower0_5_r0_7_eq line 2597
def OAI.SharpPlanar.CachedData.mpower0_5_r0_8 line 2598
lemma OAI.SharpPlanar.CachedData.mpower0_5_r0_8_eq line 2599
def OAI.SharpPlanar.CachedData.mpower0_5_r0_9 line 2600
lemma OAI.SharpPlanar.CachedData.mpower0_5_r0_9_eq line 2601
def OAI.SharpPlanar.CachedData.mpower0_5_r0_10 line 2602
lemma OAI.SharpPlanar.CachedData.mpower0_5_r0_10_eq line 2603
def OAI.SharpPlanar.CachedData.mpower0_5_r0_11 line 2604
lemma OAI.SharpPlanar.CachedData.mpower0_5_r0_11_eq line 2605
def OAI.SharpPlanar.CachedData.mpower0_5_r0_12 line 2606
lemma OAI.SharpPlanar.CachedData.mpower0_5_r0_12_eq line 2607
def OAI.SharpPlanar.CachedData.mpower0_5_r0_13 line 2608
lemma OAI.SharpPlanar.CachedData.mpower0_5_r0_13_eq line 2609
def OAI.SharpPlanar.CachedData.mpower0_5_r0_14 line 2610
lemma OAI.SharpPlanar.CachedData.mpower0_5_r0_14_eq line 2611
def OAI.SharpPlanar.CachedData.mpower0_5_r0_15 line 2612
lemma OAI.SharpPlanar.CachedData.mpower0_5_r0_15_eq line 2613
def OAI.SharpPlanar.CachedData.mpower0_5_r0 line 2614
lemma OAI.SharpPlanar.CachedData.mpower0_5_r0_eq line 2615
def OAI.SharpPlanar.CachedData.mpower0_5_r1_0 line 2633
lemma OAI.SharpPlanar.CachedData.mpower0_5_r1_0_eq line 2634
def OAI.SharpPlanar.CachedData.mpower0_5_r1_1 line 2635
lemma OAI.SharpPlanar.CachedData.mpower0_5_r1_1_eq line 2636
def OAI.SharpPlanar.CachedData.mpower0_5_r1_2 line 2637
lemma OAI.SharpPlanar.CachedData.mpower0_5_r1_2_eq line 2638
def OAI.SharpPlanar.CachedData.mpower0_5_r1_3 line 2639
lemma OAI.SharpPlanar.CachedData.mpower0_5_r1_3_eq line 2640
def OAI.SharpPlanar.CachedData.mpower0_5_r1_4 line 2641
lemma OAI.SharpPlanar.CachedData.mpower0_5_r1_4_eq line 2642
def OAI.SharpPlanar.CachedData.mpower0_5_r1_5 line 2643
lemma OAI.SharpPlanar.CachedData.mpower0_5_r1_5_eq line 2644
def OAI.SharpPlanar.CachedData.mpower0_5_r1_6 line 2645
lemma OAI.SharpPlanar.CachedData.mpower0_5_r1_6_eq line 2646
def OAI.SharpPlanar.CachedData.mpower0_5_r1_7 line 2647
lemma OAI.SharpPlanar.CachedData.mpower0_5_r1_7_eq line 2648
def OAI.SharpPlanar.CachedData.mpower0_5_r1_8 line 2649
lemma OAI.SharpPlanar.CachedData.mpower0_5_r1_8_eq line 2650
def OAI.SharpPlanar.CachedData.mpower0_5_r1_9 line 2651
lemma OAI.SharpPlanar.CachedData.mpower0_5_r1_9_eq line 2652
def OAI.SharpPlanar.CachedData.mpower0_5_r1_10 line 2653
lemma OAI.SharpPlanar.CachedData.mpower0_5_r1_10_eq line 2654
def OAI.SharpPlanar.CachedData.mpower0_5_r1_11 line 2655
lemma OAI.SharpPlanar.CachedData.mpower0_5_r1_11_eq line 2656
def OAI.SharpPlanar.CachedData.mpower0_5_r1_12 line 2657
lemma OAI.SharpPlanar.CachedData.mpower0_5_r1_12_eq line 2658
def OAI.SharpPlanar.CachedData.mpower0_5_r1_13 line 2659
lemma OAI.SharpPlanar.CachedData.mpower0_5_r1_13_eq line 2660
def OAI.SharpPlanar.CachedData.mpower0_5_r1_14 line 2661
lemma OAI.SharpPlanar.CachedData.mpower0_5_r1_14_eq line 2662
def OAI.SharpPlanar.CachedData.mpower0_5_r1_15 line 2663
lemma OAI.SharpPlanar.CachedData.mpower0_5_r1_15_eq line 2664
def OAI.SharpPlanar.CachedData.mpower0_5_r1 line 2665
lemma OAI.SharpPlanar.CachedData.mpower0_5_r1_eq line 2666
def OAI.SharpPlanar.CachedData.mpower0_5_r2_0 line 2684
lemma OAI.SharpPlanar.CachedData.mpower0_5_r2_0_eq line 2685
def OAI.SharpPlanar.CachedData.mpower0_5_r2_1 line 2686
lemma OAI.SharpPlanar.CachedData.mpower0_5_r2_1_eq line 2687
def OAI.SharpPlanar.CachedData.mpower0_5_r2_2 line 2688
lemma OAI.SharpPlanar.CachedData.mpower0_5_r2_2_eq line 2689
def OAI.SharpPlanar.CachedData.mpower0_5_r2_3 line 2690
lemma OAI.SharpPlanar.CachedData.mpower0_5_r2_3_eq line 2691
def OAI.SharpPlanar.CachedData.mpower0_5_r2_4 line 2692
lemma OAI.SharpPlanar.CachedData.mpower0_5_r2_4_eq line 2693
def OAI.SharpPlanar.CachedData.mpower0_5_r2_5 line 2694
lemma OAI.SharpPlanar.CachedData.mpower0_5_r2_5_eq line 2695
def OAI.SharpPlanar.CachedData.mpower0_5_r2_6 line 2696
lemma OAI.SharpPlanar.CachedData.mpower0_5_r2_6_eq line 2697
def OAI.SharpPlanar.CachedData.mpower0_5_r2_7 line 2698
lemma OAI.SharpPlanar.CachedData.mpower0_5_r2_7_eq line 2699
def OAI.SharpPlanar.CachedData.mpower0_5_r2_8 line 2700
lemma OAI.SharpPlanar.CachedData.mpower0_5_r2_8_eq line 2701
def OAI.SharpPlanar.CachedData.mpower0_5_r2_9 line 2702
lemma OAI.SharpPlanar.CachedData.mpower0_5_r2_9_eq line 2703
def OAI.SharpPlanar.CachedData.mpower0_5_r2_10 line 2704
lemma OAI.SharpPlanar.CachedData.mpower0_5_r2_10_eq line 2705
def OAI.SharpPlanar.CachedData.mpower0_5_r2_11 line 2706
lemma OAI.SharpPlanar.CachedData.mpower0_5_r2_11_eq line 2707
def OAI.SharpPlanar.CachedData.mpower0_5_r2_12 line 2708
lemma OAI.SharpPlanar.CachedData.mpower0_5_r2_12_eq line 2709
def OAI.SharpPlanar.CachedData.mpower0_5_r2_13 line 2710
lemma OAI.SharpPlanar.CachedData.mpower0_5_r2_13_eq line 2711
def OAI.SharpPlanar.CachedData.mpower0_5_r2_14 line 2712
lemma OAI.SharpPlanar.CachedData.mpower0_5_r2_14_eq line 2713
def OAI.SharpPlanar.CachedData.mpower0_5_r2_15 line 2714
lemma OAI.SharpPlanar.CachedData.mpower0_5_r2_15_eq line 2715
def OAI.SharpPlanar.CachedData.mpower0_5_r2 line 2716
lemma OAI.SharpPlanar.CachedData.mpower0_5_r2_eq line 2717
def OAI.SharpPlanar.CachedData.mpower0_5_r3_0 line 2735
lemma OAI.SharpPlanar.CachedData.mpower0_5_r3_0_eq line 2736
def OAI.SharpPlanar.CachedData.mpower0_5_r3_1 line 2737
lemma OAI.SharpPlanar.CachedData.mpower0_5_r3_1_eq line 2738
def OAI.SharpPlanar.CachedData.mpower0_5_r3_2 line 2739
lemma OAI.SharpPlanar.CachedData.mpower0_5_r3_2_eq line 2740
def OAI.SharpPlanar.CachedData.mpower0_5_r3_3 line 2741
lemma OAI.SharpPlanar.CachedData.mpower0_5_r3_3_eq line 2742
def OAI.SharpPlanar.CachedData.mpower0_5_r3_4 line 2743
lemma OAI.SharpPlanar.CachedData.mpower0_5_r3_4_eq line 2744
def OAI.SharpPlanar.CachedData.mpower0_5_r3_5 line 2745
lemma OAI.SharpPlanar.CachedData.mpower0_5_r3_5_eq line 2746
def OAI.SharpPlanar.CachedData.mpower0_5_r3_6 line 2747
lemma OAI.SharpPlanar.CachedData.mpower0_5_r3_6_eq line 2748
def OAI.SharpPlanar.CachedData.mpower0_5_r3_7 line 2749
lemma OAI.SharpPlanar.CachedData.mpower0_5_r3_7_eq line 2750
def OAI.SharpPlanar.CachedData.mpower0_5_r3_8 line 2751
lemma OAI.SharpPlanar.CachedData.mpower0_5_r3_8_eq line 2752
def OAI.SharpPlanar.CachedData.mpower0_5_r3_9 line 2753
lemma OAI.SharpPlanar.CachedData.mpower0_5_r3_9_eq line 2754
def OAI.SharpPlanar.CachedData.mpower0_5_r3_10 line 2755
lemma OAI.SharpPlanar.CachedData.mpower0_5_r3_10_eq line 2756
def OAI.SharpPlanar.CachedData.mpower0_5_r3_11 line 2757
lemma OAI.SharpPlanar.CachedData.mpower0_5_r3_11_eq line 2758
def OAI.SharpPlanar.CachedData.mpower0_5_r3_12 line 2759
lemma OAI.SharpPlanar.CachedData.mpower0_5_r3_12_eq line 2760
def OAI.SharpPlanar.CachedData.mpower0_5_r3_13 line 2761
lemma OAI.SharpPlanar.CachedData.mpower0_5_r3_13_eq line 2762
def OAI.SharpPlanar.CachedData.mpower0_5_r3_14 line 2763
lemma OAI.SharpPlanar.CachedData.mpower0_5_r3_14_eq line 2764
def OAI.SharpPlanar.CachedData.mpower0_5_r3_15 line 2765
lemma OAI.SharpPlanar.CachedData.mpower0_5_r3_15_eq line 2766
def OAI.SharpPlanar.CachedData.mpower0_5_r3 line 2767
lemma OAI.SharpPlanar.CachedData.mpower0_5_r3_eq line 2768
def OAI.SharpPlanar.CachedData.mpower0_5_r4_0 line 2786
lemma OAI.SharpPlanar.CachedData.mpower0_5_r4_0_eq line 2787
def OAI.SharpPlanar.CachedData.mpower0_5_r4_1 line 2788
lemma OAI.SharpPlanar.CachedData.mpower0_5_r4_1_eq line 2789
def OAI.SharpPlanar.CachedData.mpower0_5_r4_2 line 2790
lemma OAI.SharpPlanar.CachedData.mpower0_5_r4_2_eq line 2791
def OAI.SharpPlanar.CachedData.mpower0_5_r4_3 line 2792
lemma OAI.SharpPlanar.CachedData.mpower0_5_r4_3_eq line 2793
def OAI.SharpPlanar.CachedData.mpower0_5_r4_4 line 2794
lemma OAI.SharpPlanar.CachedData.mpower0_5_r4_4_eq line 2795
def OAI.SharpPlanar.CachedData.mpower0_5_r4_5 line 2796
lemma OAI.SharpPlanar.CachedData.mpower0_5_r4_5_eq line 2797
def OAI.SharpPlanar.CachedData.mpower0_5_r4_6 line 2798
lemma OAI.SharpPlanar.CachedData.mpower0_5_r4_6_eq line 2799
def OAI.SharpPlanar.CachedData.mpower0_5_r4_7 line 2800
lemma OAI.SharpPlanar.CachedData.mpower0_5_r4_7_eq line 2801
def OAI.SharpPlanar.CachedData.mpower0_5_r4_8 line 2802
lemma OAI.SharpPlanar.CachedData.mpower0_5_r4_8_eq line 2803
def OAI.SharpPlanar.CachedData.mpower0_5_r4_9 line 2804
lemma OAI.SharpPlanar.CachedData.mpower0_5_r4_9_eq line 2805
def OAI.SharpPlanar.CachedData.mpower0_5_r4_10 line 2806
lemma OAI.SharpPlanar.CachedData.mpower0_5_r4_10_eq line 2807
def OAI.SharpPlanar.CachedData.mpower0_5_r4_11 line 2808
lemma OAI.SharpPlanar.CachedData.mpower0_5_r4_11_eq line 2809
def OAI.SharpPlanar.CachedData.mpower0_5_r4_12 line 2810
lemma OAI.SharpPlanar.CachedData.mpower0_5_r4_12_eq line 2811
def OAI.SharpPlanar.CachedData.mpower0_5_r4_13 line 2812
lemma OAI.SharpPlanar.CachedData.mpower0_5_r4_13_eq line 2813
def OAI.SharpPlanar.CachedData.mpower0_5_r4_14 line 2814
lemma OAI.SharpPlanar.CachedData.mpower0_5_r4_14_eq line 2815
def OAI.SharpPlanar.CachedData.mpower0_5_r4_15 line 2816
lemma OAI.SharpPlanar.CachedData.mpower0_5_r4_15_eq line 2817
def OAI.SharpPlanar.CachedData.mpower0_5_r4 line 2818
lemma OAI.SharpPlanar.CachedData.mpower0_5_r4_eq line 2819
def OAI.SharpPlanar.CachedData.mpower0_5_r5_0 line 2837
lemma OAI.SharpPlanar.CachedData.mpower0_5_r5_0_eq line 2838
def OAI.SharpPlanar.CachedData.mpower0_5_r5_1 line 2839
lemma OAI.SharpPlanar.CachedData.mpower0_5_r5_1_eq line 2840
def OAI.SharpPlanar.CachedData.mpower0_5_r5_2 line 2841
lemma OAI.SharpPlanar.CachedData.mpower0_5_r5_2_eq line 2842
def OAI.SharpPlanar.CachedData.mpower0_5_r5_3 line 2843
lemma OAI.SharpPlanar.CachedData.mpower0_5_r5_3_eq line 2844
def OAI.SharpPlanar.CachedData.mpower0_5_r5_4 line 2845
lemma OAI.SharpPlanar.CachedData.mpower0_5_r5_4_eq line 2846
def OAI.SharpPlanar.CachedData.mpower0_5_r5_5 line 2847
lemma OAI.SharpPlanar.CachedData.mpower0_5_r5_5_eq line 2848
def OAI.SharpPlanar.CachedData.mpower0_5_r5_6 line 2849
lemma OAI.SharpPlanar.CachedData.mpower0_5_r5_6_eq line 2850
def OAI.SharpPlanar.CachedData.mpower0_5_r5_7 line 2851
lemma OAI.SharpPlanar.CachedData.mpower0_5_r5_7_eq line 2852
def OAI.SharpPlanar.CachedData.mpower0_5_r5_8 line 2853
lemma OAI.SharpPlanar.CachedData.mpower0_5_r5_8_eq line 2854
def OAI.SharpPlanar.CachedData.mpower0_5_r5_9 line 2855
lemma OAI.SharpPlanar.CachedData.mpower0_5_r5_9_eq line 2856
def OAI.SharpPlanar.CachedData.mpower0_5_r5_10 line 2857
lemma OAI.SharpPlanar.CachedData.mpower0_5_r5_10_eq line 2858
def OAI.SharpPlanar.CachedData.mpower0_5_r5_11 line 2859
lemma OAI.SharpPlanar.CachedData.mpower0_5_r5_11_eq line 2860
def OAI.SharpPlanar.CachedData.mpower0_5_r5_12 line 2861
lemma OAI.SharpPlanar.CachedData.mpower0_5_r5_12_eq line 2862
def OAI.SharpPlanar.CachedData.mpower0_5_r5_13 line 2863
lemma OAI.SharpPlanar.CachedData.mpower0_5_r5_13_eq line 2864
def OAI.SharpPlanar.CachedData.mpower0_5_r5_14 line 2865
lemma OAI.SharpPlanar.CachedData.mpower0_5_r5_14_eq line 2866
def OAI.SharpPlanar.CachedData.mpower0_5_r5_15 line 2867
lemma OAI.SharpPlanar.CachedData.mpower0_5_r5_15_eq line 2868
def OAI.SharpPlanar.CachedData.mpower0_5_r5 line 2869
lemma OAI.SharpPlanar.CachedData.mpower0_5_r5_eq line 2870
def OAI.SharpPlanar.CachedData.mpower0_5 line 2888
lemma OAI.SharpPlanar.CachedData.mpower0_5_eq line 2889
lemma OAI.SharpPlanar.CachedData.mpower0_5_contains line 2897
def OAI.SharpPlanar.CachedData.mpower1_5Expr line 2901
def OAI.SharpPlanar.CachedData.mpower1_5_r0_0 line 2902
lemma OAI.SharpPlanar.CachedData.mpower1_5_r0_0_eq line 2903
def OAI.SharpPlanar.CachedData.mpower1_5_r0_1 line 2904
lemma OAI.SharpPlanar.CachedData.mpower1_5_r0_1_eq line 2905
def OAI.SharpPlanar.CachedData.mpower1_5_r0_2 line 2906
lemma OAI.SharpPlanar.CachedData.mpower1_5_r0_2_eq line 2907
def OAI.SharpPlanar.CachedData.mpower1_5_r0_3 line 2908
lemma OAI.SharpPlanar.CachedData.mpower1_5_r0_3_eq line 2909
def OAI.SharpPlanar.CachedData.mpower1_5_r0_4 line 2910
lemma OAI.SharpPlanar.CachedData.mpower1_5_r0_4_eq line 2911
def OAI.SharpPlanar.CachedData.mpower1_5_r0_5 line 2912
lemma OAI.SharpPlanar.CachedData.mpower1_5_r0_5_eq line 2913
def OAI.SharpPlanar.CachedData.mpower1_5_r0_6 line 2914
lemma OAI.SharpPlanar.CachedData.mpower1_5_r0_6_eq line 2915
def OAI.SharpPlanar.CachedData.mpower1_5_r0_7 line 2916
lemma OAI.SharpPlanar.CachedData.mpower1_5_r0_7_eq line 2917
def OAI.SharpPlanar.CachedData.mpower1_5_r0_8 line 2918
lemma OAI.SharpPlanar.CachedData.mpower1_5_r0_8_eq line 2919
def OAI.SharpPlanar.CachedData.mpower1_5_r0_9 line 2920
lemma OAI.SharpPlanar.CachedData.mpower1_5_r0_9_eq line 2921
def OAI.SharpPlanar.CachedData.mpower1_5_r0_10 line 2922
lemma OAI.SharpPlanar.CachedData.mpower1_5_r0_10_eq line 2923
def OAI.SharpPlanar.CachedData.mpower1_5_r0_11 line 2924
lemma OAI.SharpPlanar.CachedData.mpower1_5_r0_11_eq line 2925
def OAI.SharpPlanar.CachedData.mpower1_5_r0_12 line 2926
lemma OAI.SharpPlanar.CachedData.mpower1_5_r0_12_eq line 2927
def OAI.SharpPlanar.CachedData.mpower1_5_r0_13 line 2928
lemma OAI.SharpPlanar.CachedData.mpower1_5_r0_13_eq line 2929
def OAI.SharpPlanar.CachedData.mpower1_5_r0_14 line 2930
lemma OAI.SharpPlanar.CachedData.mpower1_5_r0_14_eq line 2931
def OAI.SharpPlanar.CachedData.mpower1_5_r0_15 line 2932
lemma OAI.SharpPlanar.CachedData.mpower1_5_r0_15_eq line 2933
def OAI.SharpPlanar.CachedData.mpower1_5_r0 line 2934
lemma OAI.SharpPlanar.CachedData.mpower1_5_r0_eq line 2935
def OAI.SharpPlanar.CachedData.mpower1_5_r1_0 line 2953
lemma OAI.SharpPlanar.CachedData.mpower1_5_r1_0_eq line 2954
def OAI.SharpPlanar.CachedData.mpower1_5_r1_1 line 2955
lemma OAI.SharpPlanar.CachedData.mpower1_5_r1_1_eq line 2956
def OAI.SharpPlanar.CachedData.mpower1_5_r1_2 line 2957
lemma OAI.SharpPlanar.CachedData.mpower1_5_r1_2_eq line 2958
def OAI.SharpPlanar.CachedData.mpower1_5_r1_3 line 2959
lemma OAI.SharpPlanar.CachedData.mpower1_5_r1_3_eq line 2960
def OAI.SharpPlanar.CachedData.mpower1_5_r1_4 line 2961
lemma OAI.SharpPlanar.CachedData.mpower1_5_r1_4_eq line 2962
def OAI.SharpPlanar.CachedData.mpower1_5_r1_5 line 2963
lemma OAI.SharpPlanar.CachedData.mpower1_5_r1_5_eq line 2964
def OAI.SharpPlanar.CachedData.mpower1_5_r1_6 line 2965
lemma OAI.SharpPlanar.CachedData.mpower1_5_r1_6_eq line 2966
def OAI.SharpPlanar.CachedData.mpower1_5_r1_7 line 2967
lemma OAI.SharpPlanar.CachedData.mpower1_5_r1_7_eq line 2968
def OAI.SharpPlanar.CachedData.mpower1_5_r1_8 line 2969
lemma OAI.SharpPlanar.CachedData.mpower1_5_r1_8_eq line 2970
def OAI.SharpPlanar.CachedData.mpower1_5_r1_9 line 2971
lemma OAI.SharpPlanar.CachedData.mpower1_5_r1_9_eq line 2972
def OAI.SharpPlanar.CachedData.mpower1_5_r1_10 line 2973
lemma OAI.SharpPlanar.CachedData.mpower1_5_r1_10_eq line 2974
def OAI.SharpPlanar.CachedData.mpower1_5_r1_11 line 2975
lemma OAI.SharpPlanar.CachedData.mpower1_5_r1_11_eq line 2976
def OAI.SharpPlanar.CachedData.mpower1_5_r1_12 line 2977
lemma OAI.SharpPlanar.CachedData.mpower1_5_r1_12_eq line 2978
def OAI.SharpPlanar.CachedData.mpower1_5_r1_13 line 2979
lemma OAI.SharpPlanar.CachedData.mpower1_5_r1_13_eq line 2980
def OAI.SharpPlanar.CachedData.mpower1_5_r1_14 line 2981
lemma OAI.SharpPlanar.CachedData.mpower1_5_r1_14_eq line 2982
def OAI.SharpPlanar.CachedData.mpower1_5_r1_15 line 2983
lemma OAI.SharpPlanar.CachedData.mpower1_5_r1_15_eq line 2984
def OAI.SharpPlanar.CachedData.mpower1_5_r1 line 2985
lemma OAI.SharpPlanar.CachedData.mpower1_5_r1_eq line 2986
def OAI.SharpPlanar.CachedData.mpower1_5_r2_0 line 3004
lemma OAI.SharpPlanar.CachedData.mpower1_5_r2_0_eq line 3005
def OAI.SharpPlanar.CachedData.mpower1_5_r2_1 line 3006
lemma OAI.SharpPlanar.CachedData.mpower1_5_r2_1_eq line 3007
def OAI.SharpPlanar.CachedData.mpower1_5_r2_2 line 3008
lemma OAI.SharpPlanar.CachedData.mpower1_5_r2_2_eq line 3009
def OAI.SharpPlanar.CachedData.mpower1_5_r2_3 line 3010
lemma OAI.SharpPlanar.CachedData.mpower1_5_r2_3_eq line 3011
def OAI.SharpPlanar.CachedData.mpower1_5_r2_4 line 3012
lemma OAI.SharpPlanar.CachedData.mpower1_5_r2_4_eq line 3013
def OAI.SharpPlanar.CachedData.mpower1_5_r2_5 line 3014
lemma OAI.SharpPlanar.CachedData.mpower1_5_r2_5_eq line 3015
def OAI.SharpPlanar.CachedData.mpower1_5_r2_6 line 3016
lemma OAI.SharpPlanar.CachedData.mpower1_5_r2_6_eq line 3017
def OAI.SharpPlanar.CachedData.mpower1_5_r2_7 line 3018
lemma OAI.SharpPlanar.CachedData.mpower1_5_r2_7_eq line 3019
def OAI.SharpPlanar.CachedData.mpower1_5_r2_8 line 3020
lemma OAI.SharpPlanar.CachedData.mpower1_5_r2_8_eq line 3021
def OAI.SharpPlanar.CachedData.mpower1_5_r2_9 line 3022
lemma OAI.SharpPlanar.CachedData.mpower1_5_r2_9_eq line 3023
def OAI.SharpPlanar.CachedData.mpower1_5_r2_10 line 3024
lemma OAI.SharpPlanar.CachedData.mpower1_5_r2_10_eq line 3025
def OAI.SharpPlanar.CachedData.mpower1_5_r2_11 line 3026
lemma OAI.SharpPlanar.CachedData.mpower1_5_r2_11_eq line 3027
def OAI.SharpPlanar.CachedData.mpower1_5_r2_12 line 3028
lemma OAI.SharpPlanar.CachedData.mpower1_5_r2_12_eq line 3029
def OAI.SharpPlanar.CachedData.mpower1_5_r2_13 line 3030
lemma OAI.SharpPlanar.CachedData.mpower1_5_r2_13_eq line 3031
def OAI.SharpPlanar.CachedData.mpower1_5_r2_14 line 3032
lemma OAI.SharpPlanar.CachedData.mpower1_5_r2_14_eq line 3033
def OAI.SharpPlanar.CachedData.mpower1_5_r2_15 line 3034
lemma OAI.SharpPlanar.CachedData.mpower1_5_r2_15_eq line 3035
def OAI.SharpPlanar.CachedData.mpower1_5_r2 line 3036
lemma OAI.SharpPlanar.CachedData.mpower1_5_r2_eq line 3037
def OAI.SharpPlanar.CachedData.mpower1_5_r3_0 line 3055
lemma OAI.SharpPlanar.CachedData.mpower1_5_r3_0_eq line 3056
def OAI.SharpPlanar.CachedData.mpower1_5_r3_1 line 3057
lemma OAI.SharpPlanar.CachedData.mpower1_5_r3_1_eq line 3058
def OAI.SharpPlanar.CachedData.mpower1_5_r3_2 line 3059
lemma OAI.SharpPlanar.CachedData.mpower1_5_r3_2_eq line 3060
def OAI.SharpPlanar.CachedData.mpower1_5_r3_3 line 3061
lemma OAI.SharpPlanar.CachedData.mpower1_5_r3_3_eq line 3062
def OAI.SharpPlanar.CachedData.mpower1_5_r3_4 line 3063
lemma OAI.SharpPlanar.CachedData.mpower1_5_r3_4_eq line 3064
def OAI.SharpPlanar.CachedData.mpower1_5_r3_5 line 3065
lemma OAI.SharpPlanar.CachedData.mpower1_5_r3_5_eq line 3066
def OAI.SharpPlanar.CachedData.mpower1_5_r3_6 line 3067
lemma OAI.SharpPlanar.CachedData.mpower1_5_r3_6_eq line 3068
def OAI.SharpPlanar.CachedData.mpower1_5_r3_7 line 3069
lemma OAI.SharpPlanar.CachedData.mpower1_5_r3_7_eq line 3070
def OAI.SharpPlanar.CachedData.mpower1_5_r3_8 line 3071
lemma OAI.SharpPlanar.CachedData.mpower1_5_r3_8_eq line 3072
def OAI.SharpPlanar.CachedData.mpower1_5_r3_9 line 3073
lemma OAI.SharpPlanar.CachedData.mpower1_5_r3_9_eq line 3074
def OAI.SharpPlanar.CachedData.mpower1_5_r3_10 line 3075
lemma OAI.SharpPlanar.CachedData.mpower1_5_r3_10_eq line 3076
def OAI.SharpPlanar.CachedData.mpower1_5_r3_11 line 3077
lemma OAI.SharpPlanar.CachedData.mpower1_5_r3_11_eq line 3078
def OAI.SharpPlanar.CachedData.mpower1_5_r3_12 line 3079
lemma OAI.SharpPlanar.CachedData.mpower1_5_r3_12_eq line 3080
def OAI.SharpPlanar.CachedData.mpower1_5_r3_13 line 3081
lemma OAI.SharpPlanar.CachedData.mpower1_5_r3_13_eq line 3082
def OAI.SharpPlanar.CachedData.mpower1_5_r3_14 line 3083
lemma OAI.SharpPlanar.CachedData.mpower1_5_r3_14_eq line 3084
def OAI.SharpPlanar.CachedData.mpower1_5_r3_15 line 3085
lemma OAI.SharpPlanar.CachedData.mpower1_5_r3_15_eq line 3086
def OAI.SharpPlanar.CachedData.mpower1_5_r3 line 3087
lemma OAI.SharpPlanar.CachedData.mpower1_5_r3_eq line 3088
def OAI.SharpPlanar.CachedData.mpower1_5_r4_0 line 3106
lemma OAI.SharpPlanar.CachedData.mpower1_5_r4_0_eq line 3107
def OAI.SharpPlanar.CachedData.mpower1_5_r4_1 line 3108
lemma OAI.SharpPlanar.CachedData.mpower1_5_r4_1_eq line 3109
def OAI.SharpPlanar.CachedData.mpower1_5_r4_2 line 3110
lemma OAI.SharpPlanar.CachedData.mpower1_5_r4_2_eq line 3111
def OAI.SharpPlanar.CachedData.mpower1_5_r4_3 line 3112
lemma OAI.SharpPlanar.CachedData.mpower1_5_r4_3_eq line 3113
def OAI.SharpPlanar.CachedData.mpower1_5_r4_4 line 3114
lemma OAI.SharpPlanar.CachedData.mpower1_5_r4_4_eq line 3115
def OAI.SharpPlanar.CachedData.mpower1_5_r4_5 line 3116
lemma OAI.SharpPlanar.CachedData.mpower1_5_r4_5_eq line 3117
def OAI.SharpPlanar.CachedData.mpower1_5_r4_6 line 3118
lemma OAI.SharpPlanar.CachedData.mpower1_5_r4_6_eq line 3119
def OAI.SharpPlanar.CachedData.mpower1_5_r4_7 line 3120
lemma OAI.SharpPlanar.CachedData.mpower1_5_r4_7_eq line 3121
def OAI.SharpPlanar.CachedData.mpower1_5_r4_8 line 3122
lemma OAI.SharpPlanar.CachedData.mpower1_5_r4_8_eq line 3123
def OAI.SharpPlanar.CachedData.mpower1_5_r4_9 line 3124
lemma OAI.SharpPlanar.CachedData.mpower1_5_r4_9_eq line 3125
def OAI.SharpPlanar.CachedData.mpower1_5_r4_10 line 3126
lemma OAI.SharpPlanar.CachedData.mpower1_5_r4_10_eq line 3127
def OAI.SharpPlanar.CachedData.mpower1_5_r4_11 line 3128
lemma OAI.SharpPlanar.CachedData.mpower1_5_r4_11_eq line 3129
def OAI.SharpPlanar.CachedData.mpower1_5_r4_12 line 3130
lemma OAI.SharpPlanar.CachedData.mpower1_5_r4_12_eq line 3131
def OAI.SharpPlanar.CachedData.mpower1_5_r4_13 line 3132
lemma OAI.SharpPlanar.CachedData.mpower1_5_r4_13_eq line 3133
def OAI.SharpPlanar.CachedData.mpower1_5_r4_14 line 3134
lemma OAI.SharpPlanar.CachedData.mpower1_5_r4_14_eq line 3135
def OAI.SharpPlanar.CachedData.mpower1_5_r4_15 line 3136
lemma OAI.SharpPlanar.CachedData.mpower1_5_r4_15_eq line 3137
def OAI.SharpPlanar.CachedData.mpower1_5_r4 line 3138
lemma OAI.SharpPlanar.CachedData.mpower1_5_r4_eq line 3139
def OAI.SharpPlanar.CachedData.mpower1_5_r5_0 line 3157
lemma OAI.SharpPlanar.CachedData.mpower1_5_r5_0_eq line 3158
def OAI.SharpPlanar.CachedData.mpower1_5_r5_1 line 3159
lemma OAI.SharpPlanar.CachedData.mpower1_5_r5_1_eq line 3160
def OAI.SharpPlanar.CachedData.mpower1_5_r5_2 line 3161
lemma OAI.SharpPlanar.CachedData.mpower1_5_r5_2_eq line 3162
def OAI.SharpPlanar.CachedData.mpower1_5_r5_3 line 3163
lemma OAI.SharpPlanar.CachedData.mpower1_5_r5_3_eq line 3164
def OAI.SharpPlanar.CachedData.mpower1_5_r5_4 line 3165
lemma OAI.SharpPlanar.CachedData.mpower1_5_r5_4_eq line 3166
def OAI.SharpPlanar.CachedData.mpower1_5_r5_5 line 3167
lemma OAI.SharpPlanar.CachedData.mpower1_5_r5_5_eq line 3168
def OAI.SharpPlanar.CachedData.mpower1_5_r5_6 line 3169
lemma OAI.SharpPlanar.CachedData.mpower1_5_r5_6_eq line 3170
def OAI.SharpPlanar.CachedData.mpower1_5_r5_7 line 3171
lemma OAI.SharpPlanar.CachedData.mpower1_5_r5_7_eq line 3172
def OAI.SharpPlanar.CachedData.mpower1_5_r5_8 line 3173
lemma OAI.SharpPlanar.CachedData.mpower1_5_r5_8_eq line 3174
def OAI.SharpPlanar.CachedData.mpower1_5_r5_9 line 3175
lemma OAI.SharpPlanar.CachedData.mpower1_5_r5_9_eq line 3176
def OAI.SharpPlanar.CachedData.mpower1_5_r5_10 line 3177
lemma OAI.SharpPlanar.CachedData.mpower1_5_r5_10_eq line 3178
def OAI.SharpPlanar.CachedData.mpower1_5_r5_11 line 3179
lemma OAI.SharpPlanar.CachedData.mpower1_5_r5_11_eq line 3180
def OAI.SharpPlanar.CachedData.mpower1_5_r5_12 line 3181
lemma OAI.SharpPlanar.CachedData.mpower1_5_r5_12_eq line 3182
def OAI.SharpPlanar.CachedData.mpower1_5_r5_13 line 3183
lemma OAI.SharpPlanar.CachedData.mpower1_5_r5_13_eq line 3184
def OAI.SharpPlanar.CachedData.mpower1_5_r5_14 line 3185
lemma OAI.SharpPlanar.CachedData.mpower1_5_r5_14_eq line 3186
def OAI.SharpPlanar.CachedData.mpower1_5_r5_15 line 3187
lemma OAI.SharpPlanar.CachedData.mpower1_5_r5_15_eq line 3188
def OAI.SharpPlanar.CachedData.mpower1_5_r5 line 3189
lemma OAI.SharpPlanar.CachedData.mpower1_5_r5_eq line 3190
def OAI.SharpPlanar.CachedData.mpower1_5 line 3208
lemma OAI.SharpPlanar.CachedData.mpower1_5_eq line 3209
lemma OAI.SharpPlanar.CachedData.mpower1_5_contains line 3217