OAI/Computability/BinPacking/Packing/PackingScalarExpression.lean

GitHub source file

139 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.InventoryData.coordinateDenominator line 12
  2. theorem OAI.BinPackingGap.InventoryData.coordinateDenominator_pos line 15
  3. def OAI.BinPackingGap.InventoryData.treeBaselineInteger line 18
  4. def OAI.BinPackingGap.InventoryData.rowBaselineInteger line 25
  5. def OAI.BinPackingGap.InventoryData.treeDeadlineInteger line 30
  6. def OAI.BinPackingGap.InventoryData.deadlineInteger line 41
  7. def OAI.BinPackingGap.InventoryData.rowIntegerCoordinate line 46
  8. def OAI.BinPackingGap.InventoryData.anchorIntegerCoordinate line 49
  9. def OAI.BinPackingGap.InventoryData.globalIntegerCoordinate line 55
  10. def OAI.BinPackingGap.InventoryData.localIntegerCoordinate line 62
  11. def OAI.BinPackingGap.InventoryData.itemIntegerCoordinate line 66
  12. theorem OAI.BinPackingGap.InventoryData.coordinateDenominator_mul_treeBaseline line 76
  13. theorem OAI.BinPackingGap.InventoryData.coordinateDenominator_mul_rowBaseline line 91
  14. theorem OAI.BinPackingGap.InventoryData.coordinateDenominator_mul_treeDeadline line 99
  15. theorem OAI.BinPackingGap.InventoryData.coordinateDenominator_mul_deadline line 126
  16. theorem OAI.BinPackingGap.InventoryData.coordinateDenominator_mul_rowCoordinate line 136
  17. theorem OAI.BinPackingGap.InventoryData.coordinateDenominator_mul_anchorCoordinate line 147
  18. theorem OAI.BinPackingGap.InventoryData.coordinateDenominator_mul_globalCoordinate line 157
  19. theorem OAI.BinPackingGap.InventoryData.coordinateDenominator_mul_localCoordinate line 171
  20. theorem OAI.BinPackingGap.InventoryData.coordinateDenominator_mul_itemCoordinate line 183
  21. theorem OAI.BinPackingGap.InventoryData.itemIntegerCoordinate_ratio line 195
  22. def OAI.BinPackingGap.InventoryData.itemRawPair line 203
  23. theorem OAI.BinPackingGap.InventoryData.itemRawPair_valid line 208
  24. theorem OAI.BinPackingGap.InventoryData.itemRawPair_ratio line 215
  25. structure OAI.BinPackingGap.NaturalPackingNumerator.NatDifference line 231
  26. def OAI.BinPackingGap.NaturalPackingNumerator.NatDifference.eval line 238
  27. def OAI.BinPackingGap.NaturalPackingNumerator.NatDifference.ofNat line 240
  28. def OAI.BinPackingGap.NaturalPackingNumerator.NatDifference.ofInt line 242
  29. def OAI.BinPackingGap.NaturalPackingNumerator.NatDifference.negate line 244
  30. def OAI.BinPackingGap.NaturalPackingNumerator.NatDifference.add line 246
  31. def OAI.BinPackingGap.NaturalPackingNumerator.NatDifference.sub line 248
  32. def OAI.BinPackingGap.NaturalPackingNumerator.NatDifference.scale line 250
  33. def OAI.BinPackingGap.NaturalPackingNumerator.NatDifference.toNat line 252
  34. theorem OAI.BinPackingGap.NaturalPackingNumerator.NatDifference.eval_ofNat line 254
  35. theorem OAI.BinPackingGap.NaturalPackingNumerator.NatDifference.eval_ofInt line 257
  36. theorem OAI.BinPackingGap.NaturalPackingNumerator.NatDifference.eval_negate line 260
  37. theorem OAI.BinPackingGap.NaturalPackingNumerator.NatDifference.eval_add line 264
  38. theorem OAI.BinPackingGap.NaturalPackingNumerator.NatDifference.eval_sub line 268
  39. theorem OAI.BinPackingGap.NaturalPackingNumerator.NatDifference.eval_scale line 272
  40. theorem OAI.BinPackingGap.NaturalPackingNumerator.NatDifference.toNat_eq line 277
  41. def OAI.BinPackingGap.NaturalPackingNumerator.baselineParts line 283
  42. def OAI.BinPackingGap.NaturalPackingNumerator.betaParts line 288
  43. theorem OAI.BinPackingGap.NaturalPackingNumerator.eval_baselineParts line 291
  44. theorem OAI.BinPackingGap.NaturalPackingNumerator.eval_betaParts line 297
  45. def OAI.BinPackingGap.NaturalPackingNumerator.treeBaselineParts line 307
  46. def OAI.BinPackingGap.NaturalPackingNumerator.rowBaselineParts line 314
  47. def OAI.BinPackingGap.NaturalPackingNumerator.treeDeadlineParts line 318
  48. def OAI.BinPackingGap.NaturalPackingNumerator.deadlineParts line 329
  49. def OAI.BinPackingGap.NaturalPackingNumerator.rowParts line 334
  50. def OAI.BinPackingGap.NaturalPackingNumerator.anchorParts line 337
  51. def OAI.BinPackingGap.NaturalPackingNumerator.globalParts line 343
  52. def OAI.BinPackingGap.NaturalPackingNumerator.localParts line 350
  53. def OAI.BinPackingGap.NaturalPackingNumerator.coordinateParts line 355
  54. theorem OAI.BinPackingGap.NaturalPackingNumerator.eval_treeBaselineParts line 362
  55. theorem OAI.BinPackingGap.NaturalPackingNumerator.eval_rowBaselineParts line 367
  56. theorem OAI.BinPackingGap.NaturalPackingNumerator.eval_treeDeadlineParts line 372
  57. theorem OAI.BinPackingGap.NaturalPackingNumerator.eval_deadlineParts line 381
  58. theorem OAI.BinPackingGap.NaturalPackingNumerator.eval_rowParts line 386
  59. theorem OAI.BinPackingGap.NaturalPackingNumerator.eval_anchorParts line 391
  60. theorem OAI.BinPackingGap.NaturalPackingNumerator.eval_globalParts line 396
  61. theorem OAI.BinPackingGap.NaturalPackingNumerator.eval_localParts line 404
  62. theorem OAI.BinPackingGap.NaturalPackingNumerator.eval_coordinateParts line 409
  63. def OAI.BinPackingGap.NaturalPackingNumerator.primaryParts line 421
  64. theorem OAI.BinPackingGap.NaturalPackingNumerator.eval_primaryParts line 423
  65. def OAI.BinPackingGap.NaturalPackingNumerator.labelPower line 427
  66. def OAI.BinPackingGap.NaturalPackingNumerator.secondaryParts line 430
  67. theorem OAI.BinPackingGap.NaturalPackingNumerator.eval_secondaryParts line 438
  68. def OAI.BinPackingGap.NaturalPackingNumerator.signedParts line 443
  69. theorem OAI.BinPackingGap.NaturalPackingNumerator.signedParts_pos line 448
  70. theorem OAI.BinPackingGap.NaturalPackingNumerator.signedParts_neg line 453
  71. theorem OAI.BinPackingGap.NaturalPackingNumerator.signedParts_toNat line 458
  72. theorem OAI.BinPackingGap.NaturalPackingNumerator.eval_signedParts line 465
  73. def OAI.BinPackingGap.NaturalPackingNumerator.numeratorParts line 470
  74. theorem OAI.BinPackingGap.NaturalPackingNumerator.eval_numeratorParts line 474
  75. theorem OAI.BinPackingGap.NaturalPackingNumerator.numeratorParts_toNat line 479
  76. def OAI.BinPackingGap.NaturalPackingNumerator.inventoryParts line 484
  77. def OAI.BinPackingGap.NaturalPackingNumerator.inventoryNumerator line 488
  78. theorem OAI.BinPackingGap.NaturalPackingNumerator.inventoryNumerator_eq line 491
  79. def OAI.BinPackingGap.NaturalPackingNumerator.naturalRawItem line 497
  80. theorem OAI.BinPackingGap.NaturalPackingNumerator.naturalRawItem_eq line 500
  81. inductive OAI.BinPackingGap.PackingCoordinateExpression.Input line 512
  82. instance OAI.BinPackingGap.PackingCoordinateExpression.(instance at line 519) line 519
  83. structure OAI.BinPackingGap.PackingCoordinateExpression.Parts line 523
  84. def OAI.BinPackingGap.PackingCoordinateExpression.Parts.eval line 529
  85. def OAI.BinPackingGap.PackingCoordinateExpression.Parts.ofExpr line 532
  86. def OAI.BinPackingGap.PackingCoordinateExpression.Parts.negate line 533
  87. def OAI.BinPackingGap.PackingCoordinateExpression.Parts.add line 534
  88. def OAI.BinPackingGap.PackingCoordinateExpression.Parts.sub line 535
  89. theorem OAI.BinPackingGap.PackingCoordinateExpression.Parts.eval_ofExpr line 537
  90. theorem OAI.BinPackingGap.PackingCoordinateExpression.Parts.eval_negate line 540
  91. theorem OAI.BinPackingGap.PackingCoordinateExpression.Parts.eval_add line 543
  92. theorem OAI.BinPackingGap.PackingCoordinateExpression.Parts.eval_sub line 546
  93. inductive OAI.BinPackingGap.PackingCoordinateExpression.TreeDescriptor line 551
  94. instance OAI.BinPackingGap.PackingCoordinateExpression.(instance at line 557) line 557
  95. inductive OAI.BinPackingGap.PackingCoordinateExpression.Descriptor line 562
  96. instance OAI.BinPackingGap.PackingCoordinateExpression.(instance at line 574) line 574
  97. def OAI.BinPackingGap.PackingCoordinateExpression.treeLeftExpr line 584
  98. def OAI.BinPackingGap.PackingCoordinateExpression.treeRightExpr line 589
  99. def OAI.BinPackingGap.PackingCoordinateExpression.treeBaselineExpr line 595
  100. def OAI.BinPackingGap.PackingCoordinateExpression.treeDeadlineExpr line 601
  101. def OAI.BinPackingGap.PackingCoordinateExpression.baselineExpr line 611
  102. def OAI.BinPackingGap.PackingCoordinateExpression.betaExpr line 620
  103. def OAI.BinPackingGap.PackingCoordinateExpression.expression line 624
  104. def OAI.BinPackingGap.PackingCoordinateExpression.registers line 640
  105. def OAI.BinPackingGap.PackingCoordinateExpression.treeDescriptor line 646
  106. def OAI.BinPackingGap.PackingCoordinateExpression.coordinateDescriptor line 651
  107. def OAI.BinPackingGap.PackingCoordinateExpression.edgeIndex line 665
  108. def OAI.BinPackingGap.PackingCoordinateExpression.repetitionOne line 672
  109. def OAI.BinPackingGap.PackingCoordinateExpression.coordinateValues line 678
  110. theorem OAI.BinPackingGap.PackingCoordinateExpression.eval_treeLeftExpr line 681
  111. theorem OAI.BinPackingGap.PackingCoordinateExpression.eval_treeRightExpr line 687
  112. theorem OAI.BinPackingGap.PackingCoordinateExpression.eval_treeBaselineExpr line 695
  113. theorem OAI.BinPackingGap.PackingCoordinateExpression.eval_treeDeadlineExpr line 701
  114. theorem OAI.BinPackingGap.PackingCoordinateExpression.eval_baselineExpr line 711
  115. theorem OAI.BinPackingGap.PackingCoordinateExpression.eval_betaExpr line 717
  116. theorem OAI.BinPackingGap.PackingCoordinateExpression.eval_coordinateDescriptor line 722
  117. theorem OAI.BinPackingGap.PackingCoordinateExpression.eval_coordinate_pos line 756
  118. theorem OAI.BinPackingGap.PackingCoordinateExpression.eval_coordinate_neg line 762
  119. theorem OAI.BinPackingGap.PackingCoordinateExpression.eval_coordinate_integer line 768
  120. inductive OAI.BinPackingGap.PackingScalarExpression.Variable line 779
  121. instance OAI.BinPackingGap.PackingScalarExpression.(instance at line 783) line 783
  122. def OAI.BinPackingGap.PackingScalarExpression.values line 787
  123. def OAI.BinPackingGap.PackingScalarExpression.baseTerm line 795
  124. def OAI.BinPackingGap.PackingScalarExpression.primaryFactor line 799
  125. def OAI.BinPackingGap.PackingScalarExpression.secondaryFactor line 802
  126. def OAI.BinPackingGap.PackingScalarExpression.positiveLabel line 804
  127. def OAI.BinPackingGap.PackingScalarExpression.negativeLabel line 810
  128. def OAI.BinPackingGap.PackingScalarExpression.positiveTerm line 815
  129. def OAI.BinPackingGap.PackingScalarExpression.negativeTerm line 820
  130. def OAI.BinPackingGap.PackingScalarExpression.numerator line 824
  131. def OAI.BinPackingGap.PackingScalarExpression.denominator line 827
  132. theorem OAI.BinPackingGap.PackingScalarExpression.eval_positiveLabel line 831
  133. theorem OAI.BinPackingGap.PackingScalarExpression.eval_negativeLabel line 838
  134. theorem OAI.BinPackingGap.PackingScalarExpression.eval_positiveTerm line 845
  135. theorem OAI.BinPackingGap.PackingScalarExpression.eval_negativeTerm line 853
  136. theorem OAI.BinPackingGap.PackingScalarExpression.eval_numerator line 861
  137. theorem OAI.BinPackingGap.PackingScalarExpression.eval_denominator line 868
  138. theorem OAI.BinPackingGap.PackingScalarExpression.eval_item_numerator line 872
  139. theorem OAI.BinPackingGap.PackingScalarExpression.eval_item_denominator line 879