Fejer.lean`

GitHub source file

635 declarations, 0 contain sorry, 0 declared as axioms

Fejér quadrature enclosures

Certified nodes and weights for the 256-node cosine quadrature rule.

def OAI.SharpPlanar.fejerAngle line 13
def OAI.SharpPlanar.fejerNode line 14
def OAI.SharpPlanar.fejerWeight line 15
def OAI.SharpPlanar.fejerPartial line 25
lemma OAI.SharpPlanar.fejerPartial_zero line 29
lemma OAI.SharpPlanar.fejerPartial_succ line 31
lemma OAI.SharpPlanar.fejer_root_cos line 35
lemma OAI.SharpPlanar.weight_root_contains line 43
lemma OAI.SharpPlanar.fejerPartial_checked_step line 50
lemma OAI.SharpPlanar.fejer_partial_eq line 66
lemma OAI.SharpPlanar.fejerWeight_checked line 82
lemma OAI.SharpPlanar.fejerNode_root line 94
lemma OAI.SharpPlanar.fejerWeight_reverse line 101
def OAI.SharpPlanar.IntegerCompact.roots0 line 121
lemma OAI.SharpPlanar.IntegerCompact.roots0_contains line 122
def OAI.SharpPlanar.IntegerCompact.roots1 line 156
lemma OAI.SharpPlanar.IntegerCompact.roots1_contains line 157
def OAI.SharpPlanar.IntegerCompact.roots2 line 191
lemma OAI.SharpPlanar.IntegerCompact.roots2_contains line 192
def OAI.SharpPlanar.IntegerCompact.roots3 line 226
lemma OAI.SharpPlanar.IntegerCompact.roots3_contains line 227
def OAI.SharpPlanar.IntegerCompact.roots4 line 261
lemma OAI.SharpPlanar.IntegerCompact.roots4_contains line 262
def OAI.SharpPlanar.IntegerCompact.roots5 line 296
lemma OAI.SharpPlanar.IntegerCompact.roots5_contains line 297
def OAI.SharpPlanar.IntegerCompact.roots6 line 331
lemma OAI.SharpPlanar.IntegerCompact.roots6_contains line 332
def OAI.SharpPlanar.IntegerCompact.roots7 line 366
lemma OAI.SharpPlanar.IntegerCompact.roots7_contains line 367
def OAI.SharpPlanar.IntegerCompact.roots8 line 401
lemma OAI.SharpPlanar.IntegerCompact.roots8_contains line 402
def OAI.SharpPlanar.IntegerCompact.roots9 line 436
lemma OAI.SharpPlanar.IntegerCompact.roots9_contains line 437
def OAI.SharpPlanar.IntegerCompact.roots10 line 471
lemma OAI.SharpPlanar.IntegerCompact.roots10_contains line 472
def OAI.SharpPlanar.IntegerCompact.roots11 line 506
lemma OAI.SharpPlanar.IntegerCompact.roots11_contains line 507
def OAI.SharpPlanar.IntegerCompact.roots12 line 541
lemma OAI.SharpPlanar.IntegerCompact.roots12_contains line 542
def OAI.SharpPlanar.IntegerCompact.roots13 line 576
lemma OAI.SharpPlanar.IntegerCompact.roots13_contains line 577
def OAI.SharpPlanar.IntegerCompact.roots14 line 611
lemma OAI.SharpPlanar.IntegerCompact.roots14_contains line 612
def OAI.SharpPlanar.IntegerCompact.roots15 line 646
lemma OAI.SharpPlanar.IntegerCompact.roots15_contains line 647
def OAI.SharpPlanar.IntegerCompact.roots16 line 681
lemma OAI.SharpPlanar.IntegerCompact.roots16_contains line 682
def OAI.SharpPlanar.IntegerCompact.roots17 line 716
lemma OAI.SharpPlanar.IntegerCompact.roots17_contains line 717
def OAI.SharpPlanar.IntegerCompact.roots18 line 751
lemma OAI.SharpPlanar.IntegerCompact.roots18_contains line 752
def OAI.SharpPlanar.IntegerCompact.roots19 line 786
lemma OAI.SharpPlanar.IntegerCompact.roots19_contains line 787
def OAI.SharpPlanar.IntegerCompact.roots20 line 821
lemma OAI.SharpPlanar.IntegerCompact.roots20_contains line 822
def OAI.SharpPlanar.IntegerCompact.roots21 line 856
lemma OAI.SharpPlanar.IntegerCompact.roots21_contains line 857
def OAI.SharpPlanar.IntegerCompact.roots22 line 891
lemma OAI.SharpPlanar.IntegerCompact.roots22_contains line 892
def OAI.SharpPlanar.IntegerCompact.roots23 line 926
lemma OAI.SharpPlanar.IntegerCompact.roots23_contains line 927
def OAI.SharpPlanar.IntegerCompact.roots24 line 961
lemma OAI.SharpPlanar.IntegerCompact.roots24_contains line 962
def OAI.SharpPlanar.IntegerCompact.roots25 line 996
lemma OAI.SharpPlanar.IntegerCompact.roots25_contains line 997
def OAI.SharpPlanar.IntegerCompact.roots26 line 1031
lemma OAI.SharpPlanar.IntegerCompact.roots26_contains line 1032
def OAI.SharpPlanar.IntegerCompact.roots27 line 1066
lemma OAI.SharpPlanar.IntegerCompact.roots27_contains line 1067
def OAI.SharpPlanar.IntegerCompact.roots28 line 1101
lemma OAI.SharpPlanar.IntegerCompact.roots28_contains line 1102
def OAI.SharpPlanar.IntegerCompact.roots29 line 1136
lemma OAI.SharpPlanar.IntegerCompact.roots29_contains line 1137
def OAI.SharpPlanar.IntegerCompact.roots30 line 1171
lemma OAI.SharpPlanar.IntegerCompact.roots30_contains line 1172
def OAI.SharpPlanar.IntegerCompact.roots31 line 1206
lemma OAI.SharpPlanar.IntegerCompact.roots31_contains line 1207
def OAI.SharpPlanar.IntegerCompact.rootRows line 1241
lemma OAI.SharpPlanar.IntegerCompact.rootRows_contains line 1242
def OAI.SharpPlanar.IntegerCompact.rootLookup line 1276
lemma OAI.SharpPlanar.IntegerCompact.rootLookup_contains line 1278
def OAI.SharpPlanar.IntegerCompact.partialBox line 1282
lemma OAI.SharpPlanar.IntegerCompact.partialBox_contains line 1286
def OAI.SharpPlanar.IntegerCompact.weightBoxCalc line 1293
lemma OAI.SharpPlanar.IntegerCompact.weightBoxCalc_contains line 1295
def OAI.SharpPlanar.IntegerCompact.weight0 line 1298
lemma OAI.SharpPlanar.IntegerCompact.weight0_contains line 1299
def OAI.SharpPlanar.IntegerCompact.weight1 line 1303
lemma OAI.SharpPlanar.IntegerCompact.weight1_contains line 1304
def OAI.SharpPlanar.IntegerCompact.weight2 line 1308
lemma OAI.SharpPlanar.IntegerCompact.weight2_contains line 1309
def OAI.SharpPlanar.IntegerCompact.weight3 line 1313
lemma OAI.SharpPlanar.IntegerCompact.weight3_contains line 1314
def OAI.SharpPlanar.IntegerCompact.weight4 line 1318
lemma OAI.SharpPlanar.IntegerCompact.weight4_contains line 1319
def OAI.SharpPlanar.IntegerCompact.weight5 line 1323
lemma OAI.SharpPlanar.IntegerCompact.weight5_contains line 1324
def OAI.SharpPlanar.IntegerCompact.weight6 line 1328
lemma OAI.SharpPlanar.IntegerCompact.weight6_contains line 1329
def OAI.SharpPlanar.IntegerCompact.weight7 line 1333
lemma OAI.SharpPlanar.IntegerCompact.weight7_contains line 1334
def OAI.SharpPlanar.IntegerCompact.weight8 line 1338
lemma OAI.SharpPlanar.IntegerCompact.weight8_contains line 1339
def OAI.SharpPlanar.IntegerCompact.weight9 line 1343
lemma OAI.SharpPlanar.IntegerCompact.weight9_contains line 1344
def OAI.SharpPlanar.IntegerCompact.weight10 line 1348
lemma OAI.SharpPlanar.IntegerCompact.weight10_contains line 1349
def OAI.SharpPlanar.IntegerCompact.weight11 line 1353
lemma OAI.SharpPlanar.IntegerCompact.weight11_contains line 1354
def OAI.SharpPlanar.IntegerCompact.weight12 line 1358
lemma OAI.SharpPlanar.IntegerCompact.weight12_contains line 1359
def OAI.SharpPlanar.IntegerCompact.weight13 line 1363
lemma OAI.SharpPlanar.IntegerCompact.weight13_contains line 1364
def OAI.SharpPlanar.IntegerCompact.weight14 line 1368
lemma OAI.SharpPlanar.IntegerCompact.weight14_contains line 1369
def OAI.SharpPlanar.IntegerCompact.weight15 line 1373
lemma OAI.SharpPlanar.IntegerCompact.weight15_contains line 1374
def OAI.SharpPlanar.IntegerCompact.weight16 line 1378
lemma OAI.SharpPlanar.IntegerCompact.weight16_contains line 1379
def OAI.SharpPlanar.IntegerCompact.weight17 line 1383
lemma OAI.SharpPlanar.IntegerCompact.weight17_contains line 1384
def OAI.SharpPlanar.IntegerCompact.weight18 line 1388
lemma OAI.SharpPlanar.IntegerCompact.weight18_contains line 1389
def OAI.SharpPlanar.IntegerCompact.weight19 line 1393
lemma OAI.SharpPlanar.IntegerCompact.weight19_contains line 1394
def OAI.SharpPlanar.IntegerCompact.weight20 line 1398
lemma OAI.SharpPlanar.IntegerCompact.weight20_contains line 1399
def OAI.SharpPlanar.IntegerCompact.weight21 line 1403
lemma OAI.SharpPlanar.IntegerCompact.weight21_contains line 1404
def OAI.SharpPlanar.IntegerCompact.weight22 line 1408
lemma OAI.SharpPlanar.IntegerCompact.weight22_contains line 1409
def OAI.SharpPlanar.IntegerCompact.weight23 line 1413
lemma OAI.SharpPlanar.IntegerCompact.weight23_contains line 1414
def OAI.SharpPlanar.IntegerCompact.weight24 line 1418
lemma OAI.SharpPlanar.IntegerCompact.weight24_contains line 1419
def OAI.SharpPlanar.IntegerCompact.weight25 line 1423
lemma OAI.SharpPlanar.IntegerCompact.weight25_contains line 1424
def OAI.SharpPlanar.IntegerCompact.weight26 line 1428
lemma OAI.SharpPlanar.IntegerCompact.weight26_contains line 1429
def OAI.SharpPlanar.IntegerCompact.weight27 line 1433
lemma OAI.SharpPlanar.IntegerCompact.weight27_contains line 1434
def OAI.SharpPlanar.IntegerCompact.weight28 line 1438
lemma OAI.SharpPlanar.IntegerCompact.weight28_contains line 1439
def OAI.SharpPlanar.IntegerCompact.weight29 line 1443
lemma OAI.SharpPlanar.IntegerCompact.weight29_contains line 1444
def OAI.SharpPlanar.IntegerCompact.weight30 line 1448
lemma OAI.SharpPlanar.IntegerCompact.weight30_contains line 1449
def OAI.SharpPlanar.IntegerCompact.weight31 line 1453
lemma OAI.SharpPlanar.IntegerCompact.weight31_contains line 1454
def OAI.SharpPlanar.IntegerCompact.weight32 line 1458
lemma OAI.SharpPlanar.IntegerCompact.weight32_contains line 1459
def OAI.SharpPlanar.IntegerCompact.weight33 line 1463
lemma OAI.SharpPlanar.IntegerCompact.weight33_contains line 1464
def OAI.SharpPlanar.IntegerCompact.weight34 line 1468
lemma OAI.SharpPlanar.IntegerCompact.weight34_contains line 1469
def OAI.SharpPlanar.IntegerCompact.weight35 line 1473
lemma OAI.SharpPlanar.IntegerCompact.weight35_contains line 1474
def OAI.SharpPlanar.IntegerCompact.weight36 line 1478
lemma OAI.SharpPlanar.IntegerCompact.weight36_contains line 1479
def OAI.SharpPlanar.IntegerCompact.weight37 line 1483
lemma OAI.SharpPlanar.IntegerCompact.weight37_contains line 1484
def OAI.SharpPlanar.IntegerCompact.weight38 line 1488
lemma OAI.SharpPlanar.IntegerCompact.weight38_contains line 1489
def OAI.SharpPlanar.IntegerCompact.weight39 line 1493
lemma OAI.SharpPlanar.IntegerCompact.weight39_contains line 1494
def OAI.SharpPlanar.IntegerCompact.weight40 line 1498
lemma OAI.SharpPlanar.IntegerCompact.weight40_contains line 1499
def OAI.SharpPlanar.IntegerCompact.weight41 line 1503
lemma OAI.SharpPlanar.IntegerCompact.weight41_contains line 1504
def OAI.SharpPlanar.IntegerCompact.weight42 line 1508
lemma OAI.SharpPlanar.IntegerCompact.weight42_contains line 1509
def OAI.SharpPlanar.IntegerCompact.weight43 line 1513
lemma OAI.SharpPlanar.IntegerCompact.weight43_contains line 1514
def OAI.SharpPlanar.IntegerCompact.weight44 line 1518
lemma OAI.SharpPlanar.IntegerCompact.weight44_contains line 1519
def OAI.SharpPlanar.IntegerCompact.weight45 line 1523
lemma OAI.SharpPlanar.IntegerCompact.weight45_contains line 1524
def OAI.SharpPlanar.IntegerCompact.weight46 line 1528
lemma OAI.SharpPlanar.IntegerCompact.weight46_contains line 1529
def OAI.SharpPlanar.IntegerCompact.weight47 line 1533
lemma OAI.SharpPlanar.IntegerCompact.weight47_contains line 1534
def OAI.SharpPlanar.IntegerCompact.weight48 line 1538
lemma OAI.SharpPlanar.IntegerCompact.weight48_contains line 1539
def OAI.SharpPlanar.IntegerCompact.weight49 line 1543
lemma OAI.SharpPlanar.IntegerCompact.weight49_contains line 1544
def OAI.SharpPlanar.IntegerCompact.weight50 line 1548
lemma OAI.SharpPlanar.IntegerCompact.weight50_contains line 1549
def OAI.SharpPlanar.IntegerCompact.weight51 line 1553
lemma OAI.SharpPlanar.IntegerCompact.weight51_contains line 1554
def OAI.SharpPlanar.IntegerCompact.weight52 line 1558
lemma OAI.SharpPlanar.IntegerCompact.weight52_contains line 1559
def OAI.SharpPlanar.IntegerCompact.weight53 line 1563
lemma OAI.SharpPlanar.IntegerCompact.weight53_contains line 1564
def OAI.SharpPlanar.IntegerCompact.weight54 line 1568
lemma OAI.SharpPlanar.IntegerCompact.weight54_contains line 1569
def OAI.SharpPlanar.IntegerCompact.weight55 line 1573
lemma OAI.SharpPlanar.IntegerCompact.weight55_contains line 1574
def OAI.SharpPlanar.IntegerCompact.weight56 line 1578
lemma OAI.SharpPlanar.IntegerCompact.weight56_contains line 1579
def OAI.SharpPlanar.IntegerCompact.weight57 line 1583
lemma OAI.SharpPlanar.IntegerCompact.weight57_contains line 1584
def OAI.SharpPlanar.IntegerCompact.weight58 line 1588
lemma OAI.SharpPlanar.IntegerCompact.weight58_contains line 1589
def OAI.SharpPlanar.IntegerCompact.weight59 line 1593
lemma OAI.SharpPlanar.IntegerCompact.weight59_contains line 1594
def OAI.SharpPlanar.IntegerCompact.weight60 line 1598
lemma OAI.SharpPlanar.IntegerCompact.weight60_contains line 1599
def OAI.SharpPlanar.IntegerCompact.weight61 line 1603
lemma OAI.SharpPlanar.IntegerCompact.weight61_contains line 1604
def OAI.SharpPlanar.IntegerCompact.weight62 line 1608
lemma OAI.SharpPlanar.IntegerCompact.weight62_contains line 1609
def OAI.SharpPlanar.IntegerCompact.weight63 line 1613
lemma OAI.SharpPlanar.IntegerCompact.weight63_contains line 1614
def OAI.SharpPlanar.IntegerCompact.weight64 line 1618
lemma OAI.SharpPlanar.IntegerCompact.weight64_contains line 1619
def OAI.SharpPlanar.IntegerCompact.weight65 line 1623
lemma OAI.SharpPlanar.IntegerCompact.weight65_contains line 1624
def OAI.SharpPlanar.IntegerCompact.weight66 line 1628
lemma OAI.SharpPlanar.IntegerCompact.weight66_contains line 1629
def OAI.SharpPlanar.IntegerCompact.weight67 line 1633
lemma OAI.SharpPlanar.IntegerCompact.weight67_contains line 1634
def OAI.SharpPlanar.IntegerCompact.weight68 line 1638
lemma OAI.SharpPlanar.IntegerCompact.weight68_contains line 1639
def OAI.SharpPlanar.IntegerCompact.weight69 line 1643
lemma OAI.SharpPlanar.IntegerCompact.weight69_contains line 1644
def OAI.SharpPlanar.IntegerCompact.weight70 line 1648
lemma OAI.SharpPlanar.IntegerCompact.weight70_contains line 1649
def OAI.SharpPlanar.IntegerCompact.weight71 line 1653
lemma OAI.SharpPlanar.IntegerCompact.weight71_contains line 1654
def OAI.SharpPlanar.IntegerCompact.weight72 line 1658
lemma OAI.SharpPlanar.IntegerCompact.weight72_contains line 1659
def OAI.SharpPlanar.IntegerCompact.weight73 line 1663
lemma OAI.SharpPlanar.IntegerCompact.weight73_contains line 1664
def OAI.SharpPlanar.IntegerCompact.weight74 line 1668
lemma OAI.SharpPlanar.IntegerCompact.weight74_contains line 1669
def OAI.SharpPlanar.IntegerCompact.weight75 line 1673
lemma OAI.SharpPlanar.IntegerCompact.weight75_contains line 1674
def OAI.SharpPlanar.IntegerCompact.weight76 line 1678
lemma OAI.SharpPlanar.IntegerCompact.weight76_contains line 1679
def OAI.SharpPlanar.IntegerCompact.weight77 line 1683
lemma OAI.SharpPlanar.IntegerCompact.weight77_contains line 1684
def OAI.SharpPlanar.IntegerCompact.weight78 line 1688
lemma OAI.SharpPlanar.IntegerCompact.weight78_contains line 1689
def OAI.SharpPlanar.IntegerCompact.weight79 line 1693
lemma OAI.SharpPlanar.IntegerCompact.weight79_contains line 1694
def OAI.SharpPlanar.IntegerCompact.weight80 line 1698
lemma OAI.SharpPlanar.IntegerCompact.weight80_contains line 1699
def OAI.SharpPlanar.IntegerCompact.weight81 line 1703
lemma OAI.SharpPlanar.IntegerCompact.weight81_contains line 1704
def OAI.SharpPlanar.IntegerCompact.weight82 line 1708
lemma OAI.SharpPlanar.IntegerCompact.weight82_contains line 1709
def OAI.SharpPlanar.IntegerCompact.weight83 line 1713
lemma OAI.SharpPlanar.IntegerCompact.weight83_contains line 1714
def OAI.SharpPlanar.IntegerCompact.weight84 line 1718
lemma OAI.SharpPlanar.IntegerCompact.weight84_contains line 1719
def OAI.SharpPlanar.IntegerCompact.weight85 line 1723
lemma OAI.SharpPlanar.IntegerCompact.weight85_contains line 1724
def OAI.SharpPlanar.IntegerCompact.weight86 line 1728
lemma OAI.SharpPlanar.IntegerCompact.weight86_contains line 1729
def OAI.SharpPlanar.IntegerCompact.weight87 line 1733
lemma OAI.SharpPlanar.IntegerCompact.weight87_contains line 1734
def OAI.SharpPlanar.IntegerCompact.weight88 line 1738
lemma OAI.SharpPlanar.IntegerCompact.weight88_contains line 1739
def OAI.SharpPlanar.IntegerCompact.weight89 line 1743
lemma OAI.SharpPlanar.IntegerCompact.weight89_contains line 1744
def OAI.SharpPlanar.IntegerCompact.weight90 line 1748
lemma OAI.SharpPlanar.IntegerCompact.weight90_contains line 1749
def OAI.SharpPlanar.IntegerCompact.weight91 line 1753
lemma OAI.SharpPlanar.IntegerCompact.weight91_contains line 1754
def OAI.SharpPlanar.IntegerCompact.weight92 line 1758
lemma OAI.SharpPlanar.IntegerCompact.weight92_contains line 1759
def OAI.SharpPlanar.IntegerCompact.weight93 line 1763
lemma OAI.SharpPlanar.IntegerCompact.weight93_contains line 1764
def OAI.SharpPlanar.IntegerCompact.weight94 line 1768
lemma OAI.SharpPlanar.IntegerCompact.weight94_contains line 1769
def OAI.SharpPlanar.IntegerCompact.weight95 line 1773
lemma OAI.SharpPlanar.IntegerCompact.weight95_contains line 1774
def OAI.SharpPlanar.IntegerCompact.weight96 line 1778
lemma OAI.SharpPlanar.IntegerCompact.weight96_contains line 1779
def OAI.SharpPlanar.IntegerCompact.weight97 line 1783
lemma OAI.SharpPlanar.IntegerCompact.weight97_contains line 1784
def OAI.SharpPlanar.IntegerCompact.weight98 line 1788
lemma OAI.SharpPlanar.IntegerCompact.weight98_contains line 1789
def OAI.SharpPlanar.IntegerCompact.weight99 line 1793
lemma OAI.SharpPlanar.IntegerCompact.weight99_contains line 1794
def OAI.SharpPlanar.IntegerCompact.weight100 line 1798
lemma OAI.SharpPlanar.IntegerCompact.weight100_contains line 1799
def OAI.SharpPlanar.IntegerCompact.weight101 line 1803
lemma OAI.SharpPlanar.IntegerCompact.weight101_contains line 1804
def OAI.SharpPlanar.IntegerCompact.weight102 line 1808
lemma OAI.SharpPlanar.IntegerCompact.weight102_contains line 1809
def OAI.SharpPlanar.IntegerCompact.weight103 line 1813
lemma OAI.SharpPlanar.IntegerCompact.weight103_contains line 1814
def OAI.SharpPlanar.IntegerCompact.weight104 line 1818
lemma OAI.SharpPlanar.IntegerCompact.weight104_contains line 1819
def OAI.SharpPlanar.IntegerCompact.weight105 line 1823
lemma OAI.SharpPlanar.IntegerCompact.weight105_contains line 1824
def OAI.SharpPlanar.IntegerCompact.weight106 line 1828
lemma OAI.SharpPlanar.IntegerCompact.weight106_contains line 1829
def OAI.SharpPlanar.IntegerCompact.weight107 line 1833
lemma OAI.SharpPlanar.IntegerCompact.weight107_contains line 1834
def OAI.SharpPlanar.IntegerCompact.weight108 line 1838
lemma OAI.SharpPlanar.IntegerCompact.weight108_contains line 1839
def OAI.SharpPlanar.IntegerCompact.weight109 line 1843
lemma OAI.SharpPlanar.IntegerCompact.weight109_contains line 1844
def OAI.SharpPlanar.IntegerCompact.weight110 line 1848
lemma OAI.SharpPlanar.IntegerCompact.weight110_contains line 1849
def OAI.SharpPlanar.IntegerCompact.weight111 line 1853
lemma OAI.SharpPlanar.IntegerCompact.weight111_contains line 1854
def OAI.SharpPlanar.IntegerCompact.weight112 line 1858
lemma OAI.SharpPlanar.IntegerCompact.weight112_contains line 1859
def OAI.SharpPlanar.IntegerCompact.weight113 line 1863
lemma OAI.SharpPlanar.IntegerCompact.weight113_contains line 1864
def OAI.SharpPlanar.IntegerCompact.weight114 line 1868
lemma OAI.SharpPlanar.IntegerCompact.weight114_contains line 1869
def OAI.SharpPlanar.IntegerCompact.weight115 line 1873
lemma OAI.SharpPlanar.IntegerCompact.weight115_contains line 1874
def OAI.SharpPlanar.IntegerCompact.weight116 line 1878
lemma OAI.SharpPlanar.IntegerCompact.weight116_contains line 1879
def OAI.SharpPlanar.IntegerCompact.weight117 line 1883
lemma OAI.SharpPlanar.IntegerCompact.weight117_contains line 1884
def OAI.SharpPlanar.IntegerCompact.weight118 line 1888
lemma OAI.SharpPlanar.IntegerCompact.weight118_contains line 1889
def OAI.SharpPlanar.IntegerCompact.weight119 line 1893
lemma OAI.SharpPlanar.IntegerCompact.weight119_contains line 1894
def OAI.SharpPlanar.IntegerCompact.weight120 line 1898
lemma OAI.SharpPlanar.IntegerCompact.weight120_contains line 1899
def OAI.SharpPlanar.IntegerCompact.weight121 line 1903
lemma OAI.SharpPlanar.IntegerCompact.weight121_contains line 1904
def OAI.SharpPlanar.IntegerCompact.weight122 line 1908
lemma OAI.SharpPlanar.IntegerCompact.weight122_contains line 1909
def OAI.SharpPlanar.IntegerCompact.weight123 line 1913
lemma OAI.SharpPlanar.IntegerCompact.weight123_contains line 1914
def OAI.SharpPlanar.IntegerCompact.weight124 line 1918
lemma OAI.SharpPlanar.IntegerCompact.weight124_contains line 1919
def OAI.SharpPlanar.IntegerCompact.weight125 line 1923
lemma OAI.SharpPlanar.IntegerCompact.weight125_contains line 1924
def OAI.SharpPlanar.IntegerCompact.weight126 line 1928
lemma OAI.SharpPlanar.IntegerCompact.weight126_contains line 1929
def OAI.SharpPlanar.IntegerCompact.weight127 line 1933
lemma OAI.SharpPlanar.IntegerCompact.weight127_contains line 1934
def OAI.SharpPlanar.IntegerCompact.weight128 line 1938
lemma OAI.SharpPlanar.IntegerCompact.weight128_contains line 1939
def OAI.SharpPlanar.IntegerCompact.weight129 line 1942
lemma OAI.SharpPlanar.IntegerCompact.weight129_contains line 1943
def OAI.SharpPlanar.IntegerCompact.weight130 line 1946
lemma OAI.SharpPlanar.IntegerCompact.weight130_contains line 1947
def OAI.SharpPlanar.IntegerCompact.weight131 line 1950
lemma OAI.SharpPlanar.IntegerCompact.weight131_contains line 1951
def OAI.SharpPlanar.IntegerCompact.weight132 line 1954
lemma OAI.SharpPlanar.IntegerCompact.weight132_contains line 1955
def OAI.SharpPlanar.IntegerCompact.weight133 line 1958
lemma OAI.SharpPlanar.IntegerCompact.weight133_contains line 1959
def OAI.SharpPlanar.IntegerCompact.weight134 line 1962
lemma OAI.SharpPlanar.IntegerCompact.weight134_contains line 1963
def OAI.SharpPlanar.IntegerCompact.weight135 line 1966
lemma OAI.SharpPlanar.IntegerCompact.weight135_contains line 1967
def OAI.SharpPlanar.IntegerCompact.weight136 line 1970
lemma OAI.SharpPlanar.IntegerCompact.weight136_contains line 1971
def OAI.SharpPlanar.IntegerCompact.weight137 line 1974
lemma OAI.SharpPlanar.IntegerCompact.weight137_contains line 1975
def OAI.SharpPlanar.IntegerCompact.weight138 line 1978
lemma OAI.SharpPlanar.IntegerCompact.weight138_contains line 1979
def OAI.SharpPlanar.IntegerCompact.weight139 line 1982
lemma OAI.SharpPlanar.IntegerCompact.weight139_contains line 1983
def OAI.SharpPlanar.IntegerCompact.weight140 line 1986
lemma OAI.SharpPlanar.IntegerCompact.weight140_contains line 1987
def OAI.SharpPlanar.IntegerCompact.weight141 line 1990
lemma OAI.SharpPlanar.IntegerCompact.weight141_contains line 1991
def OAI.SharpPlanar.IntegerCompact.weight142 line 1994
lemma OAI.SharpPlanar.IntegerCompact.weight142_contains line 1995
def OAI.SharpPlanar.IntegerCompact.weight143 line 1998
lemma OAI.SharpPlanar.IntegerCompact.weight143_contains line 1999
def OAI.SharpPlanar.IntegerCompact.weight144 line 2002
lemma OAI.SharpPlanar.IntegerCompact.weight144_contains line 2003
def OAI.SharpPlanar.IntegerCompact.weight145 line 2006
lemma OAI.SharpPlanar.IntegerCompact.weight145_contains line 2007
def OAI.SharpPlanar.IntegerCompact.weight146 line 2010
lemma OAI.SharpPlanar.IntegerCompact.weight146_contains line 2011
def OAI.SharpPlanar.IntegerCompact.weight147 line 2014
lemma OAI.SharpPlanar.IntegerCompact.weight147_contains line 2015
def OAI.SharpPlanar.IntegerCompact.weight148 line 2018
lemma OAI.SharpPlanar.IntegerCompact.weight148_contains line 2019
def OAI.SharpPlanar.IntegerCompact.weight149 line 2022
lemma OAI.SharpPlanar.IntegerCompact.weight149_contains line 2023
def OAI.SharpPlanar.IntegerCompact.weight150 line 2026
lemma OAI.SharpPlanar.IntegerCompact.weight150_contains line 2027
def OAI.SharpPlanar.IntegerCompact.weight151 line 2030
lemma OAI.SharpPlanar.IntegerCompact.weight151_contains line 2031
def OAI.SharpPlanar.IntegerCompact.weight152 line 2034
lemma OAI.SharpPlanar.IntegerCompact.weight152_contains line 2035
def OAI.SharpPlanar.IntegerCompact.weight153 line 2038
lemma OAI.SharpPlanar.IntegerCompact.weight153_contains line 2039
def OAI.SharpPlanar.IntegerCompact.weight154 line 2042
lemma OAI.SharpPlanar.IntegerCompact.weight154_contains line 2043
def OAI.SharpPlanar.IntegerCompact.weight155 line 2046
lemma OAI.SharpPlanar.IntegerCompact.weight155_contains line 2047
def OAI.SharpPlanar.IntegerCompact.weight156 line 2050
lemma OAI.SharpPlanar.IntegerCompact.weight156_contains line 2051
def OAI.SharpPlanar.IntegerCompact.weight157 line 2054
lemma OAI.SharpPlanar.IntegerCompact.weight157_contains line 2055
def OAI.SharpPlanar.IntegerCompact.weight158 line 2058
lemma OAI.SharpPlanar.IntegerCompact.weight158_contains line 2059
def OAI.SharpPlanar.IntegerCompact.weight159 line 2062
lemma OAI.SharpPlanar.IntegerCompact.weight159_contains line 2063
def OAI.SharpPlanar.IntegerCompact.weight160 line 2066
lemma OAI.SharpPlanar.IntegerCompact.weight160_contains line 2067
def OAI.SharpPlanar.IntegerCompact.weight161 line 2070
lemma OAI.SharpPlanar.IntegerCompact.weight161_contains line 2071
def OAI.SharpPlanar.IntegerCompact.weight162 line 2074
lemma OAI.SharpPlanar.IntegerCompact.weight162_contains line 2075
def OAI.SharpPlanar.IntegerCompact.weight163 line 2078
lemma OAI.SharpPlanar.IntegerCompact.weight163_contains line 2079
def OAI.SharpPlanar.IntegerCompact.weight164 line 2082
lemma OAI.SharpPlanar.IntegerCompact.weight164_contains line 2083
def OAI.SharpPlanar.IntegerCompact.weight165 line 2086
lemma OAI.SharpPlanar.IntegerCompact.weight165_contains line 2087
def OAI.SharpPlanar.IntegerCompact.weight166 line 2090
lemma OAI.SharpPlanar.IntegerCompact.weight166_contains line 2091
def OAI.SharpPlanar.IntegerCompact.weight167 line 2094
lemma OAI.SharpPlanar.IntegerCompact.weight167_contains line 2095
def OAI.SharpPlanar.IntegerCompact.weight168 line 2098
lemma OAI.SharpPlanar.IntegerCompact.weight168_contains line 2099
def OAI.SharpPlanar.IntegerCompact.weight169 line 2102
lemma OAI.SharpPlanar.IntegerCompact.weight169_contains line 2103
def OAI.SharpPlanar.IntegerCompact.weight170 line 2106
lemma OAI.SharpPlanar.IntegerCompact.weight170_contains line 2107
def OAI.SharpPlanar.IntegerCompact.weight171 line 2110
lemma OAI.SharpPlanar.IntegerCompact.weight171_contains line 2111
def OAI.SharpPlanar.IntegerCompact.weight172 line 2114
lemma OAI.SharpPlanar.IntegerCompact.weight172_contains line 2115
def OAI.SharpPlanar.IntegerCompact.weight173 line 2118
lemma OAI.SharpPlanar.IntegerCompact.weight173_contains line 2119
def OAI.SharpPlanar.IntegerCompact.weight174 line 2122
lemma OAI.SharpPlanar.IntegerCompact.weight174_contains line 2123
def OAI.SharpPlanar.IntegerCompact.weight175 line 2126
lemma OAI.SharpPlanar.IntegerCompact.weight175_contains line 2127
def OAI.SharpPlanar.IntegerCompact.weight176 line 2130
lemma OAI.SharpPlanar.IntegerCompact.weight176_contains line 2131
def OAI.SharpPlanar.IntegerCompact.weight177 line 2134
lemma OAI.SharpPlanar.IntegerCompact.weight177_contains line 2135
def OAI.SharpPlanar.IntegerCompact.weight178 line 2138
lemma OAI.SharpPlanar.IntegerCompact.weight178_contains line 2139
def OAI.SharpPlanar.IntegerCompact.weight179 line 2142
lemma OAI.SharpPlanar.IntegerCompact.weight179_contains line 2143
def OAI.SharpPlanar.IntegerCompact.weight180 line 2146
lemma OAI.SharpPlanar.IntegerCompact.weight180_contains line 2147
def OAI.SharpPlanar.IntegerCompact.weight181 line 2150
lemma OAI.SharpPlanar.IntegerCompact.weight181_contains line 2151
def OAI.SharpPlanar.IntegerCompact.weight182 line 2154
lemma OAI.SharpPlanar.IntegerCompact.weight182_contains line 2155
def OAI.SharpPlanar.IntegerCompact.weight183 line 2158
lemma OAI.SharpPlanar.IntegerCompact.weight183_contains line 2159
def OAI.SharpPlanar.IntegerCompact.weight184 line 2162
lemma OAI.SharpPlanar.IntegerCompact.weight184_contains line 2163
def OAI.SharpPlanar.IntegerCompact.weight185 line 2166
lemma OAI.SharpPlanar.IntegerCompact.weight185_contains line 2167
def OAI.SharpPlanar.IntegerCompact.weight186 line 2170
lemma OAI.SharpPlanar.IntegerCompact.weight186_contains line 2171
def OAI.SharpPlanar.IntegerCompact.weight187 line 2174
lemma OAI.SharpPlanar.IntegerCompact.weight187_contains line 2175
def OAI.SharpPlanar.IntegerCompact.weight188 line 2178
lemma OAI.SharpPlanar.IntegerCompact.weight188_contains line 2179
def OAI.SharpPlanar.IntegerCompact.weight189 line 2182
lemma OAI.SharpPlanar.IntegerCompact.weight189_contains line 2183
def OAI.SharpPlanar.IntegerCompact.weight190 line 2186
lemma OAI.SharpPlanar.IntegerCompact.weight190_contains line 2187
def OAI.SharpPlanar.IntegerCompact.weight191 line 2190
lemma OAI.SharpPlanar.IntegerCompact.weight191_contains line 2191
def OAI.SharpPlanar.IntegerCompact.weight192 line 2194
lemma OAI.SharpPlanar.IntegerCompact.weight192_contains line 2195
def OAI.SharpPlanar.IntegerCompact.weight193 line 2198
lemma OAI.SharpPlanar.IntegerCompact.weight193_contains line 2199
def OAI.SharpPlanar.IntegerCompact.weight194 line 2202
lemma OAI.SharpPlanar.IntegerCompact.weight194_contains line 2203
def OAI.SharpPlanar.IntegerCompact.weight195 line 2206
lemma OAI.SharpPlanar.IntegerCompact.weight195_contains line 2207
def OAI.SharpPlanar.IntegerCompact.weight196 line 2210
lemma OAI.SharpPlanar.IntegerCompact.weight196_contains line 2211
def OAI.SharpPlanar.IntegerCompact.weight197 line 2214
lemma OAI.SharpPlanar.IntegerCompact.weight197_contains line 2215
def OAI.SharpPlanar.IntegerCompact.weight198 line 2218
lemma OAI.SharpPlanar.IntegerCompact.weight198_contains line 2219
def OAI.SharpPlanar.IntegerCompact.weight199 line 2222
lemma OAI.SharpPlanar.IntegerCompact.weight199_contains line 2223
def OAI.SharpPlanar.IntegerCompact.weight200 line 2226
lemma OAI.SharpPlanar.IntegerCompact.weight200_contains line 2227
def OAI.SharpPlanar.IntegerCompact.weight201 line 2230
lemma OAI.SharpPlanar.IntegerCompact.weight201_contains line 2231
def OAI.SharpPlanar.IntegerCompact.weight202 line 2234
lemma OAI.SharpPlanar.IntegerCompact.weight202_contains line 2235
def OAI.SharpPlanar.IntegerCompact.weight203 line 2238
lemma OAI.SharpPlanar.IntegerCompact.weight203_contains line 2239
def OAI.SharpPlanar.IntegerCompact.weight204 line 2242
lemma OAI.SharpPlanar.IntegerCompact.weight204_contains line 2243
def OAI.SharpPlanar.IntegerCompact.weight205 line 2246
lemma OAI.SharpPlanar.IntegerCompact.weight205_contains line 2247
def OAI.SharpPlanar.IntegerCompact.weight206 line 2250
lemma OAI.SharpPlanar.IntegerCompact.weight206_contains line 2251
def OAI.SharpPlanar.IntegerCompact.weight207 line 2254
lemma OAI.SharpPlanar.IntegerCompact.weight207_contains line 2255
def OAI.SharpPlanar.IntegerCompact.weight208 line 2258
lemma OAI.SharpPlanar.IntegerCompact.weight208_contains line 2259
def OAI.SharpPlanar.IntegerCompact.weight209 line 2262
lemma OAI.SharpPlanar.IntegerCompact.weight209_contains line 2263
def OAI.SharpPlanar.IntegerCompact.weight210 line 2266
lemma OAI.SharpPlanar.IntegerCompact.weight210_contains line 2267
def OAI.SharpPlanar.IntegerCompact.weight211 line 2270
lemma OAI.SharpPlanar.IntegerCompact.weight211_contains line 2271
def OAI.SharpPlanar.IntegerCompact.weight212 line 2274
lemma OAI.SharpPlanar.IntegerCompact.weight212_contains line 2275
def OAI.SharpPlanar.IntegerCompact.weight213 line 2278
lemma OAI.SharpPlanar.IntegerCompact.weight213_contains line 2279
def OAI.SharpPlanar.IntegerCompact.weight214 line 2282
lemma OAI.SharpPlanar.IntegerCompact.weight214_contains line 2283
def OAI.SharpPlanar.IntegerCompact.weight215 line 2286
lemma OAI.SharpPlanar.IntegerCompact.weight215_contains line 2287
def OAI.SharpPlanar.IntegerCompact.weight216 line 2290
lemma OAI.SharpPlanar.IntegerCompact.weight216_contains line 2291
def OAI.SharpPlanar.IntegerCompact.weight217 line 2294
lemma OAI.SharpPlanar.IntegerCompact.weight217_contains line 2295
def OAI.SharpPlanar.IntegerCompact.weight218 line 2298
lemma OAI.SharpPlanar.IntegerCompact.weight218_contains line 2299
def OAI.SharpPlanar.IntegerCompact.weight219 line 2302
lemma OAI.SharpPlanar.IntegerCompact.weight219_contains line 2303
def OAI.SharpPlanar.IntegerCompact.weight220 line 2306
lemma OAI.SharpPlanar.IntegerCompact.weight220_contains line 2307
def OAI.SharpPlanar.IntegerCompact.weight221 line 2310
lemma OAI.SharpPlanar.IntegerCompact.weight221_contains line 2311
def OAI.SharpPlanar.IntegerCompact.weight222 line 2314
lemma OAI.SharpPlanar.IntegerCompact.weight222_contains line 2315
def OAI.SharpPlanar.IntegerCompact.weight223 line 2318
lemma OAI.SharpPlanar.IntegerCompact.weight223_contains line 2319
def OAI.SharpPlanar.IntegerCompact.weight224 line 2322
lemma OAI.SharpPlanar.IntegerCompact.weight224_contains line 2323
def OAI.SharpPlanar.IntegerCompact.weight225 line 2326
lemma OAI.SharpPlanar.IntegerCompact.weight225_contains line 2327
def OAI.SharpPlanar.IntegerCompact.weight226 line 2330
lemma OAI.SharpPlanar.IntegerCompact.weight226_contains line 2331
def OAI.SharpPlanar.IntegerCompact.weight227 line 2334
lemma OAI.SharpPlanar.IntegerCompact.weight227_contains line 2335
def OAI.SharpPlanar.IntegerCompact.weight228 line 2338
lemma OAI.SharpPlanar.IntegerCompact.weight228_contains line 2339
def OAI.SharpPlanar.IntegerCompact.weight229 line 2342
lemma OAI.SharpPlanar.IntegerCompact.weight229_contains line 2343
def OAI.SharpPlanar.IntegerCompact.weight230 line 2346
lemma OAI.SharpPlanar.IntegerCompact.weight230_contains line 2347
def OAI.SharpPlanar.IntegerCompact.weight231 line 2350
lemma OAI.SharpPlanar.IntegerCompact.weight231_contains line 2351
def OAI.SharpPlanar.IntegerCompact.weight232 line 2354
lemma OAI.SharpPlanar.IntegerCompact.weight232_contains line 2355
def OAI.SharpPlanar.IntegerCompact.weight233 line 2358
lemma OAI.SharpPlanar.IntegerCompact.weight233_contains line 2359
def OAI.SharpPlanar.IntegerCompact.weight234 line 2362
lemma OAI.SharpPlanar.IntegerCompact.weight234_contains line 2363
def OAI.SharpPlanar.IntegerCompact.weight235 line 2366
lemma OAI.SharpPlanar.IntegerCompact.weight235_contains line 2367
def OAI.SharpPlanar.IntegerCompact.weight236 line 2370
lemma OAI.SharpPlanar.IntegerCompact.weight236_contains line 2371
def OAI.SharpPlanar.IntegerCompact.weight237 line 2374
lemma OAI.SharpPlanar.IntegerCompact.weight237_contains line 2375
def OAI.SharpPlanar.IntegerCompact.weight238 line 2378
lemma OAI.SharpPlanar.IntegerCompact.weight238_contains line 2379
def OAI.SharpPlanar.IntegerCompact.weight239 line 2382
lemma OAI.SharpPlanar.IntegerCompact.weight239_contains line 2383
def OAI.SharpPlanar.IntegerCompact.weight240 line 2386
lemma OAI.SharpPlanar.IntegerCompact.weight240_contains line 2387
def OAI.SharpPlanar.IntegerCompact.weight241 line 2390
lemma OAI.SharpPlanar.IntegerCompact.weight241_contains line 2391
def OAI.SharpPlanar.IntegerCompact.weight242 line 2394
lemma OAI.SharpPlanar.IntegerCompact.weight242_contains line 2395
def OAI.SharpPlanar.IntegerCompact.weight243 line 2398
lemma OAI.SharpPlanar.IntegerCompact.weight243_contains line 2399
def OAI.SharpPlanar.IntegerCompact.weight244 line 2402
lemma OAI.SharpPlanar.IntegerCompact.weight244_contains line 2403
def OAI.SharpPlanar.IntegerCompact.weight245 line 2406
lemma OAI.SharpPlanar.IntegerCompact.weight245_contains line 2407
def OAI.SharpPlanar.IntegerCompact.weight246 line 2410
lemma OAI.SharpPlanar.IntegerCompact.weight246_contains line 2411
def OAI.SharpPlanar.IntegerCompact.weight247 line 2414
lemma OAI.SharpPlanar.IntegerCompact.weight247_contains line 2415
def OAI.SharpPlanar.IntegerCompact.weight248 line 2418
lemma OAI.SharpPlanar.IntegerCompact.weight248_contains line 2419
def OAI.SharpPlanar.IntegerCompact.weight249 line 2422
lemma OAI.SharpPlanar.IntegerCompact.weight249_contains line 2423
def OAI.SharpPlanar.IntegerCompact.weight250 line 2426
lemma OAI.SharpPlanar.IntegerCompact.weight250_contains line 2427
def OAI.SharpPlanar.IntegerCompact.weight251 line 2430
lemma OAI.SharpPlanar.IntegerCompact.weight251_contains line 2431
def OAI.SharpPlanar.IntegerCompact.weight252 line 2434
lemma OAI.SharpPlanar.IntegerCompact.weight252_contains line 2435
def OAI.SharpPlanar.IntegerCompact.weight253 line 2438
lemma OAI.SharpPlanar.IntegerCompact.weight253_contains line 2439
def OAI.SharpPlanar.IntegerCompact.weight254 line 2442
lemma OAI.SharpPlanar.IntegerCompact.weight254_contains line 2443
def OAI.SharpPlanar.IntegerCompact.weight255 line 2446
lemma OAI.SharpPlanar.IntegerCompact.weight255_contains line 2447
def OAI.SharpPlanar.IntegerCompact.weights0 line 2450
lemma OAI.SharpPlanar.IntegerCompact.weights0_contains line 2451
def OAI.SharpPlanar.IntegerCompact.weights1 line 2469
lemma OAI.SharpPlanar.IntegerCompact.weights1_contains line 2470
def OAI.SharpPlanar.IntegerCompact.weights2 line 2488
lemma OAI.SharpPlanar.IntegerCompact.weights2_contains line 2489
def OAI.SharpPlanar.IntegerCompact.weights3 line 2507
lemma OAI.SharpPlanar.IntegerCompact.weights3_contains line 2508
def OAI.SharpPlanar.IntegerCompact.weights4 line 2526
lemma OAI.SharpPlanar.IntegerCompact.weights4_contains line 2527
def OAI.SharpPlanar.IntegerCompact.weights5 line 2545
lemma OAI.SharpPlanar.IntegerCompact.weights5_contains line 2546
def OAI.SharpPlanar.IntegerCompact.weights6 line 2564
lemma OAI.SharpPlanar.IntegerCompact.weights6_contains line 2565
def OAI.SharpPlanar.IntegerCompact.weights7 line 2583
lemma OAI.SharpPlanar.IntegerCompact.weights7_contains line 2584
def OAI.SharpPlanar.IntegerCompact.weights8 line 2602
lemma OAI.SharpPlanar.IntegerCompact.weights8_contains line 2603
def OAI.SharpPlanar.IntegerCompact.weights9 line 2621
lemma OAI.SharpPlanar.IntegerCompact.weights9_contains line 2622
def OAI.SharpPlanar.IntegerCompact.weights10 line 2640
lemma OAI.SharpPlanar.IntegerCompact.weights10_contains line 2641
def OAI.SharpPlanar.IntegerCompact.weights11 line 2659
lemma OAI.SharpPlanar.IntegerCompact.weights11_contains line 2660
def OAI.SharpPlanar.IntegerCompact.weights12 line 2678
lemma OAI.SharpPlanar.IntegerCompact.weights12_contains line 2679
def OAI.SharpPlanar.IntegerCompact.weights13 line 2697
lemma OAI.SharpPlanar.IntegerCompact.weights13_contains line 2698
def OAI.SharpPlanar.IntegerCompact.weights14 line 2716
lemma OAI.SharpPlanar.IntegerCompact.weights14_contains line 2717
def OAI.SharpPlanar.IntegerCompact.weights15 line 2735
lemma OAI.SharpPlanar.IntegerCompact.weights15_contains line 2736
def OAI.SharpPlanar.IntegerCompact.weightRows line 2754
lemma OAI.SharpPlanar.IntegerCompact.weightRows_contains line 2755
def OAI.SharpPlanar.IntegerCompact.weightLookup line 2773
lemma OAI.SharpPlanar.IntegerCompact.weightLookup_contains line 2775
def OAI.SharpPlanar.IntegerCompact.nodeLookup line 2779
lemma OAI.SharpPlanar.IntegerCompact.nodeLookup_contains line 2780