Powers10.lean`

2082 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.power0 line 15
lemma OAI.SharpPlanar.CachedData.power0_contains line 16
def OAI.SharpPlanar.CachedData.power1Expr line 20
def OAI.SharpPlanar.CachedData.power1_r0_0 line 21
lemma OAI.SharpPlanar.CachedData.power1_r0_0_eq line 22
def OAI.SharpPlanar.CachedData.power1_r0_1 line 23
lemma OAI.SharpPlanar.CachedData.power1_r0_1_eq line 24
def OAI.SharpPlanar.CachedData.power1_r0_2 line 25
lemma OAI.SharpPlanar.CachedData.power1_r0_2_eq line 26
def OAI.SharpPlanar.CachedData.power1_r0_3 line 27
lemma OAI.SharpPlanar.CachedData.power1_r0_3_eq line 28
def OAI.SharpPlanar.CachedData.power1_r0_4 line 29
lemma OAI.SharpPlanar.CachedData.power1_r0_4_eq line 30
def OAI.SharpPlanar.CachedData.power1_r0_5 line 31
lemma OAI.SharpPlanar.CachedData.power1_r0_5_eq line 32
def OAI.SharpPlanar.CachedData.power1_r0_6 line 33
lemma OAI.SharpPlanar.CachedData.power1_r0_6_eq line 34
def OAI.SharpPlanar.CachedData.power1_r0_7 line 35
lemma OAI.SharpPlanar.CachedData.power1_r0_7_eq line 36
def OAI.SharpPlanar.CachedData.power1_r0_8 line 37
lemma OAI.SharpPlanar.CachedData.power1_r0_8_eq line 38
def OAI.SharpPlanar.CachedData.power1_r0_9 line 39
lemma OAI.SharpPlanar.CachedData.power1_r0_9_eq line 40
def OAI.SharpPlanar.CachedData.power1_r0_10 line 41
lemma OAI.SharpPlanar.CachedData.power1_r0_10_eq line 42
def OAI.SharpPlanar.CachedData.power1_r0_11 line 43
lemma OAI.SharpPlanar.CachedData.power1_r0_11_eq line 44
def OAI.SharpPlanar.CachedData.power1_r0_12 line 45
lemma OAI.SharpPlanar.CachedData.power1_r0_12_eq line 46
def OAI.SharpPlanar.CachedData.power1_r0_13 line 47
lemma OAI.SharpPlanar.CachedData.power1_r0_13_eq line 48
def OAI.SharpPlanar.CachedData.power1_r0_14 line 49
lemma OAI.SharpPlanar.CachedData.power1_r0_14_eq line 50
def OAI.SharpPlanar.CachedData.power1_r0_15 line 51
lemma OAI.SharpPlanar.CachedData.power1_r0_15_eq line 52
def OAI.SharpPlanar.CachedData.power1_r0 line 53
lemma OAI.SharpPlanar.CachedData.power1_r0_eq line 54
def OAI.SharpPlanar.CachedData.power1_r1_0 line 72
lemma OAI.SharpPlanar.CachedData.power1_r1_0_eq line 73
def OAI.SharpPlanar.CachedData.power1_r1_1 line 74
lemma OAI.SharpPlanar.CachedData.power1_r1_1_eq line 75
def OAI.SharpPlanar.CachedData.power1_r1_2 line 76
lemma OAI.SharpPlanar.CachedData.power1_r1_2_eq line 77
def OAI.SharpPlanar.CachedData.power1_r1_3 line 78
lemma OAI.SharpPlanar.CachedData.power1_r1_3_eq line 79
def OAI.SharpPlanar.CachedData.power1_r1_4 line 80
lemma OAI.SharpPlanar.CachedData.power1_r1_4_eq line 81
def OAI.SharpPlanar.CachedData.power1_r1_5 line 82
lemma OAI.SharpPlanar.CachedData.power1_r1_5_eq line 83
def OAI.SharpPlanar.CachedData.power1_r1_6 line 84
lemma OAI.SharpPlanar.CachedData.power1_r1_6_eq line 85
def OAI.SharpPlanar.CachedData.power1_r1_7 line 86
lemma OAI.SharpPlanar.CachedData.power1_r1_7_eq line 87
def OAI.SharpPlanar.CachedData.power1_r1_8 line 88
lemma OAI.SharpPlanar.CachedData.power1_r1_8_eq line 89
def OAI.SharpPlanar.CachedData.power1_r1_9 line 90
lemma OAI.SharpPlanar.CachedData.power1_r1_9_eq line 91
def OAI.SharpPlanar.CachedData.power1_r1_10 line 92
lemma OAI.SharpPlanar.CachedData.power1_r1_10_eq line 93
def OAI.SharpPlanar.CachedData.power1_r1_11 line 94
lemma OAI.SharpPlanar.CachedData.power1_r1_11_eq line 95
def OAI.SharpPlanar.CachedData.power1_r1_12 line 96
lemma OAI.SharpPlanar.CachedData.power1_r1_12_eq line 97
def OAI.SharpPlanar.CachedData.power1_r1_13 line 98
lemma OAI.SharpPlanar.CachedData.power1_r1_13_eq line 99
def OAI.SharpPlanar.CachedData.power1_r1_14 line 100
lemma OAI.SharpPlanar.CachedData.power1_r1_14_eq line 101
def OAI.SharpPlanar.CachedData.power1_r1_15 line 102
lemma OAI.SharpPlanar.CachedData.power1_r1_15_eq line 103
def OAI.SharpPlanar.CachedData.power1_r1 line 104
lemma OAI.SharpPlanar.CachedData.power1_r1_eq line 105
def OAI.SharpPlanar.CachedData.power1_r2_0 line 123
lemma OAI.SharpPlanar.CachedData.power1_r2_0_eq line 124
def OAI.SharpPlanar.CachedData.power1_r2_1 line 125
lemma OAI.SharpPlanar.CachedData.power1_r2_1_eq line 126
def OAI.SharpPlanar.CachedData.power1_r2_2 line 127
lemma OAI.SharpPlanar.CachedData.power1_r2_2_eq line 128
def OAI.SharpPlanar.CachedData.power1_r2_3 line 129
lemma OAI.SharpPlanar.CachedData.power1_r2_3_eq line 130
def OAI.SharpPlanar.CachedData.power1_r2_4 line 131
lemma OAI.SharpPlanar.CachedData.power1_r2_4_eq line 132
def OAI.SharpPlanar.CachedData.power1_r2_5 line 133
lemma OAI.SharpPlanar.CachedData.power1_r2_5_eq line 134
def OAI.SharpPlanar.CachedData.power1_r2_6 line 135
lemma OAI.SharpPlanar.CachedData.power1_r2_6_eq line 136
def OAI.SharpPlanar.CachedData.power1_r2_7 line 137
lemma OAI.SharpPlanar.CachedData.power1_r2_7_eq line 138
def OAI.SharpPlanar.CachedData.power1_r2_8 line 139
lemma OAI.SharpPlanar.CachedData.power1_r2_8_eq line 140
def OAI.SharpPlanar.CachedData.power1_r2_9 line 141
lemma OAI.SharpPlanar.CachedData.power1_r2_9_eq line 142
def OAI.SharpPlanar.CachedData.power1_r2_10 line 143
lemma OAI.SharpPlanar.CachedData.power1_r2_10_eq line 144
def OAI.SharpPlanar.CachedData.power1_r2_11 line 145
lemma OAI.SharpPlanar.CachedData.power1_r2_11_eq line 146
def OAI.SharpPlanar.CachedData.power1_r2_12 line 147
lemma OAI.SharpPlanar.CachedData.power1_r2_12_eq line 148
def OAI.SharpPlanar.CachedData.power1_r2_13 line 149
lemma OAI.SharpPlanar.CachedData.power1_r2_13_eq line 150
def OAI.SharpPlanar.CachedData.power1_r2_14 line 151
lemma OAI.SharpPlanar.CachedData.power1_r2_14_eq line 152
def OAI.SharpPlanar.CachedData.power1_r2_15 line 153
lemma OAI.SharpPlanar.CachedData.power1_r2_15_eq line 154
def OAI.SharpPlanar.CachedData.power1_r2 line 155
lemma OAI.SharpPlanar.CachedData.power1_r2_eq line 156
def OAI.SharpPlanar.CachedData.power1_r3_0 line 174
lemma OAI.SharpPlanar.CachedData.power1_r3_0_eq line 175
def OAI.SharpPlanar.CachedData.power1_r3_1 line 176
lemma OAI.SharpPlanar.CachedData.power1_r3_1_eq line 177
def OAI.SharpPlanar.CachedData.power1_r3_2 line 178
lemma OAI.SharpPlanar.CachedData.power1_r3_2_eq line 179
def OAI.SharpPlanar.CachedData.power1_r3_3 line 180
lemma OAI.SharpPlanar.CachedData.power1_r3_3_eq line 181
def OAI.SharpPlanar.CachedData.power1_r3_4 line 182
lemma OAI.SharpPlanar.CachedData.power1_r3_4_eq line 183
def OAI.SharpPlanar.CachedData.power1_r3_5 line 184
lemma OAI.SharpPlanar.CachedData.power1_r3_5_eq line 185
def OAI.SharpPlanar.CachedData.power1_r3_6 line 186
lemma OAI.SharpPlanar.CachedData.power1_r3_6_eq line 187
def OAI.SharpPlanar.CachedData.power1_r3_7 line 188
lemma OAI.SharpPlanar.CachedData.power1_r3_7_eq line 189
def OAI.SharpPlanar.CachedData.power1_r3_8 line 190
lemma OAI.SharpPlanar.CachedData.power1_r3_8_eq line 191
def OAI.SharpPlanar.CachedData.power1_r3_9 line 192
lemma OAI.SharpPlanar.CachedData.power1_r3_9_eq line 193
def OAI.SharpPlanar.CachedData.power1_r3_10 line 194
lemma OAI.SharpPlanar.CachedData.power1_r3_10_eq line 195
def OAI.SharpPlanar.CachedData.power1_r3_11 line 196
lemma OAI.SharpPlanar.CachedData.power1_r3_11_eq line 197
def OAI.SharpPlanar.CachedData.power1_r3_12 line 198
lemma OAI.SharpPlanar.CachedData.power1_r3_12_eq line 199
def OAI.SharpPlanar.CachedData.power1_r3_13 line 200
lemma OAI.SharpPlanar.CachedData.power1_r3_13_eq line 201
def OAI.SharpPlanar.CachedData.power1_r3_14 line 202
lemma OAI.SharpPlanar.CachedData.power1_r3_14_eq line 203
def OAI.SharpPlanar.CachedData.power1_r3_15 line 204
lemma OAI.SharpPlanar.CachedData.power1_r3_15_eq line 205
def OAI.SharpPlanar.CachedData.power1_r3 line 206
lemma OAI.SharpPlanar.CachedData.power1_r3_eq line 207
def OAI.SharpPlanar.CachedData.power1_r4_0 line 225
lemma OAI.SharpPlanar.CachedData.power1_r4_0_eq line 226
def OAI.SharpPlanar.CachedData.power1_r4_1 line 227
lemma OAI.SharpPlanar.CachedData.power1_r4_1_eq line 228
def OAI.SharpPlanar.CachedData.power1_r4_2 line 229
lemma OAI.SharpPlanar.CachedData.power1_r4_2_eq line 230
def OAI.SharpPlanar.CachedData.power1_r4_3 line 231
lemma OAI.SharpPlanar.CachedData.power1_r4_3_eq line 232
def OAI.SharpPlanar.CachedData.power1_r4_4 line 233
lemma OAI.SharpPlanar.CachedData.power1_r4_4_eq line 234
def OAI.SharpPlanar.CachedData.power1_r4_5 line 235
lemma OAI.SharpPlanar.CachedData.power1_r4_5_eq line 236
def OAI.SharpPlanar.CachedData.power1_r4_6 line 237
lemma OAI.SharpPlanar.CachedData.power1_r4_6_eq line 238
def OAI.SharpPlanar.CachedData.power1_r4_7 line 239
lemma OAI.SharpPlanar.CachedData.power1_r4_7_eq line 240
def OAI.SharpPlanar.CachedData.power1_r4_8 line 241
lemma OAI.SharpPlanar.CachedData.power1_r4_8_eq line 242
def OAI.SharpPlanar.CachedData.power1_r4_9 line 243
lemma OAI.SharpPlanar.CachedData.power1_r4_9_eq line 244
def OAI.SharpPlanar.CachedData.power1_r4_10 line 245
lemma OAI.SharpPlanar.CachedData.power1_r4_10_eq line 246
def OAI.SharpPlanar.CachedData.power1_r4_11 line 247
lemma OAI.SharpPlanar.CachedData.power1_r4_11_eq line 248
def OAI.SharpPlanar.CachedData.power1_r4_12 line 249
lemma OAI.SharpPlanar.CachedData.power1_r4_12_eq line 250
def OAI.SharpPlanar.CachedData.power1_r4_13 line 251
lemma OAI.SharpPlanar.CachedData.power1_r4_13_eq line 252
def OAI.SharpPlanar.CachedData.power1_r4_14 line 253
lemma OAI.SharpPlanar.CachedData.power1_r4_14_eq line 254
def OAI.SharpPlanar.CachedData.power1_r4_15 line 255
lemma OAI.SharpPlanar.CachedData.power1_r4_15_eq line 256
def OAI.SharpPlanar.CachedData.power1_r4 line 257
lemma OAI.SharpPlanar.CachedData.power1_r4_eq line 258
def OAI.SharpPlanar.CachedData.power1_r5_0 line 276
lemma OAI.SharpPlanar.CachedData.power1_r5_0_eq line 277
def OAI.SharpPlanar.CachedData.power1_r5_1 line 278
lemma OAI.SharpPlanar.CachedData.power1_r5_1_eq line 279
def OAI.SharpPlanar.CachedData.power1_r5_2 line 280
lemma OAI.SharpPlanar.CachedData.power1_r5_2_eq line 281
def OAI.SharpPlanar.CachedData.power1_r5_3 line 282
lemma OAI.SharpPlanar.CachedData.power1_r5_3_eq line 283
def OAI.SharpPlanar.CachedData.power1_r5_4 line 284
lemma OAI.SharpPlanar.CachedData.power1_r5_4_eq line 285
def OAI.SharpPlanar.CachedData.power1_r5_5 line 286
lemma OAI.SharpPlanar.CachedData.power1_r5_5_eq line 287
def OAI.SharpPlanar.CachedData.power1_r5_6 line 288
lemma OAI.SharpPlanar.CachedData.power1_r5_6_eq line 289
def OAI.SharpPlanar.CachedData.power1_r5_7 line 290
lemma OAI.SharpPlanar.CachedData.power1_r5_7_eq line 291
def OAI.SharpPlanar.CachedData.power1_r5_8 line 292
lemma OAI.SharpPlanar.CachedData.power1_r5_8_eq line 293
def OAI.SharpPlanar.CachedData.power1_r5_9 line 294
lemma OAI.SharpPlanar.CachedData.power1_r5_9_eq line 295
def OAI.SharpPlanar.CachedData.power1_r5_10 line 296
lemma OAI.SharpPlanar.CachedData.power1_r5_10_eq line 297
def OAI.SharpPlanar.CachedData.power1_r5_11 line 298
lemma OAI.SharpPlanar.CachedData.power1_r5_11_eq line 299
def OAI.SharpPlanar.CachedData.power1_r5_12 line 300
lemma OAI.SharpPlanar.CachedData.power1_r5_12_eq line 301
def OAI.SharpPlanar.CachedData.power1_r5_13 line 302
lemma OAI.SharpPlanar.CachedData.power1_r5_13_eq line 303
def OAI.SharpPlanar.CachedData.power1_r5_14 line 304
lemma OAI.SharpPlanar.CachedData.power1_r5_14_eq line 305
def OAI.SharpPlanar.CachedData.power1_r5_15 line 306
lemma OAI.SharpPlanar.CachedData.power1_r5_15_eq line 307
def OAI.SharpPlanar.CachedData.power1_r5 line 308
lemma OAI.SharpPlanar.CachedData.power1_r5_eq line 309
def OAI.SharpPlanar.CachedData.power1 line 327
lemma OAI.SharpPlanar.CachedData.power1_eq line 328
lemma OAI.SharpPlanar.CachedData.power1_contains line 336
def OAI.SharpPlanar.CachedData.power2Expr line 342
def OAI.SharpPlanar.CachedData.power2_r0_0 line 343
lemma OAI.SharpPlanar.CachedData.power2_r0_0_eq line 344
def OAI.SharpPlanar.CachedData.power2_r0_1 line 345
lemma OAI.SharpPlanar.CachedData.power2_r0_1_eq line 346
def OAI.SharpPlanar.CachedData.power2_r0_2 line 347
lemma OAI.SharpPlanar.CachedData.power2_r0_2_eq line 348
def OAI.SharpPlanar.CachedData.power2_r0_3 line 349
lemma OAI.SharpPlanar.CachedData.power2_r0_3_eq line 350
def OAI.SharpPlanar.CachedData.power2_r0_4 line 351
lemma OAI.SharpPlanar.CachedData.power2_r0_4_eq line 352
def OAI.SharpPlanar.CachedData.power2_r0_5 line 353
lemma OAI.SharpPlanar.CachedData.power2_r0_5_eq line 354
def OAI.SharpPlanar.CachedData.power2_r0_6 line 355
lemma OAI.SharpPlanar.CachedData.power2_r0_6_eq line 356
def OAI.SharpPlanar.CachedData.power2_r0_7 line 357
lemma OAI.SharpPlanar.CachedData.power2_r0_7_eq line 358
def OAI.SharpPlanar.CachedData.power2_r0_8 line 359
lemma OAI.SharpPlanar.CachedData.power2_r0_8_eq line 360
def OAI.SharpPlanar.CachedData.power2_r0_9 line 361
lemma OAI.SharpPlanar.CachedData.power2_r0_9_eq line 362
def OAI.SharpPlanar.CachedData.power2_r0_10 line 363
lemma OAI.SharpPlanar.CachedData.power2_r0_10_eq line 364
def OAI.SharpPlanar.CachedData.power2_r0_11 line 365
lemma OAI.SharpPlanar.CachedData.power2_r0_11_eq line 366
def OAI.SharpPlanar.CachedData.power2_r0_12 line 367
lemma OAI.SharpPlanar.CachedData.power2_r0_12_eq line 368
def OAI.SharpPlanar.CachedData.power2_r0_13 line 369
lemma OAI.SharpPlanar.CachedData.power2_r0_13_eq line 370
def OAI.SharpPlanar.CachedData.power2_r0_14 line 371
lemma OAI.SharpPlanar.CachedData.power2_r0_14_eq line 372
def OAI.SharpPlanar.CachedData.power2_r0_15 line 373
lemma OAI.SharpPlanar.CachedData.power2_r0_15_eq line 374
def OAI.SharpPlanar.CachedData.power2_r0 line 375
lemma OAI.SharpPlanar.CachedData.power2_r0_eq line 376
def OAI.SharpPlanar.CachedData.power2_r1_0 line 394
lemma OAI.SharpPlanar.CachedData.power2_r1_0_eq line 395
def OAI.SharpPlanar.CachedData.power2_r1_1 line 396
lemma OAI.SharpPlanar.CachedData.power2_r1_1_eq line 397
def OAI.SharpPlanar.CachedData.power2_r1_2 line 398
lemma OAI.SharpPlanar.CachedData.power2_r1_2_eq line 399
def OAI.SharpPlanar.CachedData.power2_r1_3 line 400
lemma OAI.SharpPlanar.CachedData.power2_r1_3_eq line 401
def OAI.SharpPlanar.CachedData.power2_r1_4 line 402
lemma OAI.SharpPlanar.CachedData.power2_r1_4_eq line 403
def OAI.SharpPlanar.CachedData.power2_r1_5 line 404
lemma OAI.SharpPlanar.CachedData.power2_r1_5_eq line 405
def OAI.SharpPlanar.CachedData.power2_r1_6 line 406
lemma OAI.SharpPlanar.CachedData.power2_r1_6_eq line 407
def OAI.SharpPlanar.CachedData.power2_r1_7 line 408
lemma OAI.SharpPlanar.CachedData.power2_r1_7_eq line 409
def OAI.SharpPlanar.CachedData.power2_r1_8 line 410
lemma OAI.SharpPlanar.CachedData.power2_r1_8_eq line 411
def OAI.SharpPlanar.CachedData.power2_r1_9 line 412
lemma OAI.SharpPlanar.CachedData.power2_r1_9_eq line 413
def OAI.SharpPlanar.CachedData.power2_r1_10 line 414
lemma OAI.SharpPlanar.CachedData.power2_r1_10_eq line 415
def OAI.SharpPlanar.CachedData.power2_r1_11 line 416
lemma OAI.SharpPlanar.CachedData.power2_r1_11_eq line 417
def OAI.SharpPlanar.CachedData.power2_r1_12 line 418
lemma OAI.SharpPlanar.CachedData.power2_r1_12_eq line 419
def OAI.SharpPlanar.CachedData.power2_r1_13 line 420
lemma OAI.SharpPlanar.CachedData.power2_r1_13_eq line 421
def OAI.SharpPlanar.CachedData.power2_r1_14 line 422
lemma OAI.SharpPlanar.CachedData.power2_r1_14_eq line 423
def OAI.SharpPlanar.CachedData.power2_r1_15 line 424
lemma OAI.SharpPlanar.CachedData.power2_r1_15_eq line 425
def OAI.SharpPlanar.CachedData.power2_r1 line 426
lemma OAI.SharpPlanar.CachedData.power2_r1_eq line 427
def OAI.SharpPlanar.CachedData.power2_r2_0 line 445
lemma OAI.SharpPlanar.CachedData.power2_r2_0_eq line 446
def OAI.SharpPlanar.CachedData.power2_r2_1 line 447
lemma OAI.SharpPlanar.CachedData.power2_r2_1_eq line 448
def OAI.SharpPlanar.CachedData.power2_r2_2 line 449
lemma OAI.SharpPlanar.CachedData.power2_r2_2_eq line 450
def OAI.SharpPlanar.CachedData.power2_r2_3 line 451
lemma OAI.SharpPlanar.CachedData.power2_r2_3_eq line 452
def OAI.SharpPlanar.CachedData.power2_r2_4 line 453
lemma OAI.SharpPlanar.CachedData.power2_r2_4_eq line 454
def OAI.SharpPlanar.CachedData.power2_r2_5 line 455
lemma OAI.SharpPlanar.CachedData.power2_r2_5_eq line 456
def OAI.SharpPlanar.CachedData.power2_r2_6 line 457
lemma OAI.SharpPlanar.CachedData.power2_r2_6_eq line 458
def OAI.SharpPlanar.CachedData.power2_r2_7 line 459
lemma OAI.SharpPlanar.CachedData.power2_r2_7_eq line 460
def OAI.SharpPlanar.CachedData.power2_r2_8 line 461
lemma OAI.SharpPlanar.CachedData.power2_r2_8_eq line 462
def OAI.SharpPlanar.CachedData.power2_r2_9 line 463
lemma OAI.SharpPlanar.CachedData.power2_r2_9_eq line 464
def OAI.SharpPlanar.CachedData.power2_r2_10 line 465
lemma OAI.SharpPlanar.CachedData.power2_r2_10_eq line 466
def OAI.SharpPlanar.CachedData.power2_r2_11 line 467
lemma OAI.SharpPlanar.CachedData.power2_r2_11_eq line 468
def OAI.SharpPlanar.CachedData.power2_r2_12 line 469
lemma OAI.SharpPlanar.CachedData.power2_r2_12_eq line 470
def OAI.SharpPlanar.CachedData.power2_r2_13 line 471
lemma OAI.SharpPlanar.CachedData.power2_r2_13_eq line 472
def OAI.SharpPlanar.CachedData.power2_r2_14 line 473
lemma OAI.SharpPlanar.CachedData.power2_r2_14_eq line 474
def OAI.SharpPlanar.CachedData.power2_r2_15 line 475
lemma OAI.SharpPlanar.CachedData.power2_r2_15_eq line 476
def OAI.SharpPlanar.CachedData.power2_r2 line 477
lemma OAI.SharpPlanar.CachedData.power2_r2_eq line 478
def OAI.SharpPlanar.CachedData.power2_r3_0 line 496
lemma OAI.SharpPlanar.CachedData.power2_r3_0_eq line 497
def OAI.SharpPlanar.CachedData.power2_r3_1 line 498
lemma OAI.SharpPlanar.CachedData.power2_r3_1_eq line 499
def OAI.SharpPlanar.CachedData.power2_r3_2 line 500
lemma OAI.SharpPlanar.CachedData.power2_r3_2_eq line 501
def OAI.SharpPlanar.CachedData.power2_r3_3 line 502
lemma OAI.SharpPlanar.CachedData.power2_r3_3_eq line 503
def OAI.SharpPlanar.CachedData.power2_r3_4 line 504
lemma OAI.SharpPlanar.CachedData.power2_r3_4_eq line 505
def OAI.SharpPlanar.CachedData.power2_r3_5 line 506
lemma OAI.SharpPlanar.CachedData.power2_r3_5_eq line 507
def OAI.SharpPlanar.CachedData.power2_r3_6 line 508
lemma OAI.SharpPlanar.CachedData.power2_r3_6_eq line 509
def OAI.SharpPlanar.CachedData.power2_r3_7 line 510
lemma OAI.SharpPlanar.CachedData.power2_r3_7_eq line 511
def OAI.SharpPlanar.CachedData.power2_r3_8 line 512
lemma OAI.SharpPlanar.CachedData.power2_r3_8_eq line 513
def OAI.SharpPlanar.CachedData.power2_r3_9 line 514
lemma OAI.SharpPlanar.CachedData.power2_r3_9_eq line 515
def OAI.SharpPlanar.CachedData.power2_r3_10 line 516
lemma OAI.SharpPlanar.CachedData.power2_r3_10_eq line 517
def OAI.SharpPlanar.CachedData.power2_r3_11 line 518
lemma OAI.SharpPlanar.CachedData.power2_r3_11_eq line 519
def OAI.SharpPlanar.CachedData.power2_r3_12 line 520
lemma OAI.SharpPlanar.CachedData.power2_r3_12_eq line 521
def OAI.SharpPlanar.CachedData.power2_r3_13 line 522
lemma OAI.SharpPlanar.CachedData.power2_r3_13_eq line 523
def OAI.SharpPlanar.CachedData.power2_r3_14 line 524
lemma OAI.SharpPlanar.CachedData.power2_r3_14_eq line 525
def OAI.SharpPlanar.CachedData.power2_r3_15 line 526
lemma OAI.SharpPlanar.CachedData.power2_r3_15_eq line 527
def OAI.SharpPlanar.CachedData.power2_r3 line 528
lemma OAI.SharpPlanar.CachedData.power2_r3_eq line 529
def OAI.SharpPlanar.CachedData.power2_r4_0 line 547
lemma OAI.SharpPlanar.CachedData.power2_r4_0_eq line 548
def OAI.SharpPlanar.CachedData.power2_r4_1 line 549
lemma OAI.SharpPlanar.CachedData.power2_r4_1_eq line 550
def OAI.SharpPlanar.CachedData.power2_r4_2 line 551
lemma OAI.SharpPlanar.CachedData.power2_r4_2_eq line 552
def OAI.SharpPlanar.CachedData.power2_r4_3 line 553
lemma OAI.SharpPlanar.CachedData.power2_r4_3_eq line 554
def OAI.SharpPlanar.CachedData.power2_r4_4 line 555
lemma OAI.SharpPlanar.CachedData.power2_r4_4_eq line 556
def OAI.SharpPlanar.CachedData.power2_r4_5 line 557
lemma OAI.SharpPlanar.CachedData.power2_r4_5_eq line 558
def OAI.SharpPlanar.CachedData.power2_r4_6 line 559
lemma OAI.SharpPlanar.CachedData.power2_r4_6_eq line 560
def OAI.SharpPlanar.CachedData.power2_r4_7 line 561
lemma OAI.SharpPlanar.CachedData.power2_r4_7_eq line 562
def OAI.SharpPlanar.CachedData.power2_r4_8 line 563
lemma OAI.SharpPlanar.CachedData.power2_r4_8_eq line 564
def OAI.SharpPlanar.CachedData.power2_r4_9 line 565
lemma OAI.SharpPlanar.CachedData.power2_r4_9_eq line 566
def OAI.SharpPlanar.CachedData.power2_r4_10 line 567
lemma OAI.SharpPlanar.CachedData.power2_r4_10_eq line 568
def OAI.SharpPlanar.CachedData.power2_r4_11 line 569
lemma OAI.SharpPlanar.CachedData.power2_r4_11_eq line 570
def OAI.SharpPlanar.CachedData.power2_r4_12 line 571
lemma OAI.SharpPlanar.CachedData.power2_r4_12_eq line 572
def OAI.SharpPlanar.CachedData.power2_r4_13 line 573
lemma OAI.SharpPlanar.CachedData.power2_r4_13_eq line 574
def OAI.SharpPlanar.CachedData.power2_r4_14 line 575
lemma OAI.SharpPlanar.CachedData.power2_r4_14_eq line 576
def OAI.SharpPlanar.CachedData.power2_r4_15 line 577
lemma OAI.SharpPlanar.CachedData.power2_r4_15_eq line 578
def OAI.SharpPlanar.CachedData.power2_r4 line 579
lemma OAI.SharpPlanar.CachedData.power2_r4_eq line 580
def OAI.SharpPlanar.CachedData.power2_r5_0 line 598
lemma OAI.SharpPlanar.CachedData.power2_r5_0_eq line 599
def OAI.SharpPlanar.CachedData.power2_r5_1 line 600
lemma OAI.SharpPlanar.CachedData.power2_r5_1_eq line 601
def OAI.SharpPlanar.CachedData.power2_r5_2 line 602
lemma OAI.SharpPlanar.CachedData.power2_r5_2_eq line 603
def OAI.SharpPlanar.CachedData.power2_r5_3 line 604
lemma OAI.SharpPlanar.CachedData.power2_r5_3_eq line 605
def OAI.SharpPlanar.CachedData.power2_r5_4 line 606
lemma OAI.SharpPlanar.CachedData.power2_r5_4_eq line 607
def OAI.SharpPlanar.CachedData.power2_r5_5 line 608
lemma OAI.SharpPlanar.CachedData.power2_r5_5_eq line 609
def OAI.SharpPlanar.CachedData.power2_r5_6 line 610
lemma OAI.SharpPlanar.CachedData.power2_r5_6_eq line 611
def OAI.SharpPlanar.CachedData.power2_r5_7 line 612
lemma OAI.SharpPlanar.CachedData.power2_r5_7_eq line 613
def OAI.SharpPlanar.CachedData.power2_r5_8 line 614
lemma OAI.SharpPlanar.CachedData.power2_r5_8_eq line 615
def OAI.SharpPlanar.CachedData.power2_r5_9 line 616
lemma OAI.SharpPlanar.CachedData.power2_r5_9_eq line 617
def OAI.SharpPlanar.CachedData.power2_r5_10 line 618
lemma OAI.SharpPlanar.CachedData.power2_r5_10_eq line 619
def OAI.SharpPlanar.CachedData.power2_r5_11 line 620
lemma OAI.SharpPlanar.CachedData.power2_r5_11_eq line 621
def OAI.SharpPlanar.CachedData.power2_r5_12 line 622
lemma OAI.SharpPlanar.CachedData.power2_r5_12_eq line 623
def OAI.SharpPlanar.CachedData.power2_r5_13 line 624
lemma OAI.SharpPlanar.CachedData.power2_r5_13_eq line 625
def OAI.SharpPlanar.CachedData.power2_r5_14 line 626
lemma OAI.SharpPlanar.CachedData.power2_r5_14_eq line 627
def OAI.SharpPlanar.CachedData.power2_r5_15 line 628
lemma OAI.SharpPlanar.CachedData.power2_r5_15_eq line 629
def OAI.SharpPlanar.CachedData.power2_r5 line 630
lemma OAI.SharpPlanar.CachedData.power2_r5_eq line 631
def OAI.SharpPlanar.CachedData.power2 line 649
lemma OAI.SharpPlanar.CachedData.power2_eq line 650
lemma OAI.SharpPlanar.CachedData.power2_contains line 658
def OAI.SharpPlanar.CachedData.power3Expr line 664
def OAI.SharpPlanar.CachedData.power3_r0_0 line 665
lemma OAI.SharpPlanar.CachedData.power3_r0_0_eq line 666
def OAI.SharpPlanar.CachedData.power3_r0_1 line 667
lemma OAI.SharpPlanar.CachedData.power3_r0_1_eq line 668
def OAI.SharpPlanar.CachedData.power3_r0_2 line 669
lemma OAI.SharpPlanar.CachedData.power3_r0_2_eq line 670
def OAI.SharpPlanar.CachedData.power3_r0_3 line 671
lemma OAI.SharpPlanar.CachedData.power3_r0_3_eq line 672
def OAI.SharpPlanar.CachedData.power3_r0_4 line 673
lemma OAI.SharpPlanar.CachedData.power3_r0_4_eq line 674
def OAI.SharpPlanar.CachedData.power3_r0_5 line 675
lemma OAI.SharpPlanar.CachedData.power3_r0_5_eq line 676
def OAI.SharpPlanar.CachedData.power3_r0_6 line 677
lemma OAI.SharpPlanar.CachedData.power3_r0_6_eq line 678
def OAI.SharpPlanar.CachedData.power3_r0_7 line 679
lemma OAI.SharpPlanar.CachedData.power3_r0_7_eq line 680
def OAI.SharpPlanar.CachedData.power3_r0_8 line 681
lemma OAI.SharpPlanar.CachedData.power3_r0_8_eq line 682
def OAI.SharpPlanar.CachedData.power3_r0_9 line 683
lemma OAI.SharpPlanar.CachedData.power3_r0_9_eq line 684
def OAI.SharpPlanar.CachedData.power3_r0_10 line 685
lemma OAI.SharpPlanar.CachedData.power3_r0_10_eq line 686
def OAI.SharpPlanar.CachedData.power3_r0_11 line 687
lemma OAI.SharpPlanar.CachedData.power3_r0_11_eq line 688
def OAI.SharpPlanar.CachedData.power3_r0_12 line 689
lemma OAI.SharpPlanar.CachedData.power3_r0_12_eq line 690
def OAI.SharpPlanar.CachedData.power3_r0_13 line 691
lemma OAI.SharpPlanar.CachedData.power3_r0_13_eq line 692
def OAI.SharpPlanar.CachedData.power3_r0_14 line 693
lemma OAI.SharpPlanar.CachedData.power3_r0_14_eq line 694
def OAI.SharpPlanar.CachedData.power3_r0_15 line 695
lemma OAI.SharpPlanar.CachedData.power3_r0_15_eq line 696
def OAI.SharpPlanar.CachedData.power3_r0 line 697
lemma OAI.SharpPlanar.CachedData.power3_r0_eq line 698
def OAI.SharpPlanar.CachedData.power3_r1_0 line 716
lemma OAI.SharpPlanar.CachedData.power3_r1_0_eq line 717
def OAI.SharpPlanar.CachedData.power3_r1_1 line 718
lemma OAI.SharpPlanar.CachedData.power3_r1_1_eq line 719
def OAI.SharpPlanar.CachedData.power3_r1_2 line 720
lemma OAI.SharpPlanar.CachedData.power3_r1_2_eq line 721
def OAI.SharpPlanar.CachedData.power3_r1_3 line 722
lemma OAI.SharpPlanar.CachedData.power3_r1_3_eq line 723
def OAI.SharpPlanar.CachedData.power3_r1_4 line 724
lemma OAI.SharpPlanar.CachedData.power3_r1_4_eq line 725
def OAI.SharpPlanar.CachedData.power3_r1_5 line 726
lemma OAI.SharpPlanar.CachedData.power3_r1_5_eq line 727
def OAI.SharpPlanar.CachedData.power3_r1_6 line 728
lemma OAI.SharpPlanar.CachedData.power3_r1_6_eq line 729
def OAI.SharpPlanar.CachedData.power3_r1_7 line 730
lemma OAI.SharpPlanar.CachedData.power3_r1_7_eq line 731
def OAI.SharpPlanar.CachedData.power3_r1_8 line 732
lemma OAI.SharpPlanar.CachedData.power3_r1_8_eq line 733
def OAI.SharpPlanar.CachedData.power3_r1_9 line 734
lemma OAI.SharpPlanar.CachedData.power3_r1_9_eq line 735
def OAI.SharpPlanar.CachedData.power3_r1_10 line 736
lemma OAI.SharpPlanar.CachedData.power3_r1_10_eq line 737
def OAI.SharpPlanar.CachedData.power3_r1_11 line 738
lemma OAI.SharpPlanar.CachedData.power3_r1_11_eq line 739
def OAI.SharpPlanar.CachedData.power3_r1_12 line 740
lemma OAI.SharpPlanar.CachedData.power3_r1_12_eq line 741
def OAI.SharpPlanar.CachedData.power3_r1_13 line 742
lemma OAI.SharpPlanar.CachedData.power3_r1_13_eq line 743
def OAI.SharpPlanar.CachedData.power3_r1_14 line 744
lemma OAI.SharpPlanar.CachedData.power3_r1_14_eq line 745
def OAI.SharpPlanar.CachedData.power3_r1_15 line 746
lemma OAI.SharpPlanar.CachedData.power3_r1_15_eq line 747
def OAI.SharpPlanar.CachedData.power3_r1 line 748
lemma OAI.SharpPlanar.CachedData.power3_r1_eq line 749
def OAI.SharpPlanar.CachedData.power3_r2_0 line 767
lemma OAI.SharpPlanar.CachedData.power3_r2_0_eq line 768
def OAI.SharpPlanar.CachedData.power3_r2_1 line 769
lemma OAI.SharpPlanar.CachedData.power3_r2_1_eq line 770
def OAI.SharpPlanar.CachedData.power3_r2_2 line 771
lemma OAI.SharpPlanar.CachedData.power3_r2_2_eq line 772
def OAI.SharpPlanar.CachedData.power3_r2_3 line 773
lemma OAI.SharpPlanar.CachedData.power3_r2_3_eq line 774
def OAI.SharpPlanar.CachedData.power3_r2_4 line 775
lemma OAI.SharpPlanar.CachedData.power3_r2_4_eq line 776
def OAI.SharpPlanar.CachedData.power3_r2_5 line 777
lemma OAI.SharpPlanar.CachedData.power3_r2_5_eq line 778
def OAI.SharpPlanar.CachedData.power3_r2_6 line 779
lemma OAI.SharpPlanar.CachedData.power3_r2_6_eq line 780
def OAI.SharpPlanar.CachedData.power3_r2_7 line 781
lemma OAI.SharpPlanar.CachedData.power3_r2_7_eq line 782
def OAI.SharpPlanar.CachedData.power3_r2_8 line 783
lemma OAI.SharpPlanar.CachedData.power3_r2_8_eq line 784
def OAI.SharpPlanar.CachedData.power3_r2_9 line 785
lemma OAI.SharpPlanar.CachedData.power3_r2_9_eq line 786
def OAI.SharpPlanar.CachedData.power3_r2_10 line 787
lemma OAI.SharpPlanar.CachedData.power3_r2_10_eq line 788
def OAI.SharpPlanar.CachedData.power3_r2_11 line 789
lemma OAI.SharpPlanar.CachedData.power3_r2_11_eq line 790
def OAI.SharpPlanar.CachedData.power3_r2_12 line 791
lemma OAI.SharpPlanar.CachedData.power3_r2_12_eq line 792
def OAI.SharpPlanar.CachedData.power3_r2_13 line 793
lemma OAI.SharpPlanar.CachedData.power3_r2_13_eq line 794
def OAI.SharpPlanar.CachedData.power3_r2_14 line 795
lemma OAI.SharpPlanar.CachedData.power3_r2_14_eq line 796
def OAI.SharpPlanar.CachedData.power3_r2_15 line 797
lemma OAI.SharpPlanar.CachedData.power3_r2_15_eq line 798
def OAI.SharpPlanar.CachedData.power3_r2 line 799
lemma OAI.SharpPlanar.CachedData.power3_r2_eq line 800
def OAI.SharpPlanar.CachedData.power3_r3_0 line 818
lemma OAI.SharpPlanar.CachedData.power3_r3_0_eq line 819
def OAI.SharpPlanar.CachedData.power3_r3_1 line 820
lemma OAI.SharpPlanar.CachedData.power3_r3_1_eq line 821
def OAI.SharpPlanar.CachedData.power3_r3_2 line 822
lemma OAI.SharpPlanar.CachedData.power3_r3_2_eq line 823
def OAI.SharpPlanar.CachedData.power3_r3_3 line 824
lemma OAI.SharpPlanar.CachedData.power3_r3_3_eq line 825
def OAI.SharpPlanar.CachedData.power3_r3_4 line 826
lemma OAI.SharpPlanar.CachedData.power3_r3_4_eq line 827
def OAI.SharpPlanar.CachedData.power3_r3_5 line 828
lemma OAI.SharpPlanar.CachedData.power3_r3_5_eq line 829
def OAI.SharpPlanar.CachedData.power3_r3_6 line 830
lemma OAI.SharpPlanar.CachedData.power3_r3_6_eq line 831
def OAI.SharpPlanar.CachedData.power3_r3_7 line 832
lemma OAI.SharpPlanar.CachedData.power3_r3_7_eq line 833
def OAI.SharpPlanar.CachedData.power3_r3_8 line 834
lemma OAI.SharpPlanar.CachedData.power3_r3_8_eq line 835
def OAI.SharpPlanar.CachedData.power3_r3_9 line 836
lemma OAI.SharpPlanar.CachedData.power3_r3_9_eq line 837
def OAI.SharpPlanar.CachedData.power3_r3_10 line 838
lemma OAI.SharpPlanar.CachedData.power3_r3_10_eq line 839
def OAI.SharpPlanar.CachedData.power3_r3_11 line 840
lemma OAI.SharpPlanar.CachedData.power3_r3_11_eq line 841
def OAI.SharpPlanar.CachedData.power3_r3_12 line 842
lemma OAI.SharpPlanar.CachedData.power3_r3_12_eq line 843
def OAI.SharpPlanar.CachedData.power3_r3_13 line 844
lemma OAI.SharpPlanar.CachedData.power3_r3_13_eq line 845
def OAI.SharpPlanar.CachedData.power3_r3_14 line 846
lemma OAI.SharpPlanar.CachedData.power3_r3_14_eq line 847
def OAI.SharpPlanar.CachedData.power3_r3_15 line 848
lemma OAI.SharpPlanar.CachedData.power3_r3_15_eq line 849
def OAI.SharpPlanar.CachedData.power3_r3 line 850
lemma OAI.SharpPlanar.CachedData.power3_r3_eq line 851
def OAI.SharpPlanar.CachedData.power3_r4_0 line 869
lemma OAI.SharpPlanar.CachedData.power3_r4_0_eq line 870
def OAI.SharpPlanar.CachedData.power3_r4_1 line 871
lemma OAI.SharpPlanar.CachedData.power3_r4_1_eq line 872
def OAI.SharpPlanar.CachedData.power3_r4_2 line 873
lemma OAI.SharpPlanar.CachedData.power3_r4_2_eq line 874
def OAI.SharpPlanar.CachedData.power3_r4_3 line 875
lemma OAI.SharpPlanar.CachedData.power3_r4_3_eq line 876
def OAI.SharpPlanar.CachedData.power3_r4_4 line 877
lemma OAI.SharpPlanar.CachedData.power3_r4_4_eq line 878
def OAI.SharpPlanar.CachedData.power3_r4_5 line 879
lemma OAI.SharpPlanar.CachedData.power3_r4_5_eq line 880
def OAI.SharpPlanar.CachedData.power3_r4_6 line 881
lemma OAI.SharpPlanar.CachedData.power3_r4_6_eq line 882
def OAI.SharpPlanar.CachedData.power3_r4_7 line 883
lemma OAI.SharpPlanar.CachedData.power3_r4_7_eq line 884
def OAI.SharpPlanar.CachedData.power3_r4_8 line 885
lemma OAI.SharpPlanar.CachedData.power3_r4_8_eq line 886
def OAI.SharpPlanar.CachedData.power3_r4_9 line 887
lemma OAI.SharpPlanar.CachedData.power3_r4_9_eq line 888
def OAI.SharpPlanar.CachedData.power3_r4_10 line 889
lemma OAI.SharpPlanar.CachedData.power3_r4_10_eq line 890
def OAI.SharpPlanar.CachedData.power3_r4_11 line 891
lemma OAI.SharpPlanar.CachedData.power3_r4_11_eq line 892
def OAI.SharpPlanar.CachedData.power3_r4_12 line 893
lemma OAI.SharpPlanar.CachedData.power3_r4_12_eq line 894
def OAI.SharpPlanar.CachedData.power3_r4_13 line 895
lemma OAI.SharpPlanar.CachedData.power3_r4_13_eq line 896
def OAI.SharpPlanar.CachedData.power3_r4_14 line 897
lemma OAI.SharpPlanar.CachedData.power3_r4_14_eq line 898
def OAI.SharpPlanar.CachedData.power3_r4_15 line 899
lemma OAI.SharpPlanar.CachedData.power3_r4_15_eq line 900
def OAI.SharpPlanar.CachedData.power3_r4 line 901
lemma OAI.SharpPlanar.CachedData.power3_r4_eq line 902
def OAI.SharpPlanar.CachedData.power3_r5_0 line 920
lemma OAI.SharpPlanar.CachedData.power3_r5_0_eq line 921
def OAI.SharpPlanar.CachedData.power3_r5_1 line 922
lemma OAI.SharpPlanar.CachedData.power3_r5_1_eq line 923
def OAI.SharpPlanar.CachedData.power3_r5_2 line 924
lemma OAI.SharpPlanar.CachedData.power3_r5_2_eq line 925
def OAI.SharpPlanar.CachedData.power3_r5_3 line 926
lemma OAI.SharpPlanar.CachedData.power3_r5_3_eq line 927
def OAI.SharpPlanar.CachedData.power3_r5_4 line 928
lemma OAI.SharpPlanar.CachedData.power3_r5_4_eq line 929
def OAI.SharpPlanar.CachedData.power3_r5_5 line 930
lemma OAI.SharpPlanar.CachedData.power3_r5_5_eq line 931
def OAI.SharpPlanar.CachedData.power3_r5_6 line 932
lemma OAI.SharpPlanar.CachedData.power3_r5_6_eq line 933
def OAI.SharpPlanar.CachedData.power3_r5_7 line 934
lemma OAI.SharpPlanar.CachedData.power3_r5_7_eq line 935
def OAI.SharpPlanar.CachedData.power3_r5_8 line 936
lemma OAI.SharpPlanar.CachedData.power3_r5_8_eq line 937
def OAI.SharpPlanar.CachedData.power3_r5_9 line 938
lemma OAI.SharpPlanar.CachedData.power3_r5_9_eq line 939
def OAI.SharpPlanar.CachedData.power3_r5_10 line 940
lemma OAI.SharpPlanar.CachedData.power3_r5_10_eq line 941
def OAI.SharpPlanar.CachedData.power3_r5_11 line 942
lemma OAI.SharpPlanar.CachedData.power3_r5_11_eq line 943
def OAI.SharpPlanar.CachedData.power3_r5_12 line 944
lemma OAI.SharpPlanar.CachedData.power3_r5_12_eq line 945
def OAI.SharpPlanar.CachedData.power3_r5_13 line 946
lemma OAI.SharpPlanar.CachedData.power3_r5_13_eq line 947
def OAI.SharpPlanar.CachedData.power3_r5_14 line 948
lemma OAI.SharpPlanar.CachedData.power3_r5_14_eq line 949
def OAI.SharpPlanar.CachedData.power3_r5_15 line 950
lemma OAI.SharpPlanar.CachedData.power3_r5_15_eq line 951
def OAI.SharpPlanar.CachedData.power3_r5 line 952
lemma OAI.SharpPlanar.CachedData.power3_r5_eq line 953
def OAI.SharpPlanar.CachedData.power3 line 971
lemma OAI.SharpPlanar.CachedData.power3_eq line 972
lemma OAI.SharpPlanar.CachedData.power3_contains line 980
def OAI.SharpPlanar.CachedData.power4Expr line 986
def OAI.SharpPlanar.CachedData.power4_r0_0 line 987
lemma OAI.SharpPlanar.CachedData.power4_r0_0_eq line 988
def OAI.SharpPlanar.CachedData.power4_r0_1 line 989
lemma OAI.SharpPlanar.CachedData.power4_r0_1_eq line 990
def OAI.SharpPlanar.CachedData.power4_r0_2 line 991
lemma OAI.SharpPlanar.CachedData.power4_r0_2_eq line 992
def OAI.SharpPlanar.CachedData.power4_r0_3 line 993
lemma OAI.SharpPlanar.CachedData.power4_r0_3_eq line 994
def OAI.SharpPlanar.CachedData.power4_r0_4 line 995
lemma OAI.SharpPlanar.CachedData.power4_r0_4_eq line 996
def OAI.SharpPlanar.CachedData.power4_r0_5 line 997
lemma OAI.SharpPlanar.CachedData.power4_r0_5_eq line 998
def OAI.SharpPlanar.CachedData.power4_r0_6 line 999
lemma OAI.SharpPlanar.CachedData.power4_r0_6_eq line 1000
def OAI.SharpPlanar.CachedData.power4_r0_7 line 1001
lemma OAI.SharpPlanar.CachedData.power4_r0_7_eq line 1002
def OAI.SharpPlanar.CachedData.power4_r0_8 line 1003
lemma OAI.SharpPlanar.CachedData.power4_r0_8_eq line 1004
def OAI.SharpPlanar.CachedData.power4_r0_9 line 1005
lemma OAI.SharpPlanar.CachedData.power4_r0_9_eq line 1006
def OAI.SharpPlanar.CachedData.power4_r0_10 line 1007
lemma OAI.SharpPlanar.CachedData.power4_r0_10_eq line 1008
def OAI.SharpPlanar.CachedData.power4_r0_11 line 1009
lemma OAI.SharpPlanar.CachedData.power4_r0_11_eq line 1010
def OAI.SharpPlanar.CachedData.power4_r0_12 line 1011
lemma OAI.SharpPlanar.CachedData.power4_r0_12_eq line 1012
def OAI.SharpPlanar.CachedData.power4_r0_13 line 1013
lemma OAI.SharpPlanar.CachedData.power4_r0_13_eq line 1014
def OAI.SharpPlanar.CachedData.power4_r0_14 line 1015
lemma OAI.SharpPlanar.CachedData.power4_r0_14_eq line 1016
def OAI.SharpPlanar.CachedData.power4_r0_15 line 1017
lemma OAI.SharpPlanar.CachedData.power4_r0_15_eq line 1018
def OAI.SharpPlanar.CachedData.power4_r0 line 1019
lemma OAI.SharpPlanar.CachedData.power4_r0_eq line 1020
def OAI.SharpPlanar.CachedData.power4_r1_0 line 1038
lemma OAI.SharpPlanar.CachedData.power4_r1_0_eq line 1039
def OAI.SharpPlanar.CachedData.power4_r1_1 line 1040
lemma OAI.SharpPlanar.CachedData.power4_r1_1_eq line 1041
def OAI.SharpPlanar.CachedData.power4_r1_2 line 1042
lemma OAI.SharpPlanar.CachedData.power4_r1_2_eq line 1043
def OAI.SharpPlanar.CachedData.power4_r1_3 line 1044
lemma OAI.SharpPlanar.CachedData.power4_r1_3_eq line 1045
def OAI.SharpPlanar.CachedData.power4_r1_4 line 1046
lemma OAI.SharpPlanar.CachedData.power4_r1_4_eq line 1047
def OAI.SharpPlanar.CachedData.power4_r1_5 line 1048
lemma OAI.SharpPlanar.CachedData.power4_r1_5_eq line 1049
def OAI.SharpPlanar.CachedData.power4_r1_6 line 1050
lemma OAI.SharpPlanar.CachedData.power4_r1_6_eq line 1051
def OAI.SharpPlanar.CachedData.power4_r1_7 line 1052
lemma OAI.SharpPlanar.CachedData.power4_r1_7_eq line 1053
def OAI.SharpPlanar.CachedData.power4_r1_8 line 1054
lemma OAI.SharpPlanar.CachedData.power4_r1_8_eq line 1055
def OAI.SharpPlanar.CachedData.power4_r1_9 line 1056
lemma OAI.SharpPlanar.CachedData.power4_r1_9_eq line 1057
def OAI.SharpPlanar.CachedData.power4_r1_10 line 1058
lemma OAI.SharpPlanar.CachedData.power4_r1_10_eq line 1059
def OAI.SharpPlanar.CachedData.power4_r1_11 line 1060
lemma OAI.SharpPlanar.CachedData.power4_r1_11_eq line 1061
def OAI.SharpPlanar.CachedData.power4_r1_12 line 1062
lemma OAI.SharpPlanar.CachedData.power4_r1_12_eq line 1063
def OAI.SharpPlanar.CachedData.power4_r1_13 line 1064
lemma OAI.SharpPlanar.CachedData.power4_r1_13_eq line 1065
def OAI.SharpPlanar.CachedData.power4_r1_14 line 1066
lemma OAI.SharpPlanar.CachedData.power4_r1_14_eq line 1067
def OAI.SharpPlanar.CachedData.power4_r1_15 line 1068
lemma OAI.SharpPlanar.CachedData.power4_r1_15_eq line 1069
def OAI.SharpPlanar.CachedData.power4_r1 line 1070
lemma OAI.SharpPlanar.CachedData.power4_r1_eq line 1071
def OAI.SharpPlanar.CachedData.power4_r2_0 line 1089
lemma OAI.SharpPlanar.CachedData.power4_r2_0_eq line 1090
def OAI.SharpPlanar.CachedData.power4_r2_1 line 1091
lemma OAI.SharpPlanar.CachedData.power4_r2_1_eq line 1092
def OAI.SharpPlanar.CachedData.power4_r2_2 line 1093
lemma OAI.SharpPlanar.CachedData.power4_r2_2_eq line 1094
def OAI.SharpPlanar.CachedData.power4_r2_3 line 1095
lemma OAI.SharpPlanar.CachedData.power4_r2_3_eq line 1096
def OAI.SharpPlanar.CachedData.power4_r2_4 line 1097
lemma OAI.SharpPlanar.CachedData.power4_r2_4_eq line 1098
def OAI.SharpPlanar.CachedData.power4_r2_5 line 1099
lemma OAI.SharpPlanar.CachedData.power4_r2_5_eq line 1100
def OAI.SharpPlanar.CachedData.power4_r2_6 line 1101
lemma OAI.SharpPlanar.CachedData.power4_r2_6_eq line 1102
def OAI.SharpPlanar.CachedData.power4_r2_7 line 1103
lemma OAI.SharpPlanar.CachedData.power4_r2_7_eq line 1104
def OAI.SharpPlanar.CachedData.power4_r2_8 line 1105
lemma OAI.SharpPlanar.CachedData.power4_r2_8_eq line 1106
def OAI.SharpPlanar.CachedData.power4_r2_9 line 1107
lemma OAI.SharpPlanar.CachedData.power4_r2_9_eq line 1108
def OAI.SharpPlanar.CachedData.power4_r2_10 line 1109
lemma OAI.SharpPlanar.CachedData.power4_r2_10_eq line 1110
def OAI.SharpPlanar.CachedData.power4_r2_11 line 1111
lemma OAI.SharpPlanar.CachedData.power4_r2_11_eq line 1112
def OAI.SharpPlanar.CachedData.power4_r2_12 line 1113
lemma OAI.SharpPlanar.CachedData.power4_r2_12_eq line 1114
def OAI.SharpPlanar.CachedData.power4_r2_13 line 1115
lemma OAI.SharpPlanar.CachedData.power4_r2_13_eq line 1116
def OAI.SharpPlanar.CachedData.power4_r2_14 line 1117
lemma OAI.SharpPlanar.CachedData.power4_r2_14_eq line 1118
def OAI.SharpPlanar.CachedData.power4_r2_15 line 1119
lemma OAI.SharpPlanar.CachedData.power4_r2_15_eq line 1120
def OAI.SharpPlanar.CachedData.power4_r2 line 1121
lemma OAI.SharpPlanar.CachedData.power4_r2_eq line 1122
def OAI.SharpPlanar.CachedData.power4_r3_0 line 1140
lemma OAI.SharpPlanar.CachedData.power4_r3_0_eq line 1141
def OAI.SharpPlanar.CachedData.power4_r3_1 line 1142
lemma OAI.SharpPlanar.CachedData.power4_r3_1_eq line 1143
def OAI.SharpPlanar.CachedData.power4_r3_2 line 1144
lemma OAI.SharpPlanar.CachedData.power4_r3_2_eq line 1145
def OAI.SharpPlanar.CachedData.power4_r3_3 line 1146
lemma OAI.SharpPlanar.CachedData.power4_r3_3_eq line 1147
def OAI.SharpPlanar.CachedData.power4_r3_4 line 1148
lemma OAI.SharpPlanar.CachedData.power4_r3_4_eq line 1149
def OAI.SharpPlanar.CachedData.power4_r3_5 line 1150
lemma OAI.SharpPlanar.CachedData.power4_r3_5_eq line 1151
def OAI.SharpPlanar.CachedData.power4_r3_6 line 1152
lemma OAI.SharpPlanar.CachedData.power4_r3_6_eq line 1153
def OAI.SharpPlanar.CachedData.power4_r3_7 line 1154
lemma OAI.SharpPlanar.CachedData.power4_r3_7_eq line 1155
def OAI.SharpPlanar.CachedData.power4_r3_8 line 1156
lemma OAI.SharpPlanar.CachedData.power4_r3_8_eq line 1157
def OAI.SharpPlanar.CachedData.power4_r3_9 line 1158
lemma OAI.SharpPlanar.CachedData.power4_r3_9_eq line 1159
def OAI.SharpPlanar.CachedData.power4_r3_10 line 1160
lemma OAI.SharpPlanar.CachedData.power4_r3_10_eq line 1161
def OAI.SharpPlanar.CachedData.power4_r3_11 line 1162
lemma OAI.SharpPlanar.CachedData.power4_r3_11_eq line 1163
def OAI.SharpPlanar.CachedData.power4_r3_12 line 1164
lemma OAI.SharpPlanar.CachedData.power4_r3_12_eq line 1165
def OAI.SharpPlanar.CachedData.power4_r3_13 line 1166
lemma OAI.SharpPlanar.CachedData.power4_r3_13_eq line 1167
def OAI.SharpPlanar.CachedData.power4_r3_14 line 1168
lemma OAI.SharpPlanar.CachedData.power4_r3_14_eq line 1169
def OAI.SharpPlanar.CachedData.power4_r3_15 line 1170
lemma OAI.SharpPlanar.CachedData.power4_r3_15_eq line 1171
def OAI.SharpPlanar.CachedData.power4_r3 line 1172
lemma OAI.SharpPlanar.CachedData.power4_r3_eq line 1173
def OAI.SharpPlanar.CachedData.power4_r4_0 line 1191
lemma OAI.SharpPlanar.CachedData.power4_r4_0_eq line 1192
def OAI.SharpPlanar.CachedData.power4_r4_1 line 1193
lemma OAI.SharpPlanar.CachedData.power4_r4_1_eq line 1194
def OAI.SharpPlanar.CachedData.power4_r4_2 line 1195
lemma OAI.SharpPlanar.CachedData.power4_r4_2_eq line 1196
def OAI.SharpPlanar.CachedData.power4_r4_3 line 1197
lemma OAI.SharpPlanar.CachedData.power4_r4_3_eq line 1198
def OAI.SharpPlanar.CachedData.power4_r4_4 line 1199
lemma OAI.SharpPlanar.CachedData.power4_r4_4_eq line 1200
def OAI.SharpPlanar.CachedData.power4_r4_5 line 1201
lemma OAI.SharpPlanar.CachedData.power4_r4_5_eq line 1202
def OAI.SharpPlanar.CachedData.power4_r4_6 line 1203
lemma OAI.SharpPlanar.CachedData.power4_r4_6_eq line 1204
def OAI.SharpPlanar.CachedData.power4_r4_7 line 1205
lemma OAI.SharpPlanar.CachedData.power4_r4_7_eq line 1206
def OAI.SharpPlanar.CachedData.power4_r4_8 line 1207
lemma OAI.SharpPlanar.CachedData.power4_r4_8_eq line 1208
def OAI.SharpPlanar.CachedData.power4_r4_9 line 1209
lemma OAI.SharpPlanar.CachedData.power4_r4_9_eq line 1210
def OAI.SharpPlanar.CachedData.power4_r4_10 line 1211
lemma OAI.SharpPlanar.CachedData.power4_r4_10_eq line 1212
def OAI.SharpPlanar.CachedData.power4_r4_11 line 1213
lemma OAI.SharpPlanar.CachedData.power4_r4_11_eq line 1214
def OAI.SharpPlanar.CachedData.power4_r4_12 line 1215
lemma OAI.SharpPlanar.CachedData.power4_r4_12_eq line 1216
def OAI.SharpPlanar.CachedData.power4_r4_13 line 1217
lemma OAI.SharpPlanar.CachedData.power4_r4_13_eq line 1218
def OAI.SharpPlanar.CachedData.power4_r4_14 line 1219
lemma OAI.SharpPlanar.CachedData.power4_r4_14_eq line 1220
def OAI.SharpPlanar.CachedData.power4_r4_15 line 1221
lemma OAI.SharpPlanar.CachedData.power4_r4_15_eq line 1222
def OAI.SharpPlanar.CachedData.power4_r4 line 1223
lemma OAI.SharpPlanar.CachedData.power4_r4_eq line 1224
def OAI.SharpPlanar.CachedData.power4_r5_0 line 1242
lemma OAI.SharpPlanar.CachedData.power4_r5_0_eq line 1243
def OAI.SharpPlanar.CachedData.power4_r5_1 line 1244
lemma OAI.SharpPlanar.CachedData.power4_r5_1_eq line 1245
def OAI.SharpPlanar.CachedData.power4_r5_2 line 1246
lemma OAI.SharpPlanar.CachedData.power4_r5_2_eq line 1247
def OAI.SharpPlanar.CachedData.power4_r5_3 line 1248
lemma OAI.SharpPlanar.CachedData.power4_r5_3_eq line 1249
def OAI.SharpPlanar.CachedData.power4_r5_4 line 1250
lemma OAI.SharpPlanar.CachedData.power4_r5_4_eq line 1251
def OAI.SharpPlanar.CachedData.power4_r5_5 line 1252
lemma OAI.SharpPlanar.CachedData.power4_r5_5_eq line 1253
def OAI.SharpPlanar.CachedData.power4_r5_6 line 1254
lemma OAI.SharpPlanar.CachedData.power4_r5_6_eq line 1255
def OAI.SharpPlanar.CachedData.power4_r5_7 line 1256
lemma OAI.SharpPlanar.CachedData.power4_r5_7_eq line 1257
def OAI.SharpPlanar.CachedData.power4_r5_8 line 1258
lemma OAI.SharpPlanar.CachedData.power4_r5_8_eq line 1259
def OAI.SharpPlanar.CachedData.power4_r5_9 line 1260
lemma OAI.SharpPlanar.CachedData.power4_r5_9_eq line 1261
def OAI.SharpPlanar.CachedData.power4_r5_10 line 1262
lemma OAI.SharpPlanar.CachedData.power4_r5_10_eq line 1263
def OAI.SharpPlanar.CachedData.power4_r5_11 line 1264
lemma OAI.SharpPlanar.CachedData.power4_r5_11_eq line 1265
def OAI.SharpPlanar.CachedData.power4_r5_12 line 1266
lemma OAI.SharpPlanar.CachedData.power4_r5_12_eq line 1267
def OAI.SharpPlanar.CachedData.power4_r5_13 line 1268
lemma OAI.SharpPlanar.CachedData.power4_r5_13_eq line 1269
def OAI.SharpPlanar.CachedData.power4_r5_14 line 1270
lemma OAI.SharpPlanar.CachedData.power4_r5_14_eq line 1271
def OAI.SharpPlanar.CachedData.power4_r5_15 line 1272
lemma OAI.SharpPlanar.CachedData.power4_r5_15_eq line 1273
def OAI.SharpPlanar.CachedData.power4_r5 line 1274
lemma OAI.SharpPlanar.CachedData.power4_r5_eq line 1275
def OAI.SharpPlanar.CachedData.power4 line 1293
lemma OAI.SharpPlanar.CachedData.power4_eq line 1294
lemma OAI.SharpPlanar.CachedData.power4_contains line 1302
def OAI.SharpPlanar.CachedData.power5Expr line 1308
def OAI.SharpPlanar.CachedData.power5_r0_0 line 1309
lemma OAI.SharpPlanar.CachedData.power5_r0_0_eq line 1310
def OAI.SharpPlanar.CachedData.power5_r0_1 line 1311
lemma OAI.SharpPlanar.CachedData.power5_r0_1_eq line 1312
def OAI.SharpPlanar.CachedData.power5_r0_2 line 1313
lemma OAI.SharpPlanar.CachedData.power5_r0_2_eq line 1314
def OAI.SharpPlanar.CachedData.power5_r0_3 line 1315
lemma OAI.SharpPlanar.CachedData.power5_r0_3_eq line 1316
def OAI.SharpPlanar.CachedData.power5_r0_4 line 1317
lemma OAI.SharpPlanar.CachedData.power5_r0_4_eq line 1318
def OAI.SharpPlanar.CachedData.power5_r0_5 line 1319
lemma OAI.SharpPlanar.CachedData.power5_r0_5_eq line 1320
def OAI.SharpPlanar.CachedData.power5_r0_6 line 1321
lemma OAI.SharpPlanar.CachedData.power5_r0_6_eq line 1322
def OAI.SharpPlanar.CachedData.power5_r0_7 line 1323
lemma OAI.SharpPlanar.CachedData.power5_r0_7_eq line 1324
def OAI.SharpPlanar.CachedData.power5_r0_8 line 1325
lemma OAI.SharpPlanar.CachedData.power5_r0_8_eq line 1326
def OAI.SharpPlanar.CachedData.power5_r0_9 line 1327
lemma OAI.SharpPlanar.CachedData.power5_r0_9_eq line 1328
def OAI.SharpPlanar.CachedData.power5_r0_10 line 1329
lemma OAI.SharpPlanar.CachedData.power5_r0_10_eq line 1330
def OAI.SharpPlanar.CachedData.power5_r0_11 line 1331
lemma OAI.SharpPlanar.CachedData.power5_r0_11_eq line 1332
def OAI.SharpPlanar.CachedData.power5_r0_12 line 1333
lemma OAI.SharpPlanar.CachedData.power5_r0_12_eq line 1334
def OAI.SharpPlanar.CachedData.power5_r0_13 line 1335
lemma OAI.SharpPlanar.CachedData.power5_r0_13_eq line 1336
def OAI.SharpPlanar.CachedData.power5_r0_14 line 1337
lemma OAI.SharpPlanar.CachedData.power5_r0_14_eq line 1338
def OAI.SharpPlanar.CachedData.power5_r0_15 line 1339
lemma OAI.SharpPlanar.CachedData.power5_r0_15_eq line 1340
def OAI.SharpPlanar.CachedData.power5_r0 line 1341
lemma OAI.SharpPlanar.CachedData.power5_r0_eq line 1342
def OAI.SharpPlanar.CachedData.power5_r1_0 line 1360
lemma OAI.SharpPlanar.CachedData.power5_r1_0_eq line 1361
def OAI.SharpPlanar.CachedData.power5_r1_1 line 1362
lemma OAI.SharpPlanar.CachedData.power5_r1_1_eq line 1363
def OAI.SharpPlanar.CachedData.power5_r1_2 line 1364
lemma OAI.SharpPlanar.CachedData.power5_r1_2_eq line 1365
def OAI.SharpPlanar.CachedData.power5_r1_3 line 1366
lemma OAI.SharpPlanar.CachedData.power5_r1_3_eq line 1367
def OAI.SharpPlanar.CachedData.power5_r1_4 line 1368
lemma OAI.SharpPlanar.CachedData.power5_r1_4_eq line 1369
def OAI.SharpPlanar.CachedData.power5_r1_5 line 1370
lemma OAI.SharpPlanar.CachedData.power5_r1_5_eq line 1371
def OAI.SharpPlanar.CachedData.power5_r1_6 line 1372
lemma OAI.SharpPlanar.CachedData.power5_r1_6_eq line 1373
def OAI.SharpPlanar.CachedData.power5_r1_7 line 1374
lemma OAI.SharpPlanar.CachedData.power5_r1_7_eq line 1375
def OAI.SharpPlanar.CachedData.power5_r1_8 line 1376
lemma OAI.SharpPlanar.CachedData.power5_r1_8_eq line 1377
def OAI.SharpPlanar.CachedData.power5_r1_9 line 1378
lemma OAI.SharpPlanar.CachedData.power5_r1_9_eq line 1379
def OAI.SharpPlanar.CachedData.power5_r1_10 line 1380
lemma OAI.SharpPlanar.CachedData.power5_r1_10_eq line 1381
def OAI.SharpPlanar.CachedData.power5_r1_11 line 1382
lemma OAI.SharpPlanar.CachedData.power5_r1_11_eq line 1383
def OAI.SharpPlanar.CachedData.power5_r1_12 line 1384
lemma OAI.SharpPlanar.CachedData.power5_r1_12_eq line 1385
def OAI.SharpPlanar.CachedData.power5_r1_13 line 1386
lemma OAI.SharpPlanar.CachedData.power5_r1_13_eq line 1387
def OAI.SharpPlanar.CachedData.power5_r1_14 line 1388
lemma OAI.SharpPlanar.CachedData.power5_r1_14_eq line 1389
def OAI.SharpPlanar.CachedData.power5_r1_15 line 1390
lemma OAI.SharpPlanar.CachedData.power5_r1_15_eq line 1391
def OAI.SharpPlanar.CachedData.power5_r1 line 1392
lemma OAI.SharpPlanar.CachedData.power5_r1_eq line 1393
def OAI.SharpPlanar.CachedData.power5_r2_0 line 1411
lemma OAI.SharpPlanar.CachedData.power5_r2_0_eq line 1412
def OAI.SharpPlanar.CachedData.power5_r2_1 line 1413
lemma OAI.SharpPlanar.CachedData.power5_r2_1_eq line 1414
def OAI.SharpPlanar.CachedData.power5_r2_2 line 1415
lemma OAI.SharpPlanar.CachedData.power5_r2_2_eq line 1416
def OAI.SharpPlanar.CachedData.power5_r2_3 line 1417
lemma OAI.SharpPlanar.CachedData.power5_r2_3_eq line 1418
def OAI.SharpPlanar.CachedData.power5_r2_4 line 1419
lemma OAI.SharpPlanar.CachedData.power5_r2_4_eq line 1420
def OAI.SharpPlanar.CachedData.power5_r2_5 line 1421
lemma OAI.SharpPlanar.CachedData.power5_r2_5_eq line 1422
def OAI.SharpPlanar.CachedData.power5_r2_6 line 1423
lemma OAI.SharpPlanar.CachedData.power5_r2_6_eq line 1424
def OAI.SharpPlanar.CachedData.power5_r2_7 line 1425
lemma OAI.SharpPlanar.CachedData.power5_r2_7_eq line 1426
def OAI.SharpPlanar.CachedData.power5_r2_8 line 1427
lemma OAI.SharpPlanar.CachedData.power5_r2_8_eq line 1428
def OAI.SharpPlanar.CachedData.power5_r2_9 line 1429
lemma OAI.SharpPlanar.CachedData.power5_r2_9_eq line 1430
def OAI.SharpPlanar.CachedData.power5_r2_10 line 1431
lemma OAI.SharpPlanar.CachedData.power5_r2_10_eq line 1432
def OAI.SharpPlanar.CachedData.power5_r2_11 line 1433
lemma OAI.SharpPlanar.CachedData.power5_r2_11_eq line 1434
def OAI.SharpPlanar.CachedData.power5_r2_12 line 1435
lemma OAI.SharpPlanar.CachedData.power5_r2_12_eq line 1436
def OAI.SharpPlanar.CachedData.power5_r2_13 line 1437
lemma OAI.SharpPlanar.CachedData.power5_r2_13_eq line 1438
def OAI.SharpPlanar.CachedData.power5_r2_14 line 1439
lemma OAI.SharpPlanar.CachedData.power5_r2_14_eq line 1440
def OAI.SharpPlanar.CachedData.power5_r2_15 line 1441
lemma OAI.SharpPlanar.CachedData.power5_r2_15_eq line 1442
def OAI.SharpPlanar.CachedData.power5_r2 line 1443
lemma OAI.SharpPlanar.CachedData.power5_r2_eq line 1444
def OAI.SharpPlanar.CachedData.power5_r3_0 line 1462
lemma OAI.SharpPlanar.CachedData.power5_r3_0_eq line 1463
def OAI.SharpPlanar.CachedData.power5_r3_1 line 1464
lemma OAI.SharpPlanar.CachedData.power5_r3_1_eq line 1465
def OAI.SharpPlanar.CachedData.power5_r3_2 line 1466
lemma OAI.SharpPlanar.CachedData.power5_r3_2_eq line 1467
def OAI.SharpPlanar.CachedData.power5_r3_3 line 1468
lemma OAI.SharpPlanar.CachedData.power5_r3_3_eq line 1469
def OAI.SharpPlanar.CachedData.power5_r3_4 line 1470
lemma OAI.SharpPlanar.CachedData.power5_r3_4_eq line 1471
def OAI.SharpPlanar.CachedData.power5_r3_5 line 1472
lemma OAI.SharpPlanar.CachedData.power5_r3_5_eq line 1473
def OAI.SharpPlanar.CachedData.power5_r3_6 line 1474
lemma OAI.SharpPlanar.CachedData.power5_r3_6_eq line 1475
def OAI.SharpPlanar.CachedData.power5_r3_7 line 1476
lemma OAI.SharpPlanar.CachedData.power5_r3_7_eq line 1477
def OAI.SharpPlanar.CachedData.power5_r3_8 line 1478
lemma OAI.SharpPlanar.CachedData.power5_r3_8_eq line 1479
def OAI.SharpPlanar.CachedData.power5_r3_9 line 1480
lemma OAI.SharpPlanar.CachedData.power5_r3_9_eq line 1481
def OAI.SharpPlanar.CachedData.power5_r3_10 line 1482
lemma OAI.SharpPlanar.CachedData.power5_r3_10_eq line 1483
def OAI.SharpPlanar.CachedData.power5_r3_11 line 1484
lemma OAI.SharpPlanar.CachedData.power5_r3_11_eq line 1485
def OAI.SharpPlanar.CachedData.power5_r3_12 line 1486
lemma OAI.SharpPlanar.CachedData.power5_r3_12_eq line 1487
def OAI.SharpPlanar.CachedData.power5_r3_13 line 1488
lemma OAI.SharpPlanar.CachedData.power5_r3_13_eq line 1489
def OAI.SharpPlanar.CachedData.power5_r3_14 line 1490
lemma OAI.SharpPlanar.CachedData.power5_r3_14_eq line 1491
def OAI.SharpPlanar.CachedData.power5_r3_15 line 1492
lemma OAI.SharpPlanar.CachedData.power5_r3_15_eq line 1493
def OAI.SharpPlanar.CachedData.power5_r3 line 1494
lemma OAI.SharpPlanar.CachedData.power5_r3_eq line 1495
def OAI.SharpPlanar.CachedData.power5_r4_0 line 1513
lemma OAI.SharpPlanar.CachedData.power5_r4_0_eq line 1514
def OAI.SharpPlanar.CachedData.power5_r4_1 line 1515
lemma OAI.SharpPlanar.CachedData.power5_r4_1_eq line 1516
def OAI.SharpPlanar.CachedData.power5_r4_2 line 1517
lemma OAI.SharpPlanar.CachedData.power5_r4_2_eq line 1518
def OAI.SharpPlanar.CachedData.power5_r4_3 line 1519
lemma OAI.SharpPlanar.CachedData.power5_r4_3_eq line 1520
def OAI.SharpPlanar.CachedData.power5_r4_4 line 1521
lemma OAI.SharpPlanar.CachedData.power5_r4_4_eq line 1522
def OAI.SharpPlanar.CachedData.power5_r4_5 line 1523
lemma OAI.SharpPlanar.CachedData.power5_r4_5_eq line 1524
def OAI.SharpPlanar.CachedData.power5_r4_6 line 1525
lemma OAI.SharpPlanar.CachedData.power5_r4_6_eq line 1526
def OAI.SharpPlanar.CachedData.power5_r4_7 line 1527
lemma OAI.SharpPlanar.CachedData.power5_r4_7_eq line 1528
def OAI.SharpPlanar.CachedData.power5_r4_8 line 1529
lemma OAI.SharpPlanar.CachedData.power5_r4_8_eq line 1530
def OAI.SharpPlanar.CachedData.power5_r4_9 line 1531
lemma OAI.SharpPlanar.CachedData.power5_r4_9_eq line 1532
def OAI.SharpPlanar.CachedData.power5_r4_10 line 1533
lemma OAI.SharpPlanar.CachedData.power5_r4_10_eq line 1534
def OAI.SharpPlanar.CachedData.power5_r4_11 line 1535
lemma OAI.SharpPlanar.CachedData.power5_r4_11_eq line 1536
def OAI.SharpPlanar.CachedData.power5_r4_12 line 1537
lemma OAI.SharpPlanar.CachedData.power5_r4_12_eq line 1538
def OAI.SharpPlanar.CachedData.power5_r4_13 line 1539
lemma OAI.SharpPlanar.CachedData.power5_r4_13_eq line 1540
def OAI.SharpPlanar.CachedData.power5_r4_14 line 1541
lemma OAI.SharpPlanar.CachedData.power5_r4_14_eq line 1542
def OAI.SharpPlanar.CachedData.power5_r4_15 line 1543
lemma OAI.SharpPlanar.CachedData.power5_r4_15_eq line 1544
def OAI.SharpPlanar.CachedData.power5_r4 line 1545
lemma OAI.SharpPlanar.CachedData.power5_r4_eq line 1546
def OAI.SharpPlanar.CachedData.power5_r5_0 line 1564
lemma OAI.SharpPlanar.CachedData.power5_r5_0_eq line 1565
def OAI.SharpPlanar.CachedData.power5_r5_1 line 1566
lemma OAI.SharpPlanar.CachedData.power5_r5_1_eq line 1567
def OAI.SharpPlanar.CachedData.power5_r5_2 line 1568
lemma OAI.SharpPlanar.CachedData.power5_r5_2_eq line 1569
def OAI.SharpPlanar.CachedData.power5_r5_3 line 1570
lemma OAI.SharpPlanar.CachedData.power5_r5_3_eq line 1571
def OAI.SharpPlanar.CachedData.power5_r5_4 line 1572
lemma OAI.SharpPlanar.CachedData.power5_r5_4_eq line 1573
def OAI.SharpPlanar.CachedData.power5_r5_5 line 1574
lemma OAI.SharpPlanar.CachedData.power5_r5_5_eq line 1575
def OAI.SharpPlanar.CachedData.power5_r5_6 line 1576
lemma OAI.SharpPlanar.CachedData.power5_r5_6_eq line 1577
def OAI.SharpPlanar.CachedData.power5_r5_7 line 1578
lemma OAI.SharpPlanar.CachedData.power5_r5_7_eq line 1579
def OAI.SharpPlanar.CachedData.power5_r5_8 line 1580
lemma OAI.SharpPlanar.CachedData.power5_r5_8_eq line 1581
def OAI.SharpPlanar.CachedData.power5_r5_9 line 1582
lemma OAI.SharpPlanar.CachedData.power5_r5_9_eq line 1583
def OAI.SharpPlanar.CachedData.power5_r5_10 line 1584
lemma OAI.SharpPlanar.CachedData.power5_r5_10_eq line 1585
def OAI.SharpPlanar.CachedData.power5_r5_11 line 1586
lemma OAI.SharpPlanar.CachedData.power5_r5_11_eq line 1587
def OAI.SharpPlanar.CachedData.power5_r5_12 line 1588
lemma OAI.SharpPlanar.CachedData.power5_r5_12_eq line 1589
def OAI.SharpPlanar.CachedData.power5_r5_13 line 1590
lemma OAI.SharpPlanar.CachedData.power5_r5_13_eq line 1591
def OAI.SharpPlanar.CachedData.power5_r5_14 line 1592
lemma OAI.SharpPlanar.CachedData.power5_r5_14_eq line 1593
def OAI.SharpPlanar.CachedData.power5_r5_15 line 1594
lemma OAI.SharpPlanar.CachedData.power5_r5_15_eq line 1595
def OAI.SharpPlanar.CachedData.power5_r5 line 1596
lemma OAI.SharpPlanar.CachedData.power5_r5_eq line 1597
def OAI.SharpPlanar.CachedData.power5 line 1615
lemma OAI.SharpPlanar.CachedData.power5_eq line 1616
lemma OAI.SharpPlanar.CachedData.power5_contains line 1624
def OAI.SharpPlanar.CachedData.power6Expr line 1630
def OAI.SharpPlanar.CachedData.power6_r0_0 line 1631
lemma OAI.SharpPlanar.CachedData.power6_r0_0_eq line 1632
def OAI.SharpPlanar.CachedData.power6_r0_1 line 1633
lemma OAI.SharpPlanar.CachedData.power6_r0_1_eq line 1634
def OAI.SharpPlanar.CachedData.power6_r0_2 line 1635
lemma OAI.SharpPlanar.CachedData.power6_r0_2_eq line 1636
def OAI.SharpPlanar.CachedData.power6_r0_3 line 1637
lemma OAI.SharpPlanar.CachedData.power6_r0_3_eq line 1638
def OAI.SharpPlanar.CachedData.power6_r0_4 line 1639
lemma OAI.SharpPlanar.CachedData.power6_r0_4_eq line 1640
def OAI.SharpPlanar.CachedData.power6_r0_5 line 1641
lemma OAI.SharpPlanar.CachedData.power6_r0_5_eq line 1642
def OAI.SharpPlanar.CachedData.power6_r0_6 line 1643
lemma OAI.SharpPlanar.CachedData.power6_r0_6_eq line 1644
def OAI.SharpPlanar.CachedData.power6_r0_7 line 1645
lemma OAI.SharpPlanar.CachedData.power6_r0_7_eq line 1646
def OAI.SharpPlanar.CachedData.power6_r0_8 line 1647
lemma OAI.SharpPlanar.CachedData.power6_r0_8_eq line 1648
def OAI.SharpPlanar.CachedData.power6_r0_9 line 1649
lemma OAI.SharpPlanar.CachedData.power6_r0_9_eq line 1650
def OAI.SharpPlanar.CachedData.power6_r0_10 line 1651
lemma OAI.SharpPlanar.CachedData.power6_r0_10_eq line 1652
def OAI.SharpPlanar.CachedData.power6_r0_11 line 1653
lemma OAI.SharpPlanar.CachedData.power6_r0_11_eq line 1654
def OAI.SharpPlanar.CachedData.power6_r0_12 line 1655
lemma OAI.SharpPlanar.CachedData.power6_r0_12_eq line 1656
def OAI.SharpPlanar.CachedData.power6_r0_13 line 1657
lemma OAI.SharpPlanar.CachedData.power6_r0_13_eq line 1658
def OAI.SharpPlanar.CachedData.power6_r0_14 line 1659
lemma OAI.SharpPlanar.CachedData.power6_r0_14_eq line 1660
def OAI.SharpPlanar.CachedData.power6_r0_15 line 1661
lemma OAI.SharpPlanar.CachedData.power6_r0_15_eq line 1662
def OAI.SharpPlanar.CachedData.power6_r0 line 1663
lemma OAI.SharpPlanar.CachedData.power6_r0_eq line 1664
def OAI.SharpPlanar.CachedData.power6_r1_0 line 1682
lemma OAI.SharpPlanar.CachedData.power6_r1_0_eq line 1683
def OAI.SharpPlanar.CachedData.power6_r1_1 line 1684
lemma OAI.SharpPlanar.CachedData.power6_r1_1_eq line 1685
def OAI.SharpPlanar.CachedData.power6_r1_2 line 1686
lemma OAI.SharpPlanar.CachedData.power6_r1_2_eq line 1687
def OAI.SharpPlanar.CachedData.power6_r1_3 line 1688
lemma OAI.SharpPlanar.CachedData.power6_r1_3_eq line 1689
def OAI.SharpPlanar.CachedData.power6_r1_4 line 1690
lemma OAI.SharpPlanar.CachedData.power6_r1_4_eq line 1691
def OAI.SharpPlanar.CachedData.power6_r1_5 line 1692
lemma OAI.SharpPlanar.CachedData.power6_r1_5_eq line 1693
def OAI.SharpPlanar.CachedData.power6_r1_6 line 1694
lemma OAI.SharpPlanar.CachedData.power6_r1_6_eq line 1695
def OAI.SharpPlanar.CachedData.power6_r1_7 line 1696
lemma OAI.SharpPlanar.CachedData.power6_r1_7_eq line 1697
def OAI.SharpPlanar.CachedData.power6_r1_8 line 1698
lemma OAI.SharpPlanar.CachedData.power6_r1_8_eq line 1699
def OAI.SharpPlanar.CachedData.power6_r1_9 line 1700
lemma OAI.SharpPlanar.CachedData.power6_r1_9_eq line 1701
def OAI.SharpPlanar.CachedData.power6_r1_10 line 1702
lemma OAI.SharpPlanar.CachedData.power6_r1_10_eq line 1703
def OAI.SharpPlanar.CachedData.power6_r1_11 line 1704
lemma OAI.SharpPlanar.CachedData.power6_r1_11_eq line 1705
def OAI.SharpPlanar.CachedData.power6_r1_12 line 1706
lemma OAI.SharpPlanar.CachedData.power6_r1_12_eq line 1707
def OAI.SharpPlanar.CachedData.power6_r1_13 line 1708
lemma OAI.SharpPlanar.CachedData.power6_r1_13_eq line 1709
def OAI.SharpPlanar.CachedData.power6_r1_14 line 1710
lemma OAI.SharpPlanar.CachedData.power6_r1_14_eq line 1711
def OAI.SharpPlanar.CachedData.power6_r1_15 line 1712
lemma OAI.SharpPlanar.CachedData.power6_r1_15_eq line 1713
def OAI.SharpPlanar.CachedData.power6_r1 line 1714
lemma OAI.SharpPlanar.CachedData.power6_r1_eq line 1715
def OAI.SharpPlanar.CachedData.power6_r2_0 line 1733
lemma OAI.SharpPlanar.CachedData.power6_r2_0_eq line 1734
def OAI.SharpPlanar.CachedData.power6_r2_1 line 1735
lemma OAI.SharpPlanar.CachedData.power6_r2_1_eq line 1736
def OAI.SharpPlanar.CachedData.power6_r2_2 line 1737
lemma OAI.SharpPlanar.CachedData.power6_r2_2_eq line 1738
def OAI.SharpPlanar.CachedData.power6_r2_3 line 1739
lemma OAI.SharpPlanar.CachedData.power6_r2_3_eq line 1740
def OAI.SharpPlanar.CachedData.power6_r2_4 line 1741
lemma OAI.SharpPlanar.CachedData.power6_r2_4_eq line 1742
def OAI.SharpPlanar.CachedData.power6_r2_5 line 1743
lemma OAI.SharpPlanar.CachedData.power6_r2_5_eq line 1744
def OAI.SharpPlanar.CachedData.power6_r2_6 line 1745
lemma OAI.SharpPlanar.CachedData.power6_r2_6_eq line 1746
def OAI.SharpPlanar.CachedData.power6_r2_7 line 1747
lemma OAI.SharpPlanar.CachedData.power6_r2_7_eq line 1748
def OAI.SharpPlanar.CachedData.power6_r2_8 line 1749
lemma OAI.SharpPlanar.CachedData.power6_r2_8_eq line 1750
def OAI.SharpPlanar.CachedData.power6_r2_9 line 1751
lemma OAI.SharpPlanar.CachedData.power6_r2_9_eq line 1752
def OAI.SharpPlanar.CachedData.power6_r2_10 line 1753
lemma OAI.SharpPlanar.CachedData.power6_r2_10_eq line 1754
def OAI.SharpPlanar.CachedData.power6_r2_11 line 1755
lemma OAI.SharpPlanar.CachedData.power6_r2_11_eq line 1756
def OAI.SharpPlanar.CachedData.power6_r2_12 line 1757
lemma OAI.SharpPlanar.CachedData.power6_r2_12_eq line 1758
def OAI.SharpPlanar.CachedData.power6_r2_13 line 1759
lemma OAI.SharpPlanar.CachedData.power6_r2_13_eq line 1760
def OAI.SharpPlanar.CachedData.power6_r2_14 line 1761
lemma OAI.SharpPlanar.CachedData.power6_r2_14_eq line 1762
def OAI.SharpPlanar.CachedData.power6_r2_15 line 1763
lemma OAI.SharpPlanar.CachedData.power6_r2_15_eq line 1764
def OAI.SharpPlanar.CachedData.power6_r2 line 1765
lemma OAI.SharpPlanar.CachedData.power6_r2_eq line 1766
def OAI.SharpPlanar.CachedData.power6_r3_0 line 1784
lemma OAI.SharpPlanar.CachedData.power6_r3_0_eq line 1785
def OAI.SharpPlanar.CachedData.power6_r3_1 line 1786
lemma OAI.SharpPlanar.CachedData.power6_r3_1_eq line 1787
def OAI.SharpPlanar.CachedData.power6_r3_2 line 1788
lemma OAI.SharpPlanar.CachedData.power6_r3_2_eq line 1789
def OAI.SharpPlanar.CachedData.power6_r3_3 line 1790
lemma OAI.SharpPlanar.CachedData.power6_r3_3_eq line 1791
def OAI.SharpPlanar.CachedData.power6_r3_4 line 1792
lemma OAI.SharpPlanar.CachedData.power6_r3_4_eq line 1793
def OAI.SharpPlanar.CachedData.power6_r3_5 line 1794
lemma OAI.SharpPlanar.CachedData.power6_r3_5_eq line 1795
def OAI.SharpPlanar.CachedData.power6_r3_6 line 1796
lemma OAI.SharpPlanar.CachedData.power6_r3_6_eq line 1797
def OAI.SharpPlanar.CachedData.power6_r3_7 line 1798
lemma OAI.SharpPlanar.CachedData.power6_r3_7_eq line 1799
def OAI.SharpPlanar.CachedData.power6_r3_8 line 1800
lemma OAI.SharpPlanar.CachedData.power6_r3_8_eq line 1801
def OAI.SharpPlanar.CachedData.power6_r3_9 line 1802
lemma OAI.SharpPlanar.CachedData.power6_r3_9_eq line 1803
def OAI.SharpPlanar.CachedData.power6_r3_10 line 1804
lemma OAI.SharpPlanar.CachedData.power6_r3_10_eq line 1805
def OAI.SharpPlanar.CachedData.power6_r3_11 line 1806
lemma OAI.SharpPlanar.CachedData.power6_r3_11_eq line 1807
def OAI.SharpPlanar.CachedData.power6_r3_12 line 1808
lemma OAI.SharpPlanar.CachedData.power6_r3_12_eq line 1809
def OAI.SharpPlanar.CachedData.power6_r3_13 line 1810
lemma OAI.SharpPlanar.CachedData.power6_r3_13_eq line 1811
def OAI.SharpPlanar.CachedData.power6_r3_14 line 1812
lemma OAI.SharpPlanar.CachedData.power6_r3_14_eq line 1813
def OAI.SharpPlanar.CachedData.power6_r3_15 line 1814
lemma OAI.SharpPlanar.CachedData.power6_r3_15_eq line 1815
def OAI.SharpPlanar.CachedData.power6_r3 line 1816
lemma OAI.SharpPlanar.CachedData.power6_r3_eq line 1817
def OAI.SharpPlanar.CachedData.power6_r4_0 line 1835
lemma OAI.SharpPlanar.CachedData.power6_r4_0_eq line 1836
def OAI.SharpPlanar.CachedData.power6_r4_1 line 1837
lemma OAI.SharpPlanar.CachedData.power6_r4_1_eq line 1838
def OAI.SharpPlanar.CachedData.power6_r4_2 line 1839
lemma OAI.SharpPlanar.CachedData.power6_r4_2_eq line 1840
def OAI.SharpPlanar.CachedData.power6_r4_3 line 1841
lemma OAI.SharpPlanar.CachedData.power6_r4_3_eq line 1842
def OAI.SharpPlanar.CachedData.power6_r4_4 line 1843
lemma OAI.SharpPlanar.CachedData.power6_r4_4_eq line 1844
def OAI.SharpPlanar.CachedData.power6_r4_5 line 1845
lemma OAI.SharpPlanar.CachedData.power6_r4_5_eq line 1846
def OAI.SharpPlanar.CachedData.power6_r4_6 line 1847
lemma OAI.SharpPlanar.CachedData.power6_r4_6_eq line 1848
def OAI.SharpPlanar.CachedData.power6_r4_7 line 1849
lemma OAI.SharpPlanar.CachedData.power6_r4_7_eq line 1850
def OAI.SharpPlanar.CachedData.power6_r4_8 line 1851
lemma OAI.SharpPlanar.CachedData.power6_r4_8_eq line 1852
def OAI.SharpPlanar.CachedData.power6_r4_9 line 1853
lemma OAI.SharpPlanar.CachedData.power6_r4_9_eq line 1854
def OAI.SharpPlanar.CachedData.power6_r4_10 line 1855
lemma OAI.SharpPlanar.CachedData.power6_r4_10_eq line 1856
def OAI.SharpPlanar.CachedData.power6_r4_11 line 1857
lemma OAI.SharpPlanar.CachedData.power6_r4_11_eq line 1858
def OAI.SharpPlanar.CachedData.power6_r4_12 line 1859
lemma OAI.SharpPlanar.CachedData.power6_r4_12_eq line 1860
def OAI.SharpPlanar.CachedData.power6_r4_13 line 1861
lemma OAI.SharpPlanar.CachedData.power6_r4_13_eq line 1862
def OAI.SharpPlanar.CachedData.power6_r4_14 line 1863
lemma OAI.SharpPlanar.CachedData.power6_r4_14_eq line 1864
def OAI.SharpPlanar.CachedData.power6_r4_15 line 1865
lemma OAI.SharpPlanar.CachedData.power6_r4_15_eq line 1866
def OAI.SharpPlanar.CachedData.power6_r4 line 1867
lemma OAI.SharpPlanar.CachedData.power6_r4_eq line 1868
def OAI.SharpPlanar.CachedData.power6_r5_0 line 1886
lemma OAI.SharpPlanar.CachedData.power6_r5_0_eq line 1887
def OAI.SharpPlanar.CachedData.power6_r5_1 line 1888
lemma OAI.SharpPlanar.CachedData.power6_r5_1_eq line 1889
def OAI.SharpPlanar.CachedData.power6_r5_2 line 1890
lemma OAI.SharpPlanar.CachedData.power6_r5_2_eq line 1891
def OAI.SharpPlanar.CachedData.power6_r5_3 line 1892
lemma OAI.SharpPlanar.CachedData.power6_r5_3_eq line 1893
def OAI.SharpPlanar.CachedData.power6_r5_4 line 1894
lemma OAI.SharpPlanar.CachedData.power6_r5_4_eq line 1895
def OAI.SharpPlanar.CachedData.power6_r5_5 line 1896
lemma OAI.SharpPlanar.CachedData.power6_r5_5_eq line 1897
def OAI.SharpPlanar.CachedData.power6_r5_6 line 1898
lemma OAI.SharpPlanar.CachedData.power6_r5_6_eq line 1899
def OAI.SharpPlanar.CachedData.power6_r5_7 line 1900
lemma OAI.SharpPlanar.CachedData.power6_r5_7_eq line 1901
def OAI.SharpPlanar.CachedData.power6_r5_8 line 1902
lemma OAI.SharpPlanar.CachedData.power6_r5_8_eq line 1903
def OAI.SharpPlanar.CachedData.power6_r5_9 line 1904
lemma OAI.SharpPlanar.CachedData.power6_r5_9_eq line 1905
def OAI.SharpPlanar.CachedData.power6_r5_10 line 1906
lemma OAI.SharpPlanar.CachedData.power6_r5_10_eq line 1907
def OAI.SharpPlanar.CachedData.power6_r5_11 line 1908
lemma OAI.SharpPlanar.CachedData.power6_r5_11_eq line 1909
def OAI.SharpPlanar.CachedData.power6_r5_12 line 1910
lemma OAI.SharpPlanar.CachedData.power6_r5_12_eq line 1911
def OAI.SharpPlanar.CachedData.power6_r5_13 line 1912
lemma OAI.SharpPlanar.CachedData.power6_r5_13_eq line 1913
def OAI.SharpPlanar.CachedData.power6_r5_14 line 1914
lemma OAI.SharpPlanar.CachedData.power6_r5_14_eq line 1915
def OAI.SharpPlanar.CachedData.power6_r5_15 line 1916
lemma OAI.SharpPlanar.CachedData.power6_r5_15_eq line 1917
def OAI.SharpPlanar.CachedData.power6_r5 line 1918
lemma OAI.SharpPlanar.CachedData.power6_r5_eq line 1919
def OAI.SharpPlanar.CachedData.power6 line 1937
lemma OAI.SharpPlanar.CachedData.power6_eq line 1938
lemma OAI.SharpPlanar.CachedData.power6_contains line 1946
def OAI.SharpPlanar.CachedData.power7Expr line 1952
def OAI.SharpPlanar.CachedData.power7_r0_0 line 1953
lemma OAI.SharpPlanar.CachedData.power7_r0_0_eq line 1954
def OAI.SharpPlanar.CachedData.power7_r0_1 line 1955
lemma OAI.SharpPlanar.CachedData.power7_r0_1_eq line 1956
def OAI.SharpPlanar.CachedData.power7_r0_2 line 1957
lemma OAI.SharpPlanar.CachedData.power7_r0_2_eq line 1958
def OAI.SharpPlanar.CachedData.power7_r0_3 line 1959
lemma OAI.SharpPlanar.CachedData.power7_r0_3_eq line 1960
def OAI.SharpPlanar.CachedData.power7_r0_4 line 1961
lemma OAI.SharpPlanar.CachedData.power7_r0_4_eq line 1962
def OAI.SharpPlanar.CachedData.power7_r0_5 line 1963
lemma OAI.SharpPlanar.CachedData.power7_r0_5_eq line 1964
def OAI.SharpPlanar.CachedData.power7_r0_6 line 1965
lemma OAI.SharpPlanar.CachedData.power7_r0_6_eq line 1966
def OAI.SharpPlanar.CachedData.power7_r0_7 line 1967
lemma OAI.SharpPlanar.CachedData.power7_r0_7_eq line 1968
def OAI.SharpPlanar.CachedData.power7_r0_8 line 1969
lemma OAI.SharpPlanar.CachedData.power7_r0_8_eq line 1970
def OAI.SharpPlanar.CachedData.power7_r0_9 line 1971
lemma OAI.SharpPlanar.CachedData.power7_r0_9_eq line 1972
def OAI.SharpPlanar.CachedData.power7_r0_10 line 1973
lemma OAI.SharpPlanar.CachedData.power7_r0_10_eq line 1974
def OAI.SharpPlanar.CachedData.power7_r0_11 line 1975
lemma OAI.SharpPlanar.CachedData.power7_r0_11_eq line 1976
def OAI.SharpPlanar.CachedData.power7_r0_12 line 1977
lemma OAI.SharpPlanar.CachedData.power7_r0_12_eq line 1978
def OAI.SharpPlanar.CachedData.power7_r0_13 line 1979
lemma OAI.SharpPlanar.CachedData.power7_r0_13_eq line 1980
def OAI.SharpPlanar.CachedData.power7_r0_14 line 1981
lemma OAI.SharpPlanar.CachedData.power7_r0_14_eq line 1982
def OAI.SharpPlanar.CachedData.power7_r0_15 line 1983
lemma OAI.SharpPlanar.CachedData.power7_r0_15_eq line 1984
def OAI.SharpPlanar.CachedData.power7_r0 line 1985
lemma OAI.SharpPlanar.CachedData.power7_r0_eq line 1986
def OAI.SharpPlanar.CachedData.power7_r1_0 line 2004
lemma OAI.SharpPlanar.CachedData.power7_r1_0_eq line 2005
def OAI.SharpPlanar.CachedData.power7_r1_1 line 2006
lemma OAI.SharpPlanar.CachedData.power7_r1_1_eq line 2007
def OAI.SharpPlanar.CachedData.power7_r1_2 line 2008
lemma OAI.SharpPlanar.CachedData.power7_r1_2_eq line 2009
def OAI.SharpPlanar.CachedData.power7_r1_3 line 2010
lemma OAI.SharpPlanar.CachedData.power7_r1_3_eq line 2011
def OAI.SharpPlanar.CachedData.power7_r1_4 line 2012
lemma OAI.SharpPlanar.CachedData.power7_r1_4_eq line 2013
def OAI.SharpPlanar.CachedData.power7_r1_5 line 2014
lemma OAI.SharpPlanar.CachedData.power7_r1_5_eq line 2015
def OAI.SharpPlanar.CachedData.power7_r1_6 line 2016
lemma OAI.SharpPlanar.CachedData.power7_r1_6_eq line 2017
def OAI.SharpPlanar.CachedData.power7_r1_7 line 2018
lemma OAI.SharpPlanar.CachedData.power7_r1_7_eq line 2019
def OAI.SharpPlanar.CachedData.power7_r1_8 line 2020
lemma OAI.SharpPlanar.CachedData.power7_r1_8_eq line 2021
def OAI.SharpPlanar.CachedData.power7_r1_9 line 2022
lemma OAI.SharpPlanar.CachedData.power7_r1_9_eq line 2023
def OAI.SharpPlanar.CachedData.power7_r1_10 line 2024
lemma OAI.SharpPlanar.CachedData.power7_r1_10_eq line 2025
def OAI.SharpPlanar.CachedData.power7_r1_11 line 2026
lemma OAI.SharpPlanar.CachedData.power7_r1_11_eq line 2027
def OAI.SharpPlanar.CachedData.power7_r1_12 line 2028
lemma OAI.SharpPlanar.CachedData.power7_r1_12_eq line 2029
def OAI.SharpPlanar.CachedData.power7_r1_13 line 2030
lemma OAI.SharpPlanar.CachedData.power7_r1_13_eq line 2031
def OAI.SharpPlanar.CachedData.power7_r1_14 line 2032
lemma OAI.SharpPlanar.CachedData.power7_r1_14_eq line 2033
def OAI.SharpPlanar.CachedData.power7_r1_15 line 2034
lemma OAI.SharpPlanar.CachedData.power7_r1_15_eq line 2035
def OAI.SharpPlanar.CachedData.power7_r1 line 2036
lemma OAI.SharpPlanar.CachedData.power7_r1_eq line 2037
def OAI.SharpPlanar.CachedData.power7_r2_0 line 2055
lemma OAI.SharpPlanar.CachedData.power7_r2_0_eq line 2056
def OAI.SharpPlanar.CachedData.power7_r2_1 line 2057
lemma OAI.SharpPlanar.CachedData.power7_r2_1_eq line 2058
def OAI.SharpPlanar.CachedData.power7_r2_2 line 2059
lemma OAI.SharpPlanar.CachedData.power7_r2_2_eq line 2060
def OAI.SharpPlanar.CachedData.power7_r2_3 line 2061
lemma OAI.SharpPlanar.CachedData.power7_r2_3_eq line 2062
def OAI.SharpPlanar.CachedData.power7_r2_4 line 2063
lemma OAI.SharpPlanar.CachedData.power7_r2_4_eq line 2064
def OAI.SharpPlanar.CachedData.power7_r2_5 line 2065
lemma OAI.SharpPlanar.CachedData.power7_r2_5_eq line 2066
def OAI.SharpPlanar.CachedData.power7_r2_6 line 2067
lemma OAI.SharpPlanar.CachedData.power7_r2_6_eq line 2068
def OAI.SharpPlanar.CachedData.power7_r2_7 line 2069
lemma OAI.SharpPlanar.CachedData.power7_r2_7_eq line 2070
def OAI.SharpPlanar.CachedData.power7_r2_8 line 2071
lemma OAI.SharpPlanar.CachedData.power7_r2_8_eq line 2072
def OAI.SharpPlanar.CachedData.power7_r2_9 line 2073
lemma OAI.SharpPlanar.CachedData.power7_r2_9_eq line 2074
def OAI.SharpPlanar.CachedData.power7_r2_10 line 2075
lemma OAI.SharpPlanar.CachedData.power7_r2_10_eq line 2076
def OAI.SharpPlanar.CachedData.power7_r2_11 line 2077
lemma OAI.SharpPlanar.CachedData.power7_r2_11_eq line 2078
def OAI.SharpPlanar.CachedData.power7_r2_12 line 2079
lemma OAI.SharpPlanar.CachedData.power7_r2_12_eq line 2080
def OAI.SharpPlanar.CachedData.power7_r2_13 line 2081
lemma OAI.SharpPlanar.CachedData.power7_r2_13_eq line 2082
def OAI.SharpPlanar.CachedData.power7_r2_14 line 2083
lemma OAI.SharpPlanar.CachedData.power7_r2_14_eq line 2084
def OAI.SharpPlanar.CachedData.power7_r2_15 line 2085
lemma OAI.SharpPlanar.CachedData.power7_r2_15_eq line 2086
def OAI.SharpPlanar.CachedData.power7_r2 line 2087
lemma OAI.SharpPlanar.CachedData.power7_r2_eq line 2088
def OAI.SharpPlanar.CachedData.power7_r3_0 line 2106
lemma OAI.SharpPlanar.CachedData.power7_r3_0_eq line 2107
def OAI.SharpPlanar.CachedData.power7_r3_1 line 2108
lemma OAI.SharpPlanar.CachedData.power7_r3_1_eq line 2109
def OAI.SharpPlanar.CachedData.power7_r3_2 line 2110
lemma OAI.SharpPlanar.CachedData.power7_r3_2_eq line 2111
def OAI.SharpPlanar.CachedData.power7_r3_3 line 2112
lemma OAI.SharpPlanar.CachedData.power7_r3_3_eq line 2113
def OAI.SharpPlanar.CachedData.power7_r3_4 line 2114
lemma OAI.SharpPlanar.CachedData.power7_r3_4_eq line 2115
def OAI.SharpPlanar.CachedData.power7_r3_5 line 2116
lemma OAI.SharpPlanar.CachedData.power7_r3_5_eq line 2117
def OAI.SharpPlanar.CachedData.power7_r3_6 line 2118
lemma OAI.SharpPlanar.CachedData.power7_r3_6_eq line 2119
def OAI.SharpPlanar.CachedData.power7_r3_7 line 2120
lemma OAI.SharpPlanar.CachedData.power7_r3_7_eq line 2121
def OAI.SharpPlanar.CachedData.power7_r3_8 line 2122
lemma OAI.SharpPlanar.CachedData.power7_r3_8_eq line 2123
def OAI.SharpPlanar.CachedData.power7_r3_9 line 2124
lemma OAI.SharpPlanar.CachedData.power7_r3_9_eq line 2125
def OAI.SharpPlanar.CachedData.power7_r3_10 line 2126
lemma OAI.SharpPlanar.CachedData.power7_r3_10_eq line 2127
def OAI.SharpPlanar.CachedData.power7_r3_11 line 2128
lemma OAI.SharpPlanar.CachedData.power7_r3_11_eq line 2129
def OAI.SharpPlanar.CachedData.power7_r3_12 line 2130
lemma OAI.SharpPlanar.CachedData.power7_r3_12_eq line 2131
def OAI.SharpPlanar.CachedData.power7_r3_13 line 2132
lemma OAI.SharpPlanar.CachedData.power7_r3_13_eq line 2133
def OAI.SharpPlanar.CachedData.power7_r3_14 line 2134
lemma OAI.SharpPlanar.CachedData.power7_r3_14_eq line 2135
def OAI.SharpPlanar.CachedData.power7_r3_15 line 2136
lemma OAI.SharpPlanar.CachedData.power7_r3_15_eq line 2137
def OAI.SharpPlanar.CachedData.power7_r3 line 2138
lemma OAI.SharpPlanar.CachedData.power7_r3_eq line 2139
def OAI.SharpPlanar.CachedData.power7_r4_0 line 2157
lemma OAI.SharpPlanar.CachedData.power7_r4_0_eq line 2158
def OAI.SharpPlanar.CachedData.power7_r4_1 line 2159
lemma OAI.SharpPlanar.CachedData.power7_r4_1_eq line 2160
def OAI.SharpPlanar.CachedData.power7_r4_2 line 2161
lemma OAI.SharpPlanar.CachedData.power7_r4_2_eq line 2162
def OAI.SharpPlanar.CachedData.power7_r4_3 line 2163
lemma OAI.SharpPlanar.CachedData.power7_r4_3_eq line 2164
def OAI.SharpPlanar.CachedData.power7_r4_4 line 2165
lemma OAI.SharpPlanar.CachedData.power7_r4_4_eq line 2166
def OAI.SharpPlanar.CachedData.power7_r4_5 line 2167
lemma OAI.SharpPlanar.CachedData.power7_r4_5_eq line 2168
def OAI.SharpPlanar.CachedData.power7_r4_6 line 2169
lemma OAI.SharpPlanar.CachedData.power7_r4_6_eq line 2170
def OAI.SharpPlanar.CachedData.power7_r4_7 line 2171
lemma OAI.SharpPlanar.CachedData.power7_r4_7_eq line 2172
def OAI.SharpPlanar.CachedData.power7_r4_8 line 2173
lemma OAI.SharpPlanar.CachedData.power7_r4_8_eq line 2174
def OAI.SharpPlanar.CachedData.power7_r4_9 line 2175
lemma OAI.SharpPlanar.CachedData.power7_r4_9_eq line 2176
def OAI.SharpPlanar.CachedData.power7_r4_10 line 2177
lemma OAI.SharpPlanar.CachedData.power7_r4_10_eq line 2178
def OAI.SharpPlanar.CachedData.power7_r4_11 line 2179
lemma OAI.SharpPlanar.CachedData.power7_r4_11_eq line 2180
def OAI.SharpPlanar.CachedData.power7_r4_12 line 2181
lemma OAI.SharpPlanar.CachedData.power7_r4_12_eq line 2182
def OAI.SharpPlanar.CachedData.power7_r4_13 line 2183
lemma OAI.SharpPlanar.CachedData.power7_r4_13_eq line 2184
def OAI.SharpPlanar.CachedData.power7_r4_14 line 2185
lemma OAI.SharpPlanar.CachedData.power7_r4_14_eq line 2186
def OAI.SharpPlanar.CachedData.power7_r4_15 line 2187
lemma OAI.SharpPlanar.CachedData.power7_r4_15_eq line 2188
def OAI.SharpPlanar.CachedData.power7_r4 line 2189
lemma OAI.SharpPlanar.CachedData.power7_r4_eq line 2190
def OAI.SharpPlanar.CachedData.power7_r5_0 line 2208
lemma OAI.SharpPlanar.CachedData.power7_r5_0_eq line 2209
def OAI.SharpPlanar.CachedData.power7_r5_1 line 2210
lemma OAI.SharpPlanar.CachedData.power7_r5_1_eq line 2211
def OAI.SharpPlanar.CachedData.power7_r5_2 line 2212
lemma OAI.SharpPlanar.CachedData.power7_r5_2_eq line 2213
def OAI.SharpPlanar.CachedData.power7_r5_3 line 2214
lemma OAI.SharpPlanar.CachedData.power7_r5_3_eq line 2215
def OAI.SharpPlanar.CachedData.power7_r5_4 line 2216
lemma OAI.SharpPlanar.CachedData.power7_r5_4_eq line 2217
def OAI.SharpPlanar.CachedData.power7_r5_5 line 2218
lemma OAI.SharpPlanar.CachedData.power7_r5_5_eq line 2219
def OAI.SharpPlanar.CachedData.power7_r5_6 line 2220
lemma OAI.SharpPlanar.CachedData.power7_r5_6_eq line 2221
def OAI.SharpPlanar.CachedData.power7_r5_7 line 2222
lemma OAI.SharpPlanar.CachedData.power7_r5_7_eq line 2223
def OAI.SharpPlanar.CachedData.power7_r5_8 line 2224
lemma OAI.SharpPlanar.CachedData.power7_r5_8_eq line 2225
def OAI.SharpPlanar.CachedData.power7_r5_9 line 2226
lemma OAI.SharpPlanar.CachedData.power7_r5_9_eq line 2227
def OAI.SharpPlanar.CachedData.power7_r5_10 line 2228
lemma OAI.SharpPlanar.CachedData.power7_r5_10_eq line 2229
def OAI.SharpPlanar.CachedData.power7_r5_11 line 2230
lemma OAI.SharpPlanar.CachedData.power7_r5_11_eq line 2231
def OAI.SharpPlanar.CachedData.power7_r5_12 line 2232
lemma OAI.SharpPlanar.CachedData.power7_r5_12_eq line 2233
def OAI.SharpPlanar.CachedData.power7_r5_13 line 2234
lemma OAI.SharpPlanar.CachedData.power7_r5_13_eq line 2235
def OAI.SharpPlanar.CachedData.power7_r5_14 line 2236
lemma OAI.SharpPlanar.CachedData.power7_r5_14_eq line 2237
def OAI.SharpPlanar.CachedData.power7_r5_15 line 2238
lemma OAI.SharpPlanar.CachedData.power7_r5_15_eq line 2239
def OAI.SharpPlanar.CachedData.power7_r5 line 2240
lemma OAI.SharpPlanar.CachedData.power7_r5_eq line 2241
def OAI.SharpPlanar.CachedData.power7 line 2259
lemma OAI.SharpPlanar.CachedData.power7_eq line 2260
lemma OAI.SharpPlanar.CachedData.power7_contains line 2268
def OAI.SharpPlanar.CachedData.power8Expr line 2274
def OAI.SharpPlanar.CachedData.power8_r0_0 line 2275
lemma OAI.SharpPlanar.CachedData.power8_r0_0_eq line 2276
def OAI.SharpPlanar.CachedData.power8_r0_1 line 2277
lemma OAI.SharpPlanar.CachedData.power8_r0_1_eq line 2278
def OAI.SharpPlanar.CachedData.power8_r0_2 line 2279
lemma OAI.SharpPlanar.CachedData.power8_r0_2_eq line 2280
def OAI.SharpPlanar.CachedData.power8_r0_3 line 2281
lemma OAI.SharpPlanar.CachedData.power8_r0_3_eq line 2282
def OAI.SharpPlanar.CachedData.power8_r0_4 line 2283
lemma OAI.SharpPlanar.CachedData.power8_r0_4_eq line 2284
def OAI.SharpPlanar.CachedData.power8_r0_5 line 2285
lemma OAI.SharpPlanar.CachedData.power8_r0_5_eq line 2286
def OAI.SharpPlanar.CachedData.power8_r0_6 line 2287
lemma OAI.SharpPlanar.CachedData.power8_r0_6_eq line 2288
def OAI.SharpPlanar.CachedData.power8_r0_7 line 2289
lemma OAI.SharpPlanar.CachedData.power8_r0_7_eq line 2290
def OAI.SharpPlanar.CachedData.power8_r0_8 line 2291
lemma OAI.SharpPlanar.CachedData.power8_r0_8_eq line 2292
def OAI.SharpPlanar.CachedData.power8_r0_9 line 2293
lemma OAI.SharpPlanar.CachedData.power8_r0_9_eq line 2294
def OAI.SharpPlanar.CachedData.power8_r0_10 line 2295
lemma OAI.SharpPlanar.CachedData.power8_r0_10_eq line 2296
def OAI.SharpPlanar.CachedData.power8_r0_11 line 2297
lemma OAI.SharpPlanar.CachedData.power8_r0_11_eq line 2298
def OAI.SharpPlanar.CachedData.power8_r0_12 line 2299
lemma OAI.SharpPlanar.CachedData.power8_r0_12_eq line 2300
def OAI.SharpPlanar.CachedData.power8_r0_13 line 2301
lemma OAI.SharpPlanar.CachedData.power8_r0_13_eq line 2302
def OAI.SharpPlanar.CachedData.power8_r0_14 line 2303
lemma OAI.SharpPlanar.CachedData.power8_r0_14_eq line 2304
def OAI.SharpPlanar.CachedData.power8_r0_15 line 2305
lemma OAI.SharpPlanar.CachedData.power8_r0_15_eq line 2306
def OAI.SharpPlanar.CachedData.power8_r0 line 2307
lemma OAI.SharpPlanar.CachedData.power8_r0_eq line 2308
def OAI.SharpPlanar.CachedData.power8_r1_0 line 2326
lemma OAI.SharpPlanar.CachedData.power8_r1_0_eq line 2327
def OAI.SharpPlanar.CachedData.power8_r1_1 line 2328
lemma OAI.SharpPlanar.CachedData.power8_r1_1_eq line 2329
def OAI.SharpPlanar.CachedData.power8_r1_2 line 2330
lemma OAI.SharpPlanar.CachedData.power8_r1_2_eq line 2331
def OAI.SharpPlanar.CachedData.power8_r1_3 line 2332
lemma OAI.SharpPlanar.CachedData.power8_r1_3_eq line 2333
def OAI.SharpPlanar.CachedData.power8_r1_4 line 2334
lemma OAI.SharpPlanar.CachedData.power8_r1_4_eq line 2335
def OAI.SharpPlanar.CachedData.power8_r1_5 line 2336
lemma OAI.SharpPlanar.CachedData.power8_r1_5_eq line 2337
def OAI.SharpPlanar.CachedData.power8_r1_6 line 2338
lemma OAI.SharpPlanar.CachedData.power8_r1_6_eq line 2339
def OAI.SharpPlanar.CachedData.power8_r1_7 line 2340
lemma OAI.SharpPlanar.CachedData.power8_r1_7_eq line 2341
def OAI.SharpPlanar.CachedData.power8_r1_8 line 2342
lemma OAI.SharpPlanar.CachedData.power8_r1_8_eq line 2343
def OAI.SharpPlanar.CachedData.power8_r1_9 line 2344
lemma OAI.SharpPlanar.CachedData.power8_r1_9_eq line 2345
def OAI.SharpPlanar.CachedData.power8_r1_10 line 2346
lemma OAI.SharpPlanar.CachedData.power8_r1_10_eq line 2347
def OAI.SharpPlanar.CachedData.power8_r1_11 line 2348
lemma OAI.SharpPlanar.CachedData.power8_r1_11_eq line 2349
def OAI.SharpPlanar.CachedData.power8_r1_12 line 2350
lemma OAI.SharpPlanar.CachedData.power8_r1_12_eq line 2351
def OAI.SharpPlanar.CachedData.power8_r1_13 line 2352
lemma OAI.SharpPlanar.CachedData.power8_r1_13_eq line 2353
def OAI.SharpPlanar.CachedData.power8_r1_14 line 2354
lemma OAI.SharpPlanar.CachedData.power8_r1_14_eq line 2355
def OAI.SharpPlanar.CachedData.power8_r1_15 line 2356
lemma OAI.SharpPlanar.CachedData.power8_r1_15_eq line 2357
def OAI.SharpPlanar.CachedData.power8_r1 line 2358
lemma OAI.SharpPlanar.CachedData.power8_r1_eq line 2359
def OAI.SharpPlanar.CachedData.power8_r2_0 line 2377
lemma OAI.SharpPlanar.CachedData.power8_r2_0_eq line 2378
def OAI.SharpPlanar.CachedData.power8_r2_1 line 2379
lemma OAI.SharpPlanar.CachedData.power8_r2_1_eq line 2380
def OAI.SharpPlanar.CachedData.power8_r2_2 line 2381
lemma OAI.SharpPlanar.CachedData.power8_r2_2_eq line 2382
def OAI.SharpPlanar.CachedData.power8_r2_3 line 2383
lemma OAI.SharpPlanar.CachedData.power8_r2_3_eq line 2384
def OAI.SharpPlanar.CachedData.power8_r2_4 line 2385
lemma OAI.SharpPlanar.CachedData.power8_r2_4_eq line 2386
def OAI.SharpPlanar.CachedData.power8_r2_5 line 2387
lemma OAI.SharpPlanar.CachedData.power8_r2_5_eq line 2388
def OAI.SharpPlanar.CachedData.power8_r2_6 line 2389
lemma OAI.SharpPlanar.CachedData.power8_r2_6_eq line 2390
def OAI.SharpPlanar.CachedData.power8_r2_7 line 2391
lemma OAI.SharpPlanar.CachedData.power8_r2_7_eq line 2392
def OAI.SharpPlanar.CachedData.power8_r2_8 line 2393
lemma OAI.SharpPlanar.CachedData.power8_r2_8_eq line 2394
def OAI.SharpPlanar.CachedData.power8_r2_9 line 2395
lemma OAI.SharpPlanar.CachedData.power8_r2_9_eq line 2396
def OAI.SharpPlanar.CachedData.power8_r2_10 line 2397
lemma OAI.SharpPlanar.CachedData.power8_r2_10_eq line 2398
def OAI.SharpPlanar.CachedData.power8_r2_11 line 2399
lemma OAI.SharpPlanar.CachedData.power8_r2_11_eq line 2400
def OAI.SharpPlanar.CachedData.power8_r2_12 line 2401
lemma OAI.SharpPlanar.CachedData.power8_r2_12_eq line 2402
def OAI.SharpPlanar.CachedData.power8_r2_13 line 2403
lemma OAI.SharpPlanar.CachedData.power8_r2_13_eq line 2404
def OAI.SharpPlanar.CachedData.power8_r2_14 line 2405
lemma OAI.SharpPlanar.CachedData.power8_r2_14_eq line 2406
def OAI.SharpPlanar.CachedData.power8_r2_15 line 2407
lemma OAI.SharpPlanar.CachedData.power8_r2_15_eq line 2408
def OAI.SharpPlanar.CachedData.power8_r2 line 2409
lemma OAI.SharpPlanar.CachedData.power8_r2_eq line 2410
def OAI.SharpPlanar.CachedData.power8_r3_0 line 2428
lemma OAI.SharpPlanar.CachedData.power8_r3_0_eq line 2429
def OAI.SharpPlanar.CachedData.power8_r3_1 line 2430
lemma OAI.SharpPlanar.CachedData.power8_r3_1_eq line 2431
def OAI.SharpPlanar.CachedData.power8_r3_2 line 2432
lemma OAI.SharpPlanar.CachedData.power8_r3_2_eq line 2433
def OAI.SharpPlanar.CachedData.power8_r3_3 line 2434
lemma OAI.SharpPlanar.CachedData.power8_r3_3_eq line 2435
def OAI.SharpPlanar.CachedData.power8_r3_4 line 2436
lemma OAI.SharpPlanar.CachedData.power8_r3_4_eq line 2437
def OAI.SharpPlanar.CachedData.power8_r3_5 line 2438
lemma OAI.SharpPlanar.CachedData.power8_r3_5_eq line 2439
def OAI.SharpPlanar.CachedData.power8_r3_6 line 2440
lemma OAI.SharpPlanar.CachedData.power8_r3_6_eq line 2441
def OAI.SharpPlanar.CachedData.power8_r3_7 line 2442
lemma OAI.SharpPlanar.CachedData.power8_r3_7_eq line 2443
def OAI.SharpPlanar.CachedData.power8_r3_8 line 2444
lemma OAI.SharpPlanar.CachedData.power8_r3_8_eq line 2445
def OAI.SharpPlanar.CachedData.power8_r3_9 line 2446
lemma OAI.SharpPlanar.CachedData.power8_r3_9_eq line 2447
def OAI.SharpPlanar.CachedData.power8_r3_10 line 2448
lemma OAI.SharpPlanar.CachedData.power8_r3_10_eq line 2449
def OAI.SharpPlanar.CachedData.power8_r3_11 line 2450
lemma OAI.SharpPlanar.CachedData.power8_r3_11_eq line 2451
def OAI.SharpPlanar.CachedData.power8_r3_12 line 2452
lemma OAI.SharpPlanar.CachedData.power8_r3_12_eq line 2453
def OAI.SharpPlanar.CachedData.power8_r3_13 line 2454
lemma OAI.SharpPlanar.CachedData.power8_r3_13_eq line 2455
def OAI.SharpPlanar.CachedData.power8_r3_14 line 2456
lemma OAI.SharpPlanar.CachedData.power8_r3_14_eq line 2457
def OAI.SharpPlanar.CachedData.power8_r3_15 line 2458
lemma OAI.SharpPlanar.CachedData.power8_r3_15_eq line 2459
def OAI.SharpPlanar.CachedData.power8_r3 line 2460
lemma OAI.SharpPlanar.CachedData.power8_r3_eq line 2461
def OAI.SharpPlanar.CachedData.power8_r4_0 line 2479
lemma OAI.SharpPlanar.CachedData.power8_r4_0_eq line 2480
def OAI.SharpPlanar.CachedData.power8_r4_1 line 2481
lemma OAI.SharpPlanar.CachedData.power8_r4_1_eq line 2482
def OAI.SharpPlanar.CachedData.power8_r4_2 line 2483
lemma OAI.SharpPlanar.CachedData.power8_r4_2_eq line 2484
def OAI.SharpPlanar.CachedData.power8_r4_3 line 2485
lemma OAI.SharpPlanar.CachedData.power8_r4_3_eq line 2486
def OAI.SharpPlanar.CachedData.power8_r4_4 line 2487
lemma OAI.SharpPlanar.CachedData.power8_r4_4_eq line 2488
def OAI.SharpPlanar.CachedData.power8_r4_5 line 2489
lemma OAI.SharpPlanar.CachedData.power8_r4_5_eq line 2490
def OAI.SharpPlanar.CachedData.power8_r4_6 line 2491
lemma OAI.SharpPlanar.CachedData.power8_r4_6_eq line 2492
def OAI.SharpPlanar.CachedData.power8_r4_7 line 2493
lemma OAI.SharpPlanar.CachedData.power8_r4_7_eq line 2494
def OAI.SharpPlanar.CachedData.power8_r4_8 line 2495
lemma OAI.SharpPlanar.CachedData.power8_r4_8_eq line 2496
def OAI.SharpPlanar.CachedData.power8_r4_9 line 2497
lemma OAI.SharpPlanar.CachedData.power8_r4_9_eq line 2498
def OAI.SharpPlanar.CachedData.power8_r4_10 line 2499
lemma OAI.SharpPlanar.CachedData.power8_r4_10_eq line 2500
def OAI.SharpPlanar.CachedData.power8_r4_11 line 2501
lemma OAI.SharpPlanar.CachedData.power8_r4_11_eq line 2502
def OAI.SharpPlanar.CachedData.power8_r4_12 line 2503
lemma OAI.SharpPlanar.CachedData.power8_r4_12_eq line 2504
def OAI.SharpPlanar.CachedData.power8_r4_13 line 2505
lemma OAI.SharpPlanar.CachedData.power8_r4_13_eq line 2506
def OAI.SharpPlanar.CachedData.power8_r4_14 line 2507
lemma OAI.SharpPlanar.CachedData.power8_r4_14_eq line 2508
def OAI.SharpPlanar.CachedData.power8_r4_15 line 2509
lemma OAI.SharpPlanar.CachedData.power8_r4_15_eq line 2510
def OAI.SharpPlanar.CachedData.power8_r4 line 2511
lemma OAI.SharpPlanar.CachedData.power8_r4_eq line 2512
def OAI.SharpPlanar.CachedData.power8_r5_0 line 2530
lemma OAI.SharpPlanar.CachedData.power8_r5_0_eq line 2531
def OAI.SharpPlanar.CachedData.power8_r5_1 line 2532
lemma OAI.SharpPlanar.CachedData.power8_r5_1_eq line 2533
def OAI.SharpPlanar.CachedData.power8_r5_2 line 2534
lemma OAI.SharpPlanar.CachedData.power8_r5_2_eq line 2535
def OAI.SharpPlanar.CachedData.power8_r5_3 line 2536
lemma OAI.SharpPlanar.CachedData.power8_r5_3_eq line 2537
def OAI.SharpPlanar.CachedData.power8_r5_4 line 2538
lemma OAI.SharpPlanar.CachedData.power8_r5_4_eq line 2539
def OAI.SharpPlanar.CachedData.power8_r5_5 line 2540
lemma OAI.SharpPlanar.CachedData.power8_r5_5_eq line 2541
def OAI.SharpPlanar.CachedData.power8_r5_6 line 2542
lemma OAI.SharpPlanar.CachedData.power8_r5_6_eq line 2543
def OAI.SharpPlanar.CachedData.power8_r5_7 line 2544
lemma OAI.SharpPlanar.CachedData.power8_r5_7_eq line 2545
def OAI.SharpPlanar.CachedData.power8_r5_8 line 2546
lemma OAI.SharpPlanar.CachedData.power8_r5_8_eq line 2547
def OAI.SharpPlanar.CachedData.power8_r5_9 line 2548
lemma OAI.SharpPlanar.CachedData.power8_r5_9_eq line 2549
def OAI.SharpPlanar.CachedData.power8_r5_10 line 2550
lemma OAI.SharpPlanar.CachedData.power8_r5_10_eq line 2551
def OAI.SharpPlanar.CachedData.power8_r5_11 line 2552
lemma OAI.SharpPlanar.CachedData.power8_r5_11_eq line 2553
def OAI.SharpPlanar.CachedData.power8_r5_12 line 2554
lemma OAI.SharpPlanar.CachedData.power8_r5_12_eq line 2555
def OAI.SharpPlanar.CachedData.power8_r5_13 line 2556
lemma OAI.SharpPlanar.CachedData.power8_r5_13_eq line 2557
def OAI.SharpPlanar.CachedData.power8_r5_14 line 2558
lemma OAI.SharpPlanar.CachedData.power8_r5_14_eq line 2559
def OAI.SharpPlanar.CachedData.power8_r5_15 line 2560
lemma OAI.SharpPlanar.CachedData.power8_r5_15_eq line 2561
def OAI.SharpPlanar.CachedData.power8_r5 line 2562
lemma OAI.SharpPlanar.CachedData.power8_r5_eq line 2563
def OAI.SharpPlanar.CachedData.power8 line 2581
lemma OAI.SharpPlanar.CachedData.power8_eq line 2582
lemma OAI.SharpPlanar.CachedData.power8_contains line 2590
def OAI.SharpPlanar.CachedData.power9Expr line 2596
def OAI.SharpPlanar.CachedData.power9_r0_0 line 2597
lemma OAI.SharpPlanar.CachedData.power9_r0_0_eq line 2598
def OAI.SharpPlanar.CachedData.power9_r0_1 line 2599
lemma OAI.SharpPlanar.CachedData.power9_r0_1_eq line 2600
def OAI.SharpPlanar.CachedData.power9_r0_2 line 2601
lemma OAI.SharpPlanar.CachedData.power9_r0_2_eq line 2602
def OAI.SharpPlanar.CachedData.power9_r0_3 line 2603
lemma OAI.SharpPlanar.CachedData.power9_r0_3_eq line 2604
def OAI.SharpPlanar.CachedData.power9_r0_4 line 2605
lemma OAI.SharpPlanar.CachedData.power9_r0_4_eq line 2606
def OAI.SharpPlanar.CachedData.power9_r0_5 line 2607
lemma OAI.SharpPlanar.CachedData.power9_r0_5_eq line 2608
def OAI.SharpPlanar.CachedData.power9_r0_6 line 2609
lemma OAI.SharpPlanar.CachedData.power9_r0_6_eq line 2610
def OAI.SharpPlanar.CachedData.power9_r0_7 line 2611
lemma OAI.SharpPlanar.CachedData.power9_r0_7_eq line 2612
def OAI.SharpPlanar.CachedData.power9_r0_8 line 2613
lemma OAI.SharpPlanar.CachedData.power9_r0_8_eq line 2614
def OAI.SharpPlanar.CachedData.power9_r0_9 line 2615
lemma OAI.SharpPlanar.CachedData.power9_r0_9_eq line 2616
def OAI.SharpPlanar.CachedData.power9_r0_10 line 2617
lemma OAI.SharpPlanar.CachedData.power9_r0_10_eq line 2618
def OAI.SharpPlanar.CachedData.power9_r0_11 line 2619
lemma OAI.SharpPlanar.CachedData.power9_r0_11_eq line 2620
def OAI.SharpPlanar.CachedData.power9_r0_12 line 2621
lemma OAI.SharpPlanar.CachedData.power9_r0_12_eq line 2622
def OAI.SharpPlanar.CachedData.power9_r0_13 line 2623
lemma OAI.SharpPlanar.CachedData.power9_r0_13_eq line 2624
def OAI.SharpPlanar.CachedData.power9_r0_14 line 2625
lemma OAI.SharpPlanar.CachedData.power9_r0_14_eq line 2626
def OAI.SharpPlanar.CachedData.power9_r0_15 line 2627
lemma OAI.SharpPlanar.CachedData.power9_r0_15_eq line 2628
def OAI.SharpPlanar.CachedData.power9_r0 line 2629
lemma OAI.SharpPlanar.CachedData.power9_r0_eq line 2630
def OAI.SharpPlanar.CachedData.power9_r1_0 line 2648
lemma OAI.SharpPlanar.CachedData.power9_r1_0_eq line 2649
def OAI.SharpPlanar.CachedData.power9_r1_1 line 2650
lemma OAI.SharpPlanar.CachedData.power9_r1_1_eq line 2651
def OAI.SharpPlanar.CachedData.power9_r1_2 line 2652
lemma OAI.SharpPlanar.CachedData.power9_r1_2_eq line 2653
def OAI.SharpPlanar.CachedData.power9_r1_3 line 2654
lemma OAI.SharpPlanar.CachedData.power9_r1_3_eq line 2655
def OAI.SharpPlanar.CachedData.power9_r1_4 line 2656
lemma OAI.SharpPlanar.CachedData.power9_r1_4_eq line 2657
def OAI.SharpPlanar.CachedData.power9_r1_5 line 2658
lemma OAI.SharpPlanar.CachedData.power9_r1_5_eq line 2659
def OAI.SharpPlanar.CachedData.power9_r1_6 line 2660
lemma OAI.SharpPlanar.CachedData.power9_r1_6_eq line 2661
def OAI.SharpPlanar.CachedData.power9_r1_7 line 2662
lemma OAI.SharpPlanar.CachedData.power9_r1_7_eq line 2663
def OAI.SharpPlanar.CachedData.power9_r1_8 line 2664
lemma OAI.SharpPlanar.CachedData.power9_r1_8_eq line 2665
def OAI.SharpPlanar.CachedData.power9_r1_9 line 2666
lemma OAI.SharpPlanar.CachedData.power9_r1_9_eq line 2667
def OAI.SharpPlanar.CachedData.power9_r1_10 line 2668
lemma OAI.SharpPlanar.CachedData.power9_r1_10_eq line 2669
def OAI.SharpPlanar.CachedData.power9_r1_11 line 2670
lemma OAI.SharpPlanar.CachedData.power9_r1_11_eq line 2671
def OAI.SharpPlanar.CachedData.power9_r1_12 line 2672
lemma OAI.SharpPlanar.CachedData.power9_r1_12_eq line 2673
def OAI.SharpPlanar.CachedData.power9_r1_13 line 2674
lemma OAI.SharpPlanar.CachedData.power9_r1_13_eq line 2675
def OAI.SharpPlanar.CachedData.power9_r1_14 line 2676
lemma OAI.SharpPlanar.CachedData.power9_r1_14_eq line 2677
def OAI.SharpPlanar.CachedData.power9_r1_15 line 2678
lemma OAI.SharpPlanar.CachedData.power9_r1_15_eq line 2679
def OAI.SharpPlanar.CachedData.power9_r1 line 2680
lemma OAI.SharpPlanar.CachedData.power9_r1_eq line 2681
def OAI.SharpPlanar.CachedData.power9_r2_0 line 2699
lemma OAI.SharpPlanar.CachedData.power9_r2_0_eq line 2700
def OAI.SharpPlanar.CachedData.power9_r2_1 line 2701
lemma OAI.SharpPlanar.CachedData.power9_r2_1_eq line 2702
def OAI.SharpPlanar.CachedData.power9_r2_2 line 2703
lemma OAI.SharpPlanar.CachedData.power9_r2_2_eq line 2704
def OAI.SharpPlanar.CachedData.power9_r2_3 line 2705
lemma OAI.SharpPlanar.CachedData.power9_r2_3_eq line 2706
def OAI.SharpPlanar.CachedData.power9_r2_4 line 2707
lemma OAI.SharpPlanar.CachedData.power9_r2_4_eq line 2708
def OAI.SharpPlanar.CachedData.power9_r2_5 line 2709
lemma OAI.SharpPlanar.CachedData.power9_r2_5_eq line 2710
def OAI.SharpPlanar.CachedData.power9_r2_6 line 2711
lemma OAI.SharpPlanar.CachedData.power9_r2_6_eq line 2712
def OAI.SharpPlanar.CachedData.power9_r2_7 line 2713
lemma OAI.SharpPlanar.CachedData.power9_r2_7_eq line 2714
def OAI.SharpPlanar.CachedData.power9_r2_8 line 2715
lemma OAI.SharpPlanar.CachedData.power9_r2_8_eq line 2716
def OAI.SharpPlanar.CachedData.power9_r2_9 line 2717
lemma OAI.SharpPlanar.CachedData.power9_r2_9_eq line 2718
def OAI.SharpPlanar.CachedData.power9_r2_10 line 2719
lemma OAI.SharpPlanar.CachedData.power9_r2_10_eq line 2720
def OAI.SharpPlanar.CachedData.power9_r2_11 line 2721
lemma OAI.SharpPlanar.CachedData.power9_r2_11_eq line 2722
def OAI.SharpPlanar.CachedData.power9_r2_12 line 2723
lemma OAI.SharpPlanar.CachedData.power9_r2_12_eq line 2724
def OAI.SharpPlanar.CachedData.power9_r2_13 line 2725
lemma OAI.SharpPlanar.CachedData.power9_r2_13_eq line 2726
def OAI.SharpPlanar.CachedData.power9_r2_14 line 2727
lemma OAI.SharpPlanar.CachedData.power9_r2_14_eq line 2728
def OAI.SharpPlanar.CachedData.power9_r2_15 line 2729
lemma OAI.SharpPlanar.CachedData.power9_r2_15_eq line 2730
def OAI.SharpPlanar.CachedData.power9_r2 line 2731
lemma OAI.SharpPlanar.CachedData.power9_r2_eq line 2732
def OAI.SharpPlanar.CachedData.power9_r3_0 line 2750
lemma OAI.SharpPlanar.CachedData.power9_r3_0_eq line 2751
def OAI.SharpPlanar.CachedData.power9_r3_1 line 2752
lemma OAI.SharpPlanar.CachedData.power9_r3_1_eq line 2753
def OAI.SharpPlanar.CachedData.power9_r3_2 line 2754
lemma OAI.SharpPlanar.CachedData.power9_r3_2_eq line 2755
def OAI.SharpPlanar.CachedData.power9_r3_3 line 2756
lemma OAI.SharpPlanar.CachedData.power9_r3_3_eq line 2757
def OAI.SharpPlanar.CachedData.power9_r3_4 line 2758
lemma OAI.SharpPlanar.CachedData.power9_r3_4_eq line 2759
def OAI.SharpPlanar.CachedData.power9_r3_5 line 2760
lemma OAI.SharpPlanar.CachedData.power9_r3_5_eq line 2761
def OAI.SharpPlanar.CachedData.power9_r3_6 line 2762
lemma OAI.SharpPlanar.CachedData.power9_r3_6_eq line 2763
def OAI.SharpPlanar.CachedData.power9_r3_7 line 2764
lemma OAI.SharpPlanar.CachedData.power9_r3_7_eq line 2765
def OAI.SharpPlanar.CachedData.power9_r3_8 line 2766
lemma OAI.SharpPlanar.CachedData.power9_r3_8_eq line 2767
def OAI.SharpPlanar.CachedData.power9_r3_9 line 2768
lemma OAI.SharpPlanar.CachedData.power9_r3_9_eq line 2769
def OAI.SharpPlanar.CachedData.power9_r3_10 line 2770
lemma OAI.SharpPlanar.CachedData.power9_r3_10_eq line 2771
def OAI.SharpPlanar.CachedData.power9_r3_11 line 2772
lemma OAI.SharpPlanar.CachedData.power9_r3_11_eq line 2773
def OAI.SharpPlanar.CachedData.power9_r3_12 line 2774
lemma OAI.SharpPlanar.CachedData.power9_r3_12_eq line 2775
def OAI.SharpPlanar.CachedData.power9_r3_13 line 2776
lemma OAI.SharpPlanar.CachedData.power9_r3_13_eq line 2777
def OAI.SharpPlanar.CachedData.power9_r3_14 line 2778
lemma OAI.SharpPlanar.CachedData.power9_r3_14_eq line 2779
def OAI.SharpPlanar.CachedData.power9_r3_15 line 2780
lemma OAI.SharpPlanar.CachedData.power9_r3_15_eq line 2781
def OAI.SharpPlanar.CachedData.power9_r3 line 2782
lemma OAI.SharpPlanar.CachedData.power9_r3_eq line 2783
def OAI.SharpPlanar.CachedData.power9_r4_0 line 2801
lemma OAI.SharpPlanar.CachedData.power9_r4_0_eq line 2802
def OAI.SharpPlanar.CachedData.power9_r4_1 line 2803
lemma OAI.SharpPlanar.CachedData.power9_r4_1_eq line 2804
def OAI.SharpPlanar.CachedData.power9_r4_2 line 2805
lemma OAI.SharpPlanar.CachedData.power9_r4_2_eq line 2806
def OAI.SharpPlanar.CachedData.power9_r4_3 line 2807
lemma OAI.SharpPlanar.CachedData.power9_r4_3_eq line 2808
def OAI.SharpPlanar.CachedData.power9_r4_4 line 2809
lemma OAI.SharpPlanar.CachedData.power9_r4_4_eq line 2810
def OAI.SharpPlanar.CachedData.power9_r4_5 line 2811
lemma OAI.SharpPlanar.CachedData.power9_r4_5_eq line 2812
def OAI.SharpPlanar.CachedData.power9_r4_6 line 2813
lemma OAI.SharpPlanar.CachedData.power9_r4_6_eq line 2814
def OAI.SharpPlanar.CachedData.power9_r4_7 line 2815
lemma OAI.SharpPlanar.CachedData.power9_r4_7_eq line 2816
def OAI.SharpPlanar.CachedData.power9_r4_8 line 2817
lemma OAI.SharpPlanar.CachedData.power9_r4_8_eq line 2818
def OAI.SharpPlanar.CachedData.power9_r4_9 line 2819
lemma OAI.SharpPlanar.CachedData.power9_r4_9_eq line 2820
def OAI.SharpPlanar.CachedData.power9_r4_10 line 2821
lemma OAI.SharpPlanar.CachedData.power9_r4_10_eq line 2822
def OAI.SharpPlanar.CachedData.power9_r4_11 line 2823
lemma OAI.SharpPlanar.CachedData.power9_r4_11_eq line 2824
def OAI.SharpPlanar.CachedData.power9_r4_12 line 2825
lemma OAI.SharpPlanar.CachedData.power9_r4_12_eq line 2826
def OAI.SharpPlanar.CachedData.power9_r4_13 line 2827
lemma OAI.SharpPlanar.CachedData.power9_r4_13_eq line 2828
def OAI.SharpPlanar.CachedData.power9_r4_14 line 2829
lemma OAI.SharpPlanar.CachedData.power9_r4_14_eq line 2830
def OAI.SharpPlanar.CachedData.power9_r4_15 line 2831
lemma OAI.SharpPlanar.CachedData.power9_r4_15_eq line 2832
def OAI.SharpPlanar.CachedData.power9_r4 line 2833
lemma OAI.SharpPlanar.CachedData.power9_r4_eq line 2834
def OAI.SharpPlanar.CachedData.power9_r5_0 line 2852
lemma OAI.SharpPlanar.CachedData.power9_r5_0_eq line 2853
def OAI.SharpPlanar.CachedData.power9_r5_1 line 2854
lemma OAI.SharpPlanar.CachedData.power9_r5_1_eq line 2855
def OAI.SharpPlanar.CachedData.power9_r5_2 line 2856
lemma OAI.SharpPlanar.CachedData.power9_r5_2_eq line 2857
def OAI.SharpPlanar.CachedData.power9_r5_3 line 2858
lemma OAI.SharpPlanar.CachedData.power9_r5_3_eq line 2859
def OAI.SharpPlanar.CachedData.power9_r5_4 line 2860
lemma OAI.SharpPlanar.CachedData.power9_r5_4_eq line 2861
def OAI.SharpPlanar.CachedData.power9_r5_5 line 2862
lemma OAI.SharpPlanar.CachedData.power9_r5_5_eq line 2863
def OAI.SharpPlanar.CachedData.power9_r5_6 line 2864
lemma OAI.SharpPlanar.CachedData.power9_r5_6_eq line 2865
def OAI.SharpPlanar.CachedData.power9_r5_7 line 2866
lemma OAI.SharpPlanar.CachedData.power9_r5_7_eq line 2867
def OAI.SharpPlanar.CachedData.power9_r5_8 line 2868
lemma OAI.SharpPlanar.CachedData.power9_r5_8_eq line 2869
def OAI.SharpPlanar.CachedData.power9_r5_9 line 2870
lemma OAI.SharpPlanar.CachedData.power9_r5_9_eq line 2871
def OAI.SharpPlanar.CachedData.power9_r5_10 line 2872
lemma OAI.SharpPlanar.CachedData.power9_r5_10_eq line 2873
def OAI.SharpPlanar.CachedData.power9_r5_11 line 2874
lemma OAI.SharpPlanar.CachedData.power9_r5_11_eq line 2875
def OAI.SharpPlanar.CachedData.power9_r5_12 line 2876
lemma OAI.SharpPlanar.CachedData.power9_r5_12_eq line 2877
def OAI.SharpPlanar.CachedData.power9_r5_13 line 2878
lemma OAI.SharpPlanar.CachedData.power9_r5_13_eq line 2879
def OAI.SharpPlanar.CachedData.power9_r5_14 line 2880
lemma OAI.SharpPlanar.CachedData.power9_r5_14_eq line 2881
def OAI.SharpPlanar.CachedData.power9_r5_15 line 2882
lemma OAI.SharpPlanar.CachedData.power9_r5_15_eq line 2883
def OAI.SharpPlanar.CachedData.power9_r5 line 2884
lemma OAI.SharpPlanar.CachedData.power9_r5_eq line 2885
def OAI.SharpPlanar.CachedData.power9 line 2903
lemma OAI.SharpPlanar.CachedData.power9_eq line 2904
lemma OAI.SharpPlanar.CachedData.power9_contains line 2912
def OAI.SharpPlanar.CachedData.power10Expr line 2918
def OAI.SharpPlanar.CachedData.power10_r0_0 line 2919
lemma OAI.SharpPlanar.CachedData.power10_r0_0_eq line 2920
def OAI.SharpPlanar.CachedData.power10_r0_1 line 2921
lemma OAI.SharpPlanar.CachedData.power10_r0_1_eq line 2922
def OAI.SharpPlanar.CachedData.power10_r0_2 line 2923
lemma OAI.SharpPlanar.CachedData.power10_r0_2_eq line 2924
def OAI.SharpPlanar.CachedData.power10_r0_3 line 2925
lemma OAI.SharpPlanar.CachedData.power10_r0_3_eq line 2926
def OAI.SharpPlanar.CachedData.power10_r0_4 line 2927
lemma OAI.SharpPlanar.CachedData.power10_r0_4_eq line 2928
def OAI.SharpPlanar.CachedData.power10_r0_5 line 2929
lemma OAI.SharpPlanar.CachedData.power10_r0_5_eq line 2930
def OAI.SharpPlanar.CachedData.power10_r0_6 line 2931
lemma OAI.SharpPlanar.CachedData.power10_r0_6_eq line 2932
def OAI.SharpPlanar.CachedData.power10_r0_7 line 2933
lemma OAI.SharpPlanar.CachedData.power10_r0_7_eq line 2934
def OAI.SharpPlanar.CachedData.power10_r0_8 line 2935
lemma OAI.SharpPlanar.CachedData.power10_r0_8_eq line 2936
def OAI.SharpPlanar.CachedData.power10_r0_9 line 2937
lemma OAI.SharpPlanar.CachedData.power10_r0_9_eq line 2938
def OAI.SharpPlanar.CachedData.power10_r0_10 line 2939
lemma OAI.SharpPlanar.CachedData.power10_r0_10_eq line 2940
def OAI.SharpPlanar.CachedData.power10_r0_11 line 2941
lemma OAI.SharpPlanar.CachedData.power10_r0_11_eq line 2942
def OAI.SharpPlanar.CachedData.power10_r0_12 line 2943
lemma OAI.SharpPlanar.CachedData.power10_r0_12_eq line 2944
def OAI.SharpPlanar.CachedData.power10_r0_13 line 2945
lemma OAI.SharpPlanar.CachedData.power10_r0_13_eq line 2946
def OAI.SharpPlanar.CachedData.power10_r0_14 line 2947
lemma OAI.SharpPlanar.CachedData.power10_r0_14_eq line 2948
def OAI.SharpPlanar.CachedData.power10_r0_15 line 2949
lemma OAI.SharpPlanar.CachedData.power10_r0_15_eq line 2950
def OAI.SharpPlanar.CachedData.power10_r0 line 2951
lemma OAI.SharpPlanar.CachedData.power10_r0_eq line 2952
def OAI.SharpPlanar.CachedData.power10_r1_0 line 2970
lemma OAI.SharpPlanar.CachedData.power10_r1_0_eq line 2971
def OAI.SharpPlanar.CachedData.power10_r1_1 line 2972
lemma OAI.SharpPlanar.CachedData.power10_r1_1_eq line 2973
def OAI.SharpPlanar.CachedData.power10_r1_2 line 2974
lemma OAI.SharpPlanar.CachedData.power10_r1_2_eq line 2975
def OAI.SharpPlanar.CachedData.power10_r1_3 line 2976
lemma OAI.SharpPlanar.CachedData.power10_r1_3_eq line 2977
def OAI.SharpPlanar.CachedData.power10_r1_4 line 2978
lemma OAI.SharpPlanar.CachedData.power10_r1_4_eq line 2979
def OAI.SharpPlanar.CachedData.power10_r1_5 line 2980
lemma OAI.SharpPlanar.CachedData.power10_r1_5_eq line 2981
def OAI.SharpPlanar.CachedData.power10_r1_6 line 2982
lemma OAI.SharpPlanar.CachedData.power10_r1_6_eq line 2983
def OAI.SharpPlanar.CachedData.power10_r1_7 line 2984
lemma OAI.SharpPlanar.CachedData.power10_r1_7_eq line 2985
def OAI.SharpPlanar.CachedData.power10_r1_8 line 2986
lemma OAI.SharpPlanar.CachedData.power10_r1_8_eq line 2987
def OAI.SharpPlanar.CachedData.power10_r1_9 line 2988
lemma OAI.SharpPlanar.CachedData.power10_r1_9_eq line 2989
def OAI.SharpPlanar.CachedData.power10_r1_10 line 2990
lemma OAI.SharpPlanar.CachedData.power10_r1_10_eq line 2991
def OAI.SharpPlanar.CachedData.power10_r1_11 line 2992
lemma OAI.SharpPlanar.CachedData.power10_r1_11_eq line 2993
def OAI.SharpPlanar.CachedData.power10_r1_12 line 2994
lemma OAI.SharpPlanar.CachedData.power10_r1_12_eq line 2995
def OAI.SharpPlanar.CachedData.power10_r1_13 line 2996
lemma OAI.SharpPlanar.CachedData.power10_r1_13_eq line 2997
def OAI.SharpPlanar.CachedData.power10_r1_14 line 2998
lemma OAI.SharpPlanar.CachedData.power10_r1_14_eq line 2999
def OAI.SharpPlanar.CachedData.power10_r1_15 line 3000
lemma OAI.SharpPlanar.CachedData.power10_r1_15_eq line 3001
def OAI.SharpPlanar.CachedData.power10_r1 line 3002
lemma OAI.SharpPlanar.CachedData.power10_r1_eq line 3003
def OAI.SharpPlanar.CachedData.power10_r2_0 line 3021
lemma OAI.SharpPlanar.CachedData.power10_r2_0_eq line 3022
def OAI.SharpPlanar.CachedData.power10_r2_1 line 3023
lemma OAI.SharpPlanar.CachedData.power10_r2_1_eq line 3024
def OAI.SharpPlanar.CachedData.power10_r2_2 line 3025
lemma OAI.SharpPlanar.CachedData.power10_r2_2_eq line 3026
def OAI.SharpPlanar.CachedData.power10_r2_3 line 3027
lemma OAI.SharpPlanar.CachedData.power10_r2_3_eq line 3028
def OAI.SharpPlanar.CachedData.power10_r2_4 line 3029
lemma OAI.SharpPlanar.CachedData.power10_r2_4_eq line 3030
def OAI.SharpPlanar.CachedData.power10_r2_5 line 3031
lemma OAI.SharpPlanar.CachedData.power10_r2_5_eq line 3032
def OAI.SharpPlanar.CachedData.power10_r2_6 line 3033
lemma OAI.SharpPlanar.CachedData.power10_r2_6_eq line 3034
def OAI.SharpPlanar.CachedData.power10_r2_7 line 3035
lemma OAI.SharpPlanar.CachedData.power10_r2_7_eq line 3036
def OAI.SharpPlanar.CachedData.power10_r2_8 line 3037
lemma OAI.SharpPlanar.CachedData.power10_r2_8_eq line 3038
def OAI.SharpPlanar.CachedData.power10_r2_9 line 3039
lemma OAI.SharpPlanar.CachedData.power10_r2_9_eq line 3040
def OAI.SharpPlanar.CachedData.power10_r2_10 line 3041
lemma OAI.SharpPlanar.CachedData.power10_r2_10_eq line 3042
def OAI.SharpPlanar.CachedData.power10_r2_11 line 3043
lemma OAI.SharpPlanar.CachedData.power10_r2_11_eq line 3044
def OAI.SharpPlanar.CachedData.power10_r2_12 line 3045
lemma OAI.SharpPlanar.CachedData.power10_r2_12_eq line 3046
def OAI.SharpPlanar.CachedData.power10_r2_13 line 3047
lemma OAI.SharpPlanar.CachedData.power10_r2_13_eq line 3048
def OAI.SharpPlanar.CachedData.power10_r2_14 line 3049
lemma OAI.SharpPlanar.CachedData.power10_r2_14_eq line 3050
def OAI.SharpPlanar.CachedData.power10_r2_15 line 3051
lemma OAI.SharpPlanar.CachedData.power10_r2_15_eq line 3052
def OAI.SharpPlanar.CachedData.power10_r2 line 3053
lemma OAI.SharpPlanar.CachedData.power10_r2_eq line 3054
def OAI.SharpPlanar.CachedData.power10_r3_0 line 3072
lemma OAI.SharpPlanar.CachedData.power10_r3_0_eq line 3073
def OAI.SharpPlanar.CachedData.power10_r3_1 line 3074
lemma OAI.SharpPlanar.CachedData.power10_r3_1_eq line 3075
def OAI.SharpPlanar.CachedData.power10_r3_2 line 3076
lemma OAI.SharpPlanar.CachedData.power10_r3_2_eq line 3077
def OAI.SharpPlanar.CachedData.power10_r3_3 line 3078
lemma OAI.SharpPlanar.CachedData.power10_r3_3_eq line 3079
def OAI.SharpPlanar.CachedData.power10_r3_4 line 3080
lemma OAI.SharpPlanar.CachedData.power10_r3_4_eq line 3081
def OAI.SharpPlanar.CachedData.power10_r3_5 line 3082
lemma OAI.SharpPlanar.CachedData.power10_r3_5_eq line 3083
def OAI.SharpPlanar.CachedData.power10_r3_6 line 3084
lemma OAI.SharpPlanar.CachedData.power10_r3_6_eq line 3085
def OAI.SharpPlanar.CachedData.power10_r3_7 line 3086
lemma OAI.SharpPlanar.CachedData.power10_r3_7_eq line 3087
def OAI.SharpPlanar.CachedData.power10_r3_8 line 3088
lemma OAI.SharpPlanar.CachedData.power10_r3_8_eq line 3089
def OAI.SharpPlanar.CachedData.power10_r3_9 line 3090
lemma OAI.SharpPlanar.CachedData.power10_r3_9_eq line 3091
def OAI.SharpPlanar.CachedData.power10_r3_10 line 3092
lemma OAI.SharpPlanar.CachedData.power10_r3_10_eq line 3093
def OAI.SharpPlanar.CachedData.power10_r3_11 line 3094
lemma OAI.SharpPlanar.CachedData.power10_r3_11_eq line 3095
def OAI.SharpPlanar.CachedData.power10_r3_12 line 3096
lemma OAI.SharpPlanar.CachedData.power10_r3_12_eq line 3097
def OAI.SharpPlanar.CachedData.power10_r3_13 line 3098
lemma OAI.SharpPlanar.CachedData.power10_r3_13_eq line 3099
def OAI.SharpPlanar.CachedData.power10_r3_14 line 3100
lemma OAI.SharpPlanar.CachedData.power10_r3_14_eq line 3101
def OAI.SharpPlanar.CachedData.power10_r3_15 line 3102
lemma OAI.SharpPlanar.CachedData.power10_r3_15_eq line 3103
def OAI.SharpPlanar.CachedData.power10_r3 line 3104
lemma OAI.SharpPlanar.CachedData.power10_r3_eq line 3105
def OAI.SharpPlanar.CachedData.power10_r4_0 line 3123
lemma OAI.SharpPlanar.CachedData.power10_r4_0_eq line 3124
def OAI.SharpPlanar.CachedData.power10_r4_1 line 3125
lemma OAI.SharpPlanar.CachedData.power10_r4_1_eq line 3126
def OAI.SharpPlanar.CachedData.power10_r4_2 line 3127
lemma OAI.SharpPlanar.CachedData.power10_r4_2_eq line 3128
def OAI.SharpPlanar.CachedData.power10_r4_3 line 3129
lemma OAI.SharpPlanar.CachedData.power10_r4_3_eq line 3130
def OAI.SharpPlanar.CachedData.power10_r4_4 line 3131
lemma OAI.SharpPlanar.CachedData.power10_r4_4_eq line 3132
def OAI.SharpPlanar.CachedData.power10_r4_5 line 3133
lemma OAI.SharpPlanar.CachedData.power10_r4_5_eq line 3134
def OAI.SharpPlanar.CachedData.power10_r4_6 line 3135
lemma OAI.SharpPlanar.CachedData.power10_r4_6_eq line 3136
def OAI.SharpPlanar.CachedData.power10_r4_7 line 3137
lemma OAI.SharpPlanar.CachedData.power10_r4_7_eq line 3138
def OAI.SharpPlanar.CachedData.power10_r4_8 line 3139
lemma OAI.SharpPlanar.CachedData.power10_r4_8_eq line 3140
def OAI.SharpPlanar.CachedData.power10_r4_9 line 3141
lemma OAI.SharpPlanar.CachedData.power10_r4_9_eq line 3142
def OAI.SharpPlanar.CachedData.power10_r4_10 line 3143
lemma OAI.SharpPlanar.CachedData.power10_r4_10_eq line 3144
def OAI.SharpPlanar.CachedData.power10_r4_11 line 3145
lemma OAI.SharpPlanar.CachedData.power10_r4_11_eq line 3146
def OAI.SharpPlanar.CachedData.power10_r4_12 line 3147
lemma OAI.SharpPlanar.CachedData.power10_r4_12_eq line 3148
def OAI.SharpPlanar.CachedData.power10_r4_13 line 3149
lemma OAI.SharpPlanar.CachedData.power10_r4_13_eq line 3150
def OAI.SharpPlanar.CachedData.power10_r4_14 line 3151
lemma OAI.SharpPlanar.CachedData.power10_r4_14_eq line 3152
def OAI.SharpPlanar.CachedData.power10_r4_15 line 3153
lemma OAI.SharpPlanar.CachedData.power10_r4_15_eq line 3154
def OAI.SharpPlanar.CachedData.power10_r4 line 3155
lemma OAI.SharpPlanar.CachedData.power10_r4_eq line 3156
def OAI.SharpPlanar.CachedData.power10_r5_0 line 3174
lemma OAI.SharpPlanar.CachedData.power10_r5_0_eq line 3175
def OAI.SharpPlanar.CachedData.power10_r5_1 line 3176
lemma OAI.SharpPlanar.CachedData.power10_r5_1_eq line 3177
def OAI.SharpPlanar.CachedData.power10_r5_2 line 3178
lemma OAI.SharpPlanar.CachedData.power10_r5_2_eq line 3179
def OAI.SharpPlanar.CachedData.power10_r5_3 line 3180
lemma OAI.SharpPlanar.CachedData.power10_r5_3_eq line 3181
def OAI.SharpPlanar.CachedData.power10_r5_4 line 3182
lemma OAI.SharpPlanar.CachedData.power10_r5_4_eq line 3183
def OAI.SharpPlanar.CachedData.power10_r5_5 line 3184
lemma OAI.SharpPlanar.CachedData.power10_r5_5_eq line 3185
def OAI.SharpPlanar.CachedData.power10_r5_6 line 3186
lemma OAI.SharpPlanar.CachedData.power10_r5_6_eq line 3187
def OAI.SharpPlanar.CachedData.power10_r5_7 line 3188
lemma OAI.SharpPlanar.CachedData.power10_r5_7_eq line 3189
def OAI.SharpPlanar.CachedData.power10_r5_8 line 3190
lemma OAI.SharpPlanar.CachedData.power10_r5_8_eq line 3191
def OAI.SharpPlanar.CachedData.power10_r5_9 line 3192
lemma OAI.SharpPlanar.CachedData.power10_r5_9_eq line 3193
def OAI.SharpPlanar.CachedData.power10_r5_10 line 3194
lemma OAI.SharpPlanar.CachedData.power10_r5_10_eq line 3195
def OAI.SharpPlanar.CachedData.power10_r5_11 line 3196
lemma OAI.SharpPlanar.CachedData.power10_r5_11_eq line 3197
def OAI.SharpPlanar.CachedData.power10_r5_12 line 3198
lemma OAI.SharpPlanar.CachedData.power10_r5_12_eq line 3199
def OAI.SharpPlanar.CachedData.power10_r5_13 line 3200
lemma OAI.SharpPlanar.CachedData.power10_r5_13_eq line 3201
def OAI.SharpPlanar.CachedData.power10_r5_14 line 3202
lemma OAI.SharpPlanar.CachedData.power10_r5_14_eq line 3203
def OAI.SharpPlanar.CachedData.power10_r5_15 line 3204
lemma OAI.SharpPlanar.CachedData.power10_r5_15_eq line 3205
def OAI.SharpPlanar.CachedData.power10_r5 line 3206
lemma OAI.SharpPlanar.CachedData.power10_r5_eq line 3207
def OAI.SharpPlanar.CachedData.power10 line 3225
lemma OAI.SharpPlanar.CachedData.power10_eq line 3226
lemma OAI.SharpPlanar.CachedData.power10_contains line 3234