OAI/Computability/BinPacking/Machines/GraphPackingMachine.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.GraphPackingFinish.transfer line 17
  2. def OAI.BinPackingGap.GraphPackingFinish.resultTapes line 21
  3. theorem OAI.BinPackingGap.GraphPackingFinish.resultTapes_output line 26
  4. theorem OAI.BinPackingGap.GraphPackingFinish.resultTapes_reverse line 30
  5. theorem OAI.BinPackingGap.GraphPackingFinish.resultTapes_other line 34
  6. theorem OAI.BinPackingGap.GraphPackingFinish.transfer_exec line 39
  7. theorem OAI.BinPackingGap.GraphPackingFinish.finish_exec line 78
  8. def OAI.BinPackingGap.GraphPackingFinish.rawProgram line 97
  9. theorem OAI.BinPackingGap.GraphPackingFinish.sourceMachine_eq line 105
  10. def OAI.BinPackingGap.GraphPackingFinish.cleanupTapes line 108
  11. theorem OAI.BinPackingGap.GraphPackingFinish.cleanup_complete line 111
  12. def OAI.BinPackingGap.GraphPackingFinish.canonicalMachine line 115
  13. theorem OAI.BinPackingGap.GraphPackingFinish.canonical_finiteAlphabet line 118
  14. def OAI.BinPackingGap.GraphPackingFinish.canonicalTime line 122
  15. def OAI.BinPackingGap.GraphPackingFixedParameters.emptyGraph line 129
  16. def OAI.BinPackingGap.GraphPackingFixedParameters.fixedInventory line 135
  17. theorem OAI.BinPackingGap.GraphPackingFixedParameters.inventory_eq line 138
  18. theorem OAI.BinPackingGap.GraphPackingFixedParameters.binBound_eq_inventory line 142
  19. theorem OAI.BinPackingGap.GraphPackingFixedParameters.binBound_eq_reduction line 148
  20. theorem OAI.BinPackingGap.GraphPackingFixedParameters.rawOutput_eq line 154
  21. theorem OAI.BinPackingGap.GraphPackingFixedParameters.outputBits_eq line 160
  22. def OAI.BinPackingGap.GraphPackingJobs.setupPhases line 183
  23. def OAI.BinPackingGap.GraphPackingJobs.setupTapes line 189
  24. def OAI.BinPackingGap.GraphPackingJobs.resetInputs line 195
  25. theorem OAI.BinPackingGap.GraphPackingJobs.resetInputs_eq line 199
  26. theorem OAI.BinPackingGap.GraphPackingJobs.bounded_update line 212
  27. theorem OAI.BinPackingGap.GraphPackingJobs.vertexFinalInputs_width line 222
  28. def OAI.BinPackingGap.GraphPackingJobs.setupValues line 236
  29. theorem OAI.BinPackingGap.GraphPackingJobs.finalBase_edgeCounter line 240
  30. theorem OAI.BinPackingGap.GraphPackingJobs.tally_frame line 245
  31. def OAI.BinPackingGap.GraphPackingJobs.setupSetPolynomial line 257
  32. def OAI.BinPackingGap.GraphPackingJobs.setupTimePolynomial line 265
  33. def OAI.BinPackingGap.GraphPackingJobs.setupBound line 269
  34. theorem OAI.BinPackingGap.GraphPackingJobs.setupBound_le line 273
  35. theorem OAI.BinPackingGap.GraphPackingJobs.setup_exec line 294
  36. def OAI.BinPackingGap.GraphPackingJobs.emitted line 356
  37. def OAI.BinPackingGap.GraphPackingJobs.finalBase line 359
  38. def OAI.BinPackingGap.GraphPackingJobs.finalTapes line 362
  39. theorem OAI.BinPackingGap.GraphPackingJobs.finalBase_extra line 366
  40. def OAI.BinPackingGap.GraphPackingJobs.timePolynomial line 372
  41. theorem OAI.BinPackingGap.GraphPackingJobs.exec line 375
  42. def OAI.BinPackingGap.GraphPackingRun.globalWord line 428
  43. def OAI.BinPackingGap.GraphPackingRun.flagWord line 431
  44. def OAI.BinPackingGap.GraphPackingRun.afterGlobalBase line 434
  45. def OAI.BinPackingGap.GraphPackingRun.beforeFinishBase line 437
  46. def OAI.BinPackingGap.GraphPackingRun.beforeFinishTapes line 440
  47. def OAI.BinPackingGap.GraphPackingRun.constructorWord line 444
  48. theorem OAI.BinPackingGap.GraphPackingRun.beforeFinish_reverse line 448
  49. theorem OAI.BinPackingGap.GraphPackingRun.beforeFinish_output_empty line 457
  50. theorem OAI.BinPackingGap.GraphPackingRun.constructorWord_eq line 461
  51. def OAI.BinPackingGap.GraphPackingRun.prefixPhases line 468
  52. def OAI.BinPackingGap.GraphPackingRun.prefixProgram line 473
  53. def OAI.BinPackingGap.GraphPackingRun.prefixTimePolynomial line 476
  54. theorem OAI.BinPackingGap.GraphPackingRun.prefix_runs line 481
  55. def OAI.BinPackingGap.GraphPackingRun.prefixPushBound line 505
  56. def OAI.BinPackingGap.GraphPackingRun.wordTimePolynomial line 509
  57. theorem OAI.BinPackingGap.GraphPackingRun.constructorWord_length_le line 512
  58. def OAI.BinPackingGap.GraphPackingRun.timePolynomial line 532
  59. def OAI.BinPackingGap.GraphPackingRun.finalTapes line 535
  60. theorem OAI.BinPackingGap.GraphPackingRun.exec line 538
  61. def OAI.BinPackingGap.GraphPackingRun.terminalRun line 556
  62. def OAI.BinPackingGap.graphPackingComputation line 603
  63. theorem OAI.BinPackingGap.graphPackingComputation_finiteAlphabet line 616