OAI/Computability/BinPacking/Packing/ExtractedCover.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinPackingGap.SideChoice.card_le_of_unique_hit line 17
  2. theorem OAI.BinPackingGap.SideChoice.level_card_le_resources line 38
  3. def OAI.BinPackingGap.SideChoice.taggedDepth line 51
  4. def OAI.BinPackingGap.SideChoice.marksPlus line 53
  5. def OAI.BinPackingGap.SideChoice.marksMinus line 58
  6. theorem OAI.BinPackingGap.SideChoice.mem_marksPlus line 64
  7. theorem OAI.BinPackingGap.SideChoice.mem_marksMinus line 71
  8. theorem OAI.BinPackingGap.SideChoice.roots_not_marked line 77
  9. theorem OAI.BinPackingGap.SideChoice.marked_level_card_le line 95
  10. theorem OAI.BinPackingGap.SideChoice.exists_unhit_leaf line 123
  11. theorem OAI.BinPackingGap.SideChoice.exists_leaf_coverage_le_funded line 152
  12. theorem OAI.BinPackingGap.SideChoice.side_choice line 182
  13. def OAI.BinPackingGap.reductionTrees line 211
  14. def OAI.BinPackingGap.reductionInventory line 214
  15. def OAI.BinPackingGap.reductionInstance line 218
  16. def OAI.BinPackingGap.reductionBinBound line 221
  17. theorem OAI.BinPackingGap.reductionInventory_graph line 224
  18. theorem OAI.BinPackingGap.reductionInventory_d line 227
  19. theorem OAI.BinPackingGap.reductionInventory_k line 230
  20. theorem OAI.BinPackingGap.reductionInventory_P line 233
  21. theorem OAI.BinPackingGap.reductionInventory_R line 236
  22. theorem OAI.BinPackingGap.reductionInventory_R_pos line 240
  23. theorem OAI.BinPackingGap.reductionInventory_height_pos line 243
  24. theorem OAI.BinPackingGap.reductionInventory_plus_height line 246
  25. theorem OAI.BinPackingGap.reductionInventory_minus_height line 250
  26. theorem OAI.BinPackingGap.reductionInstance_count line 254
  27. theorem OAI.BinPackingGap.reductionInstance_size_bounds line 259
  28. theorem OAI.BinPackingGap.PackingCounts.selected_inventory_subclass line 269
  29. theorem OAI.BinPackingGap.PackingCounts.selected_row_subclass line 277
  30. theorem OAI.BinPackingGap.PackingCounts.unit_global_species line 286
  31. theorem OAI.BinPackingGap.PackingCounts.selected_row_tm_of_um line 294
  32. theorem OAI.BinPackingGap.PackingCounts.selected_row_not_tm_of_up line 308
  33. theorem OAI.BinPackingGap.PackingCounts.selected_global_resource line 322
  34. theorem OAI.BinPackingGap.PackingCounts.funded_of_species line 330
  35. theorem OAI.BinPackingGap.PackingCounts.covering_plus_unit_funded line 340
  36. theorem OAI.BinPackingGap.PackingCounts.covering_minus_unit_funded line 360
  37. theorem OAI.BinPackingGap.PackingCounts.zero_lengths_cover_jobCell line 378
  38. theorem OAI.BinPackingGap.PackingCounts.zero_lengths_not_cover_plus_leaf line 406
  39. theorem OAI.BinPackingGap.PackingCounts.zero_lengths_not_cover_minus_leaf line 421
  40. def OAI.BinPackingGap.InventoryData.plusPoint line 444
  41. def OAI.BinPackingGap.InventoryData.minusPoint line 448
  42. theorem OAI.BinPackingGap.InventoryData.plusPoint_mem_Ico line 452
  43. theorem OAI.BinPackingGap.InventoryData.minusPoint_mem_Ico line 460
  44. theorem OAI.BinPackingGap.InventoryData.plusPoint_mem_cell line 468
  45. theorem OAI.BinPackingGap.InventoryData.minusPoint_mem_cell line 472
  46. def OAI.BinPackingGap.InventoryData.taggedAddress line 476
  47. theorem OAI.BinPackingGap.InventoryData.taggedAddress_injective line 480
  48. def OAI.BinPackingGap.InventoryData.taggedNodeDepth line 492
  49. def OAI.BinPackingGap.InventoryData.taggedNodeCell line 495
  50. theorem OAI.BinPackingGap.InventoryData.taggedAddress_bounded line 499
  51. def OAI.BinPackingGap.PackingCounts.tupleHits line 511
  52. theorem OAI.BinPackingGap.PackingCounts.selected_hits_unique line 516
  53. theorem OAI.BinPackingGap.PackingCounts.main_local_nonzero_positive line 527
  54. theorem OAI.BinPackingGap.PackingCounts.selected_hits_plus_ancestor line 549
  55. theorem OAI.BinPackingGap.PackingCounts.selected_hits_minus_ancestor line 565
  56. theorem OAI.BinPackingGap.PackingCounts.covering_plus_classification line 581
  57. theorem OAI.BinPackingGap.PackingCounts.covering_minus_classification line 605
  58. theorem OAI.BinPackingGap.PackingCounts.side_choice_of_competingTrees line 629
  59. theorem OAI.BinPackingGap.PackingCounts.side_choice_of_test_coverage line 667
  60. def OAI.BinPackingGap.extractedCover line 687
  61. theorem OAI.BinPackingGap.reduction_side_choice line 692
  62. theorem OAI.BinPackingGap.extractedCover_card_le line 707