OAI/Computability/BinPacking/Packing/PackingCoordinates.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.InventoryData.treeBaseline line 10
  2. def OAI.BinPackingGap.InventoryData.rowBaseline line 17
  3. def OAI.BinPackingGap.InventoryData.mainBaseline line 21
  4. def OAI.BinPackingGap.InventoryData.treeDeadline line 25
  5. def OAI.BinPackingGap.InventoryData.deadline line 36
  6. def OAI.BinPackingGap.InventoryData.rowCoordinate line 41
  7. def OAI.BinPackingGap.InventoryData.anchorCoordinate line 45
  8. def OAI.BinPackingGap.InventoryData.globalLength line 50
  9. def OAI.BinPackingGap.InventoryData.globalCoordinate line 55
  10. def OAI.BinPackingGap.InventoryData.localLength line 61
  11. def OAI.BinPackingGap.InventoryData.localCoordinate line 66
  12. def OAI.BinPackingGap.InventoryData.itemCoordinate line 68
  13. theorem OAI.BinPackingGap.InventoryData.mainBaseline_designated line 75
  14. theorem OAI.BinPackingGap.InventoryData.deadline_designated line 80
  15. theorem OAI.BinPackingGap.InventoryData.globalLength_nonneg line 88
  16. theorem OAI.BinPackingGap.InventoryData.globalLength_le_one line 95
  17. theorem OAI.BinPackingGap.InventoryData.node_endpoint_bounds line 102
  18. theorem OAI.BinPackingGap.InventoryData.treeBaseline_bounds line 115
  19. theorem OAI.BinPackingGap.InventoryData.treeDeadline_bounds line 122
  20. theorem OAI.BinPackingGap.InventoryData.jobBaseline_bounds line 137
  21. theorem OAI.BinPackingGap.InventoryData.rowBaseline_bounds line 143
  22. theorem OAI.BinPackingGap.InventoryData.mainBaseline_bounds line 149
  23. theorem OAI.BinPackingGap.InventoryData.deadline_bounds line 155
  24. theorem OAI.BinPackingGap.InventoryData.rowCoordinate_bounds line 167
  25. theorem OAI.BinPackingGap.InventoryData.anchorCoordinate_bounds line 181
  26. theorem OAI.BinPackingGap.InventoryData.globalCoordinate_bounds line 193
  27. theorem OAI.BinPackingGap.InventoryData.localLength_nonneg line 209
  28. theorem OAI.BinPackingGap.InventoryData.localLength_le_lambda_one line 215
  29. theorem OAI.BinPackingGap.InventoryData.localLength_le_one line 223
  30. theorem OAI.BinPackingGap.InventoryData.localCoordinate_bounds line 227
  31. theorem OAI.BinPackingGap.InventoryData.itemCoordinate_bounds line 234
  32. theorem OAI.BinPackingGap.InventoryData.itemCoordinate_abs_le_six line 259
  33. def OAI.BinPackingGap.InventoryData.stateRowEquiv line 264
  34. theorem OAI.BinPackingGap.InventoryData.stateRowEquiv_tree line 279
  35. theorem OAI.BinPackingGap.InventoryData.stateRowEquiv_mainJob line 282
  36. theorem OAI.BinPackingGap.InventoryData.stateRowEquiv_edgeJob line 285
  37. def OAI.BinPackingGap.InventoryData.stateMainRow line 288
  38. theorem OAI.BinPackingGap.InventoryData.stateMainRow_injective line 291
  39. theorem OAI.BinPackingGap.InventoryData.stateMainRow_baseline line 296
  40. def OAI.BinPackingGap.InventoryData.stateFlagSpecies line 300
  41. def OAI.BinPackingGap.InventoryData.stateMainGlobalSpecies line 305
  42. def OAI.BinPackingGap.InventoryData.stateGlobalSpecies line 312
  43. def OAI.BinPackingGap.InventoryData.globalSpeciesLength line 317
  44. theorem OAI.BinPackingGap.InventoryData.globalLength_eq_species line 322
  45. def OAI.BinPackingGap.InventoryData.stateMainLength line 327
  46. theorem OAI.BinPackingGap.InventoryData.stateMainLength_nonneg line 330
  47. theorem OAI.BinPackingGap.InventoryData.stateMainLength_le_one line 336
  48. def OAI.BinPackingGap.InventoryData.fundedRoot line 342
  49. theorem OAI.BinPackingGap.InventoryData.fundedRoot_injective line 346
  50. theorem OAI.BinPackingGap.InventoryData.stateMainLength_fundedRoot line 351
  51. abbrev OAI.BinPackingGap.InventoryData.PhysicalBins line 356
  52. theorem OAI.BinPackingGap.InventoryData.card_physicalBins line 358
  53. structure OAI.BinPackingGap.InventoryData.LocalState line 361
  54. def OAI.BinPackingGap.InventoryData.LocalState.anchorAtEquiv line 372
  55. def OAI.BinPackingGap.InventoryData.LocalState.localAtEquiv line 375
  56. theorem OAI.BinPackingGap.InventoryData.LocalState.anchorAtEquiv_main line 378
  57. theorem OAI.BinPackingGap.InventoryData.LocalState.anchorAtEquiv_edge line 381
  58. theorem OAI.BinPackingGap.InventoryData.LocalState.localAtEquiv_main line 384
  59. theorem OAI.BinPackingGap.InventoryData.LocalState.localAtEquiv_edge line 387
  60. def OAI.BinPackingGap.PackingCounts.tupleBaseline line 401
  61. def OAI.BinPackingGap.PackingCounts.tupleShort line 404
  62. def OAI.BinPackingGap.PackingCounts.tupleGlobalLength line 407
  63. def OAI.BinPackingGap.PackingCounts.tupleLocalLength line 410
  64. def OAI.BinPackingGap.PackingCounts.tupleFinish line 413
  65. def OAI.BinPackingGap.PackingCounts.tupleClosedInterval line 419
  66. def OAI.BinPackingGap.PackingCounts.tupleCoveringInterval line 423
  67. def OAI.BinPackingGap.PackingCounts.tupleCovering line 427
  68. theorem OAI.BinPackingGap.PackingCounts.mem_tupleCovering line 433
  69. theorem OAI.BinPackingGap.PackingCounts.tupleGlobalLength_nonneg line 441
  70. theorem OAI.BinPackingGap.PackingCounts.tupleGlobalLength_le_one line 445
  71. theorem OAI.BinPackingGap.PackingCounts.tupleGlobalLength_eq_of_unit_false line 449
  72. theorem OAI.BinPackingGap.PackingCounts.localLength_nonneg line 458
  73. theorem OAI.BinPackingGap.PackingCounts.localLength_le_first line 464
  74. theorem OAI.BinPackingGap.PackingCounts.tupleLocalLength_nonneg line 471
  75. theorem OAI.BinPackingGap.PackingCounts.tupleLocalLength_le_first line 475
  76. theorem OAI.BinPackingGap.PackingCounts.tupleLocalLength_eq_zero_of_not_positive line 480
  77. theorem OAI.BinPackingGap.PackingCounts.tupleFinish_le_baseline line 501
  78. theorem OAI.BinPackingGap.PackingCounts.selected_localLength line 506
  79. theorem OAI.BinPackingGap.PackingCounts.selected_interval_length line 516
  80. theorem OAI.BinPackingGap.PackingCounts.selected_interval_length_first line 526