OAI/Computability/BinPacking/Inventory/EdgeLongConsumption.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.InventoryData.earlierKeyItems line 17
  2. def OAI.BinPackingGap.InventoryData.earlierWItems line 20
  3. theorem OAI.BinPackingGap.InventoryData.earlierKeyItems_card line 23
  4. theorem OAI.BinPackingGap.InventoryData.earlierWItems_card line 28
  5. theorem OAI.BinPackingGap.InventoryData.mem_earlierKeyItems line 33
  6. theorem OAI.BinPackingGap.InventoryData.mem_earlierWItems line 48
  7. theorem OAI.BinPackingGap.InventoryData.keyItem_mem_earlierKeyItems line 63
  8. theorem OAI.BinPackingGap.InventoryData.edgeResourceItem_mem_earlierWItems line 76
  9. def OAI.BinPackingGap.InventoryData.earlierGoodKeyTuples line 88
  10. theorem OAI.BinPackingGap.InventoryData.mem_earlierGoodKeyTuples line 94
  11. theorem OAI.BinPackingGap.InventoryData.earlierGoodKeyTuples_anchor_subset line 102
  12. theorem OAI.BinPackingGap.InventoryData.earlierGoodKeyTuples_edge line 110
  13. theorem OAI.BinPackingGap.InventoryData.earlierGoodKeyTuples_global_subset line 128
  14. def OAI.BinPackingGap.InventoryData.remainingEarlierW line 159
  15. theorem OAI.BinPackingGap.InventoryData.remainingEarlierW_card_eq_missingKeys line 164
  16. theorem OAI.BinPackingGap.InventoryData.missingEarlierKeys_subset_bad line 174
  17. theorem OAI.BinPackingGap.InventoryData.remainingEarlierW_card_le line 199
  18. def OAI.BinPackingGap.InventoryData.edgeLongTuplesAt line 214
  19. theorem OAI.BinPackingGap.InventoryData.mem_edgeLongTuplesAt line 223
  20. theorem OAI.BinPackingGap.InventoryData.edgeLongTuplesAt_disjoint line 240
  21. def OAI.BinPackingGap.InventoryData.edgeLongTuples line 259
  22. theorem OAI.BinPackingGap.InventoryData.edgeLongTuples_card line 264
  23. theorem OAI.BinPackingGap.InventoryData.edgeLongTuplesAt_witness line 278
  24. theorem OAI.BinPackingGap.InventoryData.witness_key_item line 299
  25. theorem OAI.BinPackingGap.InventoryData.witness_global_item line 309
  26. theorem OAI.BinPackingGap.InventoryData.edgeLongTuplesAt_not_earlierGoodKeyTuples line 318
  27. theorem OAI.BinPackingGap.InventoryData.edgeLongTuplesAt_global_not_used_earlier line 328
  28. theorem OAI.BinPackingGap.InventoryData.edgeLongTuplesAt_global_mem line 340
  29. theorem OAI.BinPackingGap.InventoryData.edgeLongTuples_global_subset line 363
  30. theorem OAI.BinPackingGap.InventoryData.edge_long_matches_capacity line 374
  31. theorem OAI.BinPackingGap.InventoryData.edge_long_matches_capacity_raw line 388