OAI/Computability/BinPacking/Packing/LocalTemplateBases.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinPackingGap.encoded_pattern_role_sum line 9
  2. def OAI.BinPackingGap.InventoryData.localTemplateItems line 35
  3. theorem OAI.BinPackingGap.InventoryData.localTemplateItems_role line 43
  4. theorem OAI.BinPackingGap.InventoryData.localTemplateItems_injective line 49
  5. theorem OAI.BinPackingGap.InventoryData.localTemplateItems_label line 56
  6. theorem OAI.BinPackingGap.InventoryData.localTemplate_coordinate_sum line 63
  7. theorem OAI.BinPackingGap.InventoryData.localTemplate_size_sum line 73
  8. def OAI.BinPackingGap.InventoryData.stateMainPattern line 84
  9. theorem OAI.BinPackingGap.InventoryData.stateMainTemplate_pattern line 90
  10. theorem OAI.BinPackingGap.InventoryData.stateMainGlobal_coordinate line 105
  11. theorem OAI.BinPackingGap.InventoryData.stateMainTemplate_size_eq line 114
  12. theorem OAI.BinPackingGap.InventoryData.stateMainTemplate_feasible_iff line 128
  13. theorem OAI.BinPackingGap.InventoryData.edgeTemplate_size_eq line 148
  14. theorem OAI.BinPackingGap.InventoryData.edgeTemplate_feasible_iff line 168
  15. theorem OAI.BinPackingGap.InventoryData.edgeTemplate_short_feasible line 179
  16. theorem OAI.BinPackingGap.InventoryData.edgeTemplate_long_feasible_iff line 186
  17. theorem OAI.BinPackingGap.InventoryData.stateEdgeTemplate_size_eq_one line 193
  18. abbrev OAI.BinPackingGap.InventoryData.Template line 213
  19. def OAI.BinPackingGap.InventoryData.templateGlobalSpecies line 215
  20. def OAI.BinPackingGap.InventoryData.templateFlagSpecies line 218
  21. def OAI.BinPackingGap.InventoryData.templateRowCopy line 221
  22. def OAI.BinPackingGap.InventoryData.templateAnchorCopy line 224
  23. def OAI.BinPackingGap.InventoryData.templateLocalCopy line 228
  24. def OAI.BinPackingGap.InventoryData.templateBase line 232
  25. theorem OAI.BinPackingGap.InventoryData.templateBase_subset_labeledItems line 238
  26. theorem OAI.BinPackingGap.InventoryData.templateTagged_ne line 244
  27. theorem OAI.BinPackingGap.InventoryData.templateTagged_eq_iff line 250
  28. theorem OAI.BinPackingGap.InventoryData.card_templateBase line 258
  29. def OAI.BinPackingGap.InventoryData.templateCopyEquiv line 266
  30. theorem OAI.BinPackingGap.InventoryData.templateCopyEquiv_apply line 277
  31. def OAI.BinPackingGap.InventoryData.templateFiberBoolEquiv line 281
  32. theorem OAI.BinPackingGap.InventoryData.card_templateCopy_fiber line 296
  33. theorem OAI.BinPackingGap.InventoryData.card_templatePredicate line 306
  34. theorem OAI.BinPackingGap.InventoryData.itemEquiv_x_mem_templateBase line 315
  35. theorem OAI.BinPackingGap.InventoryData.itemEquiv_anchor_mem_templateBase line 325
  36. theorem OAI.BinPackingGap.InventoryData.itemEquiv_local_mem_templateBase line 336
  37. theorem OAI.BinPackingGap.InventoryData.itemEquiv_global_not_mem_templateBase line 346
  38. theorem OAI.BinPackingGap.InventoryData.itemEquiv_flag_not_mem_templateBase line 354
  39. theorem OAI.BinPackingGap.InventoryData.templateBase_appearance_count line 362
  40. theorem OAI.BinPackingGap.InventoryData.packingInstance_size_itemEquiv line 395
  41. theorem OAI.BinPackingGap.InventoryData.templateBase_complete_eq_image line 400
  42. theorem OAI.BinPackingGap.InventoryData.templateBase_size_sum line 442
  43. theorem OAI.BinPackingGap.InventoryData.templateBase_capacity line 454