OAI/Computability/BinPacking/Hardness/LiteralSlotGraph.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.LiteralSlotGraph.vertexCount line 17
  2. abbrev OAI.BinPackingGap.LiteralSlotGraph.Vertex line 19
  3. def OAI.BinPackingGap.LiteralSlotGraph.occurrence line 21
  4. def OAI.BinPackingGap.LiteralSlotGraph.slot line 24
  5. def OAI.BinPackingGap.LiteralSlotGraph.index line 27
  6. theorem OAI.BinPackingGap.LiteralSlotGraph.occurrence_index line 34
  7. theorem OAI.BinPackingGap.LiteralSlotGraph.slot_index line 41
  8. theorem OAI.BinPackingGap.LiteralSlotGraph.index_occurrence_slot line 48
  9. def OAI.BinPackingGap.LiteralSlotGraph.literal line 54
  10. theorem OAI.BinPackingGap.LiteralSlotGraph.literal_index line 57
  11. def OAI.BinPackingGap.LiteralSlotGraph.Conflict line 61
  12. instance OAI.BinPackingGap.LiteralSlotGraph.(instance at line 66) line 66
  13. theorem OAI.BinPackingGap.LiteralSlotGraph.conflict_symm line 70
  14. def OAI.BinPackingGap.LiteralSlotGraph.edgeList line 76
  15. theorem OAI.BinPackingGap.LiteralSlotGraph.mem_edgeList line 80
  16. def OAI.BinPackingGap.LiteralSlotGraph.graph line 84
  17. theorem OAI.BinPackingGap.LiteralSlotGraph.graph_n line 94
  18. theorem OAI.BinPackingGap.LiteralSlotGraph.graph_edges_nonempty line 96
  19. def OAI.BinPackingGap.LiteralSlotGraph.Independent line 110
  20. theorem OAI.BinPackingGap.LiteralSlotGraph.independent_complement_of_cover line 113
  21. theorem OAI.BinPackingGap.LiteralSlotGraph.cover_complement_of_independent line 128
  22. theorem OAI.BinPackingGap.LiteralSlotGraph.occurrence_injective_on_independent line 142
  23. theorem OAI.BinPackingGap.LiteralSlotGraph.literal_true_iff line 148
  24. theorem OAI.BinPackingGap.LiteralSlotGraph.true_literals_not_complementary line 153
  25. theorem OAI.BinPackingGap.LiteralSlotGraph.assignment_of_independent line 162
  26. def OAI.BinPackingGap.LiteralSlotGraph.chosenSlot line 188
  27. theorem OAI.BinPackingGap.LiteralSlotGraph.chosenSlot_true line 193
  28. def OAI.BinPackingGap.LiteralSlotGraph.selectedSlots line 206
  29. theorem OAI.BinPackingGap.LiteralSlotGraph.selectedSlots_card line 209
  30. theorem OAI.BinPackingGap.LiteralSlotGraph.selectedSlots_independent line 218
  31. theorem OAI.BinPackingGap.LiteralSlotGraph.coverAtMost_of_satisfiable line 233