OAI/Computability/BinPacking/Machines/GraphPackingOutput.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.InventoryData.rawItemList line 14
  2. theorem OAI.BinPackingGap.InventoryData.rawItemList_length_items line 16
  3. theorem OAI.BinPackingGap.InventoryData.rawItemList_length line 19
  4. theorem OAI.BinPackingGap.InventoryData.rawItemList_valid line 23
  5. def OAI.BinPackingGap.InventoryData.rawItemListEquiv line 30
  6. theorem OAI.BinPackingGap.InventoryData.rawItemListEquiv_apply line 33
  7. theorem OAI.BinPackingGap.InventoryData.rawItemList_get line 38
  8. theorem OAI.BinPackingGap.InventoryData.rawItemList_get_ratio line 47
  9. def OAI.BinPackingGap.InventoryData.rawItemListReindexing line 54
  10. theorem OAI.BinPackingGap.InventoryData.rawItemList_hasPacking_iff line 66
  11. theorem OAI.BinPackingGap.InventoryData.rawItemList_opt_eq line 72
  12. def OAI.BinPackingGap.InventoryData.rawOutput line 78
  13. theorem OAI.BinPackingGap.InventoryData.rawOutput_bins line 80
  14. theorem OAI.BinPackingGap.InventoryData.rawOutput_items line 82
  15. theorem OAI.BinPackingGap.InventoryData.rawOutput_valid line 84
  16. theorem OAI.BinPackingGap.InventoryData.rawOutput_length line 88
  17. def OAI.BinPackingGap.graphPackingOutput line 95
  18. theorem OAI.BinPackingGap.graphPackingOutput_bins line 98
  19. theorem OAI.BinPackingGap.graphPackingOutput_valid line 101
  20. theorem OAI.BinPackingGap.graphPackingOutput_length line 107
  21. def OAI.BinPackingGap.graphPackingOutputInstance line 111
  22. def OAI.BinPackingGap.graphPackingOutputReindexing line 114
  23. theorem OAI.BinPackingGap.graphPackingOutput_count line 121
  24. theorem OAI.BinPackingGap.graphPackingOutput_size_bounds line 125
  25. theorem OAI.BinPackingGap.graphPackingOutput_hasPacking_iff line 132
  26. theorem OAI.BinPackingGap.graphPackingOutput_opt_eq line 138