OAI/Computability/BinPacking/Machines/GraphPackingVerticesBound.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.GraphPackingVertices.startInputs line 17
  2. def OAI.BinPackingGap.GraphPackingVertices.startBase line 24
  3. def OAI.BinPackingGap.GraphPackingVertices.startValues line 28
  4. def OAI.BinPackingGap.GraphPackingVertices.startTapes line 32
  5. theorem OAI.BinPackingGap.GraphPackingVertices.update_width line 37
  6. theorem OAI.BinPackingGap.GraphPackingVertices.startInputs_width line 47
  7. theorem OAI.BinPackingGap.GraphPackingVertices.startValues_count_n line 62
  8. theorem OAI.BinPackingGap.GraphPackingVertices.startValues_counter line 65
  9. theorem OAI.BinPackingGap.GraphPackingVertices.startValues_one line 68
  10. theorem OAI.BinPackingGap.GraphPackingVertices.startValues_temporary line 71
  11. theorem OAI.BinPackingGap.GraphPackingVertices.startBase_vertexCounter line 74
  12. def OAI.BinPackingGap.GraphPackingVertices.setupPhases line 77
  13. def OAI.BinPackingGap.GraphPackingVertices.setupBound line 83
  14. theorem OAI.BinPackingGap.GraphPackingVertices.tally_frame line 92
  15. theorem OAI.BinPackingGap.GraphPackingVertices.setup_exec line 108
  16. def OAI.BinPackingGap.GraphPackingVertices.data line 168
  17. def OAI.BinPackingGap.GraphPackingVertices.inputValues line 172
  18. theorem OAI.BinPackingGap.GraphPackingVertices.startInputs_eq line 175
  19. theorem OAI.BinPackingGap.GraphPackingVertices.inputValues_width line 187
  20. def OAI.BinPackingGap.GraphPackingVertices.emitted line 198
  21. theorem OAI.BinPackingGap.GraphPackingVertices.stream_eq_emitted line 201
  22. def OAI.BinPackingGap.GraphPackingVertices.finalInputs line 218
  23. def OAI.BinPackingGap.GraphPackingVertices.finalBase line 221
  24. def OAI.BinPackingGap.GraphPackingVertices.finalTapes line 224
  25. theorem OAI.BinPackingGap.GraphPackingVertices.final_labelPower line 229
  26. theorem OAI.BinPackingGap.GraphPackingVertices.final_edgePower line 233
  27. theorem OAI.BinPackingGap.GraphPackingVertices.final_repetition line 237
  28. theorem OAI.BinPackingGap.GraphPackingVertices.final_counter_empty line 241
  29. theorem OAI.BinPackingGap.GraphPackingVertices.final_output line 245
  30. theorem OAI.BinPackingGap.GraphPackingVertices.finalTapes_eq_frame line 252
  31. def OAI.BinPackingGap.GraphPackingVertices.loopBudget line 265
  32. theorem OAI.BinPackingGap.GraphPackingVertices.loop_exec line 270
  33. def OAI.BinPackingGap.GraphPackingVertices.phaseBudget line 291
  34. theorem OAI.BinPackingGap.GraphPackingVertices.exec line 294
  35. def OAI.BinPackingGap.GraphPackingVerticesBound.setPolynomial line 320
  36. def OAI.BinPackingGap.GraphPackingVerticesBound.bodyPolynomial line 328
  37. def OAI.BinPackingGap.GraphPackingVerticesBound.polynomial line 332
  38. theorem OAI.BinPackingGap.GraphPackingVerticesBound.polynomial_eval line 339
  39. theorem OAI.BinPackingGap.GraphPackingVerticesBound.tallyBound_le line 347
  40. theorem OAI.BinPackingGap.GraphPackingVerticesBound.phaseBudget_le line 357
  41. theorem OAI.BinPackingGap.GraphPackingVerticesBound.exec line 385