OAI/Computability/BinPacking/Inventory/IntegralSpeciesCounts.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinPackingGap.InventoryData.up_indicator_add line 13
  2. theorem OAI.BinPackingGap.InventoryData.um_indicator_add line 21
  3. theorem OAI.BinPackingGap.InventoryData.root_copy_indicator_sum line 29
  4. theorem OAI.BinPackingGap.InventoryData.stateGlobalSpecies_up_true_count line 35
  5. theorem OAI.BinPackingGap.InventoryData.stateGlobalSpecies_um_true_count line 46
  6. theorem OAI.BinPackingGap.InventoryData.stateGlobalSpecies_up_total line 57
  7. theorem OAI.BinPackingGap.InventoryData.stateGlobalSpecies_um_total line 68
  8. theorem OAI.BinPackingGap.InventoryData.stateGlobalSpecies_up_false_count line 78
  9. theorem OAI.BinPackingGap.InventoryData.stateGlobalSpecies_um_false_count line 86
  10. theorem OAI.BinPackingGap.InventoryData.stateGlobalSpecies_edge_count line 94
  11. theorem OAI.BinPackingGap.InventoryData.stateGlobalSpecies_count line 109
  12. theorem OAI.BinPackingGap.InventoryData.stateFlagSpecies_count line 131
  13. def OAI.BinPackingGap.InventoryData.allGlobalRequests line 139
  14. theorem OAI.BinPackingGap.InventoryData.allGlobalRequests_up_true line 143
  15. theorem OAI.BinPackingGap.InventoryData.allGlobalRequests_um_true line 147
  16. theorem OAI.BinPackingGap.InventoryData.allGlobalRequests_up_total line 151
  17. theorem OAI.BinPackingGap.InventoryData.allGlobalRequests_um_total line 165
  18. theorem OAI.BinPackingGap.InventoryData.allGlobalRequests_edge line 179
  19. theorem OAI.BinPackingGap.InventoryData.allGlobalRequests_eq_twice_stock line 193
  20. theorem OAI.BinPackingGap.InventoryData.doubled_stateGlobalSpecies_count line 223
  21. theorem OAI.BinPackingGap.InventoryData.doubled_stateFlagSpecies_count line 236
  22. theorem OAI.BinPackingGap.GraphInput.IsCover.mono line 257
  23. theorem OAI.BinPackingGap.GraphInput.CoverAtMost.exists_exact line 262
  24. theorem OAI.BinPackingGap.GraphInput.IsCover.endpoints line 271
  25. def OAI.BinPackingGap.InventoryData.coverSelected line 281
  26. def OAI.BinPackingGap.InventoryData.permitLeft line 283
  27. def OAI.BinPackingGap.InventoryData.integralPermit line 286
  28. theorem OAI.BinPackingGap.InventoryData.integralPermit_zero line 289
  29. theorem OAI.BinPackingGap.InventoryData.integralPermit_one line 292
  30. theorem OAI.BinPackingGap.InventoryData.integralPermit_of_unselected line 295
  31. def OAI.BinPackingGap.InventoryData.integralGlobalSpecies line 306
  32. def OAI.BinPackingGap.InventoryData.integralFlagSpecies line 310
  33. theorem OAI.BinPackingGap.InventoryData.integral_edge_permit_of_unselected line 313
  34. theorem OAI.BinPackingGap.InventoryData.integral_up_count_eq_sum line 330
  35. theorem OAI.BinPackingGap.InventoryData.integral_um_count_eq_sum line 345
  36. theorem OAI.BinPackingGap.InventoryData.sum_coverSelected line 360
  37. theorem OAI.BinPackingGap.InventoryData.sum_coverUnselected line 365
  38. theorem OAI.BinPackingGap.InventoryData.integral_up_true_count line 379
  39. theorem OAI.BinPackingGap.InventoryData.integral_um_true_count line 386
  40. theorem OAI.BinPackingGap.InventoryData.integral_up_total line 394
  41. theorem OAI.BinPackingGap.InventoryData.integral_um_total line 404
  42. theorem OAI.BinPackingGap.InventoryData.card_integralEdgeJobs line 414
  43. theorem OAI.BinPackingGap.InventoryData.card_integralGlobalSpecies line 449
  44. theorem OAI.BinPackingGap.InventoryData.card_integralFlagSpecies line 486