OAI/Computability/BinPacking/Machines/GraphPackingPreparationFinish.lean

GitHub source file

98 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.PackingEndpointPower.values line 15
  2. def OAI.BinPackingGap.PackingEndpointPower.tallyRegister line 17
  3. def OAI.BinPackingGap.PackingEndpointPower.tallySlots line 25
  4. theorem OAI.BinPackingGap.PackingEndpointPower.tallySlots_reg line 30
  5. theorem OAI.BinPackingGap.PackingEndpointPower.tallySlots_scratch line 35
  6. def OAI.BinPackingGap.PackingEndpointPower.updateRegister line 38
  7. def OAI.BinPackingGap.PackingEndpointPower.updateSlots line 42
  8. theorem OAI.BinPackingGap.PackingEndpointPower.updateSlots_reg line 46
  9. theorem OAI.BinPackingGap.PackingEndpointPower.updateSlots_scratch line 50
  10. def OAI.BinPackingGap.PackingEndpointPower.powerSlots line 53
  11. structure OAI.BinPackingGap.PackingEndpointPower.Ready line 64
  12. def OAI.BinPackingGap.PackingEndpointPower.code line 70
  13. def OAI.BinPackingGap.PackingEndpointPower.resultTapes line 78
  14. def OAI.BinPackingGap.PackingEndpointPower.timePolynomial line 81
  15. theorem OAI.BinPackingGap.PackingEndpointPower.timePolynomial_eval line 87
  16. theorem OAI.BinPackingGap.PackingEndpointPower.size_three line 92
  17. theorem OAI.BinPackingGap.PackingEndpointPower.tally_budget_le line 94
  18. theorem OAI.BinPackingGap.PackingEndpointPower.power_budget line 102
  19. theorem OAI.BinPackingGap.PackingEndpointPower.multiply_budget_le line 109
  20. theorem OAI.BinPackingGap.PackingEndpointPower.register_frame_eq line 117
  21. theorem OAI.BinPackingGap.PackingEndpointPower.exec line 129
  22. abbrev OAI.BinPackingGap.PackingVertexLoop.VertexTape line 238
  23. def OAI.BinPackingGap.PackingVertexLoop.body line 241
  24. def OAI.BinPackingGap.PackingVertexLoop.code line 249
  25. def OAI.BinPackingGap.PackingVertexLoop.bodyTimePolynomial line 255
  26. theorem OAI.BinPackingGap.PackingVertexLoop.bodyTimePolynomial_eval line 261
  27. theorem OAI.BinPackingGap.PackingVertexLoop.layout_external_update line 268
  28. theorem OAI.BinPackingGap.PackingVertexLoop.layout_output line 277
  29. theorem OAI.BinPackingGap.PackingVertexLoop.layout_counter line 285
  30. theorem OAI.BinPackingGap.PackingVertexLoop.output_counter line 292
  31. theorem OAI.BinPackingGap.PackingVertexLoop.body_exec line 306
  32. theorem OAI.BinPackingGap.PackingVertexLoop.exec_bounded line 348
  33. theorem OAI.BinPackingGap.PackingVertexLoop.exec line 411
  34. def OAI.BinPackingGap.PackingVertexLoop.timePolynomial line 434
  35. theorem OAI.BinPackingGap.PackingVertexLoop.exec_polynomial line 437
  36. abbrev OAI.BinPackingGap.GraphPackingProgram.Program line 478
  37. def OAI.BinPackingGap.GraphPackingProgram.chain line 480
  38. def OAI.BinPackingGap.GraphPackingProgram.regTape line 484
  39. def OAI.BinPackingGap.GraphPackingProgram.otherSetup line 486
  40. def OAI.BinPackingGap.GraphPackingProgram.tally line 489
  41. def OAI.BinPackingGap.GraphPackingProgram.tallyToBinary line 493
  42. def OAI.BinPackingGap.GraphPackingProgram.power line 499
  43. def OAI.BinPackingGap.GraphPackingProgram.setItem line 503
  44. def OAI.BinPackingGap.GraphPackingProgram.setWork line 506
  45. def OAI.BinPackingGap.GraphPackingProgram.geometryOperands line 510
  46. def OAI.BinPackingGap.GraphPackingProgram.geometry line 524
  47. def OAI.BinPackingGap.GraphPackingProgram.header line 529
  48. def OAI.BinPackingGap.GraphPackingProgram.prepare line 536
  49. def OAI.BinPackingGap.GraphPackingProgram.vertices line 550
  50. def OAI.BinPackingGap.GraphPackingProgram.endpoint line 559
  51. def OAI.BinPackingGap.GraphPackingProgram.incrementEdge line 565
  52. def OAI.BinPackingGap.GraphPackingProgram.edgeBody line 570
  53. def OAI.BinPackingGap.GraphPackingProgram.jobs line 591
  54. def OAI.BinPackingGap.GraphPackingProgram.pool line 597
  55. def OAI.BinPackingGap.GraphPackingProgram.globalEdgeBody line 604
  56. def OAI.BinPackingGap.GraphPackingProgram.globals line 608
  57. def OAI.BinPackingGap.GraphPackingProgram.flags line 619
  58. def OAI.BinPackingGap.GraphPackingProgram.finish line 624
  59. def OAI.BinPackingGap.GraphPackingProgram.code line 631
  60. def OAI.BinPackingGap.GraphPackingProgram.machine line 635
  61. theorem OAI.BinPackingGap.GraphPackingProgram.finiteAlphabet line 638
  62. inductive OAI.BinPackingGap.GraphPackingProgram.PhaseRuns line 647
  63. theorem OAI.BinPackingGap.GraphPackingProgram.PhaseRuns.single line 657
  64. theorem OAI.BinPackingGap.GraphPackingProgram.PhaseRuns.append line 661
  65. theorem OAI.BinPackingGap.GraphPackingProgram.PhaseRuns.toExec line 669
  66. theorem OAI.BinPackingGap.GraphPackingTapeBlocks.slots_outside line 688
  67. theorem OAI.BinPackingGap.GraphPackingTapeBlocks.frame_extra line 692
  68. theorem OAI.BinPackingGap.GraphPackingTapeBlocks.tally_exec line 699
  69. theorem OAI.BinPackingGap.GraphPackingTapeBlocks.power_exec line 738
  70. def OAI.BinPackingGap.GraphPackingPreparation.setupValues line 795
  71. def OAI.BinPackingGap.GraphPackingPreparation.firstPowerValues line 799
  72. def OAI.BinPackingGap.GraphPackingPreparation.secondPowerValues line 802
  73. def OAI.BinPackingGap.GraphPackingPreparation.factorValues line 806
  74. def OAI.BinPackingGap.GraphPackingPreparation.finalValues line 810
  75. theorem OAI.BinPackingGap.GraphPackingPreparation.setupValues_item line 814
  76. theorem OAI.BinPackingGap.GraphPackingPreparation.setupValues_work line 817
  77. theorem OAI.BinPackingGap.GraphPackingPreparation.setupValues_input line 820
  78. theorem OAI.BinPackingGap.GraphPackingPreparation.setupValues_output line 824
  79. theorem OAI.BinPackingGap.GraphPackingPreparation.base_powerCounter line 829
  80. theorem OAI.BinPackingGap.GraphPackingPreparation.setup_exec line 832
  81. def OAI.BinPackingGap.GraphPackingPreparation.powerPhases line 866
  82. def OAI.BinPackingGap.GraphPackingPreparation.powerBudget line 872
  83. theorem OAI.BinPackingGap.GraphPackingPreparation.powers_exec line 878
  84. theorem OAI.BinPackingGap.GraphPackingPreparation.item_register line 978
  85. theorem OAI.BinPackingGap.GraphPackingPreparation.work_register line 981
  86. theorem OAI.BinPackingGap.GraphPackingPreparation.setupValues_width line 984
  87. theorem OAI.BinPackingGap.GraphPackingPreparation.firstPowerValues_width line 993
  88. theorem OAI.BinPackingGap.GraphPackingPreparation.secondPowerValues_width line 998
  89. theorem OAI.BinPackingGap.GraphPackingPreparation.factorValues_width line 1003
  90. theorem OAI.BinPackingGap.GraphPackingPreparation.finalValues_eq line 1008
  91. theorem OAI.BinPackingGap.GraphPackingPreparation.finalValues_width line 1026
  92. def OAI.BinPackingGap.GraphPackingPreparation.geometryPolynomial line 1033
  93. theorem OAI.BinPackingGap.GraphPackingPreparation.geometry_exec line 1039
  94. theorem OAI.BinPackingGap.GraphPackingPreparation.headerDifferent line 1074
  95. def OAI.BinPackingGap.GraphPackingPreparation.headerPolynomial line 1077
  96. theorem OAI.BinPackingGap.GraphPackingPreparation.header_exec line 1082
  97. def OAI.BinPackingGap.GraphPackingPreparation.finishPolynomial line 1135
  98. theorem OAI.BinPackingGap.GraphPackingPreparation.finish_exec line 1137