OAI/Computability/BinPacking/Inventory/InventoryPrefixConservation.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.InventoryData.itemSize line 20
  2. theorem OAI.BinPackingGap.InventoryData.itemSize_mem_interval line 23
  3. theorem OAI.BinPackingGap.InventoryData.itemSize_pos line 27
  4. theorem OAI.BinPackingGap.InventoryData.itemSize_le_one line 30
  5. def OAI.BinPackingGap.InventoryData.packingInstance line 33
  6. def OAI.BinPackingGap.InventoryData.itemEquiv line 36
  7. def OAI.BinPackingGap.InventoryData.encodedSubclass line 38
  8. def OAI.BinPackingGap.InventoryData.encodedLabel line 41
  9. def OAI.BinPackingGap.InventoryData.encodedCoordinate line 44
  10. theorem OAI.BinPackingGap.InventoryData.packingInstance_size_eq line 47
  11. theorem OAI.BinPackingGap.InventoryData.encodedCoordinate_abs_le_six line 51
  12. theorem OAI.BinPackingGap.InventoryData.packingInstance_size_mem_interval line 54
  13. theorem OAI.BinPackingGap.InventoryData.packingInstance_n line 58
  14. theorem OAI.BinPackingGap.InventoryData.encoded_primaryScore_sum_eq_zero line 61
  15. theorem OAI.BinPackingGap.InventoryData.encoded_secondaryScore_sum_eq_zero line 67
  16. theorem OAI.BinPackingGap.InventoryData.encoded_labelledRoleCount line 76
  17. theorem OAI.BinPackingGap.InventoryData.encoded_labelledRoleCount_x line 84
  18. theorem OAI.BinPackingGap.InventoryData.encoded_labelledRoleCount_anchor line 89
  19. theorem OAI.BinPackingGap.InventoryData.encoded_labelledRoleCount_local line 94
  20. theorem OAI.BinPackingGap.InventoryData.itemLabel_some_of_labelled line 99
  21. theorem OAI.BinPackingGap.InventoryData.itemLabel_none_of_unlabelled line 110
  22. theorem OAI.BinPackingGap.InventoryData.encodedLabel_some_of_labelled line 116
  23. theorem OAI.BinPackingGap.InventoryData.encodedLabel_none_of_unlabelled line 123
  24. def OAI.BinPackingGap.InventoryData.roleLabelData line 139
  25. theorem OAI.BinPackingGap.InventoryData.roleLabelData_anchor_row_count line 143
  26. theorem OAI.BinPackingGap.InventoryData.roleLabelData_anchor_local_count line 153
  27. theorem OAI.BinPackingGap.InventoryData.outsideTableItems_card_lt_lossAllowance line 163
  28. theorem OAI.BinPackingGap.InventoryData.badAnchorsAt_card_le line 171
  29. theorem OAI.BinPackingGap.InventoryData.anchor_subset_loss_le line 181
  30. theorem OAI.BinPackingGap.InventoryData.badAnchors_global_card_le line 194
  31. def OAI.BinPackingGap.InventoryData.taggedItem line 214
  32. theorem OAI.BinPackingGap.InventoryData.taggedItem_apply line 217
  33. def OAI.BinPackingGap.InventoryData.globalCopyEmbedding line 220
  34. def OAI.BinPackingGap.InventoryData.flagCopyEmbedding line 224
  35. theorem OAI.BinPackingGap.InventoryData.globalCopyEmbedding_apply line 228
  36. theorem OAI.BinPackingGap.InventoryData.flagCopyEmbedding_apply line 232
  37. def OAI.BinPackingGap.InventoryData.physicalGlobalPool line 235
  38. def OAI.BinPackingGap.InventoryData.physicalFlagPool line 238
  39. def OAI.BinPackingGap.InventoryData.labeledItems line 241
  40. theorem OAI.BinPackingGap.InventoryData.card_physicalGlobalPool line 246
  41. theorem OAI.BinPackingGap.InventoryData.card_physicalFlagPool line 250
  42. theorem OAI.BinPackingGap.InventoryData.physicalGlobalPool_nonempty_iff line 254
  43. theorem OAI.BinPackingGap.InventoryData.physicalFlagPool_nonempty_iff line 258
  44. theorem OAI.BinPackingGap.InventoryData.mem_physicalGlobalPool line 262
  45. theorem OAI.BinPackingGap.InventoryData.mem_physicalFlagPool line 268
  46. theorem OAI.BinPackingGap.InventoryData.itemEquiv_mem_physicalGlobalPool_iff line 274
  47. theorem OAI.BinPackingGap.InventoryData.itemEquiv_mem_physicalFlagPool_iff line 284
  48. theorem OAI.BinPackingGap.InventoryData.mem_labeledItems line 294
  49. theorem OAI.BinPackingGap.InventoryData.itemEquiv_mem_labeledItems line 300
  50. theorem OAI.BinPackingGap.InventoryData.globalItem_mem_physicalGlobalPool line 305
  51. theorem OAI.BinPackingGap.InventoryData.flagItem_mem_physicalFlagPool line 318
  52. theorem OAI.BinPackingGap.InventoryData.role_eq_global_of_mem_physicalGlobalPool line 331
  53. theorem OAI.BinPackingGap.InventoryData.role_eq_flag_of_mem_physicalFlagPool line 337
  54. theorem OAI.BinPackingGap.InventoryData.physicalGlobalPool_disjoint line 343
  55. theorem OAI.BinPackingGap.InventoryData.physicalFlagPool_disjoint line 350
  56. theorem OAI.BinPackingGap.InventoryData.physicalGlobalPool_disjoint_physicalFlagPool line 357
  57. theorem OAI.BinPackingGap.InventoryData.labeledItems_disjoint_physicalGlobalPool line 366
  58. theorem OAI.BinPackingGap.InventoryData.labeledItems_disjoint_physicalFlagPool line 374
  59. theorem OAI.BinPackingGap.InventoryData.not_mem_physicalGlobalPool_of_role_ne line 382
  60. theorem OAI.BinPackingGap.InventoryData.not_mem_physicalFlagPool_of_role_ne line 389
  61. theorem OAI.BinPackingGap.InventoryData.physicalInventory_indicator_partition line 396
  62. def OAI.BinPackingGap.InventoryData.rowPrefixExports line 429
  63. def OAI.BinPackingGap.InventoryData.localPrefixExports line 433
  64. def OAI.BinPackingGap.InventoryData.outsideAnchorPrefix line 437
  65. def OAI.BinPackingGap.InventoryData.outsideRowPrefix line 441
  66. def OAI.BinPackingGap.InventoryData.outsideLocalPrefix line 445
  67. theorem OAI.BinPackingGap.InventoryData.rowPrefixExports_add_outsideRow_eq line 449
  68. theorem OAI.BinPackingGap.InventoryData.localPrefixExports_add_outsideLocal_eq line 462
  69. theorem OAI.BinPackingGap.InventoryData.rowPrefixExports_eq_outside_sub line 475
  70. theorem OAI.BinPackingGap.InventoryData.localPrefixExports_eq_outside_sub line 481
  71. theorem OAI.BinPackingGap.InventoryData.rowPrefixExports_card_lt_lossAllowance line 487
  72. theorem OAI.BinPackingGap.InventoryData.localPrefixExports_card_lt_lossAllowance line 498