OAI/Computability/BinPacking/Inventory/InventoryScores.lean

GitHub source file

130 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.BinPackingGap.InventoryData line 16
  2. abbrev OAI.BinPackingGap.InventoryData.Vertex line 30
  3. abbrev OAI.BinPackingGap.InventoryData.Edge line 31
  4. abbrev OAI.BinPackingGap.InventoryData.Position line 32
  5. abbrev OAI.BinPackingGap.InventoryData.IncidencePosition line 33
  6. abbrev OAI.BinPackingGap.InventoryData.JobCopy line 34
  7. abbrev OAI.BinPackingGap.InventoryData.Depth line 35
  8. def OAI.BinPackingGap.InventoryData.P line 37
  9. def OAI.BinPackingGap.InventoryData.tPlus line 39
  10. def OAI.BinPackingGap.InventoryData.tMinus line 40
  11. def OAI.BinPackingGap.InventoryData.t line 41
  12. def OAI.BinPackingGap.InventoryData.J line 42
  13. def OAI.BinPackingGap.InventoryData.B line 43
  14. abbrev OAI.BinPackingGap.InventoryData.TreeRow line 45
  15. abbrev OAI.BinPackingGap.InventoryData.RowAt line 48
  16. abbrev OAI.BinPackingGap.InventoryData.MBase line 50
  17. abbrev OAI.BinPackingGap.InventoryData.AnchorAt line 52
  18. abbrev OAI.BinPackingGap.InventoryData.PositiveLocal line 54
  19. abbrev OAI.BinPackingGap.InventoryData.ZeroLocalAt line 56
  20. abbrev OAI.BinPackingGap.InventoryData.DMAt line 57
  21. abbrev OAI.BinPackingGap.InventoryData.LocalAt line 58
  22. abbrev OAI.BinPackingGap.InventoryData.LocalBin line 60
  23. abbrev OAI.BinPackingGap.InventoryData.PlusLeaf line 62
  24. abbrev OAI.BinPackingGap.InventoryData.MinusLeaf line 63
  25. abbrev OAI.BinPackingGap.InventoryData.TestAt line 64
  26. def OAI.BinPackingGap.InventoryData.designated line 67
  27. def OAI.BinPackingGap.InventoryData.plusSlots line 72
  28. def OAI.BinPackingGap.InventoryData.minusSlots line 73
  29. def OAI.BinPackingGap.InventoryData.treeFlags line 74
  30. def OAI.BinPackingGap.InventoryData.jobFlags line 75
  31. inductive OAI.BinPackingGap.GlobalSpecies line 79
  32. instance OAI.BinPackingGap.(instance at line 85) line 85
  33. inductive OAI.BinPackingGap.FlagSpecies line 94
  34. instance OAI.BinPackingGap.(instance at line 100) line 100
  35. def OAI.BinPackingGap.InventoryData.globalStock line 108
  36. def OAI.BinPackingGap.InventoryData.flagStock line 115
  37. abbrev OAI.BinPackingGap.InventoryData.GlobalCopy line 120
  38. abbrev OAI.BinPackingGap.InventoryData.FlagCopy line 121
  39. def OAI.BinPackingGap.InventoryData.RoleCopies line 123
  40. instance OAI.BinPackingGap.InventoryData.roleCopiesFintype line 130
  41. abbrev OAI.BinPackingGap.InventoryData.Item line 133
  42. def OAI.BinPackingGap.InventoryData.itemRole line 135
  43. def OAI.BinPackingGap.InventoryData.itemLabel line 137
  44. def OAI.BinPackingGap.InventoryData.treeSubclass line 144
  45. def OAI.BinPackingGap.InventoryData.rowSubclass line 149
  46. def OAI.BinPackingGap.InventoryData.itemSubclass line 153
  47. theorem OAI.BinPackingGap.InventoryData.itemSubclass_role line 166
  48. def OAI.BinPackingGap.InventoryData.rowShort line 182
  49. def OAI.BinPackingGap.InventoryData.jobPosition line 186
  50. def OAI.BinPackingGap.InventoryData.rowPosition line 189
  51. def OAI.BinPackingGap.InventoryData.keyPosition line 193
  52. def OAI.BinPackingGap.InventoryData.globalUnit line 196
  53. def OAI.BinPackingGap.InventoryData.globalEdge line 201
  54. def OAI.BinPackingGap.InventoryData.globalPermit line 205
  55. def OAI.BinPackingGap.InventoryData.localDepth line 209
  56. theorem OAI.BinPackingGap.sum_primaryScore_eq_zero_of_inventory line 215
  57. def OAI.BinPackingGap.labelledRoleCount line 252
  58. theorem OAI.BinPackingGap.sum_secondaryScore_eq line 256
  59. theorem OAI.BinPackingGap.sum_secondaryScore_eq_zero_of_inventory line 283
  60. def OAI.BinPackingGap.GlobalSpecies.equivSum line 297
  61. theorem OAI.BinPackingGap.GlobalSpecies.sum_univ line 310
  62. theorem OAI.BinPackingGap.FlagSpecies.sum_univ line 325
  63. theorem OAI.BinPackingGap.InventoryData.card_treeRow line 337
  64. theorem OAI.BinPackingGap.InventoryData.card_jobCopy line 341
  65. theorem OAI.BinPackingGap.InventoryData.card_rowAt line 344
  66. theorem OAI.BinPackingGap.InventoryData.card_mBase line 349
  67. theorem OAI.BinPackingGap.InventoryData.card_anchorAt line 353
  68. theorem OAI.BinPackingGap.InventoryData.card_localBin line 359
  69. theorem OAI.BinPackingGap.InventoryData.P_le_t line 363
  70. theorem OAI.BinPackingGap.InventoryData.d_le_tPlus line 367
  71. theorem OAI.BinPackingGap.InventoryData.d_le_tMinus line 371
  72. theorem OAI.BinPackingGap.InventoryData.two_mul_d_le_t_sub_P line 375
  73. theorem OAI.BinPackingGap.InventoryData.card_positiveLocal line 381
  74. theorem OAI.BinPackingGap.InventoryData.card_zeroLocalAt line 386
  75. theorem OAI.BinPackingGap.InventoryData.card_dmAt line 392
  76. theorem OAI.BinPackingGap.InventoryData.card_localAt line 398
  77. theorem OAI.BinPackingGap.InventoryData.sum_J line 403
  78. theorem OAI.BinPackingGap.InventoryData.plusSlots_eq line 406
  79. theorem OAI.BinPackingGap.InventoryData.B_eq line 409
  80. theorem OAI.BinPackingGap.InventoryData.B_closed line 412
  81. theorem OAI.BinPackingGap.InventoryData.unitPlus_le_stock line 416
  82. theorem OAI.BinPackingGap.InventoryData.unitMinus_le_stock line 423
  83. theorem OAI.BinPackingGap.InventoryData.up_species_total line 431
  84. theorem OAI.BinPackingGap.InventoryData.um_species_total line 436
  85. theorem OAI.BinPackingGap.InventoryData.card_globalCopy line 441
  86. theorem OAI.BinPackingGap.InventoryData.card_flagCopy line 454
  87. theorem OAI.BinPackingGap.InventoryData.card_roleCopies line 462
  88. theorem OAI.BinPackingGap.InventoryData.card_item line 471
  89. def OAI.BinPackingGap.InventoryData.allJobEquiv line 487
  90. def OAI.BinPackingGap.InventoryData.keyItem line 498
  91. def OAI.BinPackingGap.InventoryData.keyData line 501
  92. theorem OAI.BinPackingGap.InventoryData.keyData_keyItem line 505
  93. theorem OAI.BinPackingGap.InventoryData.keyItem_injective line 508
  94. theorem OAI.BinPackingGap.InventoryData.keyItem_role line 512
  95. theorem OAI.BinPackingGap.InventoryData.keyItem_subclass line 515
  96. theorem OAI.BinPackingGap.InventoryData.keyItem_label line 518
  97. def OAI.BinPackingGap.InventoryData.edgeResourceItem line 521
  98. def OAI.BinPackingGap.InventoryData.edgeResourceData line 524
  99. theorem OAI.BinPackingGap.InventoryData.edgeResourceData_edgeResourceItem line 528
  100. theorem OAI.BinPackingGap.InventoryData.edgeResourceItem_injective line 532
  101. def OAI.BinPackingGap.InventoryData.prefixJobIndex line 537
  102. theorem OAI.BinPackingGap.InventoryData.prefixJobIndex_injective line 542
  103. def OAI.BinPackingGap.InventoryData.earlierKeys line 554
  104. theorem OAI.BinPackingGap.InventoryData.earlierKeys_card line 558
  105. theorem OAI.BinPackingGap.InventoryData.mem_earlierKeys line 569
  106. def OAI.BinPackingGap.InventoryData.prefixWIndex line 594
  107. theorem OAI.BinPackingGap.InventoryData.prefixWIndex_injective line 599
  108. def OAI.BinPackingGap.InventoryData.earlierW line 609
  109. theorem OAI.BinPackingGap.InventoryData.earlierW_card line 613
  110. theorem OAI.BinPackingGap.InventoryData.mem_earlierW line 623
  111. theorem OAI.BinPackingGap.InventoryData.earlierW_card_eq_keys line 643
  112. theorem OAI.BinPackingGap.InventoryData.subclassCount_by_role line 660
  113. theorem OAI.BinPackingGap.InventoryData.roleCount_itemSubclass line 679
  114. theorem OAI.BinPackingGap.InventoryData.subclassCount_tp line 688
  115. theorem OAI.BinPackingGap.InventoryData.subclassCount_tm line 698
  116. theorem OAI.BinPackingGap.InventoryData.subclassCount_s line 707
  117. theorem OAI.BinPackingGap.InventoryData.subclassCount_z line 716
  118. theorem OAI.BinPackingGap.InventoryData.subclassCount_y line 725
  119. theorem OAI.BinPackingGap.InventoryData.subclassCount_up line 734
  120. theorem OAI.BinPackingGap.InventoryData.subclassCount_um line 745
  121. theorem OAI.BinPackingGap.InventoryData.subclassCount_dm line 756
  122. theorem OAI.BinPackingGap.InventoryData.subclassCount_dg line 765
  123. theorem OAI.BinPackingGap.InventoryData.subclassCount_ft line 774
  124. theorem OAI.BinPackingGap.InventoryData.subclassCount_fm line 784
  125. theorem OAI.BinPackingGap.InventoryData.subclassCount_fg line 794
  126. theorem OAI.BinPackingGap.InventoryData.total_primaryScore_eq_zero line 804
  127. theorem OAI.BinPackingGap.InventoryData.labelledRoleCount_x line 824
  128. theorem OAI.BinPackingGap.InventoryData.labelledRoleCount_anchor line 834
  129. theorem OAI.BinPackingGap.InventoryData.labelledRoleCount_local line 844
  130. theorem OAI.BinPackingGap.InventoryData.total_secondaryScore_eq_zero line 854