OAI/Computability/BinPacking/Packing/ItemEnumeration.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinPackingGap.InventoryData.length_flatMap_constant line 13
  2. def OAI.BinPackingGap.InventoryData.treeRowList line 20
  3. def OAI.BinPackingGap.InventoryData.positiveLocalList line 27
  4. theorem OAI.BinPackingGap.InventoryData.mem_treeRowList line 30
  5. theorem OAI.BinPackingGap.InventoryData.mem_positiveLocalList line 35
  6. theorem OAI.BinPackingGap.InventoryData.treeRowList_length line 39
  7. theorem OAI.BinPackingGap.InventoryData.positiveLocalList_length line 52
  8. def OAI.BinPackingGap.InventoryData.vertexChunk line 57
  9. def OAI.BinPackingGap.InventoryData.vertexItems line 64
  10. def OAI.BinPackingGap.InventoryData.listedJobCopy line 67
  11. def OAI.BinPackingGap.InventoryData.jobChunk line 71
  12. def OAI.BinPackingGap.InventoryData.jobItems line 82
  13. def OAI.BinPackingGap.InventoryData.globalPool line 87
  14. def OAI.BinPackingGap.InventoryData.globalItems line 90
  15. def OAI.BinPackingGap.InventoryData.flagPool line 96
  16. def OAI.BinPackingGap.InventoryData.flagItems line 99
  17. def OAI.BinPackingGap.InventoryData.itemList line 102
  18. theorem OAI.BinPackingGap.InventoryData.vertexChunk_length line 105
  19. theorem OAI.BinPackingGap.InventoryData.vertexItems_length line 111
  20. theorem OAI.BinPackingGap.InventoryData.jobChunk_length line 116
  21. theorem OAI.BinPackingGap.InventoryData.jobItems_length line 121
  22. theorem OAI.BinPackingGap.InventoryData.globalPool_length line 134
  23. theorem OAI.BinPackingGap.InventoryData.globalItems_length line 137
  24. theorem OAI.BinPackingGap.InventoryData.flagPool_length line 152
  25. theorem OAI.BinPackingGap.InventoryData.flagItems_length line 155
  26. theorem OAI.BinPackingGap.InventoryData.itemList_length line 160
  27. theorem OAI.BinPackingGap.InventoryData.mem_itemList_of_vertex line 166
  28. theorem OAI.BinPackingGap.InventoryData.mem_itemList_of_job line 173
  29. theorem OAI.BinPackingGap.InventoryData.mem_globalItems line 181
  30. theorem OAI.BinPackingGap.InventoryData.mem_flagItems line 197
  31. theorem OAI.BinPackingGap.InventoryData.mem_itemList line 201
  32. theorem OAI.BinPackingGap.InventoryData.itemList_toFinset line 253
  33. theorem OAI.BinPackingGap.InventoryData.itemList_nodup line 258
  34. def OAI.BinPackingGap.InventoryData.itemListEquiv line 265
  35. theorem OAI.BinPackingGap.InventoryData.itemListEquiv_apply line 269