TransformedPowers10.lean`

2290 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.transStepExpr line 15
def OAI.SharpPlanar.CachedData.transStep_r0_0 line 16
lemma OAI.SharpPlanar.CachedData.transStep_r0_0_eq line 17
def OAI.SharpPlanar.CachedData.transStep_r0_1 line 18
lemma OAI.SharpPlanar.CachedData.transStep_r0_1_eq line 19
def OAI.SharpPlanar.CachedData.transStep_r0_2 line 20
lemma OAI.SharpPlanar.CachedData.transStep_r0_2_eq line 21
def OAI.SharpPlanar.CachedData.transStep_r0_3 line 22
lemma OAI.SharpPlanar.CachedData.transStep_r0_3_eq line 23
def OAI.SharpPlanar.CachedData.transStep_r0_4 line 24
lemma OAI.SharpPlanar.CachedData.transStep_r0_4_eq line 25
def OAI.SharpPlanar.CachedData.transStep_r0_5 line 26
lemma OAI.SharpPlanar.CachedData.transStep_r0_5_eq line 27
def OAI.SharpPlanar.CachedData.transStep_r0_6 line 28
lemma OAI.SharpPlanar.CachedData.transStep_r0_6_eq line 29
def OAI.SharpPlanar.CachedData.transStep_r0_7 line 30
lemma OAI.SharpPlanar.CachedData.transStep_r0_7_eq line 31
def OAI.SharpPlanar.CachedData.transStep_r0_8 line 32
lemma OAI.SharpPlanar.CachedData.transStep_r0_8_eq line 33
def OAI.SharpPlanar.CachedData.transStep_r0_9 line 34
lemma OAI.SharpPlanar.CachedData.transStep_r0_9_eq line 35
def OAI.SharpPlanar.CachedData.transStep_r0_10 line 36
lemma OAI.SharpPlanar.CachedData.transStep_r0_10_eq line 37
def OAI.SharpPlanar.CachedData.transStep_r0_11 line 38
lemma OAI.SharpPlanar.CachedData.transStep_r0_11_eq line 39
def OAI.SharpPlanar.CachedData.transStep_r0_12 line 40
lemma OAI.SharpPlanar.CachedData.transStep_r0_12_eq line 41
def OAI.SharpPlanar.CachedData.transStep_r0_13 line 42
lemma OAI.SharpPlanar.CachedData.transStep_r0_13_eq line 43
def OAI.SharpPlanar.CachedData.transStep_r0_14 line 44
lemma OAI.SharpPlanar.CachedData.transStep_r0_14_eq line 45
def OAI.SharpPlanar.CachedData.transStep_r0_15 line 46
lemma OAI.SharpPlanar.CachedData.transStep_r0_15_eq line 47
def OAI.SharpPlanar.CachedData.transStep_r0 line 48
lemma OAI.SharpPlanar.CachedData.transStep_r0_eq line 49
def OAI.SharpPlanar.CachedData.transStep_r1_0 line 67
lemma OAI.SharpPlanar.CachedData.transStep_r1_0_eq line 68
def OAI.SharpPlanar.CachedData.transStep_r1_1 line 69
lemma OAI.SharpPlanar.CachedData.transStep_r1_1_eq line 70
def OAI.SharpPlanar.CachedData.transStep_r1_2 line 71
lemma OAI.SharpPlanar.CachedData.transStep_r1_2_eq line 72
def OAI.SharpPlanar.CachedData.transStep_r1_3 line 73
lemma OAI.SharpPlanar.CachedData.transStep_r1_3_eq line 74
def OAI.SharpPlanar.CachedData.transStep_r1_4 line 75
lemma OAI.SharpPlanar.CachedData.transStep_r1_4_eq line 76
def OAI.SharpPlanar.CachedData.transStep_r1_5 line 77
lemma OAI.SharpPlanar.CachedData.transStep_r1_5_eq line 78
def OAI.SharpPlanar.CachedData.transStep_r1_6 line 79
lemma OAI.SharpPlanar.CachedData.transStep_r1_6_eq line 80
def OAI.SharpPlanar.CachedData.transStep_r1_7 line 81
lemma OAI.SharpPlanar.CachedData.transStep_r1_7_eq line 82
def OAI.SharpPlanar.CachedData.transStep_r1_8 line 83
lemma OAI.SharpPlanar.CachedData.transStep_r1_8_eq line 84
def OAI.SharpPlanar.CachedData.transStep_r1_9 line 85
lemma OAI.SharpPlanar.CachedData.transStep_r1_9_eq line 86
def OAI.SharpPlanar.CachedData.transStep_r1_10 line 87
lemma OAI.SharpPlanar.CachedData.transStep_r1_10_eq line 88
def OAI.SharpPlanar.CachedData.transStep_r1_11 line 89
lemma OAI.SharpPlanar.CachedData.transStep_r1_11_eq line 90
def OAI.SharpPlanar.CachedData.transStep_r1_12 line 91
lemma OAI.SharpPlanar.CachedData.transStep_r1_12_eq line 92
def OAI.SharpPlanar.CachedData.transStep_r1_13 line 93
lemma OAI.SharpPlanar.CachedData.transStep_r1_13_eq line 94
def OAI.SharpPlanar.CachedData.transStep_r1_14 line 95
lemma OAI.SharpPlanar.CachedData.transStep_r1_14_eq line 96
def OAI.SharpPlanar.CachedData.transStep_r1_15 line 97
lemma OAI.SharpPlanar.CachedData.transStep_r1_15_eq line 98
def OAI.SharpPlanar.CachedData.transStep_r1 line 99
lemma OAI.SharpPlanar.CachedData.transStep_r1_eq line 100
def OAI.SharpPlanar.CachedData.transStep_r2_0 line 118
lemma OAI.SharpPlanar.CachedData.transStep_r2_0_eq line 119
def OAI.SharpPlanar.CachedData.transStep_r2_1 line 120
lemma OAI.SharpPlanar.CachedData.transStep_r2_1_eq line 121
def OAI.SharpPlanar.CachedData.transStep_r2_2 line 122
lemma OAI.SharpPlanar.CachedData.transStep_r2_2_eq line 123
def OAI.SharpPlanar.CachedData.transStep_r2_3 line 124
lemma OAI.SharpPlanar.CachedData.transStep_r2_3_eq line 125
def OAI.SharpPlanar.CachedData.transStep_r2_4 line 126
lemma OAI.SharpPlanar.CachedData.transStep_r2_4_eq line 127
def OAI.SharpPlanar.CachedData.transStep_r2_5 line 128
lemma OAI.SharpPlanar.CachedData.transStep_r2_5_eq line 129
def OAI.SharpPlanar.CachedData.transStep_r2_6 line 130
lemma OAI.SharpPlanar.CachedData.transStep_r2_6_eq line 131
def OAI.SharpPlanar.CachedData.transStep_r2_7 line 132
lemma OAI.SharpPlanar.CachedData.transStep_r2_7_eq line 133
def OAI.SharpPlanar.CachedData.transStep_r2_8 line 134
lemma OAI.SharpPlanar.CachedData.transStep_r2_8_eq line 135
def OAI.SharpPlanar.CachedData.transStep_r2_9 line 136
lemma OAI.SharpPlanar.CachedData.transStep_r2_9_eq line 137
def OAI.SharpPlanar.CachedData.transStep_r2_10 line 138
lemma OAI.SharpPlanar.CachedData.transStep_r2_10_eq line 139
def OAI.SharpPlanar.CachedData.transStep_r2_11 line 140
lemma OAI.SharpPlanar.CachedData.transStep_r2_11_eq line 141
def OAI.SharpPlanar.CachedData.transStep_r2_12 line 142
lemma OAI.SharpPlanar.CachedData.transStep_r2_12_eq line 143
def OAI.SharpPlanar.CachedData.transStep_r2_13 line 144
lemma OAI.SharpPlanar.CachedData.transStep_r2_13_eq line 145
def OAI.SharpPlanar.CachedData.transStep_r2_14 line 146
lemma OAI.SharpPlanar.CachedData.transStep_r2_14_eq line 147
def OAI.SharpPlanar.CachedData.transStep_r2_15 line 148
lemma OAI.SharpPlanar.CachedData.transStep_r2_15_eq line 149
def OAI.SharpPlanar.CachedData.transStep_r2 line 150
lemma OAI.SharpPlanar.CachedData.transStep_r2_eq line 151
def OAI.SharpPlanar.CachedData.transStep_r3_0 line 169
lemma OAI.SharpPlanar.CachedData.transStep_r3_0_eq line 170
def OAI.SharpPlanar.CachedData.transStep_r3_1 line 171
lemma OAI.SharpPlanar.CachedData.transStep_r3_1_eq line 172
def OAI.SharpPlanar.CachedData.transStep_r3_2 line 173
lemma OAI.SharpPlanar.CachedData.transStep_r3_2_eq line 174
def OAI.SharpPlanar.CachedData.transStep_r3_3 line 175
lemma OAI.SharpPlanar.CachedData.transStep_r3_3_eq line 176
def OAI.SharpPlanar.CachedData.transStep_r3_4 line 177
lemma OAI.SharpPlanar.CachedData.transStep_r3_4_eq line 178
def OAI.SharpPlanar.CachedData.transStep_r3_5 line 179
lemma OAI.SharpPlanar.CachedData.transStep_r3_5_eq line 180
def OAI.SharpPlanar.CachedData.transStep_r3_6 line 181
lemma OAI.SharpPlanar.CachedData.transStep_r3_6_eq line 182
def OAI.SharpPlanar.CachedData.transStep_r3_7 line 183
lemma OAI.SharpPlanar.CachedData.transStep_r3_7_eq line 184
def OAI.SharpPlanar.CachedData.transStep_r3_8 line 185
lemma OAI.SharpPlanar.CachedData.transStep_r3_8_eq line 186
def OAI.SharpPlanar.CachedData.transStep_r3_9 line 187
lemma OAI.SharpPlanar.CachedData.transStep_r3_9_eq line 188
def OAI.SharpPlanar.CachedData.transStep_r3_10 line 189
lemma OAI.SharpPlanar.CachedData.transStep_r3_10_eq line 190
def OAI.SharpPlanar.CachedData.transStep_r3_11 line 191
lemma OAI.SharpPlanar.CachedData.transStep_r3_11_eq line 192
def OAI.SharpPlanar.CachedData.transStep_r3_12 line 193
lemma OAI.SharpPlanar.CachedData.transStep_r3_12_eq line 194
def OAI.SharpPlanar.CachedData.transStep_r3_13 line 195
lemma OAI.SharpPlanar.CachedData.transStep_r3_13_eq line 196
def OAI.SharpPlanar.CachedData.transStep_r3_14 line 197
lemma OAI.SharpPlanar.CachedData.transStep_r3_14_eq line 198
def OAI.SharpPlanar.CachedData.transStep_r3_15 line 199
lemma OAI.SharpPlanar.CachedData.transStep_r3_15_eq line 200
def OAI.SharpPlanar.CachedData.transStep_r3 line 201
lemma OAI.SharpPlanar.CachedData.transStep_r3_eq line 202
def OAI.SharpPlanar.CachedData.transStep_r4_0 line 220
lemma OAI.SharpPlanar.CachedData.transStep_r4_0_eq line 221
def OAI.SharpPlanar.CachedData.transStep_r4_1 line 222
lemma OAI.SharpPlanar.CachedData.transStep_r4_1_eq line 223
def OAI.SharpPlanar.CachedData.transStep_r4_2 line 224
lemma OAI.SharpPlanar.CachedData.transStep_r4_2_eq line 225
def OAI.SharpPlanar.CachedData.transStep_r4_3 line 226
lemma OAI.SharpPlanar.CachedData.transStep_r4_3_eq line 227
def OAI.SharpPlanar.CachedData.transStep_r4_4 line 228
lemma OAI.SharpPlanar.CachedData.transStep_r4_4_eq line 229
def OAI.SharpPlanar.CachedData.transStep_r4_5 line 230
lemma OAI.SharpPlanar.CachedData.transStep_r4_5_eq line 231
def OAI.SharpPlanar.CachedData.transStep_r4_6 line 232
lemma OAI.SharpPlanar.CachedData.transStep_r4_6_eq line 233
def OAI.SharpPlanar.CachedData.transStep_r4_7 line 234
lemma OAI.SharpPlanar.CachedData.transStep_r4_7_eq line 235
def OAI.SharpPlanar.CachedData.transStep_r4_8 line 236
lemma OAI.SharpPlanar.CachedData.transStep_r4_8_eq line 237
def OAI.SharpPlanar.CachedData.transStep_r4_9 line 238
lemma OAI.SharpPlanar.CachedData.transStep_r4_9_eq line 239
def OAI.SharpPlanar.CachedData.transStep_r4_10 line 240
lemma OAI.SharpPlanar.CachedData.transStep_r4_10_eq line 241
def OAI.SharpPlanar.CachedData.transStep_r4_11 line 242
lemma OAI.SharpPlanar.CachedData.transStep_r4_11_eq line 243
def OAI.SharpPlanar.CachedData.transStep_r4_12 line 244
lemma OAI.SharpPlanar.CachedData.transStep_r4_12_eq line 245
def OAI.SharpPlanar.CachedData.transStep_r4_13 line 246
lemma OAI.SharpPlanar.CachedData.transStep_r4_13_eq line 247
def OAI.SharpPlanar.CachedData.transStep_r4_14 line 248
lemma OAI.SharpPlanar.CachedData.transStep_r4_14_eq line 249
def OAI.SharpPlanar.CachedData.transStep_r4_15 line 250
lemma OAI.SharpPlanar.CachedData.transStep_r4_15_eq line 251
def OAI.SharpPlanar.CachedData.transStep_r4 line 252
lemma OAI.SharpPlanar.CachedData.transStep_r4_eq line 253
def OAI.SharpPlanar.CachedData.transStep_r5_0 line 271
lemma OAI.SharpPlanar.CachedData.transStep_r5_0_eq line 272
def OAI.SharpPlanar.CachedData.transStep_r5_1 line 273
lemma OAI.SharpPlanar.CachedData.transStep_r5_1_eq line 274
def OAI.SharpPlanar.CachedData.transStep_r5_2 line 275
lemma OAI.SharpPlanar.CachedData.transStep_r5_2_eq line 276
def OAI.SharpPlanar.CachedData.transStep_r5_3 line 277
lemma OAI.SharpPlanar.CachedData.transStep_r5_3_eq line 278
def OAI.SharpPlanar.CachedData.transStep_r5_4 line 279
lemma OAI.SharpPlanar.CachedData.transStep_r5_4_eq line 280
def OAI.SharpPlanar.CachedData.transStep_r5_5 line 281
lemma OAI.SharpPlanar.CachedData.transStep_r5_5_eq line 282
def OAI.SharpPlanar.CachedData.transStep_r5_6 line 283
lemma OAI.SharpPlanar.CachedData.transStep_r5_6_eq line 284
def OAI.SharpPlanar.CachedData.transStep_r5_7 line 285
lemma OAI.SharpPlanar.CachedData.transStep_r5_7_eq line 286
def OAI.SharpPlanar.CachedData.transStep_r5_8 line 287
lemma OAI.SharpPlanar.CachedData.transStep_r5_8_eq line 288
def OAI.SharpPlanar.CachedData.transStep_r5_9 line 289
lemma OAI.SharpPlanar.CachedData.transStep_r5_9_eq line 290
def OAI.SharpPlanar.CachedData.transStep_r5_10 line 291
lemma OAI.SharpPlanar.CachedData.transStep_r5_10_eq line 292
def OAI.SharpPlanar.CachedData.transStep_r5_11 line 293
lemma OAI.SharpPlanar.CachedData.transStep_r5_11_eq line 294
def OAI.SharpPlanar.CachedData.transStep_r5_12 line 295
lemma OAI.SharpPlanar.CachedData.transStep_r5_12_eq line 296
def OAI.SharpPlanar.CachedData.transStep_r5_13 line 297
lemma OAI.SharpPlanar.CachedData.transStep_r5_13_eq line 298
def OAI.SharpPlanar.CachedData.transStep_r5_14 line 299
lemma OAI.SharpPlanar.CachedData.transStep_r5_14_eq line 300
def OAI.SharpPlanar.CachedData.transStep_r5_15 line 301
lemma OAI.SharpPlanar.CachedData.transStep_r5_15_eq line 302
def OAI.SharpPlanar.CachedData.transStep_r5 line 303
lemma OAI.SharpPlanar.CachedData.transStep_r5_eq line 304
def OAI.SharpPlanar.CachedData.transStep line 322
lemma OAI.SharpPlanar.CachedData.transStep_eq line 323
lemma OAI.SharpPlanar.CachedData.transStep_contains line 331
def OAI.SharpPlanar.CachedData.trans0 line 335
lemma OAI.SharpPlanar.CachedData.trans0_contains line 336
def OAI.SharpPlanar.CachedData.trans1Expr line 340
def OAI.SharpPlanar.CachedData.trans1_r0_0 line 341
lemma OAI.SharpPlanar.CachedData.trans1_r0_0_eq line 342
def OAI.SharpPlanar.CachedData.trans1_r0_1 line 343
lemma OAI.SharpPlanar.CachedData.trans1_r0_1_eq line 344
def OAI.SharpPlanar.CachedData.trans1_r0_2 line 345
lemma OAI.SharpPlanar.CachedData.trans1_r0_2_eq line 346
def OAI.SharpPlanar.CachedData.trans1_r0_3 line 347
lemma OAI.SharpPlanar.CachedData.trans1_r0_3_eq line 348
def OAI.SharpPlanar.CachedData.trans1_r0_4 line 349
lemma OAI.SharpPlanar.CachedData.trans1_r0_4_eq line 350
def OAI.SharpPlanar.CachedData.trans1_r0_5 line 351
lemma OAI.SharpPlanar.CachedData.trans1_r0_5_eq line 352
def OAI.SharpPlanar.CachedData.trans1_r0_6 line 353
lemma OAI.SharpPlanar.CachedData.trans1_r0_6_eq line 354
def OAI.SharpPlanar.CachedData.trans1_r0_7 line 355
lemma OAI.SharpPlanar.CachedData.trans1_r0_7_eq line 356
def OAI.SharpPlanar.CachedData.trans1_r0_8 line 357
lemma OAI.SharpPlanar.CachedData.trans1_r0_8_eq line 358
def OAI.SharpPlanar.CachedData.trans1_r0_9 line 359
lemma OAI.SharpPlanar.CachedData.trans1_r0_9_eq line 360
def OAI.SharpPlanar.CachedData.trans1_r0_10 line 361
lemma OAI.SharpPlanar.CachedData.trans1_r0_10_eq line 362
def OAI.SharpPlanar.CachedData.trans1_r0_11 line 363
lemma OAI.SharpPlanar.CachedData.trans1_r0_11_eq line 364
def OAI.SharpPlanar.CachedData.trans1_r0_12 line 365
lemma OAI.SharpPlanar.CachedData.trans1_r0_12_eq line 366
def OAI.SharpPlanar.CachedData.trans1_r0_13 line 367
lemma OAI.SharpPlanar.CachedData.trans1_r0_13_eq line 368
def OAI.SharpPlanar.CachedData.trans1_r0_14 line 369
lemma OAI.SharpPlanar.CachedData.trans1_r0_14_eq line 370
def OAI.SharpPlanar.CachedData.trans1_r0_15 line 371
lemma OAI.SharpPlanar.CachedData.trans1_r0_15_eq line 372
def OAI.SharpPlanar.CachedData.trans1_r0 line 373
lemma OAI.SharpPlanar.CachedData.trans1_r0_eq line 374
def OAI.SharpPlanar.CachedData.trans1_r1_0 line 392
lemma OAI.SharpPlanar.CachedData.trans1_r1_0_eq line 393
def OAI.SharpPlanar.CachedData.trans1_r1_1 line 394
lemma OAI.SharpPlanar.CachedData.trans1_r1_1_eq line 395
def OAI.SharpPlanar.CachedData.trans1_r1_2 line 396
lemma OAI.SharpPlanar.CachedData.trans1_r1_2_eq line 397
def OAI.SharpPlanar.CachedData.trans1_r1_3 line 398
lemma OAI.SharpPlanar.CachedData.trans1_r1_3_eq line 399
def OAI.SharpPlanar.CachedData.trans1_r1_4 line 400
lemma OAI.SharpPlanar.CachedData.trans1_r1_4_eq line 401
def OAI.SharpPlanar.CachedData.trans1_r1_5 line 402
lemma OAI.SharpPlanar.CachedData.trans1_r1_5_eq line 403
def OAI.SharpPlanar.CachedData.trans1_r1_6 line 404
lemma OAI.SharpPlanar.CachedData.trans1_r1_6_eq line 405
def OAI.SharpPlanar.CachedData.trans1_r1_7 line 406
lemma OAI.SharpPlanar.CachedData.trans1_r1_7_eq line 407
def OAI.SharpPlanar.CachedData.trans1_r1_8 line 408
lemma OAI.SharpPlanar.CachedData.trans1_r1_8_eq line 409
def OAI.SharpPlanar.CachedData.trans1_r1_9 line 410
lemma OAI.SharpPlanar.CachedData.trans1_r1_9_eq line 411
def OAI.SharpPlanar.CachedData.trans1_r1_10 line 412
lemma OAI.SharpPlanar.CachedData.trans1_r1_10_eq line 413
def OAI.SharpPlanar.CachedData.trans1_r1_11 line 414
lemma OAI.SharpPlanar.CachedData.trans1_r1_11_eq line 415
def OAI.SharpPlanar.CachedData.trans1_r1_12 line 416
lemma OAI.SharpPlanar.CachedData.trans1_r1_12_eq line 417
def OAI.SharpPlanar.CachedData.trans1_r1_13 line 418
lemma OAI.SharpPlanar.CachedData.trans1_r1_13_eq line 419
def OAI.SharpPlanar.CachedData.trans1_r1_14 line 420
lemma OAI.SharpPlanar.CachedData.trans1_r1_14_eq line 421
def OAI.SharpPlanar.CachedData.trans1_r1_15 line 422
lemma OAI.SharpPlanar.CachedData.trans1_r1_15_eq line 423
def OAI.SharpPlanar.CachedData.trans1_r1 line 424
lemma OAI.SharpPlanar.CachedData.trans1_r1_eq line 425
def OAI.SharpPlanar.CachedData.trans1_r2_0 line 443
lemma OAI.SharpPlanar.CachedData.trans1_r2_0_eq line 444
def OAI.SharpPlanar.CachedData.trans1_r2_1 line 445
lemma OAI.SharpPlanar.CachedData.trans1_r2_1_eq line 446
def OAI.SharpPlanar.CachedData.trans1_r2_2 line 447
lemma OAI.SharpPlanar.CachedData.trans1_r2_2_eq line 448
def OAI.SharpPlanar.CachedData.trans1_r2_3 line 449
lemma OAI.SharpPlanar.CachedData.trans1_r2_3_eq line 450
def OAI.SharpPlanar.CachedData.trans1_r2_4 line 451
lemma OAI.SharpPlanar.CachedData.trans1_r2_4_eq line 452
def OAI.SharpPlanar.CachedData.trans1_r2_5 line 453
lemma OAI.SharpPlanar.CachedData.trans1_r2_5_eq line 454
def OAI.SharpPlanar.CachedData.trans1_r2_6 line 455
lemma OAI.SharpPlanar.CachedData.trans1_r2_6_eq line 456
def OAI.SharpPlanar.CachedData.trans1_r2_7 line 457
lemma OAI.SharpPlanar.CachedData.trans1_r2_7_eq line 458
def OAI.SharpPlanar.CachedData.trans1_r2_8 line 459
lemma OAI.SharpPlanar.CachedData.trans1_r2_8_eq line 460
def OAI.SharpPlanar.CachedData.trans1_r2_9 line 461
lemma OAI.SharpPlanar.CachedData.trans1_r2_9_eq line 462
def OAI.SharpPlanar.CachedData.trans1_r2_10 line 463
lemma OAI.SharpPlanar.CachedData.trans1_r2_10_eq line 464
def OAI.SharpPlanar.CachedData.trans1_r2_11 line 465
lemma OAI.SharpPlanar.CachedData.trans1_r2_11_eq line 466
def OAI.SharpPlanar.CachedData.trans1_r2_12 line 467
lemma OAI.SharpPlanar.CachedData.trans1_r2_12_eq line 468
def OAI.SharpPlanar.CachedData.trans1_r2_13 line 469
lemma OAI.SharpPlanar.CachedData.trans1_r2_13_eq line 470
def OAI.SharpPlanar.CachedData.trans1_r2_14 line 471
lemma OAI.SharpPlanar.CachedData.trans1_r2_14_eq line 472
def OAI.SharpPlanar.CachedData.trans1_r2_15 line 473
lemma OAI.SharpPlanar.CachedData.trans1_r2_15_eq line 474
def OAI.SharpPlanar.CachedData.trans1_r2 line 475
lemma OAI.SharpPlanar.CachedData.trans1_r2_eq line 476
def OAI.SharpPlanar.CachedData.trans1_r3_0 line 494
lemma OAI.SharpPlanar.CachedData.trans1_r3_0_eq line 495
def OAI.SharpPlanar.CachedData.trans1_r3_1 line 496
lemma OAI.SharpPlanar.CachedData.trans1_r3_1_eq line 497
def OAI.SharpPlanar.CachedData.trans1_r3_2 line 498
lemma OAI.SharpPlanar.CachedData.trans1_r3_2_eq line 499
def OAI.SharpPlanar.CachedData.trans1_r3_3 line 500
lemma OAI.SharpPlanar.CachedData.trans1_r3_3_eq line 501
def OAI.SharpPlanar.CachedData.trans1_r3_4 line 502
lemma OAI.SharpPlanar.CachedData.trans1_r3_4_eq line 503
def OAI.SharpPlanar.CachedData.trans1_r3_5 line 504
lemma OAI.SharpPlanar.CachedData.trans1_r3_5_eq line 505
def OAI.SharpPlanar.CachedData.trans1_r3_6 line 506
lemma OAI.SharpPlanar.CachedData.trans1_r3_6_eq line 507
def OAI.SharpPlanar.CachedData.trans1_r3_7 line 508
lemma OAI.SharpPlanar.CachedData.trans1_r3_7_eq line 509
def OAI.SharpPlanar.CachedData.trans1_r3_8 line 510
lemma OAI.SharpPlanar.CachedData.trans1_r3_8_eq line 511
def OAI.SharpPlanar.CachedData.trans1_r3_9 line 512
lemma OAI.SharpPlanar.CachedData.trans1_r3_9_eq line 513
def OAI.SharpPlanar.CachedData.trans1_r3_10 line 514
lemma OAI.SharpPlanar.CachedData.trans1_r3_10_eq line 515
def OAI.SharpPlanar.CachedData.trans1_r3_11 line 516
lemma OAI.SharpPlanar.CachedData.trans1_r3_11_eq line 517
def OAI.SharpPlanar.CachedData.trans1_r3_12 line 518
lemma OAI.SharpPlanar.CachedData.trans1_r3_12_eq line 519
def OAI.SharpPlanar.CachedData.trans1_r3_13 line 520
lemma OAI.SharpPlanar.CachedData.trans1_r3_13_eq line 521
def OAI.SharpPlanar.CachedData.trans1_r3_14 line 522
lemma OAI.SharpPlanar.CachedData.trans1_r3_14_eq line 523
def OAI.SharpPlanar.CachedData.trans1_r3_15 line 524
lemma OAI.SharpPlanar.CachedData.trans1_r3_15_eq line 525
def OAI.SharpPlanar.CachedData.trans1_r3 line 526
lemma OAI.SharpPlanar.CachedData.trans1_r3_eq line 527
def OAI.SharpPlanar.CachedData.trans1_r4_0 line 545
lemma OAI.SharpPlanar.CachedData.trans1_r4_0_eq line 546
def OAI.SharpPlanar.CachedData.trans1_r4_1 line 547
lemma OAI.SharpPlanar.CachedData.trans1_r4_1_eq line 548
def OAI.SharpPlanar.CachedData.trans1_r4_2 line 549
lemma OAI.SharpPlanar.CachedData.trans1_r4_2_eq line 550
def OAI.SharpPlanar.CachedData.trans1_r4_3 line 551
lemma OAI.SharpPlanar.CachedData.trans1_r4_3_eq line 552
def OAI.SharpPlanar.CachedData.trans1_r4_4 line 553
lemma OAI.SharpPlanar.CachedData.trans1_r4_4_eq line 554
def OAI.SharpPlanar.CachedData.trans1_r4_5 line 555
lemma OAI.SharpPlanar.CachedData.trans1_r4_5_eq line 556
def OAI.SharpPlanar.CachedData.trans1_r4_6 line 557
lemma OAI.SharpPlanar.CachedData.trans1_r4_6_eq line 558
def OAI.SharpPlanar.CachedData.trans1_r4_7 line 559
lemma OAI.SharpPlanar.CachedData.trans1_r4_7_eq line 560
def OAI.SharpPlanar.CachedData.trans1_r4_8 line 561
lemma OAI.SharpPlanar.CachedData.trans1_r4_8_eq line 562
def OAI.SharpPlanar.CachedData.trans1_r4_9 line 563
lemma OAI.SharpPlanar.CachedData.trans1_r4_9_eq line 564
def OAI.SharpPlanar.CachedData.trans1_r4_10 line 565
lemma OAI.SharpPlanar.CachedData.trans1_r4_10_eq line 566
def OAI.SharpPlanar.CachedData.trans1_r4_11 line 567
lemma OAI.SharpPlanar.CachedData.trans1_r4_11_eq line 568
def OAI.SharpPlanar.CachedData.trans1_r4_12 line 569
lemma OAI.SharpPlanar.CachedData.trans1_r4_12_eq line 570
def OAI.SharpPlanar.CachedData.trans1_r4_13 line 571
lemma OAI.SharpPlanar.CachedData.trans1_r4_13_eq line 572
def OAI.SharpPlanar.CachedData.trans1_r4_14 line 573
lemma OAI.SharpPlanar.CachedData.trans1_r4_14_eq line 574
def OAI.SharpPlanar.CachedData.trans1_r4_15 line 575
lemma OAI.SharpPlanar.CachedData.trans1_r4_15_eq line 576
def OAI.SharpPlanar.CachedData.trans1_r4 line 577
lemma OAI.SharpPlanar.CachedData.trans1_r4_eq line 578
def OAI.SharpPlanar.CachedData.trans1_r5_0 line 596
lemma OAI.SharpPlanar.CachedData.trans1_r5_0_eq line 597
def OAI.SharpPlanar.CachedData.trans1_r5_1 line 598
lemma OAI.SharpPlanar.CachedData.trans1_r5_1_eq line 599
def OAI.SharpPlanar.CachedData.trans1_r5_2 line 600
lemma OAI.SharpPlanar.CachedData.trans1_r5_2_eq line 601
def OAI.SharpPlanar.CachedData.trans1_r5_3 line 602
lemma OAI.SharpPlanar.CachedData.trans1_r5_3_eq line 603
def OAI.SharpPlanar.CachedData.trans1_r5_4 line 604
lemma OAI.SharpPlanar.CachedData.trans1_r5_4_eq line 605
def OAI.SharpPlanar.CachedData.trans1_r5_5 line 606
lemma OAI.SharpPlanar.CachedData.trans1_r5_5_eq line 607
def OAI.SharpPlanar.CachedData.trans1_r5_6 line 608
lemma OAI.SharpPlanar.CachedData.trans1_r5_6_eq line 609
def OAI.SharpPlanar.CachedData.trans1_r5_7 line 610
lemma OAI.SharpPlanar.CachedData.trans1_r5_7_eq line 611
def OAI.SharpPlanar.CachedData.trans1_r5_8 line 612
lemma OAI.SharpPlanar.CachedData.trans1_r5_8_eq line 613
def OAI.SharpPlanar.CachedData.trans1_r5_9 line 614
lemma OAI.SharpPlanar.CachedData.trans1_r5_9_eq line 615
def OAI.SharpPlanar.CachedData.trans1_r5_10 line 616
lemma OAI.SharpPlanar.CachedData.trans1_r5_10_eq line 617
def OAI.SharpPlanar.CachedData.trans1_r5_11 line 618
lemma OAI.SharpPlanar.CachedData.trans1_r5_11_eq line 619
def OAI.SharpPlanar.CachedData.trans1_r5_12 line 620
lemma OAI.SharpPlanar.CachedData.trans1_r5_12_eq line 621
def OAI.SharpPlanar.CachedData.trans1_r5_13 line 622
lemma OAI.SharpPlanar.CachedData.trans1_r5_13_eq line 623
def OAI.SharpPlanar.CachedData.trans1_r5_14 line 624
lemma OAI.SharpPlanar.CachedData.trans1_r5_14_eq line 625
def OAI.SharpPlanar.CachedData.trans1_r5_15 line 626
lemma OAI.SharpPlanar.CachedData.trans1_r5_15_eq line 627
def OAI.SharpPlanar.CachedData.trans1_r5 line 628
lemma OAI.SharpPlanar.CachedData.trans1_r5_eq line 629
def OAI.SharpPlanar.CachedData.trans1 line 647
lemma OAI.SharpPlanar.CachedData.trans1_eq line 648
lemma OAI.SharpPlanar.CachedData.trans1_contains line 656
def OAI.SharpPlanar.CachedData.trans2Expr line 661
def OAI.SharpPlanar.CachedData.trans2_r0_0 line 662
lemma OAI.SharpPlanar.CachedData.trans2_r0_0_eq line 663
def OAI.SharpPlanar.CachedData.trans2_r0_1 line 664
lemma OAI.SharpPlanar.CachedData.trans2_r0_1_eq line 665
def OAI.SharpPlanar.CachedData.trans2_r0_2 line 666
lemma OAI.SharpPlanar.CachedData.trans2_r0_2_eq line 667
def OAI.SharpPlanar.CachedData.trans2_r0_3 line 668
lemma OAI.SharpPlanar.CachedData.trans2_r0_3_eq line 669
def OAI.SharpPlanar.CachedData.trans2_r0_4 line 670
lemma OAI.SharpPlanar.CachedData.trans2_r0_4_eq line 671
def OAI.SharpPlanar.CachedData.trans2_r0_5 line 672
lemma OAI.SharpPlanar.CachedData.trans2_r0_5_eq line 673
def OAI.SharpPlanar.CachedData.trans2_r0_6 line 674
lemma OAI.SharpPlanar.CachedData.trans2_r0_6_eq line 675
def OAI.SharpPlanar.CachedData.trans2_r0_7 line 676
lemma OAI.SharpPlanar.CachedData.trans2_r0_7_eq line 677
def OAI.SharpPlanar.CachedData.trans2_r0_8 line 678
lemma OAI.SharpPlanar.CachedData.trans2_r0_8_eq line 679
def OAI.SharpPlanar.CachedData.trans2_r0_9 line 680
lemma OAI.SharpPlanar.CachedData.trans2_r0_9_eq line 681
def OAI.SharpPlanar.CachedData.trans2_r0_10 line 682
lemma OAI.SharpPlanar.CachedData.trans2_r0_10_eq line 683
def OAI.SharpPlanar.CachedData.trans2_r0_11 line 684
lemma OAI.SharpPlanar.CachedData.trans2_r0_11_eq line 685
def OAI.SharpPlanar.CachedData.trans2_r0_12 line 686
lemma OAI.SharpPlanar.CachedData.trans2_r0_12_eq line 687
def OAI.SharpPlanar.CachedData.trans2_r0_13 line 688
lemma OAI.SharpPlanar.CachedData.trans2_r0_13_eq line 689
def OAI.SharpPlanar.CachedData.trans2_r0_14 line 690
lemma OAI.SharpPlanar.CachedData.trans2_r0_14_eq line 691
def OAI.SharpPlanar.CachedData.trans2_r0_15 line 692
lemma OAI.SharpPlanar.CachedData.trans2_r0_15_eq line 693
def OAI.SharpPlanar.CachedData.trans2_r0 line 694
lemma OAI.SharpPlanar.CachedData.trans2_r0_eq line 695
def OAI.SharpPlanar.CachedData.trans2_r1_0 line 713
lemma OAI.SharpPlanar.CachedData.trans2_r1_0_eq line 714
def OAI.SharpPlanar.CachedData.trans2_r1_1 line 715
lemma OAI.SharpPlanar.CachedData.trans2_r1_1_eq line 716
def OAI.SharpPlanar.CachedData.trans2_r1_2 line 717
lemma OAI.SharpPlanar.CachedData.trans2_r1_2_eq line 718
def OAI.SharpPlanar.CachedData.trans2_r1_3 line 719
lemma OAI.SharpPlanar.CachedData.trans2_r1_3_eq line 720
def OAI.SharpPlanar.CachedData.trans2_r1_4 line 721
lemma OAI.SharpPlanar.CachedData.trans2_r1_4_eq line 722
def OAI.SharpPlanar.CachedData.trans2_r1_5 line 723
lemma OAI.SharpPlanar.CachedData.trans2_r1_5_eq line 724
def OAI.SharpPlanar.CachedData.trans2_r1_6 line 725
lemma OAI.SharpPlanar.CachedData.trans2_r1_6_eq line 726
def OAI.SharpPlanar.CachedData.trans2_r1_7 line 727
lemma OAI.SharpPlanar.CachedData.trans2_r1_7_eq line 728
def OAI.SharpPlanar.CachedData.trans2_r1_8 line 729
lemma OAI.SharpPlanar.CachedData.trans2_r1_8_eq line 730
def OAI.SharpPlanar.CachedData.trans2_r1_9 line 731
lemma OAI.SharpPlanar.CachedData.trans2_r1_9_eq line 732
def OAI.SharpPlanar.CachedData.trans2_r1_10 line 733
lemma OAI.SharpPlanar.CachedData.trans2_r1_10_eq line 734
def OAI.SharpPlanar.CachedData.trans2_r1_11 line 735
lemma OAI.SharpPlanar.CachedData.trans2_r1_11_eq line 736
def OAI.SharpPlanar.CachedData.trans2_r1_12 line 737
lemma OAI.SharpPlanar.CachedData.trans2_r1_12_eq line 738
def OAI.SharpPlanar.CachedData.trans2_r1_13 line 739
lemma OAI.SharpPlanar.CachedData.trans2_r1_13_eq line 740
def OAI.SharpPlanar.CachedData.trans2_r1_14 line 741
lemma OAI.SharpPlanar.CachedData.trans2_r1_14_eq line 742
def OAI.SharpPlanar.CachedData.trans2_r1_15 line 743
lemma OAI.SharpPlanar.CachedData.trans2_r1_15_eq line 744
def OAI.SharpPlanar.CachedData.trans2_r1 line 745
lemma OAI.SharpPlanar.CachedData.trans2_r1_eq line 746
def OAI.SharpPlanar.CachedData.trans2_r2_0 line 764
lemma OAI.SharpPlanar.CachedData.trans2_r2_0_eq line 765
def OAI.SharpPlanar.CachedData.trans2_r2_1 line 766
lemma OAI.SharpPlanar.CachedData.trans2_r2_1_eq line 767
def OAI.SharpPlanar.CachedData.trans2_r2_2 line 768
lemma OAI.SharpPlanar.CachedData.trans2_r2_2_eq line 769
def OAI.SharpPlanar.CachedData.trans2_r2_3 line 770
lemma OAI.SharpPlanar.CachedData.trans2_r2_3_eq line 771
def OAI.SharpPlanar.CachedData.trans2_r2_4 line 772
lemma OAI.SharpPlanar.CachedData.trans2_r2_4_eq line 773
def OAI.SharpPlanar.CachedData.trans2_r2_5 line 774
lemma OAI.SharpPlanar.CachedData.trans2_r2_5_eq line 775
def OAI.SharpPlanar.CachedData.trans2_r2_6 line 776
lemma OAI.SharpPlanar.CachedData.trans2_r2_6_eq line 777
def OAI.SharpPlanar.CachedData.trans2_r2_7 line 778
lemma OAI.SharpPlanar.CachedData.trans2_r2_7_eq line 779
def OAI.SharpPlanar.CachedData.trans2_r2_8 line 780
lemma OAI.SharpPlanar.CachedData.trans2_r2_8_eq line 781
def OAI.SharpPlanar.CachedData.trans2_r2_9 line 782
lemma OAI.SharpPlanar.CachedData.trans2_r2_9_eq line 783
def OAI.SharpPlanar.CachedData.trans2_r2_10 line 784
lemma OAI.SharpPlanar.CachedData.trans2_r2_10_eq line 785
def OAI.SharpPlanar.CachedData.trans2_r2_11 line 786
lemma OAI.SharpPlanar.CachedData.trans2_r2_11_eq line 787
def OAI.SharpPlanar.CachedData.trans2_r2_12 line 788
lemma OAI.SharpPlanar.CachedData.trans2_r2_12_eq line 789
def OAI.SharpPlanar.CachedData.trans2_r2_13 line 790
lemma OAI.SharpPlanar.CachedData.trans2_r2_13_eq line 791
def OAI.SharpPlanar.CachedData.trans2_r2_14 line 792
lemma OAI.SharpPlanar.CachedData.trans2_r2_14_eq line 793
def OAI.SharpPlanar.CachedData.trans2_r2_15 line 794
lemma OAI.SharpPlanar.CachedData.trans2_r2_15_eq line 795
def OAI.SharpPlanar.CachedData.trans2_r2 line 796
lemma OAI.SharpPlanar.CachedData.trans2_r2_eq line 797
def OAI.SharpPlanar.CachedData.trans2_r3_0 line 815
lemma OAI.SharpPlanar.CachedData.trans2_r3_0_eq line 816
def OAI.SharpPlanar.CachedData.trans2_r3_1 line 817
lemma OAI.SharpPlanar.CachedData.trans2_r3_1_eq line 818
def OAI.SharpPlanar.CachedData.trans2_r3_2 line 819
lemma OAI.SharpPlanar.CachedData.trans2_r3_2_eq line 820
def OAI.SharpPlanar.CachedData.trans2_r3_3 line 821
lemma OAI.SharpPlanar.CachedData.trans2_r3_3_eq line 822
def OAI.SharpPlanar.CachedData.trans2_r3_4 line 823
lemma OAI.SharpPlanar.CachedData.trans2_r3_4_eq line 824
def OAI.SharpPlanar.CachedData.trans2_r3_5 line 825
lemma OAI.SharpPlanar.CachedData.trans2_r3_5_eq line 826
def OAI.SharpPlanar.CachedData.trans2_r3_6 line 827
lemma OAI.SharpPlanar.CachedData.trans2_r3_6_eq line 828
def OAI.SharpPlanar.CachedData.trans2_r3_7 line 829
lemma OAI.SharpPlanar.CachedData.trans2_r3_7_eq line 830
def OAI.SharpPlanar.CachedData.trans2_r3_8 line 831
lemma OAI.SharpPlanar.CachedData.trans2_r3_8_eq line 832
def OAI.SharpPlanar.CachedData.trans2_r3_9 line 833
lemma OAI.SharpPlanar.CachedData.trans2_r3_9_eq line 834
def OAI.SharpPlanar.CachedData.trans2_r3_10 line 835
lemma OAI.SharpPlanar.CachedData.trans2_r3_10_eq line 836
def OAI.SharpPlanar.CachedData.trans2_r3_11 line 837
lemma OAI.SharpPlanar.CachedData.trans2_r3_11_eq line 838
def OAI.SharpPlanar.CachedData.trans2_r3_12 line 839
lemma OAI.SharpPlanar.CachedData.trans2_r3_12_eq line 840
def OAI.SharpPlanar.CachedData.trans2_r3_13 line 841
lemma OAI.SharpPlanar.CachedData.trans2_r3_13_eq line 842
def OAI.SharpPlanar.CachedData.trans2_r3_14 line 843
lemma OAI.SharpPlanar.CachedData.trans2_r3_14_eq line 844
def OAI.SharpPlanar.CachedData.trans2_r3_15 line 845
lemma OAI.SharpPlanar.CachedData.trans2_r3_15_eq line 846
def OAI.SharpPlanar.CachedData.trans2_r3 line 847
lemma OAI.SharpPlanar.CachedData.trans2_r3_eq line 848
def OAI.SharpPlanar.CachedData.trans2_r4_0 line 866
lemma OAI.SharpPlanar.CachedData.trans2_r4_0_eq line 867
def OAI.SharpPlanar.CachedData.trans2_r4_1 line 868
lemma OAI.SharpPlanar.CachedData.trans2_r4_1_eq line 869
def OAI.SharpPlanar.CachedData.trans2_r4_2 line 870
lemma OAI.SharpPlanar.CachedData.trans2_r4_2_eq line 871
def OAI.SharpPlanar.CachedData.trans2_r4_3 line 872
lemma OAI.SharpPlanar.CachedData.trans2_r4_3_eq line 873
def OAI.SharpPlanar.CachedData.trans2_r4_4 line 874
lemma OAI.SharpPlanar.CachedData.trans2_r4_4_eq line 875
def OAI.SharpPlanar.CachedData.trans2_r4_5 line 876
lemma OAI.SharpPlanar.CachedData.trans2_r4_5_eq line 877
def OAI.SharpPlanar.CachedData.trans2_r4_6 line 878
lemma OAI.SharpPlanar.CachedData.trans2_r4_6_eq line 879
def OAI.SharpPlanar.CachedData.trans2_r4_7 line 880
lemma OAI.SharpPlanar.CachedData.trans2_r4_7_eq line 881
def OAI.SharpPlanar.CachedData.trans2_r4_8 line 882
lemma OAI.SharpPlanar.CachedData.trans2_r4_8_eq line 883
def OAI.SharpPlanar.CachedData.trans2_r4_9 line 884
lemma OAI.SharpPlanar.CachedData.trans2_r4_9_eq line 885
def OAI.SharpPlanar.CachedData.trans2_r4_10 line 886
lemma OAI.SharpPlanar.CachedData.trans2_r4_10_eq line 887
def OAI.SharpPlanar.CachedData.trans2_r4_11 line 888
lemma OAI.SharpPlanar.CachedData.trans2_r4_11_eq line 889
def OAI.SharpPlanar.CachedData.trans2_r4_12 line 890
lemma OAI.SharpPlanar.CachedData.trans2_r4_12_eq line 891
def OAI.SharpPlanar.CachedData.trans2_r4_13 line 892
lemma OAI.SharpPlanar.CachedData.trans2_r4_13_eq line 893
def OAI.SharpPlanar.CachedData.trans2_r4_14 line 894
lemma OAI.SharpPlanar.CachedData.trans2_r4_14_eq line 895
def OAI.SharpPlanar.CachedData.trans2_r4_15 line 896
lemma OAI.SharpPlanar.CachedData.trans2_r4_15_eq line 897
def OAI.SharpPlanar.CachedData.trans2_r4 line 898
lemma OAI.SharpPlanar.CachedData.trans2_r4_eq line 899
def OAI.SharpPlanar.CachedData.trans2_r5_0 line 917
lemma OAI.SharpPlanar.CachedData.trans2_r5_0_eq line 918
def OAI.SharpPlanar.CachedData.trans2_r5_1 line 919
lemma OAI.SharpPlanar.CachedData.trans2_r5_1_eq line 920
def OAI.SharpPlanar.CachedData.trans2_r5_2 line 921
lemma OAI.SharpPlanar.CachedData.trans2_r5_2_eq line 922
def OAI.SharpPlanar.CachedData.trans2_r5_3 line 923
lemma OAI.SharpPlanar.CachedData.trans2_r5_3_eq line 924
def OAI.SharpPlanar.CachedData.trans2_r5_4 line 925
lemma OAI.SharpPlanar.CachedData.trans2_r5_4_eq line 926
def OAI.SharpPlanar.CachedData.trans2_r5_5 line 927
lemma OAI.SharpPlanar.CachedData.trans2_r5_5_eq line 928
def OAI.SharpPlanar.CachedData.trans2_r5_6 line 929
lemma OAI.SharpPlanar.CachedData.trans2_r5_6_eq line 930
def OAI.SharpPlanar.CachedData.trans2_r5_7 line 931
lemma OAI.SharpPlanar.CachedData.trans2_r5_7_eq line 932
def OAI.SharpPlanar.CachedData.trans2_r5_8 line 933
lemma OAI.SharpPlanar.CachedData.trans2_r5_8_eq line 934
def OAI.SharpPlanar.CachedData.trans2_r5_9 line 935
lemma OAI.SharpPlanar.CachedData.trans2_r5_9_eq line 936
def OAI.SharpPlanar.CachedData.trans2_r5_10 line 937
lemma OAI.SharpPlanar.CachedData.trans2_r5_10_eq line 938
def OAI.SharpPlanar.CachedData.trans2_r5_11 line 939
lemma OAI.SharpPlanar.CachedData.trans2_r5_11_eq line 940
def OAI.SharpPlanar.CachedData.trans2_r5_12 line 941
lemma OAI.SharpPlanar.CachedData.trans2_r5_12_eq line 942
def OAI.SharpPlanar.CachedData.trans2_r5_13 line 943
lemma OAI.SharpPlanar.CachedData.trans2_r5_13_eq line 944
def OAI.SharpPlanar.CachedData.trans2_r5_14 line 945
lemma OAI.SharpPlanar.CachedData.trans2_r5_14_eq line 946
def OAI.SharpPlanar.CachedData.trans2_r5_15 line 947
lemma OAI.SharpPlanar.CachedData.trans2_r5_15_eq line 948
def OAI.SharpPlanar.CachedData.trans2_r5 line 949
lemma OAI.SharpPlanar.CachedData.trans2_r5_eq line 950
def OAI.SharpPlanar.CachedData.trans2 line 968
lemma OAI.SharpPlanar.CachedData.trans2_eq line 969
lemma OAI.SharpPlanar.CachedData.trans2_contains line 977
def OAI.SharpPlanar.CachedData.trans3Expr line 982
def OAI.SharpPlanar.CachedData.trans3_r0_0 line 983
lemma OAI.SharpPlanar.CachedData.trans3_r0_0_eq line 984
def OAI.SharpPlanar.CachedData.trans3_r0_1 line 985
lemma OAI.SharpPlanar.CachedData.trans3_r0_1_eq line 986
def OAI.SharpPlanar.CachedData.trans3_r0_2 line 987
lemma OAI.SharpPlanar.CachedData.trans3_r0_2_eq line 988
def OAI.SharpPlanar.CachedData.trans3_r0_3 line 989
lemma OAI.SharpPlanar.CachedData.trans3_r0_3_eq line 990
def OAI.SharpPlanar.CachedData.trans3_r0_4 line 991
lemma OAI.SharpPlanar.CachedData.trans3_r0_4_eq line 992
def OAI.SharpPlanar.CachedData.trans3_r0_5 line 993
lemma OAI.SharpPlanar.CachedData.trans3_r0_5_eq line 994
def OAI.SharpPlanar.CachedData.trans3_r0_6 line 995
lemma OAI.SharpPlanar.CachedData.trans3_r0_6_eq line 996
def OAI.SharpPlanar.CachedData.trans3_r0_7 line 997
lemma OAI.SharpPlanar.CachedData.trans3_r0_7_eq line 998
def OAI.SharpPlanar.CachedData.trans3_r0_8 line 999
lemma OAI.SharpPlanar.CachedData.trans3_r0_8_eq line 1000
def OAI.SharpPlanar.CachedData.trans3_r0_9 line 1001
lemma OAI.SharpPlanar.CachedData.trans3_r0_9_eq line 1002
def OAI.SharpPlanar.CachedData.trans3_r0_10 line 1003
lemma OAI.SharpPlanar.CachedData.trans3_r0_10_eq line 1004
def OAI.SharpPlanar.CachedData.trans3_r0_11 line 1005
lemma OAI.SharpPlanar.CachedData.trans3_r0_11_eq line 1006
def OAI.SharpPlanar.CachedData.trans3_r0_12 line 1007
lemma OAI.SharpPlanar.CachedData.trans3_r0_12_eq line 1008
def OAI.SharpPlanar.CachedData.trans3_r0_13 line 1009
lemma OAI.SharpPlanar.CachedData.trans3_r0_13_eq line 1010
def OAI.SharpPlanar.CachedData.trans3_r0_14 line 1011
lemma OAI.SharpPlanar.CachedData.trans3_r0_14_eq line 1012
def OAI.SharpPlanar.CachedData.trans3_r0_15 line 1013
lemma OAI.SharpPlanar.CachedData.trans3_r0_15_eq line 1014
def OAI.SharpPlanar.CachedData.trans3_r0 line 1015
lemma OAI.SharpPlanar.CachedData.trans3_r0_eq line 1016
def OAI.SharpPlanar.CachedData.trans3_r1_0 line 1034
lemma OAI.SharpPlanar.CachedData.trans3_r1_0_eq line 1035
def OAI.SharpPlanar.CachedData.trans3_r1_1 line 1036
lemma OAI.SharpPlanar.CachedData.trans3_r1_1_eq line 1037
def OAI.SharpPlanar.CachedData.trans3_r1_2 line 1038
lemma OAI.SharpPlanar.CachedData.trans3_r1_2_eq line 1039
def OAI.SharpPlanar.CachedData.trans3_r1_3 line 1040
lemma OAI.SharpPlanar.CachedData.trans3_r1_3_eq line 1041
def OAI.SharpPlanar.CachedData.trans3_r1_4 line 1042
lemma OAI.SharpPlanar.CachedData.trans3_r1_4_eq line 1043
def OAI.SharpPlanar.CachedData.trans3_r1_5 line 1044
lemma OAI.SharpPlanar.CachedData.trans3_r1_5_eq line 1045
def OAI.SharpPlanar.CachedData.trans3_r1_6 line 1046
lemma OAI.SharpPlanar.CachedData.trans3_r1_6_eq line 1047
def OAI.SharpPlanar.CachedData.trans3_r1_7 line 1048
lemma OAI.SharpPlanar.CachedData.trans3_r1_7_eq line 1049
def OAI.SharpPlanar.CachedData.trans3_r1_8 line 1050
lemma OAI.SharpPlanar.CachedData.trans3_r1_8_eq line 1051
def OAI.SharpPlanar.CachedData.trans3_r1_9 line 1052
lemma OAI.SharpPlanar.CachedData.trans3_r1_9_eq line 1053
def OAI.SharpPlanar.CachedData.trans3_r1_10 line 1054
lemma OAI.SharpPlanar.CachedData.trans3_r1_10_eq line 1055
def OAI.SharpPlanar.CachedData.trans3_r1_11 line 1056
lemma OAI.SharpPlanar.CachedData.trans3_r1_11_eq line 1057
def OAI.SharpPlanar.CachedData.trans3_r1_12 line 1058
lemma OAI.SharpPlanar.CachedData.trans3_r1_12_eq line 1059
def OAI.SharpPlanar.CachedData.trans3_r1_13 line 1060
lemma OAI.SharpPlanar.CachedData.trans3_r1_13_eq line 1061
def OAI.SharpPlanar.CachedData.trans3_r1_14 line 1062
lemma OAI.SharpPlanar.CachedData.trans3_r1_14_eq line 1063
def OAI.SharpPlanar.CachedData.trans3_r1_15 line 1064
lemma OAI.SharpPlanar.CachedData.trans3_r1_15_eq line 1065
def OAI.SharpPlanar.CachedData.trans3_r1 line 1066
lemma OAI.SharpPlanar.CachedData.trans3_r1_eq line 1067
def OAI.SharpPlanar.CachedData.trans3_r2_0 line 1085
lemma OAI.SharpPlanar.CachedData.trans3_r2_0_eq line 1086
def OAI.SharpPlanar.CachedData.trans3_r2_1 line 1087
lemma OAI.SharpPlanar.CachedData.trans3_r2_1_eq line 1088
def OAI.SharpPlanar.CachedData.trans3_r2_2 line 1089
lemma OAI.SharpPlanar.CachedData.trans3_r2_2_eq line 1090
def OAI.SharpPlanar.CachedData.trans3_r2_3 line 1091
lemma OAI.SharpPlanar.CachedData.trans3_r2_3_eq line 1092
def OAI.SharpPlanar.CachedData.trans3_r2_4 line 1093
lemma OAI.SharpPlanar.CachedData.trans3_r2_4_eq line 1094
def OAI.SharpPlanar.CachedData.trans3_r2_5 line 1095
lemma OAI.SharpPlanar.CachedData.trans3_r2_5_eq line 1096
def OAI.SharpPlanar.CachedData.trans3_r2_6 line 1097
lemma OAI.SharpPlanar.CachedData.trans3_r2_6_eq line 1098
def OAI.SharpPlanar.CachedData.trans3_r2_7 line 1099
lemma OAI.SharpPlanar.CachedData.trans3_r2_7_eq line 1100
def OAI.SharpPlanar.CachedData.trans3_r2_8 line 1101
lemma OAI.SharpPlanar.CachedData.trans3_r2_8_eq line 1102
def OAI.SharpPlanar.CachedData.trans3_r2_9 line 1103
lemma OAI.SharpPlanar.CachedData.trans3_r2_9_eq line 1104
def OAI.SharpPlanar.CachedData.trans3_r2_10 line 1105
lemma OAI.SharpPlanar.CachedData.trans3_r2_10_eq line 1106
def OAI.SharpPlanar.CachedData.trans3_r2_11 line 1107
lemma OAI.SharpPlanar.CachedData.trans3_r2_11_eq line 1108
def OAI.SharpPlanar.CachedData.trans3_r2_12 line 1109
lemma OAI.SharpPlanar.CachedData.trans3_r2_12_eq line 1110
def OAI.SharpPlanar.CachedData.trans3_r2_13 line 1111
lemma OAI.SharpPlanar.CachedData.trans3_r2_13_eq line 1112
def OAI.SharpPlanar.CachedData.trans3_r2_14 line 1113
lemma OAI.SharpPlanar.CachedData.trans3_r2_14_eq line 1114
def OAI.SharpPlanar.CachedData.trans3_r2_15 line 1115
lemma OAI.SharpPlanar.CachedData.trans3_r2_15_eq line 1116
def OAI.SharpPlanar.CachedData.trans3_r2 line 1117
lemma OAI.SharpPlanar.CachedData.trans3_r2_eq line 1118
def OAI.SharpPlanar.CachedData.trans3_r3_0 line 1136
lemma OAI.SharpPlanar.CachedData.trans3_r3_0_eq line 1137
def OAI.SharpPlanar.CachedData.trans3_r3_1 line 1138
lemma OAI.SharpPlanar.CachedData.trans3_r3_1_eq line 1139
def OAI.SharpPlanar.CachedData.trans3_r3_2 line 1140
lemma OAI.SharpPlanar.CachedData.trans3_r3_2_eq line 1141
def OAI.SharpPlanar.CachedData.trans3_r3_3 line 1142
lemma OAI.SharpPlanar.CachedData.trans3_r3_3_eq line 1143
def OAI.SharpPlanar.CachedData.trans3_r3_4 line 1144
lemma OAI.SharpPlanar.CachedData.trans3_r3_4_eq line 1145
def OAI.SharpPlanar.CachedData.trans3_r3_5 line 1146
lemma OAI.SharpPlanar.CachedData.trans3_r3_5_eq line 1147
def OAI.SharpPlanar.CachedData.trans3_r3_6 line 1148
lemma OAI.SharpPlanar.CachedData.trans3_r3_6_eq line 1149
def OAI.SharpPlanar.CachedData.trans3_r3_7 line 1150
lemma OAI.SharpPlanar.CachedData.trans3_r3_7_eq line 1151
def OAI.SharpPlanar.CachedData.trans3_r3_8 line 1152
lemma OAI.SharpPlanar.CachedData.trans3_r3_8_eq line 1153
def OAI.SharpPlanar.CachedData.trans3_r3_9 line 1154
lemma OAI.SharpPlanar.CachedData.trans3_r3_9_eq line 1155
def OAI.SharpPlanar.CachedData.trans3_r3_10 line 1156
lemma OAI.SharpPlanar.CachedData.trans3_r3_10_eq line 1157
def OAI.SharpPlanar.CachedData.trans3_r3_11 line 1158
lemma OAI.SharpPlanar.CachedData.trans3_r3_11_eq line 1159
def OAI.SharpPlanar.CachedData.trans3_r3_12 line 1160
lemma OAI.SharpPlanar.CachedData.trans3_r3_12_eq line 1161
def OAI.SharpPlanar.CachedData.trans3_r3_13 line 1162
lemma OAI.SharpPlanar.CachedData.trans3_r3_13_eq line 1163
def OAI.SharpPlanar.CachedData.trans3_r3_14 line 1164
lemma OAI.SharpPlanar.CachedData.trans3_r3_14_eq line 1165
def OAI.SharpPlanar.CachedData.trans3_r3_15 line 1166
lemma OAI.SharpPlanar.CachedData.trans3_r3_15_eq line 1167
def OAI.SharpPlanar.CachedData.trans3_r3 line 1168
lemma OAI.SharpPlanar.CachedData.trans3_r3_eq line 1169
def OAI.SharpPlanar.CachedData.trans3_r4_0 line 1187
lemma OAI.SharpPlanar.CachedData.trans3_r4_0_eq line 1188
def OAI.SharpPlanar.CachedData.trans3_r4_1 line 1189
lemma OAI.SharpPlanar.CachedData.trans3_r4_1_eq line 1190
def OAI.SharpPlanar.CachedData.trans3_r4_2 line 1191
lemma OAI.SharpPlanar.CachedData.trans3_r4_2_eq line 1192
def OAI.SharpPlanar.CachedData.trans3_r4_3 line 1193
lemma OAI.SharpPlanar.CachedData.trans3_r4_3_eq line 1194
def OAI.SharpPlanar.CachedData.trans3_r4_4 line 1195
lemma OAI.SharpPlanar.CachedData.trans3_r4_4_eq line 1196
def OAI.SharpPlanar.CachedData.trans3_r4_5 line 1197
lemma OAI.SharpPlanar.CachedData.trans3_r4_5_eq line 1198
def OAI.SharpPlanar.CachedData.trans3_r4_6 line 1199
lemma OAI.SharpPlanar.CachedData.trans3_r4_6_eq line 1200
def OAI.SharpPlanar.CachedData.trans3_r4_7 line 1201
lemma OAI.SharpPlanar.CachedData.trans3_r4_7_eq line 1202
def OAI.SharpPlanar.CachedData.trans3_r4_8 line 1203
lemma OAI.SharpPlanar.CachedData.trans3_r4_8_eq line 1204
def OAI.SharpPlanar.CachedData.trans3_r4_9 line 1205
lemma OAI.SharpPlanar.CachedData.trans3_r4_9_eq line 1206
def OAI.SharpPlanar.CachedData.trans3_r4_10 line 1207
lemma OAI.SharpPlanar.CachedData.trans3_r4_10_eq line 1208
def OAI.SharpPlanar.CachedData.trans3_r4_11 line 1209
lemma OAI.SharpPlanar.CachedData.trans3_r4_11_eq line 1210
def OAI.SharpPlanar.CachedData.trans3_r4_12 line 1211
lemma OAI.SharpPlanar.CachedData.trans3_r4_12_eq line 1212
def OAI.SharpPlanar.CachedData.trans3_r4_13 line 1213
lemma OAI.SharpPlanar.CachedData.trans3_r4_13_eq line 1214
def OAI.SharpPlanar.CachedData.trans3_r4_14 line 1215
lemma OAI.SharpPlanar.CachedData.trans3_r4_14_eq line 1216
def OAI.SharpPlanar.CachedData.trans3_r4_15 line 1217
lemma OAI.SharpPlanar.CachedData.trans3_r4_15_eq line 1218
def OAI.SharpPlanar.CachedData.trans3_r4 line 1219
lemma OAI.SharpPlanar.CachedData.trans3_r4_eq line 1220
def OAI.SharpPlanar.CachedData.trans3_r5_0 line 1238
lemma OAI.SharpPlanar.CachedData.trans3_r5_0_eq line 1239
def OAI.SharpPlanar.CachedData.trans3_r5_1 line 1240
lemma OAI.SharpPlanar.CachedData.trans3_r5_1_eq line 1241
def OAI.SharpPlanar.CachedData.trans3_r5_2 line 1242
lemma OAI.SharpPlanar.CachedData.trans3_r5_2_eq line 1243
def OAI.SharpPlanar.CachedData.trans3_r5_3 line 1244
lemma OAI.SharpPlanar.CachedData.trans3_r5_3_eq line 1245
def OAI.SharpPlanar.CachedData.trans3_r5_4 line 1246
lemma OAI.SharpPlanar.CachedData.trans3_r5_4_eq line 1247
def OAI.SharpPlanar.CachedData.trans3_r5_5 line 1248
lemma OAI.SharpPlanar.CachedData.trans3_r5_5_eq line 1249
def OAI.SharpPlanar.CachedData.trans3_r5_6 line 1250
lemma OAI.SharpPlanar.CachedData.trans3_r5_6_eq line 1251
def OAI.SharpPlanar.CachedData.trans3_r5_7 line 1252
lemma OAI.SharpPlanar.CachedData.trans3_r5_7_eq line 1253
def OAI.SharpPlanar.CachedData.trans3_r5_8 line 1254
lemma OAI.SharpPlanar.CachedData.trans3_r5_8_eq line 1255
def OAI.SharpPlanar.CachedData.trans3_r5_9 line 1256
lemma OAI.SharpPlanar.CachedData.trans3_r5_9_eq line 1257
def OAI.SharpPlanar.CachedData.trans3_r5_10 line 1258
lemma OAI.SharpPlanar.CachedData.trans3_r5_10_eq line 1259
def OAI.SharpPlanar.CachedData.trans3_r5_11 line 1260
lemma OAI.SharpPlanar.CachedData.trans3_r5_11_eq line 1261
def OAI.SharpPlanar.CachedData.trans3_r5_12 line 1262
lemma OAI.SharpPlanar.CachedData.trans3_r5_12_eq line 1263
def OAI.SharpPlanar.CachedData.trans3_r5_13 line 1264
lemma OAI.SharpPlanar.CachedData.trans3_r5_13_eq line 1265
def OAI.SharpPlanar.CachedData.trans3_r5_14 line 1266
lemma OAI.SharpPlanar.CachedData.trans3_r5_14_eq line 1267
def OAI.SharpPlanar.CachedData.trans3_r5_15 line 1268
lemma OAI.SharpPlanar.CachedData.trans3_r5_15_eq line 1269
def OAI.SharpPlanar.CachedData.trans3_r5 line 1270
lemma OAI.SharpPlanar.CachedData.trans3_r5_eq line 1271
def OAI.SharpPlanar.CachedData.trans3 line 1289
lemma OAI.SharpPlanar.CachedData.trans3_eq line 1290
lemma OAI.SharpPlanar.CachedData.trans3_contains line 1298
def OAI.SharpPlanar.CachedData.trans4Expr line 1303
def OAI.SharpPlanar.CachedData.trans4_r0_0 line 1304
lemma OAI.SharpPlanar.CachedData.trans4_r0_0_eq line 1305
def OAI.SharpPlanar.CachedData.trans4_r0_1 line 1306
lemma OAI.SharpPlanar.CachedData.trans4_r0_1_eq line 1307
def OAI.SharpPlanar.CachedData.trans4_r0_2 line 1308
lemma OAI.SharpPlanar.CachedData.trans4_r0_2_eq line 1309
def OAI.SharpPlanar.CachedData.trans4_r0_3 line 1310
lemma OAI.SharpPlanar.CachedData.trans4_r0_3_eq line 1311
def OAI.SharpPlanar.CachedData.trans4_r0_4 line 1312
lemma OAI.SharpPlanar.CachedData.trans4_r0_4_eq line 1313
def OAI.SharpPlanar.CachedData.trans4_r0_5 line 1314
lemma OAI.SharpPlanar.CachedData.trans4_r0_5_eq line 1315
def OAI.SharpPlanar.CachedData.trans4_r0_6 line 1316
lemma OAI.SharpPlanar.CachedData.trans4_r0_6_eq line 1317
def OAI.SharpPlanar.CachedData.trans4_r0_7 line 1318
lemma OAI.SharpPlanar.CachedData.trans4_r0_7_eq line 1319
def OAI.SharpPlanar.CachedData.trans4_r0_8 line 1320
lemma OAI.SharpPlanar.CachedData.trans4_r0_8_eq line 1321
def OAI.SharpPlanar.CachedData.trans4_r0_9 line 1322
lemma OAI.SharpPlanar.CachedData.trans4_r0_9_eq line 1323
def OAI.SharpPlanar.CachedData.trans4_r0_10 line 1324
lemma OAI.SharpPlanar.CachedData.trans4_r0_10_eq line 1325
def OAI.SharpPlanar.CachedData.trans4_r0_11 line 1326
lemma OAI.SharpPlanar.CachedData.trans4_r0_11_eq line 1327
def OAI.SharpPlanar.CachedData.trans4_r0_12 line 1328
lemma OAI.SharpPlanar.CachedData.trans4_r0_12_eq line 1329
def OAI.SharpPlanar.CachedData.trans4_r0_13 line 1330
lemma OAI.SharpPlanar.CachedData.trans4_r0_13_eq line 1331
def OAI.SharpPlanar.CachedData.trans4_r0_14 line 1332
lemma OAI.SharpPlanar.CachedData.trans4_r0_14_eq line 1333
def OAI.SharpPlanar.CachedData.trans4_r0_15 line 1334
lemma OAI.SharpPlanar.CachedData.trans4_r0_15_eq line 1335
def OAI.SharpPlanar.CachedData.trans4_r0 line 1336
lemma OAI.SharpPlanar.CachedData.trans4_r0_eq line 1337
def OAI.SharpPlanar.CachedData.trans4_r1_0 line 1355
lemma OAI.SharpPlanar.CachedData.trans4_r1_0_eq line 1356
def OAI.SharpPlanar.CachedData.trans4_r1_1 line 1357
lemma OAI.SharpPlanar.CachedData.trans4_r1_1_eq line 1358
def OAI.SharpPlanar.CachedData.trans4_r1_2 line 1359
lemma OAI.SharpPlanar.CachedData.trans4_r1_2_eq line 1360
def OAI.SharpPlanar.CachedData.trans4_r1_3 line 1361
lemma OAI.SharpPlanar.CachedData.trans4_r1_3_eq line 1362
def OAI.SharpPlanar.CachedData.trans4_r1_4 line 1363
lemma OAI.SharpPlanar.CachedData.trans4_r1_4_eq line 1364
def OAI.SharpPlanar.CachedData.trans4_r1_5 line 1365
lemma OAI.SharpPlanar.CachedData.trans4_r1_5_eq line 1366
def OAI.SharpPlanar.CachedData.trans4_r1_6 line 1367
lemma OAI.SharpPlanar.CachedData.trans4_r1_6_eq line 1368
def OAI.SharpPlanar.CachedData.trans4_r1_7 line 1369
lemma OAI.SharpPlanar.CachedData.trans4_r1_7_eq line 1370
def OAI.SharpPlanar.CachedData.trans4_r1_8 line 1371
lemma OAI.SharpPlanar.CachedData.trans4_r1_8_eq line 1372
def OAI.SharpPlanar.CachedData.trans4_r1_9 line 1373
lemma OAI.SharpPlanar.CachedData.trans4_r1_9_eq line 1374
def OAI.SharpPlanar.CachedData.trans4_r1_10 line 1375
lemma OAI.SharpPlanar.CachedData.trans4_r1_10_eq line 1376
def OAI.SharpPlanar.CachedData.trans4_r1_11 line 1377
lemma OAI.SharpPlanar.CachedData.trans4_r1_11_eq line 1378
def OAI.SharpPlanar.CachedData.trans4_r1_12 line 1379
lemma OAI.SharpPlanar.CachedData.trans4_r1_12_eq line 1380
def OAI.SharpPlanar.CachedData.trans4_r1_13 line 1381
lemma OAI.SharpPlanar.CachedData.trans4_r1_13_eq line 1382
def OAI.SharpPlanar.CachedData.trans4_r1_14 line 1383
lemma OAI.SharpPlanar.CachedData.trans4_r1_14_eq line 1384
def OAI.SharpPlanar.CachedData.trans4_r1_15 line 1385
lemma OAI.SharpPlanar.CachedData.trans4_r1_15_eq line 1386
def OAI.SharpPlanar.CachedData.trans4_r1 line 1387
lemma OAI.SharpPlanar.CachedData.trans4_r1_eq line 1388
def OAI.SharpPlanar.CachedData.trans4_r2_0 line 1406
lemma OAI.SharpPlanar.CachedData.trans4_r2_0_eq line 1407
def OAI.SharpPlanar.CachedData.trans4_r2_1 line 1408
lemma OAI.SharpPlanar.CachedData.trans4_r2_1_eq line 1409
def OAI.SharpPlanar.CachedData.trans4_r2_2 line 1410
lemma OAI.SharpPlanar.CachedData.trans4_r2_2_eq line 1411
def OAI.SharpPlanar.CachedData.trans4_r2_3 line 1412
lemma OAI.SharpPlanar.CachedData.trans4_r2_3_eq line 1413
def OAI.SharpPlanar.CachedData.trans4_r2_4 line 1414
lemma OAI.SharpPlanar.CachedData.trans4_r2_4_eq line 1415
def OAI.SharpPlanar.CachedData.trans4_r2_5 line 1416
lemma OAI.SharpPlanar.CachedData.trans4_r2_5_eq line 1417
def OAI.SharpPlanar.CachedData.trans4_r2_6 line 1418
lemma OAI.SharpPlanar.CachedData.trans4_r2_6_eq line 1419
def OAI.SharpPlanar.CachedData.trans4_r2_7 line 1420
lemma OAI.SharpPlanar.CachedData.trans4_r2_7_eq line 1421
def OAI.SharpPlanar.CachedData.trans4_r2_8 line 1422
lemma OAI.SharpPlanar.CachedData.trans4_r2_8_eq line 1423
def OAI.SharpPlanar.CachedData.trans4_r2_9 line 1424
lemma OAI.SharpPlanar.CachedData.trans4_r2_9_eq line 1425
def OAI.SharpPlanar.CachedData.trans4_r2_10 line 1426
lemma OAI.SharpPlanar.CachedData.trans4_r2_10_eq line 1427
def OAI.SharpPlanar.CachedData.trans4_r2_11 line 1428
lemma OAI.SharpPlanar.CachedData.trans4_r2_11_eq line 1429
def OAI.SharpPlanar.CachedData.trans4_r2_12 line 1430
lemma OAI.SharpPlanar.CachedData.trans4_r2_12_eq line 1431
def OAI.SharpPlanar.CachedData.trans4_r2_13 line 1432
lemma OAI.SharpPlanar.CachedData.trans4_r2_13_eq line 1433
def OAI.SharpPlanar.CachedData.trans4_r2_14 line 1434
lemma OAI.SharpPlanar.CachedData.trans4_r2_14_eq line 1435
def OAI.SharpPlanar.CachedData.trans4_r2_15 line 1436
lemma OAI.SharpPlanar.CachedData.trans4_r2_15_eq line 1437
def OAI.SharpPlanar.CachedData.trans4_r2 line 1438
lemma OAI.SharpPlanar.CachedData.trans4_r2_eq line 1439
def OAI.SharpPlanar.CachedData.trans4_r3_0 line 1457
lemma OAI.SharpPlanar.CachedData.trans4_r3_0_eq line 1458
def OAI.SharpPlanar.CachedData.trans4_r3_1 line 1459
lemma OAI.SharpPlanar.CachedData.trans4_r3_1_eq line 1460
def OAI.SharpPlanar.CachedData.trans4_r3_2 line 1461
lemma OAI.SharpPlanar.CachedData.trans4_r3_2_eq line 1462
def OAI.SharpPlanar.CachedData.trans4_r3_3 line 1463
lemma OAI.SharpPlanar.CachedData.trans4_r3_3_eq line 1464
def OAI.SharpPlanar.CachedData.trans4_r3_4 line 1465
lemma OAI.SharpPlanar.CachedData.trans4_r3_4_eq line 1466
def OAI.SharpPlanar.CachedData.trans4_r3_5 line 1467
lemma OAI.SharpPlanar.CachedData.trans4_r3_5_eq line 1468
def OAI.SharpPlanar.CachedData.trans4_r3_6 line 1469
lemma OAI.SharpPlanar.CachedData.trans4_r3_6_eq line 1470
def OAI.SharpPlanar.CachedData.trans4_r3_7 line 1471
lemma OAI.SharpPlanar.CachedData.trans4_r3_7_eq line 1472
def OAI.SharpPlanar.CachedData.trans4_r3_8 line 1473
lemma OAI.SharpPlanar.CachedData.trans4_r3_8_eq line 1474
def OAI.SharpPlanar.CachedData.trans4_r3_9 line 1475
lemma OAI.SharpPlanar.CachedData.trans4_r3_9_eq line 1476
def OAI.SharpPlanar.CachedData.trans4_r3_10 line 1477
lemma OAI.SharpPlanar.CachedData.trans4_r3_10_eq line 1478
def OAI.SharpPlanar.CachedData.trans4_r3_11 line 1479
lemma OAI.SharpPlanar.CachedData.trans4_r3_11_eq line 1480
def OAI.SharpPlanar.CachedData.trans4_r3_12 line 1481
lemma OAI.SharpPlanar.CachedData.trans4_r3_12_eq line 1482
def OAI.SharpPlanar.CachedData.trans4_r3_13 line 1483
lemma OAI.SharpPlanar.CachedData.trans4_r3_13_eq line 1484
def OAI.SharpPlanar.CachedData.trans4_r3_14 line 1485
lemma OAI.SharpPlanar.CachedData.trans4_r3_14_eq line 1486
def OAI.SharpPlanar.CachedData.trans4_r3_15 line 1487
lemma OAI.SharpPlanar.CachedData.trans4_r3_15_eq line 1488
def OAI.SharpPlanar.CachedData.trans4_r3 line 1489
lemma OAI.SharpPlanar.CachedData.trans4_r3_eq line 1490
def OAI.SharpPlanar.CachedData.trans4_r4_0 line 1508
lemma OAI.SharpPlanar.CachedData.trans4_r4_0_eq line 1509
def OAI.SharpPlanar.CachedData.trans4_r4_1 line 1510
lemma OAI.SharpPlanar.CachedData.trans4_r4_1_eq line 1511
def OAI.SharpPlanar.CachedData.trans4_r4_2 line 1512
lemma OAI.SharpPlanar.CachedData.trans4_r4_2_eq line 1513
def OAI.SharpPlanar.CachedData.trans4_r4_3 line 1514
lemma OAI.SharpPlanar.CachedData.trans4_r4_3_eq line 1515
def OAI.SharpPlanar.CachedData.trans4_r4_4 line 1516
lemma OAI.SharpPlanar.CachedData.trans4_r4_4_eq line 1517
def OAI.SharpPlanar.CachedData.trans4_r4_5 line 1518
lemma OAI.SharpPlanar.CachedData.trans4_r4_5_eq line 1519
def OAI.SharpPlanar.CachedData.trans4_r4_6 line 1520
lemma OAI.SharpPlanar.CachedData.trans4_r4_6_eq line 1521
def OAI.SharpPlanar.CachedData.trans4_r4_7 line 1522
lemma OAI.SharpPlanar.CachedData.trans4_r4_7_eq line 1523
def OAI.SharpPlanar.CachedData.trans4_r4_8 line 1524
lemma OAI.SharpPlanar.CachedData.trans4_r4_8_eq line 1525
def OAI.SharpPlanar.CachedData.trans4_r4_9 line 1526
lemma OAI.SharpPlanar.CachedData.trans4_r4_9_eq line 1527
def OAI.SharpPlanar.CachedData.trans4_r4_10 line 1528
lemma OAI.SharpPlanar.CachedData.trans4_r4_10_eq line 1529
def OAI.SharpPlanar.CachedData.trans4_r4_11 line 1530
lemma OAI.SharpPlanar.CachedData.trans4_r4_11_eq line 1531
def OAI.SharpPlanar.CachedData.trans4_r4_12 line 1532
lemma OAI.SharpPlanar.CachedData.trans4_r4_12_eq line 1533
def OAI.SharpPlanar.CachedData.trans4_r4_13 line 1534
lemma OAI.SharpPlanar.CachedData.trans4_r4_13_eq line 1535
def OAI.SharpPlanar.CachedData.trans4_r4_14 line 1536
lemma OAI.SharpPlanar.CachedData.trans4_r4_14_eq line 1537
def OAI.SharpPlanar.CachedData.trans4_r4_15 line 1538
lemma OAI.SharpPlanar.CachedData.trans4_r4_15_eq line 1539
def OAI.SharpPlanar.CachedData.trans4_r4 line 1540
lemma OAI.SharpPlanar.CachedData.trans4_r4_eq line 1541
def OAI.SharpPlanar.CachedData.trans4_r5_0 line 1559
lemma OAI.SharpPlanar.CachedData.trans4_r5_0_eq line 1560
def OAI.SharpPlanar.CachedData.trans4_r5_1 line 1561
lemma OAI.SharpPlanar.CachedData.trans4_r5_1_eq line 1562
def OAI.SharpPlanar.CachedData.trans4_r5_2 line 1563
lemma OAI.SharpPlanar.CachedData.trans4_r5_2_eq line 1564
def OAI.SharpPlanar.CachedData.trans4_r5_3 line 1565
lemma OAI.SharpPlanar.CachedData.trans4_r5_3_eq line 1566
def OAI.SharpPlanar.CachedData.trans4_r5_4 line 1567
lemma OAI.SharpPlanar.CachedData.trans4_r5_4_eq line 1568
def OAI.SharpPlanar.CachedData.trans4_r5_5 line 1569
lemma OAI.SharpPlanar.CachedData.trans4_r5_5_eq line 1570
def OAI.SharpPlanar.CachedData.trans4_r5_6 line 1571
lemma OAI.SharpPlanar.CachedData.trans4_r5_6_eq line 1572
def OAI.SharpPlanar.CachedData.trans4_r5_7 line 1573
lemma OAI.SharpPlanar.CachedData.trans4_r5_7_eq line 1574
def OAI.SharpPlanar.CachedData.trans4_r5_8 line 1575
lemma OAI.SharpPlanar.CachedData.trans4_r5_8_eq line 1576
def OAI.SharpPlanar.CachedData.trans4_r5_9 line 1577
lemma OAI.SharpPlanar.CachedData.trans4_r5_9_eq line 1578
def OAI.SharpPlanar.CachedData.trans4_r5_10 line 1579
lemma OAI.SharpPlanar.CachedData.trans4_r5_10_eq line 1580
def OAI.SharpPlanar.CachedData.trans4_r5_11 line 1581
lemma OAI.SharpPlanar.CachedData.trans4_r5_11_eq line 1582
def OAI.SharpPlanar.CachedData.trans4_r5_12 line 1583
lemma OAI.SharpPlanar.CachedData.trans4_r5_12_eq line 1584
def OAI.SharpPlanar.CachedData.trans4_r5_13 line 1585
lemma OAI.SharpPlanar.CachedData.trans4_r5_13_eq line 1586
def OAI.SharpPlanar.CachedData.trans4_r5_14 line 1587
lemma OAI.SharpPlanar.CachedData.trans4_r5_14_eq line 1588
def OAI.SharpPlanar.CachedData.trans4_r5_15 line 1589
lemma OAI.SharpPlanar.CachedData.trans4_r5_15_eq line 1590
def OAI.SharpPlanar.CachedData.trans4_r5 line 1591
lemma OAI.SharpPlanar.CachedData.trans4_r5_eq line 1592
def OAI.SharpPlanar.CachedData.trans4 line 1610
lemma OAI.SharpPlanar.CachedData.trans4_eq line 1611
lemma OAI.SharpPlanar.CachedData.trans4_contains line 1619
def OAI.SharpPlanar.CachedData.trans5Expr line 1624
def OAI.SharpPlanar.CachedData.trans5_r0_0 line 1625
lemma OAI.SharpPlanar.CachedData.trans5_r0_0_eq line 1626
def OAI.SharpPlanar.CachedData.trans5_r0_1 line 1627
lemma OAI.SharpPlanar.CachedData.trans5_r0_1_eq line 1628
def OAI.SharpPlanar.CachedData.trans5_r0_2 line 1629
lemma OAI.SharpPlanar.CachedData.trans5_r0_2_eq line 1630
def OAI.SharpPlanar.CachedData.trans5_r0_3 line 1631
lemma OAI.SharpPlanar.CachedData.trans5_r0_3_eq line 1632
def OAI.SharpPlanar.CachedData.trans5_r0_4 line 1633
lemma OAI.SharpPlanar.CachedData.trans5_r0_4_eq line 1634
def OAI.SharpPlanar.CachedData.trans5_r0_5 line 1635
lemma OAI.SharpPlanar.CachedData.trans5_r0_5_eq line 1636
def OAI.SharpPlanar.CachedData.trans5_r0_6 line 1637
lemma OAI.SharpPlanar.CachedData.trans5_r0_6_eq line 1638
def OAI.SharpPlanar.CachedData.trans5_r0_7 line 1639
lemma OAI.SharpPlanar.CachedData.trans5_r0_7_eq line 1640
def OAI.SharpPlanar.CachedData.trans5_r0_8 line 1641
lemma OAI.SharpPlanar.CachedData.trans5_r0_8_eq line 1642
def OAI.SharpPlanar.CachedData.trans5_r0_9 line 1643
lemma OAI.SharpPlanar.CachedData.trans5_r0_9_eq line 1644
def OAI.SharpPlanar.CachedData.trans5_r0_10 line 1645
lemma OAI.SharpPlanar.CachedData.trans5_r0_10_eq line 1646
def OAI.SharpPlanar.CachedData.trans5_r0_11 line 1647
lemma OAI.SharpPlanar.CachedData.trans5_r0_11_eq line 1648
def OAI.SharpPlanar.CachedData.trans5_r0_12 line 1649
lemma OAI.SharpPlanar.CachedData.trans5_r0_12_eq line 1650
def OAI.SharpPlanar.CachedData.trans5_r0_13 line 1651
lemma OAI.SharpPlanar.CachedData.trans5_r0_13_eq line 1652
def OAI.SharpPlanar.CachedData.trans5_r0_14 line 1653
lemma OAI.SharpPlanar.CachedData.trans5_r0_14_eq line 1654
def OAI.SharpPlanar.CachedData.trans5_r0_15 line 1655
lemma OAI.SharpPlanar.CachedData.trans5_r0_15_eq line 1656
def OAI.SharpPlanar.CachedData.trans5_r0 line 1657
lemma OAI.SharpPlanar.CachedData.trans5_r0_eq line 1658
def OAI.SharpPlanar.CachedData.trans5_r1_0 line 1676
lemma OAI.SharpPlanar.CachedData.trans5_r1_0_eq line 1677
def OAI.SharpPlanar.CachedData.trans5_r1_1 line 1678
lemma OAI.SharpPlanar.CachedData.trans5_r1_1_eq line 1679
def OAI.SharpPlanar.CachedData.trans5_r1_2 line 1680
lemma OAI.SharpPlanar.CachedData.trans5_r1_2_eq line 1681
def OAI.SharpPlanar.CachedData.trans5_r1_3 line 1682
lemma OAI.SharpPlanar.CachedData.trans5_r1_3_eq line 1683
def OAI.SharpPlanar.CachedData.trans5_r1_4 line 1684
lemma OAI.SharpPlanar.CachedData.trans5_r1_4_eq line 1685
def OAI.SharpPlanar.CachedData.trans5_r1_5 line 1686
lemma OAI.SharpPlanar.CachedData.trans5_r1_5_eq line 1687
def OAI.SharpPlanar.CachedData.trans5_r1_6 line 1688
lemma OAI.SharpPlanar.CachedData.trans5_r1_6_eq line 1689
def OAI.SharpPlanar.CachedData.trans5_r1_7 line 1690
lemma OAI.SharpPlanar.CachedData.trans5_r1_7_eq line 1691
def OAI.SharpPlanar.CachedData.trans5_r1_8 line 1692
lemma OAI.SharpPlanar.CachedData.trans5_r1_8_eq line 1693
def OAI.SharpPlanar.CachedData.trans5_r1_9 line 1694
lemma OAI.SharpPlanar.CachedData.trans5_r1_9_eq line 1695
def OAI.SharpPlanar.CachedData.trans5_r1_10 line 1696
lemma OAI.SharpPlanar.CachedData.trans5_r1_10_eq line 1697
def OAI.SharpPlanar.CachedData.trans5_r1_11 line 1698
lemma OAI.SharpPlanar.CachedData.trans5_r1_11_eq line 1699
def OAI.SharpPlanar.CachedData.trans5_r1_12 line 1700
lemma OAI.SharpPlanar.CachedData.trans5_r1_12_eq line 1701
def OAI.SharpPlanar.CachedData.trans5_r1_13 line 1702
lemma OAI.SharpPlanar.CachedData.trans5_r1_13_eq line 1703
def OAI.SharpPlanar.CachedData.trans5_r1_14 line 1704
lemma OAI.SharpPlanar.CachedData.trans5_r1_14_eq line 1705
def OAI.SharpPlanar.CachedData.trans5_r1_15 line 1706
lemma OAI.SharpPlanar.CachedData.trans5_r1_15_eq line 1707
def OAI.SharpPlanar.CachedData.trans5_r1 line 1708
lemma OAI.SharpPlanar.CachedData.trans5_r1_eq line 1709
def OAI.SharpPlanar.CachedData.trans5_r2_0 line 1727
lemma OAI.SharpPlanar.CachedData.trans5_r2_0_eq line 1728
def OAI.SharpPlanar.CachedData.trans5_r2_1 line 1729
lemma OAI.SharpPlanar.CachedData.trans5_r2_1_eq line 1730
def OAI.SharpPlanar.CachedData.trans5_r2_2 line 1731
lemma OAI.SharpPlanar.CachedData.trans5_r2_2_eq line 1732
def OAI.SharpPlanar.CachedData.trans5_r2_3 line 1733
lemma OAI.SharpPlanar.CachedData.trans5_r2_3_eq line 1734
def OAI.SharpPlanar.CachedData.trans5_r2_4 line 1735
lemma OAI.SharpPlanar.CachedData.trans5_r2_4_eq line 1736
def OAI.SharpPlanar.CachedData.trans5_r2_5 line 1737
lemma OAI.SharpPlanar.CachedData.trans5_r2_5_eq line 1738
def OAI.SharpPlanar.CachedData.trans5_r2_6 line 1739
lemma OAI.SharpPlanar.CachedData.trans5_r2_6_eq line 1740
def OAI.SharpPlanar.CachedData.trans5_r2_7 line 1741
lemma OAI.SharpPlanar.CachedData.trans5_r2_7_eq line 1742
def OAI.SharpPlanar.CachedData.trans5_r2_8 line 1743
lemma OAI.SharpPlanar.CachedData.trans5_r2_8_eq line 1744
def OAI.SharpPlanar.CachedData.trans5_r2_9 line 1745
lemma OAI.SharpPlanar.CachedData.trans5_r2_9_eq line 1746
def OAI.SharpPlanar.CachedData.trans5_r2_10 line 1747
lemma OAI.SharpPlanar.CachedData.trans5_r2_10_eq line 1748
def OAI.SharpPlanar.CachedData.trans5_r2_11 line 1749
lemma OAI.SharpPlanar.CachedData.trans5_r2_11_eq line 1750
def OAI.SharpPlanar.CachedData.trans5_r2_12 line 1751
lemma OAI.SharpPlanar.CachedData.trans5_r2_12_eq line 1752
def OAI.SharpPlanar.CachedData.trans5_r2_13 line 1753
lemma OAI.SharpPlanar.CachedData.trans5_r2_13_eq line 1754
def OAI.SharpPlanar.CachedData.trans5_r2_14 line 1755
lemma OAI.SharpPlanar.CachedData.trans5_r2_14_eq line 1756
def OAI.SharpPlanar.CachedData.trans5_r2_15 line 1757
lemma OAI.SharpPlanar.CachedData.trans5_r2_15_eq line 1758
def OAI.SharpPlanar.CachedData.trans5_r2 line 1759
lemma OAI.SharpPlanar.CachedData.trans5_r2_eq line 1760
def OAI.SharpPlanar.CachedData.trans5_r3_0 line 1778
lemma OAI.SharpPlanar.CachedData.trans5_r3_0_eq line 1779
def OAI.SharpPlanar.CachedData.trans5_r3_1 line 1780
lemma OAI.SharpPlanar.CachedData.trans5_r3_1_eq line 1781
def OAI.SharpPlanar.CachedData.trans5_r3_2 line 1782
lemma OAI.SharpPlanar.CachedData.trans5_r3_2_eq line 1783
def OAI.SharpPlanar.CachedData.trans5_r3_3 line 1784
lemma OAI.SharpPlanar.CachedData.trans5_r3_3_eq line 1785
def OAI.SharpPlanar.CachedData.trans5_r3_4 line 1786
lemma OAI.SharpPlanar.CachedData.trans5_r3_4_eq line 1787
def OAI.SharpPlanar.CachedData.trans5_r3_5 line 1788
lemma OAI.SharpPlanar.CachedData.trans5_r3_5_eq line 1789
def OAI.SharpPlanar.CachedData.trans5_r3_6 line 1790
lemma OAI.SharpPlanar.CachedData.trans5_r3_6_eq line 1791
def OAI.SharpPlanar.CachedData.trans5_r3_7 line 1792
lemma OAI.SharpPlanar.CachedData.trans5_r3_7_eq line 1793
def OAI.SharpPlanar.CachedData.trans5_r3_8 line 1794
lemma OAI.SharpPlanar.CachedData.trans5_r3_8_eq line 1795
def OAI.SharpPlanar.CachedData.trans5_r3_9 line 1796
lemma OAI.SharpPlanar.CachedData.trans5_r3_9_eq line 1797
def OAI.SharpPlanar.CachedData.trans5_r3_10 line 1798
lemma OAI.SharpPlanar.CachedData.trans5_r3_10_eq line 1799
def OAI.SharpPlanar.CachedData.trans5_r3_11 line 1800
lemma OAI.SharpPlanar.CachedData.trans5_r3_11_eq line 1801
def OAI.SharpPlanar.CachedData.trans5_r3_12 line 1802
lemma OAI.SharpPlanar.CachedData.trans5_r3_12_eq line 1803
def OAI.SharpPlanar.CachedData.trans5_r3_13 line 1804
lemma OAI.SharpPlanar.CachedData.trans5_r3_13_eq line 1805
def OAI.SharpPlanar.CachedData.trans5_r3_14 line 1806
lemma OAI.SharpPlanar.CachedData.trans5_r3_14_eq line 1807
def OAI.SharpPlanar.CachedData.trans5_r3_15 line 1808
lemma OAI.SharpPlanar.CachedData.trans5_r3_15_eq line 1809
def OAI.SharpPlanar.CachedData.trans5_r3 line 1810
lemma OAI.SharpPlanar.CachedData.trans5_r3_eq line 1811
def OAI.SharpPlanar.CachedData.trans5_r4_0 line 1829
lemma OAI.SharpPlanar.CachedData.trans5_r4_0_eq line 1830
def OAI.SharpPlanar.CachedData.trans5_r4_1 line 1831
lemma OAI.SharpPlanar.CachedData.trans5_r4_1_eq line 1832
def OAI.SharpPlanar.CachedData.trans5_r4_2 line 1833
lemma OAI.SharpPlanar.CachedData.trans5_r4_2_eq line 1834
def OAI.SharpPlanar.CachedData.trans5_r4_3 line 1835
lemma OAI.SharpPlanar.CachedData.trans5_r4_3_eq line 1836
def OAI.SharpPlanar.CachedData.trans5_r4_4 line 1837
lemma OAI.SharpPlanar.CachedData.trans5_r4_4_eq line 1838
def OAI.SharpPlanar.CachedData.trans5_r4_5 line 1839
lemma OAI.SharpPlanar.CachedData.trans5_r4_5_eq line 1840
def OAI.SharpPlanar.CachedData.trans5_r4_6 line 1841
lemma OAI.SharpPlanar.CachedData.trans5_r4_6_eq line 1842
def OAI.SharpPlanar.CachedData.trans5_r4_7 line 1843
lemma OAI.SharpPlanar.CachedData.trans5_r4_7_eq line 1844
def OAI.SharpPlanar.CachedData.trans5_r4_8 line 1845
lemma OAI.SharpPlanar.CachedData.trans5_r4_8_eq line 1846
def OAI.SharpPlanar.CachedData.trans5_r4_9 line 1847
lemma OAI.SharpPlanar.CachedData.trans5_r4_9_eq line 1848
def OAI.SharpPlanar.CachedData.trans5_r4_10 line 1849
lemma OAI.SharpPlanar.CachedData.trans5_r4_10_eq line 1850
def OAI.SharpPlanar.CachedData.trans5_r4_11 line 1851
lemma OAI.SharpPlanar.CachedData.trans5_r4_11_eq line 1852
def OAI.SharpPlanar.CachedData.trans5_r4_12 line 1853
lemma OAI.SharpPlanar.CachedData.trans5_r4_12_eq line 1854
def OAI.SharpPlanar.CachedData.trans5_r4_13 line 1855
lemma OAI.SharpPlanar.CachedData.trans5_r4_13_eq line 1856
def OAI.SharpPlanar.CachedData.trans5_r4_14 line 1857
lemma OAI.SharpPlanar.CachedData.trans5_r4_14_eq line 1858
def OAI.SharpPlanar.CachedData.trans5_r4_15 line 1859
lemma OAI.SharpPlanar.CachedData.trans5_r4_15_eq line 1860
def OAI.SharpPlanar.CachedData.trans5_r4 line 1861
lemma OAI.SharpPlanar.CachedData.trans5_r4_eq line 1862
def OAI.SharpPlanar.CachedData.trans5_r5_0 line 1880
lemma OAI.SharpPlanar.CachedData.trans5_r5_0_eq line 1881
def OAI.SharpPlanar.CachedData.trans5_r5_1 line 1882
lemma OAI.SharpPlanar.CachedData.trans5_r5_1_eq line 1883
def OAI.SharpPlanar.CachedData.trans5_r5_2 line 1884
lemma OAI.SharpPlanar.CachedData.trans5_r5_2_eq line 1885
def OAI.SharpPlanar.CachedData.trans5_r5_3 line 1886
lemma OAI.SharpPlanar.CachedData.trans5_r5_3_eq line 1887
def OAI.SharpPlanar.CachedData.trans5_r5_4 line 1888
lemma OAI.SharpPlanar.CachedData.trans5_r5_4_eq line 1889
def OAI.SharpPlanar.CachedData.trans5_r5_5 line 1890
lemma OAI.SharpPlanar.CachedData.trans5_r5_5_eq line 1891
def OAI.SharpPlanar.CachedData.trans5_r5_6 line 1892
lemma OAI.SharpPlanar.CachedData.trans5_r5_6_eq line 1893
def OAI.SharpPlanar.CachedData.trans5_r5_7 line 1894
lemma OAI.SharpPlanar.CachedData.trans5_r5_7_eq line 1895
def OAI.SharpPlanar.CachedData.trans5_r5_8 line 1896
lemma OAI.SharpPlanar.CachedData.trans5_r5_8_eq line 1897
def OAI.SharpPlanar.CachedData.trans5_r5_9 line 1898
lemma OAI.SharpPlanar.CachedData.trans5_r5_9_eq line 1899
def OAI.SharpPlanar.CachedData.trans5_r5_10 line 1900
lemma OAI.SharpPlanar.CachedData.trans5_r5_10_eq line 1901
def OAI.SharpPlanar.CachedData.trans5_r5_11 line 1902
lemma OAI.SharpPlanar.CachedData.trans5_r5_11_eq line 1903
def OAI.SharpPlanar.CachedData.trans5_r5_12 line 1904
lemma OAI.SharpPlanar.CachedData.trans5_r5_12_eq line 1905
def OAI.SharpPlanar.CachedData.trans5_r5_13 line 1906
lemma OAI.SharpPlanar.CachedData.trans5_r5_13_eq line 1907
def OAI.SharpPlanar.CachedData.trans5_r5_14 line 1908
lemma OAI.SharpPlanar.CachedData.trans5_r5_14_eq line 1909
def OAI.SharpPlanar.CachedData.trans5_r5_15 line 1910
lemma OAI.SharpPlanar.CachedData.trans5_r5_15_eq line 1911
def OAI.SharpPlanar.CachedData.trans5_r5 line 1912
lemma OAI.SharpPlanar.CachedData.trans5_r5_eq line 1913
def OAI.SharpPlanar.CachedData.trans5 line 1931
lemma OAI.SharpPlanar.CachedData.trans5_eq line 1932
lemma OAI.SharpPlanar.CachedData.trans5_contains line 1940
def OAI.SharpPlanar.CachedData.trans6Expr line 1945
def OAI.SharpPlanar.CachedData.trans6_r0_0 line 1946
lemma OAI.SharpPlanar.CachedData.trans6_r0_0_eq line 1947
def OAI.SharpPlanar.CachedData.trans6_r0_1 line 1948
lemma OAI.SharpPlanar.CachedData.trans6_r0_1_eq line 1949
def OAI.SharpPlanar.CachedData.trans6_r0_2 line 1950
lemma OAI.SharpPlanar.CachedData.trans6_r0_2_eq line 1951
def OAI.SharpPlanar.CachedData.trans6_r0_3 line 1952
lemma OAI.SharpPlanar.CachedData.trans6_r0_3_eq line 1953
def OAI.SharpPlanar.CachedData.trans6_r0_4 line 1954
lemma OAI.SharpPlanar.CachedData.trans6_r0_4_eq line 1955
def OAI.SharpPlanar.CachedData.trans6_r0_5 line 1956
lemma OAI.SharpPlanar.CachedData.trans6_r0_5_eq line 1957
def OAI.SharpPlanar.CachedData.trans6_r0_6 line 1958
lemma OAI.SharpPlanar.CachedData.trans6_r0_6_eq line 1959
def OAI.SharpPlanar.CachedData.trans6_r0_7 line 1960
lemma OAI.SharpPlanar.CachedData.trans6_r0_7_eq line 1961
def OAI.SharpPlanar.CachedData.trans6_r0_8 line 1962
lemma OAI.SharpPlanar.CachedData.trans6_r0_8_eq line 1963
def OAI.SharpPlanar.CachedData.trans6_r0_9 line 1964
lemma OAI.SharpPlanar.CachedData.trans6_r0_9_eq line 1965
def OAI.SharpPlanar.CachedData.trans6_r0_10 line 1966
lemma OAI.SharpPlanar.CachedData.trans6_r0_10_eq line 1967
def OAI.SharpPlanar.CachedData.trans6_r0_11 line 1968
lemma OAI.SharpPlanar.CachedData.trans6_r0_11_eq line 1969
def OAI.SharpPlanar.CachedData.trans6_r0_12 line 1970
lemma OAI.SharpPlanar.CachedData.trans6_r0_12_eq line 1971
def OAI.SharpPlanar.CachedData.trans6_r0_13 line 1972
lemma OAI.SharpPlanar.CachedData.trans6_r0_13_eq line 1973
def OAI.SharpPlanar.CachedData.trans6_r0_14 line 1974
lemma OAI.SharpPlanar.CachedData.trans6_r0_14_eq line 1975
def OAI.SharpPlanar.CachedData.trans6_r0_15 line 1976
lemma OAI.SharpPlanar.CachedData.trans6_r0_15_eq line 1977
def OAI.SharpPlanar.CachedData.trans6_r0 line 1978
lemma OAI.SharpPlanar.CachedData.trans6_r0_eq line 1979
def OAI.SharpPlanar.CachedData.trans6_r1_0 line 1997
lemma OAI.SharpPlanar.CachedData.trans6_r1_0_eq line 1998
def OAI.SharpPlanar.CachedData.trans6_r1_1 line 1999
lemma OAI.SharpPlanar.CachedData.trans6_r1_1_eq line 2000
def OAI.SharpPlanar.CachedData.trans6_r1_2 line 2001
lemma OAI.SharpPlanar.CachedData.trans6_r1_2_eq line 2002
def OAI.SharpPlanar.CachedData.trans6_r1_3 line 2003
lemma OAI.SharpPlanar.CachedData.trans6_r1_3_eq line 2004
def OAI.SharpPlanar.CachedData.trans6_r1_4 line 2005
lemma OAI.SharpPlanar.CachedData.trans6_r1_4_eq line 2006
def OAI.SharpPlanar.CachedData.trans6_r1_5 line 2007
lemma OAI.SharpPlanar.CachedData.trans6_r1_5_eq line 2008
def OAI.SharpPlanar.CachedData.trans6_r1_6 line 2009
lemma OAI.SharpPlanar.CachedData.trans6_r1_6_eq line 2010
def OAI.SharpPlanar.CachedData.trans6_r1_7 line 2011
lemma OAI.SharpPlanar.CachedData.trans6_r1_7_eq line 2012
def OAI.SharpPlanar.CachedData.trans6_r1_8 line 2013
lemma OAI.SharpPlanar.CachedData.trans6_r1_8_eq line 2014
def OAI.SharpPlanar.CachedData.trans6_r1_9 line 2015
lemma OAI.SharpPlanar.CachedData.trans6_r1_9_eq line 2016
def OAI.SharpPlanar.CachedData.trans6_r1_10 line 2017
lemma OAI.SharpPlanar.CachedData.trans6_r1_10_eq line 2018
def OAI.SharpPlanar.CachedData.trans6_r1_11 line 2019
lemma OAI.SharpPlanar.CachedData.trans6_r1_11_eq line 2020
def OAI.SharpPlanar.CachedData.trans6_r1_12 line 2021
lemma OAI.SharpPlanar.CachedData.trans6_r1_12_eq line 2022
def OAI.SharpPlanar.CachedData.trans6_r1_13 line 2023
lemma OAI.SharpPlanar.CachedData.trans6_r1_13_eq line 2024
def OAI.SharpPlanar.CachedData.trans6_r1_14 line 2025
lemma OAI.SharpPlanar.CachedData.trans6_r1_14_eq line 2026
def OAI.SharpPlanar.CachedData.trans6_r1_15 line 2027
lemma OAI.SharpPlanar.CachedData.trans6_r1_15_eq line 2028
def OAI.SharpPlanar.CachedData.trans6_r1 line 2029
lemma OAI.SharpPlanar.CachedData.trans6_r1_eq line 2030
def OAI.SharpPlanar.CachedData.trans6_r2_0 line 2048
lemma OAI.SharpPlanar.CachedData.trans6_r2_0_eq line 2049
def OAI.SharpPlanar.CachedData.trans6_r2_1 line 2050
lemma OAI.SharpPlanar.CachedData.trans6_r2_1_eq line 2051
def OAI.SharpPlanar.CachedData.trans6_r2_2 line 2052
lemma OAI.SharpPlanar.CachedData.trans6_r2_2_eq line 2053
def OAI.SharpPlanar.CachedData.trans6_r2_3 line 2054
lemma OAI.SharpPlanar.CachedData.trans6_r2_3_eq line 2055
def OAI.SharpPlanar.CachedData.trans6_r2_4 line 2056
lemma OAI.SharpPlanar.CachedData.trans6_r2_4_eq line 2057
def OAI.SharpPlanar.CachedData.trans6_r2_5 line 2058
lemma OAI.SharpPlanar.CachedData.trans6_r2_5_eq line 2059
def OAI.SharpPlanar.CachedData.trans6_r2_6 line 2060
lemma OAI.SharpPlanar.CachedData.trans6_r2_6_eq line 2061
def OAI.SharpPlanar.CachedData.trans6_r2_7 line 2062
lemma OAI.SharpPlanar.CachedData.trans6_r2_7_eq line 2063
def OAI.SharpPlanar.CachedData.trans6_r2_8 line 2064
lemma OAI.SharpPlanar.CachedData.trans6_r2_8_eq line 2065
def OAI.SharpPlanar.CachedData.trans6_r2_9 line 2066
lemma OAI.SharpPlanar.CachedData.trans6_r2_9_eq line 2067
def OAI.SharpPlanar.CachedData.trans6_r2_10 line 2068
lemma OAI.SharpPlanar.CachedData.trans6_r2_10_eq line 2069
def OAI.SharpPlanar.CachedData.trans6_r2_11 line 2070
lemma OAI.SharpPlanar.CachedData.trans6_r2_11_eq line 2071
def OAI.SharpPlanar.CachedData.trans6_r2_12 line 2072
lemma OAI.SharpPlanar.CachedData.trans6_r2_12_eq line 2073
def OAI.SharpPlanar.CachedData.trans6_r2_13 line 2074
lemma OAI.SharpPlanar.CachedData.trans6_r2_13_eq line 2075
def OAI.SharpPlanar.CachedData.trans6_r2_14 line 2076
lemma OAI.SharpPlanar.CachedData.trans6_r2_14_eq line 2077
def OAI.SharpPlanar.CachedData.trans6_r2_15 line 2078
lemma OAI.SharpPlanar.CachedData.trans6_r2_15_eq line 2079
def OAI.SharpPlanar.CachedData.trans6_r2 line 2080
lemma OAI.SharpPlanar.CachedData.trans6_r2_eq line 2081
def OAI.SharpPlanar.CachedData.trans6_r3_0 line 2099
lemma OAI.SharpPlanar.CachedData.trans6_r3_0_eq line 2100
def OAI.SharpPlanar.CachedData.trans6_r3_1 line 2101
lemma OAI.SharpPlanar.CachedData.trans6_r3_1_eq line 2102
def OAI.SharpPlanar.CachedData.trans6_r3_2 line 2103
lemma OAI.SharpPlanar.CachedData.trans6_r3_2_eq line 2104
def OAI.SharpPlanar.CachedData.trans6_r3_3 line 2105
lemma OAI.SharpPlanar.CachedData.trans6_r3_3_eq line 2106
def OAI.SharpPlanar.CachedData.trans6_r3_4 line 2107
lemma OAI.SharpPlanar.CachedData.trans6_r3_4_eq line 2108
def OAI.SharpPlanar.CachedData.trans6_r3_5 line 2109
lemma OAI.SharpPlanar.CachedData.trans6_r3_5_eq line 2110
def OAI.SharpPlanar.CachedData.trans6_r3_6 line 2111
lemma OAI.SharpPlanar.CachedData.trans6_r3_6_eq line 2112
def OAI.SharpPlanar.CachedData.trans6_r3_7 line 2113
lemma OAI.SharpPlanar.CachedData.trans6_r3_7_eq line 2114
def OAI.SharpPlanar.CachedData.trans6_r3_8 line 2115
lemma OAI.SharpPlanar.CachedData.trans6_r3_8_eq line 2116
def OAI.SharpPlanar.CachedData.trans6_r3_9 line 2117
lemma OAI.SharpPlanar.CachedData.trans6_r3_9_eq line 2118
def OAI.SharpPlanar.CachedData.trans6_r3_10 line 2119
lemma OAI.SharpPlanar.CachedData.trans6_r3_10_eq line 2120
def OAI.SharpPlanar.CachedData.trans6_r3_11 line 2121
lemma OAI.SharpPlanar.CachedData.trans6_r3_11_eq line 2122
def OAI.SharpPlanar.CachedData.trans6_r3_12 line 2123
lemma OAI.SharpPlanar.CachedData.trans6_r3_12_eq line 2124
def OAI.SharpPlanar.CachedData.trans6_r3_13 line 2125
lemma OAI.SharpPlanar.CachedData.trans6_r3_13_eq line 2126
def OAI.SharpPlanar.CachedData.trans6_r3_14 line 2127
lemma OAI.SharpPlanar.CachedData.trans6_r3_14_eq line 2128
def OAI.SharpPlanar.CachedData.trans6_r3_15 line 2129
lemma OAI.SharpPlanar.CachedData.trans6_r3_15_eq line 2130
def OAI.SharpPlanar.CachedData.trans6_r3 line 2131
lemma OAI.SharpPlanar.CachedData.trans6_r3_eq line 2132
def OAI.SharpPlanar.CachedData.trans6_r4_0 line 2150
lemma OAI.SharpPlanar.CachedData.trans6_r4_0_eq line 2151
def OAI.SharpPlanar.CachedData.trans6_r4_1 line 2152
lemma OAI.SharpPlanar.CachedData.trans6_r4_1_eq line 2153
def OAI.SharpPlanar.CachedData.trans6_r4_2 line 2154
lemma OAI.SharpPlanar.CachedData.trans6_r4_2_eq line 2155
def OAI.SharpPlanar.CachedData.trans6_r4_3 line 2156
lemma OAI.SharpPlanar.CachedData.trans6_r4_3_eq line 2157
def OAI.SharpPlanar.CachedData.trans6_r4_4 line 2158
lemma OAI.SharpPlanar.CachedData.trans6_r4_4_eq line 2159
def OAI.SharpPlanar.CachedData.trans6_r4_5 line 2160
lemma OAI.SharpPlanar.CachedData.trans6_r4_5_eq line 2161
def OAI.SharpPlanar.CachedData.trans6_r4_6 line 2162
lemma OAI.SharpPlanar.CachedData.trans6_r4_6_eq line 2163
def OAI.SharpPlanar.CachedData.trans6_r4_7 line 2164
lemma OAI.SharpPlanar.CachedData.trans6_r4_7_eq line 2165
def OAI.SharpPlanar.CachedData.trans6_r4_8 line 2166
lemma OAI.SharpPlanar.CachedData.trans6_r4_8_eq line 2167
def OAI.SharpPlanar.CachedData.trans6_r4_9 line 2168
lemma OAI.SharpPlanar.CachedData.trans6_r4_9_eq line 2169
def OAI.SharpPlanar.CachedData.trans6_r4_10 line 2170
lemma OAI.SharpPlanar.CachedData.trans6_r4_10_eq line 2171
def OAI.SharpPlanar.CachedData.trans6_r4_11 line 2172
lemma OAI.SharpPlanar.CachedData.trans6_r4_11_eq line 2173
def OAI.SharpPlanar.CachedData.trans6_r4_12 line 2174
lemma OAI.SharpPlanar.CachedData.trans6_r4_12_eq line 2175
def OAI.SharpPlanar.CachedData.trans6_r4_13 line 2176
lemma OAI.SharpPlanar.CachedData.trans6_r4_13_eq line 2177
def OAI.SharpPlanar.CachedData.trans6_r4_14 line 2178
lemma OAI.SharpPlanar.CachedData.trans6_r4_14_eq line 2179
def OAI.SharpPlanar.CachedData.trans6_r4_15 line 2180
lemma OAI.SharpPlanar.CachedData.trans6_r4_15_eq line 2181
def OAI.SharpPlanar.CachedData.trans6_r4 line 2182
lemma OAI.SharpPlanar.CachedData.trans6_r4_eq line 2183
def OAI.SharpPlanar.CachedData.trans6_r5_0 line 2201
lemma OAI.SharpPlanar.CachedData.trans6_r5_0_eq line 2202
def OAI.SharpPlanar.CachedData.trans6_r5_1 line 2203
lemma OAI.SharpPlanar.CachedData.trans6_r5_1_eq line 2204
def OAI.SharpPlanar.CachedData.trans6_r5_2 line 2205
lemma OAI.SharpPlanar.CachedData.trans6_r5_2_eq line 2206
def OAI.SharpPlanar.CachedData.trans6_r5_3 line 2207
lemma OAI.SharpPlanar.CachedData.trans6_r5_3_eq line 2208
def OAI.SharpPlanar.CachedData.trans6_r5_4 line 2209
lemma OAI.SharpPlanar.CachedData.trans6_r5_4_eq line 2210
def OAI.SharpPlanar.CachedData.trans6_r5_5 line 2211
lemma OAI.SharpPlanar.CachedData.trans6_r5_5_eq line 2212
def OAI.SharpPlanar.CachedData.trans6_r5_6 line 2213
lemma OAI.SharpPlanar.CachedData.trans6_r5_6_eq line 2214
def OAI.SharpPlanar.CachedData.trans6_r5_7 line 2215
lemma OAI.SharpPlanar.CachedData.trans6_r5_7_eq line 2216
def OAI.SharpPlanar.CachedData.trans6_r5_8 line 2217
lemma OAI.SharpPlanar.CachedData.trans6_r5_8_eq line 2218
def OAI.SharpPlanar.CachedData.trans6_r5_9 line 2219
lemma OAI.SharpPlanar.CachedData.trans6_r5_9_eq line 2220
def OAI.SharpPlanar.CachedData.trans6_r5_10 line 2221
lemma OAI.SharpPlanar.CachedData.trans6_r5_10_eq line 2222
def OAI.SharpPlanar.CachedData.trans6_r5_11 line 2223
lemma OAI.SharpPlanar.CachedData.trans6_r5_11_eq line 2224
def OAI.SharpPlanar.CachedData.trans6_r5_12 line 2225
lemma OAI.SharpPlanar.CachedData.trans6_r5_12_eq line 2226
def OAI.SharpPlanar.CachedData.trans6_r5_13 line 2227
lemma OAI.SharpPlanar.CachedData.trans6_r5_13_eq line 2228
def OAI.SharpPlanar.CachedData.trans6_r5_14 line 2229
lemma OAI.SharpPlanar.CachedData.trans6_r5_14_eq line 2230
def OAI.SharpPlanar.CachedData.trans6_r5_15 line 2231
lemma OAI.SharpPlanar.CachedData.trans6_r5_15_eq line 2232
def OAI.SharpPlanar.CachedData.trans6_r5 line 2233
lemma OAI.SharpPlanar.CachedData.trans6_r5_eq line 2234
def OAI.SharpPlanar.CachedData.trans6 line 2252
lemma OAI.SharpPlanar.CachedData.trans6_eq line 2253
lemma OAI.SharpPlanar.CachedData.trans6_contains line 2261
def OAI.SharpPlanar.CachedData.trans7Expr line 2266
def OAI.SharpPlanar.CachedData.trans7_r0_0 line 2267
lemma OAI.SharpPlanar.CachedData.trans7_r0_0_eq line 2268
def OAI.SharpPlanar.CachedData.trans7_r0_1 line 2269
lemma OAI.SharpPlanar.CachedData.trans7_r0_1_eq line 2270
def OAI.SharpPlanar.CachedData.trans7_r0_2 line 2271
lemma OAI.SharpPlanar.CachedData.trans7_r0_2_eq line 2272
def OAI.SharpPlanar.CachedData.trans7_r0_3 line 2273
lemma OAI.SharpPlanar.CachedData.trans7_r0_3_eq line 2274
def OAI.SharpPlanar.CachedData.trans7_r0_4 line 2275
lemma OAI.SharpPlanar.CachedData.trans7_r0_4_eq line 2276
def OAI.SharpPlanar.CachedData.trans7_r0_5 line 2277
lemma OAI.SharpPlanar.CachedData.trans7_r0_5_eq line 2278
def OAI.SharpPlanar.CachedData.trans7_r0_6 line 2279
lemma OAI.SharpPlanar.CachedData.trans7_r0_6_eq line 2280
def OAI.SharpPlanar.CachedData.trans7_r0_7 line 2281
lemma OAI.SharpPlanar.CachedData.trans7_r0_7_eq line 2282
def OAI.SharpPlanar.CachedData.trans7_r0_8 line 2283
lemma OAI.SharpPlanar.CachedData.trans7_r0_8_eq line 2284
def OAI.SharpPlanar.CachedData.trans7_r0_9 line 2285
lemma OAI.SharpPlanar.CachedData.trans7_r0_9_eq line 2286
def OAI.SharpPlanar.CachedData.trans7_r0_10 line 2287
lemma OAI.SharpPlanar.CachedData.trans7_r0_10_eq line 2288
def OAI.SharpPlanar.CachedData.trans7_r0_11 line 2289
lemma OAI.SharpPlanar.CachedData.trans7_r0_11_eq line 2290
def OAI.SharpPlanar.CachedData.trans7_r0_12 line 2291
lemma OAI.SharpPlanar.CachedData.trans7_r0_12_eq line 2292
def OAI.SharpPlanar.CachedData.trans7_r0_13 line 2293
lemma OAI.SharpPlanar.CachedData.trans7_r0_13_eq line 2294
def OAI.SharpPlanar.CachedData.trans7_r0_14 line 2295
lemma OAI.SharpPlanar.CachedData.trans7_r0_14_eq line 2296
def OAI.SharpPlanar.CachedData.trans7_r0_15 line 2297
lemma OAI.SharpPlanar.CachedData.trans7_r0_15_eq line 2298
def OAI.SharpPlanar.CachedData.trans7_r0 line 2299
lemma OAI.SharpPlanar.CachedData.trans7_r0_eq line 2300
def OAI.SharpPlanar.CachedData.trans7_r1_0 line 2318
lemma OAI.SharpPlanar.CachedData.trans7_r1_0_eq line 2319
def OAI.SharpPlanar.CachedData.trans7_r1_1 line 2320
lemma OAI.SharpPlanar.CachedData.trans7_r1_1_eq line 2321
def OAI.SharpPlanar.CachedData.trans7_r1_2 line 2322
lemma OAI.SharpPlanar.CachedData.trans7_r1_2_eq line 2323
def OAI.SharpPlanar.CachedData.trans7_r1_3 line 2324
lemma OAI.SharpPlanar.CachedData.trans7_r1_3_eq line 2325
def OAI.SharpPlanar.CachedData.trans7_r1_4 line 2326
lemma OAI.SharpPlanar.CachedData.trans7_r1_4_eq line 2327
def OAI.SharpPlanar.CachedData.trans7_r1_5 line 2328
lemma OAI.SharpPlanar.CachedData.trans7_r1_5_eq line 2329
def OAI.SharpPlanar.CachedData.trans7_r1_6 line 2330
lemma OAI.SharpPlanar.CachedData.trans7_r1_6_eq line 2331
def OAI.SharpPlanar.CachedData.trans7_r1_7 line 2332
lemma OAI.SharpPlanar.CachedData.trans7_r1_7_eq line 2333
def OAI.SharpPlanar.CachedData.trans7_r1_8 line 2334
lemma OAI.SharpPlanar.CachedData.trans7_r1_8_eq line 2335
def OAI.SharpPlanar.CachedData.trans7_r1_9 line 2336
lemma OAI.SharpPlanar.CachedData.trans7_r1_9_eq line 2337
def OAI.SharpPlanar.CachedData.trans7_r1_10 line 2338
lemma OAI.SharpPlanar.CachedData.trans7_r1_10_eq line 2339
def OAI.SharpPlanar.CachedData.trans7_r1_11 line 2340
lemma OAI.SharpPlanar.CachedData.trans7_r1_11_eq line 2341
def OAI.SharpPlanar.CachedData.trans7_r1_12 line 2342
lemma OAI.SharpPlanar.CachedData.trans7_r1_12_eq line 2343
def OAI.SharpPlanar.CachedData.trans7_r1_13 line 2344
lemma OAI.SharpPlanar.CachedData.trans7_r1_13_eq line 2345
def OAI.SharpPlanar.CachedData.trans7_r1_14 line 2346
lemma OAI.SharpPlanar.CachedData.trans7_r1_14_eq line 2347
def OAI.SharpPlanar.CachedData.trans7_r1_15 line 2348
lemma OAI.SharpPlanar.CachedData.trans7_r1_15_eq line 2349
def OAI.SharpPlanar.CachedData.trans7_r1 line 2350
lemma OAI.SharpPlanar.CachedData.trans7_r1_eq line 2351
def OAI.SharpPlanar.CachedData.trans7_r2_0 line 2369
lemma OAI.SharpPlanar.CachedData.trans7_r2_0_eq line 2370
def OAI.SharpPlanar.CachedData.trans7_r2_1 line 2371
lemma OAI.SharpPlanar.CachedData.trans7_r2_1_eq line 2372
def OAI.SharpPlanar.CachedData.trans7_r2_2 line 2373
lemma OAI.SharpPlanar.CachedData.trans7_r2_2_eq line 2374
def OAI.SharpPlanar.CachedData.trans7_r2_3 line 2375
lemma OAI.SharpPlanar.CachedData.trans7_r2_3_eq line 2376
def OAI.SharpPlanar.CachedData.trans7_r2_4 line 2377
lemma OAI.SharpPlanar.CachedData.trans7_r2_4_eq line 2378
def OAI.SharpPlanar.CachedData.trans7_r2_5 line 2379
lemma OAI.SharpPlanar.CachedData.trans7_r2_5_eq line 2380
def OAI.SharpPlanar.CachedData.trans7_r2_6 line 2381
lemma OAI.SharpPlanar.CachedData.trans7_r2_6_eq line 2382
def OAI.SharpPlanar.CachedData.trans7_r2_7 line 2383
lemma OAI.SharpPlanar.CachedData.trans7_r2_7_eq line 2384
def OAI.SharpPlanar.CachedData.trans7_r2_8 line 2385
lemma OAI.SharpPlanar.CachedData.trans7_r2_8_eq line 2386
def OAI.SharpPlanar.CachedData.trans7_r2_9 line 2387
lemma OAI.SharpPlanar.CachedData.trans7_r2_9_eq line 2388
def OAI.SharpPlanar.CachedData.trans7_r2_10 line 2389
lemma OAI.SharpPlanar.CachedData.trans7_r2_10_eq line 2390
def OAI.SharpPlanar.CachedData.trans7_r2_11 line 2391
lemma OAI.SharpPlanar.CachedData.trans7_r2_11_eq line 2392
def OAI.SharpPlanar.CachedData.trans7_r2_12 line 2393
lemma OAI.SharpPlanar.CachedData.trans7_r2_12_eq line 2394
def OAI.SharpPlanar.CachedData.trans7_r2_13 line 2395
lemma OAI.SharpPlanar.CachedData.trans7_r2_13_eq line 2396
def OAI.SharpPlanar.CachedData.trans7_r2_14 line 2397
lemma OAI.SharpPlanar.CachedData.trans7_r2_14_eq line 2398
def OAI.SharpPlanar.CachedData.trans7_r2_15 line 2399
lemma OAI.SharpPlanar.CachedData.trans7_r2_15_eq line 2400
def OAI.SharpPlanar.CachedData.trans7_r2 line 2401
lemma OAI.SharpPlanar.CachedData.trans7_r2_eq line 2402
def OAI.SharpPlanar.CachedData.trans7_r3_0 line 2420
lemma OAI.SharpPlanar.CachedData.trans7_r3_0_eq line 2421
def OAI.SharpPlanar.CachedData.trans7_r3_1 line 2422
lemma OAI.SharpPlanar.CachedData.trans7_r3_1_eq line 2423
def OAI.SharpPlanar.CachedData.trans7_r3_2 line 2424
lemma OAI.SharpPlanar.CachedData.trans7_r3_2_eq line 2425
def OAI.SharpPlanar.CachedData.trans7_r3_3 line 2426
lemma OAI.SharpPlanar.CachedData.trans7_r3_3_eq line 2427
def OAI.SharpPlanar.CachedData.trans7_r3_4 line 2428
lemma OAI.SharpPlanar.CachedData.trans7_r3_4_eq line 2429
def OAI.SharpPlanar.CachedData.trans7_r3_5 line 2430
lemma OAI.SharpPlanar.CachedData.trans7_r3_5_eq line 2431
def OAI.SharpPlanar.CachedData.trans7_r3_6 line 2432
lemma OAI.SharpPlanar.CachedData.trans7_r3_6_eq line 2433
def OAI.SharpPlanar.CachedData.trans7_r3_7 line 2434
lemma OAI.SharpPlanar.CachedData.trans7_r3_7_eq line 2435
def OAI.SharpPlanar.CachedData.trans7_r3_8 line 2436
lemma OAI.SharpPlanar.CachedData.trans7_r3_8_eq line 2437
def OAI.SharpPlanar.CachedData.trans7_r3_9 line 2438
lemma OAI.SharpPlanar.CachedData.trans7_r3_9_eq line 2439
def OAI.SharpPlanar.CachedData.trans7_r3_10 line 2440
lemma OAI.SharpPlanar.CachedData.trans7_r3_10_eq line 2441
def OAI.SharpPlanar.CachedData.trans7_r3_11 line 2442
lemma OAI.SharpPlanar.CachedData.trans7_r3_11_eq line 2443
def OAI.SharpPlanar.CachedData.trans7_r3_12 line 2444
lemma OAI.SharpPlanar.CachedData.trans7_r3_12_eq line 2445
def OAI.SharpPlanar.CachedData.trans7_r3_13 line 2446
lemma OAI.SharpPlanar.CachedData.trans7_r3_13_eq line 2447
def OAI.SharpPlanar.CachedData.trans7_r3_14 line 2448
lemma OAI.SharpPlanar.CachedData.trans7_r3_14_eq line 2449
def OAI.SharpPlanar.CachedData.trans7_r3_15 line 2450
lemma OAI.SharpPlanar.CachedData.trans7_r3_15_eq line 2451
def OAI.SharpPlanar.CachedData.trans7_r3 line 2452
lemma OAI.SharpPlanar.CachedData.trans7_r3_eq line 2453
def OAI.SharpPlanar.CachedData.trans7_r4_0 line 2471
lemma OAI.SharpPlanar.CachedData.trans7_r4_0_eq line 2472
def OAI.SharpPlanar.CachedData.trans7_r4_1 line 2473
lemma OAI.SharpPlanar.CachedData.trans7_r4_1_eq line 2474
def OAI.SharpPlanar.CachedData.trans7_r4_2 line 2475
lemma OAI.SharpPlanar.CachedData.trans7_r4_2_eq line 2476
def OAI.SharpPlanar.CachedData.trans7_r4_3 line 2477
lemma OAI.SharpPlanar.CachedData.trans7_r4_3_eq line 2478
def OAI.SharpPlanar.CachedData.trans7_r4_4 line 2479
lemma OAI.SharpPlanar.CachedData.trans7_r4_4_eq line 2480
def OAI.SharpPlanar.CachedData.trans7_r4_5 line 2481
lemma OAI.SharpPlanar.CachedData.trans7_r4_5_eq line 2482
def OAI.SharpPlanar.CachedData.trans7_r4_6 line 2483
lemma OAI.SharpPlanar.CachedData.trans7_r4_6_eq line 2484
def OAI.SharpPlanar.CachedData.trans7_r4_7 line 2485
lemma OAI.SharpPlanar.CachedData.trans7_r4_7_eq line 2486
def OAI.SharpPlanar.CachedData.trans7_r4_8 line 2487
lemma OAI.SharpPlanar.CachedData.trans7_r4_8_eq line 2488
def OAI.SharpPlanar.CachedData.trans7_r4_9 line 2489
lemma OAI.SharpPlanar.CachedData.trans7_r4_9_eq line 2490
def OAI.SharpPlanar.CachedData.trans7_r4_10 line 2491
lemma OAI.SharpPlanar.CachedData.trans7_r4_10_eq line 2492
def OAI.SharpPlanar.CachedData.trans7_r4_11 line 2493
lemma OAI.SharpPlanar.CachedData.trans7_r4_11_eq line 2494
def OAI.SharpPlanar.CachedData.trans7_r4_12 line 2495
lemma OAI.SharpPlanar.CachedData.trans7_r4_12_eq line 2496
def OAI.SharpPlanar.CachedData.trans7_r4_13 line 2497
lemma OAI.SharpPlanar.CachedData.trans7_r4_13_eq line 2498
def OAI.SharpPlanar.CachedData.trans7_r4_14 line 2499
lemma OAI.SharpPlanar.CachedData.trans7_r4_14_eq line 2500
def OAI.SharpPlanar.CachedData.trans7_r4_15 line 2501
lemma OAI.SharpPlanar.CachedData.trans7_r4_15_eq line 2502
def OAI.SharpPlanar.CachedData.trans7_r4 line 2503
lemma OAI.SharpPlanar.CachedData.trans7_r4_eq line 2504
def OAI.SharpPlanar.CachedData.trans7_r5_0 line 2522
lemma OAI.SharpPlanar.CachedData.trans7_r5_0_eq line 2523
def OAI.SharpPlanar.CachedData.trans7_r5_1 line 2524
lemma OAI.SharpPlanar.CachedData.trans7_r5_1_eq line 2525
def OAI.SharpPlanar.CachedData.trans7_r5_2 line 2526
lemma OAI.SharpPlanar.CachedData.trans7_r5_2_eq line 2527
def OAI.SharpPlanar.CachedData.trans7_r5_3 line 2528
lemma OAI.SharpPlanar.CachedData.trans7_r5_3_eq line 2529
def OAI.SharpPlanar.CachedData.trans7_r5_4 line 2530
lemma OAI.SharpPlanar.CachedData.trans7_r5_4_eq line 2531
def OAI.SharpPlanar.CachedData.trans7_r5_5 line 2532
lemma OAI.SharpPlanar.CachedData.trans7_r5_5_eq line 2533
def OAI.SharpPlanar.CachedData.trans7_r5_6 line 2534
lemma OAI.SharpPlanar.CachedData.trans7_r5_6_eq line 2535
def OAI.SharpPlanar.CachedData.trans7_r5_7 line 2536
lemma OAI.SharpPlanar.CachedData.trans7_r5_7_eq line 2537
def OAI.SharpPlanar.CachedData.trans7_r5_8 line 2538
lemma OAI.SharpPlanar.CachedData.trans7_r5_8_eq line 2539
def OAI.SharpPlanar.CachedData.trans7_r5_9 line 2540
lemma OAI.SharpPlanar.CachedData.trans7_r5_9_eq line 2541
def OAI.SharpPlanar.CachedData.trans7_r5_10 line 2542
lemma OAI.SharpPlanar.CachedData.trans7_r5_10_eq line 2543
def OAI.SharpPlanar.CachedData.trans7_r5_11 line 2544
lemma OAI.SharpPlanar.CachedData.trans7_r5_11_eq line 2545
def OAI.SharpPlanar.CachedData.trans7_r5_12 line 2546
lemma OAI.SharpPlanar.CachedData.trans7_r5_12_eq line 2547
def OAI.SharpPlanar.CachedData.trans7_r5_13 line 2548
lemma OAI.SharpPlanar.CachedData.trans7_r5_13_eq line 2549
def OAI.SharpPlanar.CachedData.trans7_r5_14 line 2550
lemma OAI.SharpPlanar.CachedData.trans7_r5_14_eq line 2551
def OAI.SharpPlanar.CachedData.trans7_r5_15 line 2552
lemma OAI.SharpPlanar.CachedData.trans7_r5_15_eq line 2553
def OAI.SharpPlanar.CachedData.trans7_r5 line 2554
lemma OAI.SharpPlanar.CachedData.trans7_r5_eq line 2555
def OAI.SharpPlanar.CachedData.trans7 line 2573
lemma OAI.SharpPlanar.CachedData.trans7_eq line 2574
lemma OAI.SharpPlanar.CachedData.trans7_contains line 2582
def OAI.SharpPlanar.CachedData.trans8Expr line 2587
def OAI.SharpPlanar.CachedData.trans8_r0_0 line 2588
lemma OAI.SharpPlanar.CachedData.trans8_r0_0_eq line 2589
def OAI.SharpPlanar.CachedData.trans8_r0_1 line 2590
lemma OAI.SharpPlanar.CachedData.trans8_r0_1_eq line 2591
def OAI.SharpPlanar.CachedData.trans8_r0_2 line 2592
lemma OAI.SharpPlanar.CachedData.trans8_r0_2_eq line 2593
def OAI.SharpPlanar.CachedData.trans8_r0_3 line 2594
lemma OAI.SharpPlanar.CachedData.trans8_r0_3_eq line 2595
def OAI.SharpPlanar.CachedData.trans8_r0_4 line 2596
lemma OAI.SharpPlanar.CachedData.trans8_r0_4_eq line 2597
def OAI.SharpPlanar.CachedData.trans8_r0_5 line 2598
lemma OAI.SharpPlanar.CachedData.trans8_r0_5_eq line 2599
def OAI.SharpPlanar.CachedData.trans8_r0_6 line 2600
lemma OAI.SharpPlanar.CachedData.trans8_r0_6_eq line 2601
def OAI.SharpPlanar.CachedData.trans8_r0_7 line 2602
lemma OAI.SharpPlanar.CachedData.trans8_r0_7_eq line 2603
def OAI.SharpPlanar.CachedData.trans8_r0_8 line 2604
lemma OAI.SharpPlanar.CachedData.trans8_r0_8_eq line 2605
def OAI.SharpPlanar.CachedData.trans8_r0_9 line 2606
lemma OAI.SharpPlanar.CachedData.trans8_r0_9_eq line 2607
def OAI.SharpPlanar.CachedData.trans8_r0_10 line 2608
lemma OAI.SharpPlanar.CachedData.trans8_r0_10_eq line 2609
def OAI.SharpPlanar.CachedData.trans8_r0_11 line 2610
lemma OAI.SharpPlanar.CachedData.trans8_r0_11_eq line 2611
def OAI.SharpPlanar.CachedData.trans8_r0_12 line 2612
lemma OAI.SharpPlanar.CachedData.trans8_r0_12_eq line 2613
def OAI.SharpPlanar.CachedData.trans8_r0_13 line 2614
lemma OAI.SharpPlanar.CachedData.trans8_r0_13_eq line 2615
def OAI.SharpPlanar.CachedData.trans8_r0_14 line 2616
lemma OAI.SharpPlanar.CachedData.trans8_r0_14_eq line 2617
def OAI.SharpPlanar.CachedData.trans8_r0_15 line 2618
lemma OAI.SharpPlanar.CachedData.trans8_r0_15_eq line 2619
def OAI.SharpPlanar.CachedData.trans8_r0 line 2620
lemma OAI.SharpPlanar.CachedData.trans8_r0_eq line 2621
def OAI.SharpPlanar.CachedData.trans8_r1_0 line 2639
lemma OAI.SharpPlanar.CachedData.trans8_r1_0_eq line 2640
def OAI.SharpPlanar.CachedData.trans8_r1_1 line 2641
lemma OAI.SharpPlanar.CachedData.trans8_r1_1_eq line 2642
def OAI.SharpPlanar.CachedData.trans8_r1_2 line 2643
lemma OAI.SharpPlanar.CachedData.trans8_r1_2_eq line 2644
def OAI.SharpPlanar.CachedData.trans8_r1_3 line 2645
lemma OAI.SharpPlanar.CachedData.trans8_r1_3_eq line 2646
def OAI.SharpPlanar.CachedData.trans8_r1_4 line 2647
lemma OAI.SharpPlanar.CachedData.trans8_r1_4_eq line 2648
def OAI.SharpPlanar.CachedData.trans8_r1_5 line 2649
lemma OAI.SharpPlanar.CachedData.trans8_r1_5_eq line 2650
def OAI.SharpPlanar.CachedData.trans8_r1_6 line 2651
lemma OAI.SharpPlanar.CachedData.trans8_r1_6_eq line 2652
def OAI.SharpPlanar.CachedData.trans8_r1_7 line 2653
lemma OAI.SharpPlanar.CachedData.trans8_r1_7_eq line 2654
def OAI.SharpPlanar.CachedData.trans8_r1_8 line 2655
lemma OAI.SharpPlanar.CachedData.trans8_r1_8_eq line 2656
def OAI.SharpPlanar.CachedData.trans8_r1_9 line 2657
lemma OAI.SharpPlanar.CachedData.trans8_r1_9_eq line 2658
def OAI.SharpPlanar.CachedData.trans8_r1_10 line 2659
lemma OAI.SharpPlanar.CachedData.trans8_r1_10_eq line 2660
def OAI.SharpPlanar.CachedData.trans8_r1_11 line 2661
lemma OAI.SharpPlanar.CachedData.trans8_r1_11_eq line 2662
def OAI.SharpPlanar.CachedData.trans8_r1_12 line 2663
lemma OAI.SharpPlanar.CachedData.trans8_r1_12_eq line 2664
def OAI.SharpPlanar.CachedData.trans8_r1_13 line 2665
lemma OAI.SharpPlanar.CachedData.trans8_r1_13_eq line 2666
def OAI.SharpPlanar.CachedData.trans8_r1_14 line 2667
lemma OAI.SharpPlanar.CachedData.trans8_r1_14_eq line 2668
def OAI.SharpPlanar.CachedData.trans8_r1_15 line 2669
lemma OAI.SharpPlanar.CachedData.trans8_r1_15_eq line 2670
def OAI.SharpPlanar.CachedData.trans8_r1 line 2671
lemma OAI.SharpPlanar.CachedData.trans8_r1_eq line 2672
def OAI.SharpPlanar.CachedData.trans8_r2_0 line 2690
lemma OAI.SharpPlanar.CachedData.trans8_r2_0_eq line 2691
def OAI.SharpPlanar.CachedData.trans8_r2_1 line 2692
lemma OAI.SharpPlanar.CachedData.trans8_r2_1_eq line 2693
def OAI.SharpPlanar.CachedData.trans8_r2_2 line 2694
lemma OAI.SharpPlanar.CachedData.trans8_r2_2_eq line 2695
def OAI.SharpPlanar.CachedData.trans8_r2_3 line 2696
lemma OAI.SharpPlanar.CachedData.trans8_r2_3_eq line 2697
def OAI.SharpPlanar.CachedData.trans8_r2_4 line 2698
lemma OAI.SharpPlanar.CachedData.trans8_r2_4_eq line 2699
def OAI.SharpPlanar.CachedData.trans8_r2_5 line 2700
lemma OAI.SharpPlanar.CachedData.trans8_r2_5_eq line 2701
def OAI.SharpPlanar.CachedData.trans8_r2_6 line 2702
lemma OAI.SharpPlanar.CachedData.trans8_r2_6_eq line 2703
def OAI.SharpPlanar.CachedData.trans8_r2_7 line 2704
lemma OAI.SharpPlanar.CachedData.trans8_r2_7_eq line 2705
def OAI.SharpPlanar.CachedData.trans8_r2_8 line 2706
lemma OAI.SharpPlanar.CachedData.trans8_r2_8_eq line 2707
def OAI.SharpPlanar.CachedData.trans8_r2_9 line 2708
lemma OAI.SharpPlanar.CachedData.trans8_r2_9_eq line 2709
def OAI.SharpPlanar.CachedData.trans8_r2_10 line 2710
lemma OAI.SharpPlanar.CachedData.trans8_r2_10_eq line 2711
def OAI.SharpPlanar.CachedData.trans8_r2_11 line 2712
lemma OAI.SharpPlanar.CachedData.trans8_r2_11_eq line 2713
def OAI.SharpPlanar.CachedData.trans8_r2_12 line 2714
lemma OAI.SharpPlanar.CachedData.trans8_r2_12_eq line 2715
def OAI.SharpPlanar.CachedData.trans8_r2_13 line 2716
lemma OAI.SharpPlanar.CachedData.trans8_r2_13_eq line 2717
def OAI.SharpPlanar.CachedData.trans8_r2_14 line 2718
lemma OAI.SharpPlanar.CachedData.trans8_r2_14_eq line 2719
def OAI.SharpPlanar.CachedData.trans8_r2_15 line 2720
lemma OAI.SharpPlanar.CachedData.trans8_r2_15_eq line 2721
def OAI.SharpPlanar.CachedData.trans8_r2 line 2722
lemma OAI.SharpPlanar.CachedData.trans8_r2_eq line 2723
def OAI.SharpPlanar.CachedData.trans8_r3_0 line 2741
lemma OAI.SharpPlanar.CachedData.trans8_r3_0_eq line 2742
def OAI.SharpPlanar.CachedData.trans8_r3_1 line 2743
lemma OAI.SharpPlanar.CachedData.trans8_r3_1_eq line 2744
def OAI.SharpPlanar.CachedData.trans8_r3_2 line 2745
lemma OAI.SharpPlanar.CachedData.trans8_r3_2_eq line 2746
def OAI.SharpPlanar.CachedData.trans8_r3_3 line 2747
lemma OAI.SharpPlanar.CachedData.trans8_r3_3_eq line 2748
def OAI.SharpPlanar.CachedData.trans8_r3_4 line 2749
lemma OAI.SharpPlanar.CachedData.trans8_r3_4_eq line 2750
def OAI.SharpPlanar.CachedData.trans8_r3_5 line 2751
lemma OAI.SharpPlanar.CachedData.trans8_r3_5_eq line 2752
def OAI.SharpPlanar.CachedData.trans8_r3_6 line 2753
lemma OAI.SharpPlanar.CachedData.trans8_r3_6_eq line 2754
def OAI.SharpPlanar.CachedData.trans8_r3_7 line 2755
lemma OAI.SharpPlanar.CachedData.trans8_r3_7_eq line 2756
def OAI.SharpPlanar.CachedData.trans8_r3_8 line 2757
lemma OAI.SharpPlanar.CachedData.trans8_r3_8_eq line 2758
def OAI.SharpPlanar.CachedData.trans8_r3_9 line 2759
lemma OAI.SharpPlanar.CachedData.trans8_r3_9_eq line 2760
def OAI.SharpPlanar.CachedData.trans8_r3_10 line 2761
lemma OAI.SharpPlanar.CachedData.trans8_r3_10_eq line 2762
def OAI.SharpPlanar.CachedData.trans8_r3_11 line 2763
lemma OAI.SharpPlanar.CachedData.trans8_r3_11_eq line 2764
def OAI.SharpPlanar.CachedData.trans8_r3_12 line 2765
lemma OAI.SharpPlanar.CachedData.trans8_r3_12_eq line 2766
def OAI.SharpPlanar.CachedData.trans8_r3_13 line 2767
lemma OAI.SharpPlanar.CachedData.trans8_r3_13_eq line 2768
def OAI.SharpPlanar.CachedData.trans8_r3_14 line 2769
lemma OAI.SharpPlanar.CachedData.trans8_r3_14_eq line 2770
def OAI.SharpPlanar.CachedData.trans8_r3_15 line 2771
lemma OAI.SharpPlanar.CachedData.trans8_r3_15_eq line 2772
def OAI.SharpPlanar.CachedData.trans8_r3 line 2773
lemma OAI.SharpPlanar.CachedData.trans8_r3_eq line 2774
def OAI.SharpPlanar.CachedData.trans8_r4_0 line 2792
lemma OAI.SharpPlanar.CachedData.trans8_r4_0_eq line 2793
def OAI.SharpPlanar.CachedData.trans8_r4_1 line 2794
lemma OAI.SharpPlanar.CachedData.trans8_r4_1_eq line 2795
def OAI.SharpPlanar.CachedData.trans8_r4_2 line 2796
lemma OAI.SharpPlanar.CachedData.trans8_r4_2_eq line 2797
def OAI.SharpPlanar.CachedData.trans8_r4_3 line 2798
lemma OAI.SharpPlanar.CachedData.trans8_r4_3_eq line 2799
def OAI.SharpPlanar.CachedData.trans8_r4_4 line 2800
lemma OAI.SharpPlanar.CachedData.trans8_r4_4_eq line 2801
def OAI.SharpPlanar.CachedData.trans8_r4_5 line 2802
lemma OAI.SharpPlanar.CachedData.trans8_r4_5_eq line 2803
def OAI.SharpPlanar.CachedData.trans8_r4_6 line 2804
lemma OAI.SharpPlanar.CachedData.trans8_r4_6_eq line 2805
def OAI.SharpPlanar.CachedData.trans8_r4_7 line 2806
lemma OAI.SharpPlanar.CachedData.trans8_r4_7_eq line 2807
def OAI.SharpPlanar.CachedData.trans8_r4_8 line 2808
lemma OAI.SharpPlanar.CachedData.trans8_r4_8_eq line 2809
def OAI.SharpPlanar.CachedData.trans8_r4_9 line 2810
lemma OAI.SharpPlanar.CachedData.trans8_r4_9_eq line 2811
def OAI.SharpPlanar.CachedData.trans8_r4_10 line 2812
lemma OAI.SharpPlanar.CachedData.trans8_r4_10_eq line 2813
def OAI.SharpPlanar.CachedData.trans8_r4_11 line 2814
lemma OAI.SharpPlanar.CachedData.trans8_r4_11_eq line 2815
def OAI.SharpPlanar.CachedData.trans8_r4_12 line 2816
lemma OAI.SharpPlanar.CachedData.trans8_r4_12_eq line 2817
def OAI.SharpPlanar.CachedData.trans8_r4_13 line 2818
lemma OAI.SharpPlanar.CachedData.trans8_r4_13_eq line 2819
def OAI.SharpPlanar.CachedData.trans8_r4_14 line 2820
lemma OAI.SharpPlanar.CachedData.trans8_r4_14_eq line 2821
def OAI.SharpPlanar.CachedData.trans8_r4_15 line 2822
lemma OAI.SharpPlanar.CachedData.trans8_r4_15_eq line 2823
def OAI.SharpPlanar.CachedData.trans8_r4 line 2824
lemma OAI.SharpPlanar.CachedData.trans8_r4_eq line 2825
def OAI.SharpPlanar.CachedData.trans8_r5_0 line 2843
lemma OAI.SharpPlanar.CachedData.trans8_r5_0_eq line 2844
def OAI.SharpPlanar.CachedData.trans8_r5_1 line 2845
lemma OAI.SharpPlanar.CachedData.trans8_r5_1_eq line 2846
def OAI.SharpPlanar.CachedData.trans8_r5_2 line 2847
lemma OAI.SharpPlanar.CachedData.trans8_r5_2_eq line 2848
def OAI.SharpPlanar.CachedData.trans8_r5_3 line 2849
lemma OAI.SharpPlanar.CachedData.trans8_r5_3_eq line 2850
def OAI.SharpPlanar.CachedData.trans8_r5_4 line 2851
lemma OAI.SharpPlanar.CachedData.trans8_r5_4_eq line 2852
def OAI.SharpPlanar.CachedData.trans8_r5_5 line 2853
lemma OAI.SharpPlanar.CachedData.trans8_r5_5_eq line 2854
def OAI.SharpPlanar.CachedData.trans8_r5_6 line 2855
lemma OAI.SharpPlanar.CachedData.trans8_r5_6_eq line 2856
def OAI.SharpPlanar.CachedData.trans8_r5_7 line 2857
lemma OAI.SharpPlanar.CachedData.trans8_r5_7_eq line 2858
def OAI.SharpPlanar.CachedData.trans8_r5_8 line 2859
lemma OAI.SharpPlanar.CachedData.trans8_r5_8_eq line 2860
def OAI.SharpPlanar.CachedData.trans8_r5_9 line 2861
lemma OAI.SharpPlanar.CachedData.trans8_r5_9_eq line 2862
def OAI.SharpPlanar.CachedData.trans8_r5_10 line 2863
lemma OAI.SharpPlanar.CachedData.trans8_r5_10_eq line 2864
def OAI.SharpPlanar.CachedData.trans8_r5_11 line 2865
lemma OAI.SharpPlanar.CachedData.trans8_r5_11_eq line 2866
def OAI.SharpPlanar.CachedData.trans8_r5_12 line 2867
lemma OAI.SharpPlanar.CachedData.trans8_r5_12_eq line 2868
def OAI.SharpPlanar.CachedData.trans8_r5_13 line 2869
lemma OAI.SharpPlanar.CachedData.trans8_r5_13_eq line 2870
def OAI.SharpPlanar.CachedData.trans8_r5_14 line 2871
lemma OAI.SharpPlanar.CachedData.trans8_r5_14_eq line 2872
def OAI.SharpPlanar.CachedData.trans8_r5_15 line 2873
lemma OAI.SharpPlanar.CachedData.trans8_r5_15_eq line 2874
def OAI.SharpPlanar.CachedData.trans8_r5 line 2875
lemma OAI.SharpPlanar.CachedData.trans8_r5_eq line 2876
def OAI.SharpPlanar.CachedData.trans8 line 2894
lemma OAI.SharpPlanar.CachedData.trans8_eq line 2895
lemma OAI.SharpPlanar.CachedData.trans8_contains line 2903
def OAI.SharpPlanar.CachedData.trans9Expr line 2908
def OAI.SharpPlanar.CachedData.trans9_r0_0 line 2909
lemma OAI.SharpPlanar.CachedData.trans9_r0_0_eq line 2910
def OAI.SharpPlanar.CachedData.trans9_r0_1 line 2911
lemma OAI.SharpPlanar.CachedData.trans9_r0_1_eq line 2912
def OAI.SharpPlanar.CachedData.trans9_r0_2 line 2913
lemma OAI.SharpPlanar.CachedData.trans9_r0_2_eq line 2914
def OAI.SharpPlanar.CachedData.trans9_r0_3 line 2915
lemma OAI.SharpPlanar.CachedData.trans9_r0_3_eq line 2916
def OAI.SharpPlanar.CachedData.trans9_r0_4 line 2917
lemma OAI.SharpPlanar.CachedData.trans9_r0_4_eq line 2918
def OAI.SharpPlanar.CachedData.trans9_r0_5 line 2919
lemma OAI.SharpPlanar.CachedData.trans9_r0_5_eq line 2920
def OAI.SharpPlanar.CachedData.trans9_r0_6 line 2921
lemma OAI.SharpPlanar.CachedData.trans9_r0_6_eq line 2922
def OAI.SharpPlanar.CachedData.trans9_r0_7 line 2923
lemma OAI.SharpPlanar.CachedData.trans9_r0_7_eq line 2924
def OAI.SharpPlanar.CachedData.trans9_r0_8 line 2925
lemma OAI.SharpPlanar.CachedData.trans9_r0_8_eq line 2926
def OAI.SharpPlanar.CachedData.trans9_r0_9 line 2927
lemma OAI.SharpPlanar.CachedData.trans9_r0_9_eq line 2928
def OAI.SharpPlanar.CachedData.trans9_r0_10 line 2929
lemma OAI.SharpPlanar.CachedData.trans9_r0_10_eq line 2930
def OAI.SharpPlanar.CachedData.trans9_r0_11 line 2931
lemma OAI.SharpPlanar.CachedData.trans9_r0_11_eq line 2932
def OAI.SharpPlanar.CachedData.trans9_r0_12 line 2933
lemma OAI.SharpPlanar.CachedData.trans9_r0_12_eq line 2934
def OAI.SharpPlanar.CachedData.trans9_r0_13 line 2935
lemma OAI.SharpPlanar.CachedData.trans9_r0_13_eq line 2936
def OAI.SharpPlanar.CachedData.trans9_r0_14 line 2937
lemma OAI.SharpPlanar.CachedData.trans9_r0_14_eq line 2938
def OAI.SharpPlanar.CachedData.trans9_r0_15 line 2939
lemma OAI.SharpPlanar.CachedData.trans9_r0_15_eq line 2940
def OAI.SharpPlanar.CachedData.trans9_r0 line 2941
lemma OAI.SharpPlanar.CachedData.trans9_r0_eq line 2942
def OAI.SharpPlanar.CachedData.trans9_r1_0 line 2960
lemma OAI.SharpPlanar.CachedData.trans9_r1_0_eq line 2961
def OAI.SharpPlanar.CachedData.trans9_r1_1 line 2962
lemma OAI.SharpPlanar.CachedData.trans9_r1_1_eq line 2963
def OAI.SharpPlanar.CachedData.trans9_r1_2 line 2964
lemma OAI.SharpPlanar.CachedData.trans9_r1_2_eq line 2965
def OAI.SharpPlanar.CachedData.trans9_r1_3 line 2966
lemma OAI.SharpPlanar.CachedData.trans9_r1_3_eq line 2967
def OAI.SharpPlanar.CachedData.trans9_r1_4 line 2968
lemma OAI.SharpPlanar.CachedData.trans9_r1_4_eq line 2969
def OAI.SharpPlanar.CachedData.trans9_r1_5 line 2970
lemma OAI.SharpPlanar.CachedData.trans9_r1_5_eq line 2971
def OAI.SharpPlanar.CachedData.trans9_r1_6 line 2972
lemma OAI.SharpPlanar.CachedData.trans9_r1_6_eq line 2973
def OAI.SharpPlanar.CachedData.trans9_r1_7 line 2974
lemma OAI.SharpPlanar.CachedData.trans9_r1_7_eq line 2975
def OAI.SharpPlanar.CachedData.trans9_r1_8 line 2976
lemma OAI.SharpPlanar.CachedData.trans9_r1_8_eq line 2977
def OAI.SharpPlanar.CachedData.trans9_r1_9 line 2978
lemma OAI.SharpPlanar.CachedData.trans9_r1_9_eq line 2979
def OAI.SharpPlanar.CachedData.trans9_r1_10 line 2980
lemma OAI.SharpPlanar.CachedData.trans9_r1_10_eq line 2981
def OAI.SharpPlanar.CachedData.trans9_r1_11 line 2982
lemma OAI.SharpPlanar.CachedData.trans9_r1_11_eq line 2983
def OAI.SharpPlanar.CachedData.trans9_r1_12 line 2984
lemma OAI.SharpPlanar.CachedData.trans9_r1_12_eq line 2985
def OAI.SharpPlanar.CachedData.trans9_r1_13 line 2986
lemma OAI.SharpPlanar.CachedData.trans9_r1_13_eq line 2987
def OAI.SharpPlanar.CachedData.trans9_r1_14 line 2988
lemma OAI.SharpPlanar.CachedData.trans9_r1_14_eq line 2989
def OAI.SharpPlanar.CachedData.trans9_r1_15 line 2990
lemma OAI.SharpPlanar.CachedData.trans9_r1_15_eq line 2991
def OAI.SharpPlanar.CachedData.trans9_r1 line 2992
lemma OAI.SharpPlanar.CachedData.trans9_r1_eq line 2993
def OAI.SharpPlanar.CachedData.trans9_r2_0 line 3011
lemma OAI.SharpPlanar.CachedData.trans9_r2_0_eq line 3012
def OAI.SharpPlanar.CachedData.trans9_r2_1 line 3013
lemma OAI.SharpPlanar.CachedData.trans9_r2_1_eq line 3014
def OAI.SharpPlanar.CachedData.trans9_r2_2 line 3015
lemma OAI.SharpPlanar.CachedData.trans9_r2_2_eq line 3016
def OAI.SharpPlanar.CachedData.trans9_r2_3 line 3017
lemma OAI.SharpPlanar.CachedData.trans9_r2_3_eq line 3018
def OAI.SharpPlanar.CachedData.trans9_r2_4 line 3019
lemma OAI.SharpPlanar.CachedData.trans9_r2_4_eq line 3020
def OAI.SharpPlanar.CachedData.trans9_r2_5 line 3021
lemma OAI.SharpPlanar.CachedData.trans9_r2_5_eq line 3022
def OAI.SharpPlanar.CachedData.trans9_r2_6 line 3023
lemma OAI.SharpPlanar.CachedData.trans9_r2_6_eq line 3024
def OAI.SharpPlanar.CachedData.trans9_r2_7 line 3025
lemma OAI.SharpPlanar.CachedData.trans9_r2_7_eq line 3026
def OAI.SharpPlanar.CachedData.trans9_r2_8 line 3027
lemma OAI.SharpPlanar.CachedData.trans9_r2_8_eq line 3028
def OAI.SharpPlanar.CachedData.trans9_r2_9 line 3029
lemma OAI.SharpPlanar.CachedData.trans9_r2_9_eq line 3030
def OAI.SharpPlanar.CachedData.trans9_r2_10 line 3031
lemma OAI.SharpPlanar.CachedData.trans9_r2_10_eq line 3032
def OAI.SharpPlanar.CachedData.trans9_r2_11 line 3033
lemma OAI.SharpPlanar.CachedData.trans9_r2_11_eq line 3034
def OAI.SharpPlanar.CachedData.trans9_r2_12 line 3035
lemma OAI.SharpPlanar.CachedData.trans9_r2_12_eq line 3036
def OAI.SharpPlanar.CachedData.trans9_r2_13 line 3037
lemma OAI.SharpPlanar.CachedData.trans9_r2_13_eq line 3038
def OAI.SharpPlanar.CachedData.trans9_r2_14 line 3039
lemma OAI.SharpPlanar.CachedData.trans9_r2_14_eq line 3040
def OAI.SharpPlanar.CachedData.trans9_r2_15 line 3041
lemma OAI.SharpPlanar.CachedData.trans9_r2_15_eq line 3042
def OAI.SharpPlanar.CachedData.trans9_r2 line 3043
lemma OAI.SharpPlanar.CachedData.trans9_r2_eq line 3044
def OAI.SharpPlanar.CachedData.trans9_r3_0 line 3062
lemma OAI.SharpPlanar.CachedData.trans9_r3_0_eq line 3063
def OAI.SharpPlanar.CachedData.trans9_r3_1 line 3064
lemma OAI.SharpPlanar.CachedData.trans9_r3_1_eq line 3065
def OAI.SharpPlanar.CachedData.trans9_r3_2 line 3066
lemma OAI.SharpPlanar.CachedData.trans9_r3_2_eq line 3067
def OAI.SharpPlanar.CachedData.trans9_r3_3 line 3068
lemma OAI.SharpPlanar.CachedData.trans9_r3_3_eq line 3069
def OAI.SharpPlanar.CachedData.trans9_r3_4 line 3070
lemma OAI.SharpPlanar.CachedData.trans9_r3_4_eq line 3071
def OAI.SharpPlanar.CachedData.trans9_r3_5 line 3072
lemma OAI.SharpPlanar.CachedData.trans9_r3_5_eq line 3073
def OAI.SharpPlanar.CachedData.trans9_r3_6 line 3074
lemma OAI.SharpPlanar.CachedData.trans9_r3_6_eq line 3075
def OAI.SharpPlanar.CachedData.trans9_r3_7 line 3076
lemma OAI.SharpPlanar.CachedData.trans9_r3_7_eq line 3077
def OAI.SharpPlanar.CachedData.trans9_r3_8 line 3078
lemma OAI.SharpPlanar.CachedData.trans9_r3_8_eq line 3079
def OAI.SharpPlanar.CachedData.trans9_r3_9 line 3080
lemma OAI.SharpPlanar.CachedData.trans9_r3_9_eq line 3081
def OAI.SharpPlanar.CachedData.trans9_r3_10 line 3082
lemma OAI.SharpPlanar.CachedData.trans9_r3_10_eq line 3083
def OAI.SharpPlanar.CachedData.trans9_r3_11 line 3084
lemma OAI.SharpPlanar.CachedData.trans9_r3_11_eq line 3085
def OAI.SharpPlanar.CachedData.trans9_r3_12 line 3086
lemma OAI.SharpPlanar.CachedData.trans9_r3_12_eq line 3087
def OAI.SharpPlanar.CachedData.trans9_r3_13 line 3088
lemma OAI.SharpPlanar.CachedData.trans9_r3_13_eq line 3089
def OAI.SharpPlanar.CachedData.trans9_r3_14 line 3090
lemma OAI.SharpPlanar.CachedData.trans9_r3_14_eq line 3091
def OAI.SharpPlanar.CachedData.trans9_r3_15 line 3092
lemma OAI.SharpPlanar.CachedData.trans9_r3_15_eq line 3093
def OAI.SharpPlanar.CachedData.trans9_r3 line 3094
lemma OAI.SharpPlanar.CachedData.trans9_r3_eq line 3095
def OAI.SharpPlanar.CachedData.trans9_r4_0 line 3113
lemma OAI.SharpPlanar.CachedData.trans9_r4_0_eq line 3114
def OAI.SharpPlanar.CachedData.trans9_r4_1 line 3115
lemma OAI.SharpPlanar.CachedData.trans9_r4_1_eq line 3116
def OAI.SharpPlanar.CachedData.trans9_r4_2 line 3117
lemma OAI.SharpPlanar.CachedData.trans9_r4_2_eq line 3118
def OAI.SharpPlanar.CachedData.trans9_r4_3 line 3119
lemma OAI.SharpPlanar.CachedData.trans9_r4_3_eq line 3120
def OAI.SharpPlanar.CachedData.trans9_r4_4 line 3121
lemma OAI.SharpPlanar.CachedData.trans9_r4_4_eq line 3122
def OAI.SharpPlanar.CachedData.trans9_r4_5 line 3123
lemma OAI.SharpPlanar.CachedData.trans9_r4_5_eq line 3124
def OAI.SharpPlanar.CachedData.trans9_r4_6 line 3125
lemma OAI.SharpPlanar.CachedData.trans9_r4_6_eq line 3126
def OAI.SharpPlanar.CachedData.trans9_r4_7 line 3127
lemma OAI.SharpPlanar.CachedData.trans9_r4_7_eq line 3128
def OAI.SharpPlanar.CachedData.trans9_r4_8 line 3129
lemma OAI.SharpPlanar.CachedData.trans9_r4_8_eq line 3130
def OAI.SharpPlanar.CachedData.trans9_r4_9 line 3131
lemma OAI.SharpPlanar.CachedData.trans9_r4_9_eq line 3132
def OAI.SharpPlanar.CachedData.trans9_r4_10 line 3133
lemma OAI.SharpPlanar.CachedData.trans9_r4_10_eq line 3134
def OAI.SharpPlanar.CachedData.trans9_r4_11 line 3135
lemma OAI.SharpPlanar.CachedData.trans9_r4_11_eq line 3136
def OAI.SharpPlanar.CachedData.trans9_r4_12 line 3137
lemma OAI.SharpPlanar.CachedData.trans9_r4_12_eq line 3138
def OAI.SharpPlanar.CachedData.trans9_r4_13 line 3139
lemma OAI.SharpPlanar.CachedData.trans9_r4_13_eq line 3140
def OAI.SharpPlanar.CachedData.trans9_r4_14 line 3141
lemma OAI.SharpPlanar.CachedData.trans9_r4_14_eq line 3142
def OAI.SharpPlanar.CachedData.trans9_r4_15 line 3143
lemma OAI.SharpPlanar.CachedData.trans9_r4_15_eq line 3144
def OAI.SharpPlanar.CachedData.trans9_r4 line 3145
lemma OAI.SharpPlanar.CachedData.trans9_r4_eq line 3146
def OAI.SharpPlanar.CachedData.trans9_r5_0 line 3164
lemma OAI.SharpPlanar.CachedData.trans9_r5_0_eq line 3165
def OAI.SharpPlanar.CachedData.trans9_r5_1 line 3166
lemma OAI.SharpPlanar.CachedData.trans9_r5_1_eq line 3167
def OAI.SharpPlanar.CachedData.trans9_r5_2 line 3168
lemma OAI.SharpPlanar.CachedData.trans9_r5_2_eq line 3169
def OAI.SharpPlanar.CachedData.trans9_r5_3 line 3170
lemma OAI.SharpPlanar.CachedData.trans9_r5_3_eq line 3171
def OAI.SharpPlanar.CachedData.trans9_r5_4 line 3172
lemma OAI.SharpPlanar.CachedData.trans9_r5_4_eq line 3173
def OAI.SharpPlanar.CachedData.trans9_r5_5 line 3174
lemma OAI.SharpPlanar.CachedData.trans9_r5_5_eq line 3175
def OAI.SharpPlanar.CachedData.trans9_r5_6 line 3176
lemma OAI.SharpPlanar.CachedData.trans9_r5_6_eq line 3177
def OAI.SharpPlanar.CachedData.trans9_r5_7 line 3178
lemma OAI.SharpPlanar.CachedData.trans9_r5_7_eq line 3179
def OAI.SharpPlanar.CachedData.trans9_r5_8 line 3180
lemma OAI.SharpPlanar.CachedData.trans9_r5_8_eq line 3181
def OAI.SharpPlanar.CachedData.trans9_r5_9 line 3182
lemma OAI.SharpPlanar.CachedData.trans9_r5_9_eq line 3183
def OAI.SharpPlanar.CachedData.trans9_r5_10 line 3184
lemma OAI.SharpPlanar.CachedData.trans9_r5_10_eq line 3185
def OAI.SharpPlanar.CachedData.trans9_r5_11 line 3186
lemma OAI.SharpPlanar.CachedData.trans9_r5_11_eq line 3187
def OAI.SharpPlanar.CachedData.trans9_r5_12 line 3188
lemma OAI.SharpPlanar.CachedData.trans9_r5_12_eq line 3189
def OAI.SharpPlanar.CachedData.trans9_r5_13 line 3190
lemma OAI.SharpPlanar.CachedData.trans9_r5_13_eq line 3191
def OAI.SharpPlanar.CachedData.trans9_r5_14 line 3192
lemma OAI.SharpPlanar.CachedData.trans9_r5_14_eq line 3193
def OAI.SharpPlanar.CachedData.trans9_r5_15 line 3194
lemma OAI.SharpPlanar.CachedData.trans9_r5_15_eq line 3195
def OAI.SharpPlanar.CachedData.trans9_r5 line 3196
lemma OAI.SharpPlanar.CachedData.trans9_r5_eq line 3197
def OAI.SharpPlanar.CachedData.trans9 line 3215
lemma OAI.SharpPlanar.CachedData.trans9_eq line 3216
lemma OAI.SharpPlanar.CachedData.trans9_contains line 3224
def OAI.SharpPlanar.CachedData.trans10Expr line 3229
def OAI.SharpPlanar.CachedData.trans10_r0_0 line 3230
lemma OAI.SharpPlanar.CachedData.trans10_r0_0_eq line 3231
def OAI.SharpPlanar.CachedData.trans10_r0_1 line 3232
lemma OAI.SharpPlanar.CachedData.trans10_r0_1_eq line 3233
def OAI.SharpPlanar.CachedData.trans10_r0_2 line 3234
lemma OAI.SharpPlanar.CachedData.trans10_r0_2_eq line 3235
def OAI.SharpPlanar.CachedData.trans10_r0_3 line 3236
lemma OAI.SharpPlanar.CachedData.trans10_r0_3_eq line 3237
def OAI.SharpPlanar.CachedData.trans10_r0_4 line 3238
lemma OAI.SharpPlanar.CachedData.trans10_r0_4_eq line 3239
def OAI.SharpPlanar.CachedData.trans10_r0_5 line 3240
lemma OAI.SharpPlanar.CachedData.trans10_r0_5_eq line 3241
def OAI.SharpPlanar.CachedData.trans10_r0_6 line 3242
lemma OAI.SharpPlanar.CachedData.trans10_r0_6_eq line 3243
def OAI.SharpPlanar.CachedData.trans10_r0_7 line 3244
lemma OAI.SharpPlanar.CachedData.trans10_r0_7_eq line 3245
def OAI.SharpPlanar.CachedData.trans10_r0_8 line 3246
lemma OAI.SharpPlanar.CachedData.trans10_r0_8_eq line 3247
def OAI.SharpPlanar.CachedData.trans10_r0_9 line 3248
lemma OAI.SharpPlanar.CachedData.trans10_r0_9_eq line 3249
def OAI.SharpPlanar.CachedData.trans10_r0_10 line 3250
lemma OAI.SharpPlanar.CachedData.trans10_r0_10_eq line 3251
def OAI.SharpPlanar.CachedData.trans10_r0_11 line 3252
lemma OAI.SharpPlanar.CachedData.trans10_r0_11_eq line 3253
def OAI.SharpPlanar.CachedData.trans10_r0_12 line 3254
lemma OAI.SharpPlanar.CachedData.trans10_r0_12_eq line 3255
def OAI.SharpPlanar.CachedData.trans10_r0_13 line 3256
lemma OAI.SharpPlanar.CachedData.trans10_r0_13_eq line 3257
def OAI.SharpPlanar.CachedData.trans10_r0_14 line 3258
lemma OAI.SharpPlanar.CachedData.trans10_r0_14_eq line 3259
def OAI.SharpPlanar.CachedData.trans10_r0_15 line 3260
lemma OAI.SharpPlanar.CachedData.trans10_r0_15_eq line 3261
def OAI.SharpPlanar.CachedData.trans10_r0 line 3262
lemma OAI.SharpPlanar.CachedData.trans10_r0_eq line 3263
def OAI.SharpPlanar.CachedData.trans10_r1_0 line 3281
lemma OAI.SharpPlanar.CachedData.trans10_r1_0_eq line 3282
def OAI.SharpPlanar.CachedData.trans10_r1_1 line 3283
lemma OAI.SharpPlanar.CachedData.trans10_r1_1_eq line 3284
def OAI.SharpPlanar.CachedData.trans10_r1_2 line 3285
lemma OAI.SharpPlanar.CachedData.trans10_r1_2_eq line 3286
def OAI.SharpPlanar.CachedData.trans10_r1_3 line 3287
lemma OAI.SharpPlanar.CachedData.trans10_r1_3_eq line 3288
def OAI.SharpPlanar.CachedData.trans10_r1_4 line 3289
lemma OAI.SharpPlanar.CachedData.trans10_r1_4_eq line 3290
def OAI.SharpPlanar.CachedData.trans10_r1_5 line 3291
lemma OAI.SharpPlanar.CachedData.trans10_r1_5_eq line 3292
def OAI.SharpPlanar.CachedData.trans10_r1_6 line 3293
lemma OAI.SharpPlanar.CachedData.trans10_r1_6_eq line 3294
def OAI.SharpPlanar.CachedData.trans10_r1_7 line 3295
lemma OAI.SharpPlanar.CachedData.trans10_r1_7_eq line 3296
def OAI.SharpPlanar.CachedData.trans10_r1_8 line 3297
lemma OAI.SharpPlanar.CachedData.trans10_r1_8_eq line 3298
def OAI.SharpPlanar.CachedData.trans10_r1_9 line 3299
lemma OAI.SharpPlanar.CachedData.trans10_r1_9_eq line 3300
def OAI.SharpPlanar.CachedData.trans10_r1_10 line 3301
lemma OAI.SharpPlanar.CachedData.trans10_r1_10_eq line 3302
def OAI.SharpPlanar.CachedData.trans10_r1_11 line 3303
lemma OAI.SharpPlanar.CachedData.trans10_r1_11_eq line 3304
def OAI.SharpPlanar.CachedData.trans10_r1_12 line 3305
lemma OAI.SharpPlanar.CachedData.trans10_r1_12_eq line 3306
def OAI.SharpPlanar.CachedData.trans10_r1_13 line 3307
lemma OAI.SharpPlanar.CachedData.trans10_r1_13_eq line 3308
def OAI.SharpPlanar.CachedData.trans10_r1_14 line 3309
lemma OAI.SharpPlanar.CachedData.trans10_r1_14_eq line 3310
def OAI.SharpPlanar.CachedData.trans10_r1_15 line 3311
lemma OAI.SharpPlanar.CachedData.trans10_r1_15_eq line 3312
def OAI.SharpPlanar.CachedData.trans10_r1 line 3313
lemma OAI.SharpPlanar.CachedData.trans10_r1_eq line 3314
def OAI.SharpPlanar.CachedData.trans10_r2_0 line 3332
lemma OAI.SharpPlanar.CachedData.trans10_r2_0_eq line 3333
def OAI.SharpPlanar.CachedData.trans10_r2_1 line 3334
lemma OAI.SharpPlanar.CachedData.trans10_r2_1_eq line 3335
def OAI.SharpPlanar.CachedData.trans10_r2_2 line 3336
lemma OAI.SharpPlanar.CachedData.trans10_r2_2_eq line 3337
def OAI.SharpPlanar.CachedData.trans10_r2_3 line 3338
lemma OAI.SharpPlanar.CachedData.trans10_r2_3_eq line 3339
def OAI.SharpPlanar.CachedData.trans10_r2_4 line 3340
lemma OAI.SharpPlanar.CachedData.trans10_r2_4_eq line 3341
def OAI.SharpPlanar.CachedData.trans10_r2_5 line 3342
lemma OAI.SharpPlanar.CachedData.trans10_r2_5_eq line 3343
def OAI.SharpPlanar.CachedData.trans10_r2_6 line 3344
lemma OAI.SharpPlanar.CachedData.trans10_r2_6_eq line 3345
def OAI.SharpPlanar.CachedData.trans10_r2_7 line 3346
lemma OAI.SharpPlanar.CachedData.trans10_r2_7_eq line 3347
def OAI.SharpPlanar.CachedData.trans10_r2_8 line 3348
lemma OAI.SharpPlanar.CachedData.trans10_r2_8_eq line 3349
def OAI.SharpPlanar.CachedData.trans10_r2_9 line 3350
lemma OAI.SharpPlanar.CachedData.trans10_r2_9_eq line 3351
def OAI.SharpPlanar.CachedData.trans10_r2_10 line 3352
lemma OAI.SharpPlanar.CachedData.trans10_r2_10_eq line 3353
def OAI.SharpPlanar.CachedData.trans10_r2_11 line 3354
lemma OAI.SharpPlanar.CachedData.trans10_r2_11_eq line 3355
def OAI.SharpPlanar.CachedData.trans10_r2_12 line 3356
lemma OAI.SharpPlanar.CachedData.trans10_r2_12_eq line 3357
def OAI.SharpPlanar.CachedData.trans10_r2_13 line 3358
lemma OAI.SharpPlanar.CachedData.trans10_r2_13_eq line 3359
def OAI.SharpPlanar.CachedData.trans10_r2_14 line 3360
lemma OAI.SharpPlanar.CachedData.trans10_r2_14_eq line 3361
def OAI.SharpPlanar.CachedData.trans10_r2_15 line 3362
lemma OAI.SharpPlanar.CachedData.trans10_r2_15_eq line 3363
def OAI.SharpPlanar.CachedData.trans10_r2 line 3364
lemma OAI.SharpPlanar.CachedData.trans10_r2_eq line 3365
def OAI.SharpPlanar.CachedData.trans10_r3_0 line 3383
lemma OAI.SharpPlanar.CachedData.trans10_r3_0_eq line 3384
def OAI.SharpPlanar.CachedData.trans10_r3_1 line 3385
lemma OAI.SharpPlanar.CachedData.trans10_r3_1_eq line 3386
def OAI.SharpPlanar.CachedData.trans10_r3_2 line 3387
lemma OAI.SharpPlanar.CachedData.trans10_r3_2_eq line 3388
def OAI.SharpPlanar.CachedData.trans10_r3_3 line 3389
lemma OAI.SharpPlanar.CachedData.trans10_r3_3_eq line 3390
def OAI.SharpPlanar.CachedData.trans10_r3_4 line 3391
lemma OAI.SharpPlanar.CachedData.trans10_r3_4_eq line 3392
def OAI.SharpPlanar.CachedData.trans10_r3_5 line 3393
lemma OAI.SharpPlanar.CachedData.trans10_r3_5_eq line 3394
def OAI.SharpPlanar.CachedData.trans10_r3_6 line 3395
lemma OAI.SharpPlanar.CachedData.trans10_r3_6_eq line 3396
def OAI.SharpPlanar.CachedData.trans10_r3_7 line 3397
lemma OAI.SharpPlanar.CachedData.trans10_r3_7_eq line 3398
def OAI.SharpPlanar.CachedData.trans10_r3_8 line 3399
lemma OAI.SharpPlanar.CachedData.trans10_r3_8_eq line 3400
def OAI.SharpPlanar.CachedData.trans10_r3_9 line 3401
lemma OAI.SharpPlanar.CachedData.trans10_r3_9_eq line 3402
def OAI.SharpPlanar.CachedData.trans10_r3_10 line 3403
lemma OAI.SharpPlanar.CachedData.trans10_r3_10_eq line 3404
def OAI.SharpPlanar.CachedData.trans10_r3_11 line 3405
lemma OAI.SharpPlanar.CachedData.trans10_r3_11_eq line 3406
def OAI.SharpPlanar.CachedData.trans10_r3_12 line 3407
lemma OAI.SharpPlanar.CachedData.trans10_r3_12_eq line 3408
def OAI.SharpPlanar.CachedData.trans10_r3_13 line 3409
lemma OAI.SharpPlanar.CachedData.trans10_r3_13_eq line 3410
def OAI.SharpPlanar.CachedData.trans10_r3_14 line 3411
lemma OAI.SharpPlanar.CachedData.trans10_r3_14_eq line 3412
def OAI.SharpPlanar.CachedData.trans10_r3_15 line 3413
lemma OAI.SharpPlanar.CachedData.trans10_r3_15_eq line 3414
def OAI.SharpPlanar.CachedData.trans10_r3 line 3415
lemma OAI.SharpPlanar.CachedData.trans10_r3_eq line 3416
def OAI.SharpPlanar.CachedData.trans10_r4_0 line 3434
lemma OAI.SharpPlanar.CachedData.trans10_r4_0_eq line 3435
def OAI.SharpPlanar.CachedData.trans10_r4_1 line 3436
lemma OAI.SharpPlanar.CachedData.trans10_r4_1_eq line 3437
def OAI.SharpPlanar.CachedData.trans10_r4_2 line 3438
lemma OAI.SharpPlanar.CachedData.trans10_r4_2_eq line 3439
def OAI.SharpPlanar.CachedData.trans10_r4_3 line 3440
lemma OAI.SharpPlanar.CachedData.trans10_r4_3_eq line 3441
def OAI.SharpPlanar.CachedData.trans10_r4_4 line 3442
lemma OAI.SharpPlanar.CachedData.trans10_r4_4_eq line 3443
def OAI.SharpPlanar.CachedData.trans10_r4_5 line 3444
lemma OAI.SharpPlanar.CachedData.trans10_r4_5_eq line 3445
def OAI.SharpPlanar.CachedData.trans10_r4_6 line 3446
lemma OAI.SharpPlanar.CachedData.trans10_r4_6_eq line 3447
def OAI.SharpPlanar.CachedData.trans10_r4_7 line 3448
lemma OAI.SharpPlanar.CachedData.trans10_r4_7_eq line 3449
def OAI.SharpPlanar.CachedData.trans10_r4_8 line 3450
lemma OAI.SharpPlanar.CachedData.trans10_r4_8_eq line 3451
def OAI.SharpPlanar.CachedData.trans10_r4_9 line 3452
lemma OAI.SharpPlanar.CachedData.trans10_r4_9_eq line 3453
def OAI.SharpPlanar.CachedData.trans10_r4_10 line 3454
lemma OAI.SharpPlanar.CachedData.trans10_r4_10_eq line 3455
def OAI.SharpPlanar.CachedData.trans10_r4_11 line 3456
lemma OAI.SharpPlanar.CachedData.trans10_r4_11_eq line 3457
def OAI.SharpPlanar.CachedData.trans10_r4_12 line 3458
lemma OAI.SharpPlanar.CachedData.trans10_r4_12_eq line 3459
def OAI.SharpPlanar.CachedData.trans10_r4_13 line 3460
lemma OAI.SharpPlanar.CachedData.trans10_r4_13_eq line 3461
def OAI.SharpPlanar.CachedData.trans10_r4_14 line 3462
lemma OAI.SharpPlanar.CachedData.trans10_r4_14_eq line 3463
def OAI.SharpPlanar.CachedData.trans10_r4_15 line 3464
lemma OAI.SharpPlanar.CachedData.trans10_r4_15_eq line 3465
def OAI.SharpPlanar.CachedData.trans10_r4 line 3466
lemma OAI.SharpPlanar.CachedData.trans10_r4_eq line 3467
def OAI.SharpPlanar.CachedData.trans10_r5_0 line 3485
lemma OAI.SharpPlanar.CachedData.trans10_r5_0_eq line 3486
def OAI.SharpPlanar.CachedData.trans10_r5_1 line 3487
lemma OAI.SharpPlanar.CachedData.trans10_r5_1_eq line 3488
def OAI.SharpPlanar.CachedData.trans10_r5_2 line 3489
lemma OAI.SharpPlanar.CachedData.trans10_r5_2_eq line 3490
def OAI.SharpPlanar.CachedData.trans10_r5_3 line 3491
lemma OAI.SharpPlanar.CachedData.trans10_r5_3_eq line 3492
def OAI.SharpPlanar.CachedData.trans10_r5_4 line 3493
lemma OAI.SharpPlanar.CachedData.trans10_r5_4_eq line 3494
def OAI.SharpPlanar.CachedData.trans10_r5_5 line 3495
lemma OAI.SharpPlanar.CachedData.trans10_r5_5_eq line 3496
def OAI.SharpPlanar.CachedData.trans10_r5_6 line 3497
lemma OAI.SharpPlanar.CachedData.trans10_r5_6_eq line 3498
def OAI.SharpPlanar.CachedData.trans10_r5_7 line 3499
lemma OAI.SharpPlanar.CachedData.trans10_r5_7_eq line 3500
def OAI.SharpPlanar.CachedData.trans10_r5_8 line 3501
lemma OAI.SharpPlanar.CachedData.trans10_r5_8_eq line 3502
def OAI.SharpPlanar.CachedData.trans10_r5_9 line 3503
lemma OAI.SharpPlanar.CachedData.trans10_r5_9_eq line 3504
def OAI.SharpPlanar.CachedData.trans10_r5_10 line 3505
lemma OAI.SharpPlanar.CachedData.trans10_r5_10_eq line 3506
def OAI.SharpPlanar.CachedData.trans10_r5_11 line 3507
lemma OAI.SharpPlanar.CachedData.trans10_r5_11_eq line 3508
def OAI.SharpPlanar.CachedData.trans10_r5_12 line 3509
lemma OAI.SharpPlanar.CachedData.trans10_r5_12_eq line 3510
def OAI.SharpPlanar.CachedData.trans10_r5_13 line 3511
lemma OAI.SharpPlanar.CachedData.trans10_r5_13_eq line 3512
def OAI.SharpPlanar.CachedData.trans10_r5_14 line 3513
lemma OAI.SharpPlanar.CachedData.trans10_r5_14_eq line 3514
def OAI.SharpPlanar.CachedData.trans10_r5_15 line 3515
lemma OAI.SharpPlanar.CachedData.trans10_r5_15_eq line 3516
def OAI.SharpPlanar.CachedData.trans10_r5 line 3517
lemma OAI.SharpPlanar.CachedData.trans10_r5_eq line 3518
def OAI.SharpPlanar.CachedData.trans10 line 3536
lemma OAI.SharpPlanar.CachedData.trans10_eq line 3537
lemma OAI.SharpPlanar.CachedData.trans10_contains line 3545