OAI/Computability/BinPacking/Machines/GraphPackingPreparation.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinPackingGap.GraphPackingPreparation.graphSlots_apply line 18
  2. theorem OAI.BinPackingGap.GraphPackingPreparation.thresholdSlots_apply line 24
  3. theorem OAI.BinPackingGap.GraphPackingPreparation.setup_apply line 29
  4. def OAI.BinPackingGap.GraphPackingPreparation.parsePhases line 32
  5. def OAI.BinPackingGap.GraphPackingPreparation.parsePolynomial line 38
  6. def OAI.BinPackingGap.GraphPackingPreparation.fieldTapes line 41
  7. theorem OAI.BinPackingGap.GraphPackingPreparation.preparation_frame line 49
  8. def OAI.BinPackingGap.GraphPackingPreparation.vertexTapes line 80
  9. def OAI.BinPackingGap.GraphPackingPreparation.edgeTapes line 84
  10. theorem OAI.BinPackingGap.GraphPackingPreparation.decoded_frame line 88
  11. theorem OAI.BinPackingGap.GraphPackingPreparation.tally_exec line 142
  12. theorem OAI.BinPackingGap.GraphPackingPreparation.parse_exec line 169
  13. def OAI.BinPackingGap.GraphPackingPreparation.powerPolynomial line 222
  14. theorem OAI.BinPackingGap.GraphPackingPreparation.tally_bound line 226
  15. theorem OAI.BinPackingGap.GraphPackingPreparation.powerBudget_le line 236
  16. def OAI.BinPackingGap.GraphPackingPreparation.arithmeticPolynomial line 259
  17. def OAI.BinPackingGap.GraphPackingPreparation.timePolynomial line 270
  18. theorem OAI.BinPackingGap.GraphPackingPreparation.prepare_exec line 273