OAI/Computability/BinPacking/Machines/GraphPackingGlobalExecution.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinPackingGap.GraphPackingPoolExec.layout_external_update line 21
  2. theorem OAI.BinPackingGap.GraphPackingPoolExec.layout_output line 30
  3. theorem OAI.BinPackingGap.GraphPackingPoolExec.layout_counter line 38
  4. def OAI.BinPackingGap.GraphPackingPoolExec.poolWord line 52
  5. def OAI.BinPackingGap.GraphPackingPoolExec.poolBudget line 58
  6. theorem OAI.BinPackingGap.GraphPackingPoolExec.pool_exec line 64
  7. def OAI.BinPackingGap.GraphPackingGlobalLoop.radix line 162
  8. def OAI.BinPackingGap.GraphPackingGlobalLoop.edgeInput line 165
  9. theorem OAI.BinPackingGap.GraphPackingGlobalLoop.edgeInput_power line 168
  10. theorem OAI.BinPackingGap.GraphPackingGlobalLoop.edgeInput_update line 172
  11. def OAI.BinPackingGap.GraphPackingGlobalLoop.aggregateWidth line 179
  12. theorem OAI.BinPackingGap.GraphPackingGlobalLoop.edgeInput_size_le line 182
  13. def OAI.BinPackingGap.GraphPackingGlobalLoop.edgeWord line 200
  14. def OAI.BinPackingGap.GraphPackingGlobalLoop.bodyBudget line 204
  15. theorem OAI.BinPackingGap.GraphPackingGlobalLoop.body_exec line 209
  16. def OAI.BinPackingGap.GraphPackingGlobalLoop.stream line 251
  17. theorem OAI.BinPackingGap.GraphPackingGlobalLoop.layout_counter line 257
  18. theorem OAI.BinPackingGap.GraphPackingGlobalLoop.exec_bounded line 263
  19. theorem OAI.BinPackingGap.GraphPackingGlobalLoop.exec line 330
  20. abbrev OAI.BinPackingGap.GraphPackingGlobalPhases.Pool line 362
  21. def OAI.BinPackingGap.GraphPackingGlobalPhases.poolListWord line 364
  22. def OAI.BinPackingGap.GraphPackingGlobalPhases.poolListBudget line 368
  23. theorem OAI.BinPackingGap.GraphPackingGlobalPhases.pool_runs line 372
  24. def OAI.BinPackingGap.GraphPackingGlobalPhases.unitPools line 408
  25. def OAI.BinPackingGap.GraphPackingGlobalPhases.flagPools line 412
  26. theorem OAI.BinPackingGap.GraphPackingGlobalPhases.update_width line 415
  27. def OAI.BinPackingGap.GraphPackingGlobalPhases.flagInput line 425
  28. def OAI.BinPackingGap.GraphPackingGlobalPhases.flagsBudget line 427
  29. theorem OAI.BinPackingGap.GraphPackingGlobalPhases.flags_exec line 432
  30. def OAI.BinPackingGap.GraphPackingGlobalPhases.unitInput line 461
  31. def OAI.BinPackingGap.GraphPackingGlobalPhases.globalCount line 464
  32. def OAI.BinPackingGap.GraphPackingGlobalPhases.globalsWord line 467
  33. def OAI.BinPackingGap.GraphPackingGlobalPhases.globalsInput line 471
  34. def OAI.BinPackingGap.GraphPackingGlobalPhases.resetBudget line 474
  35. def OAI.BinPackingGap.GraphPackingGlobalPhases.globalsBudget line 482
  36. theorem OAI.BinPackingGap.GraphPackingGlobalPhases.globals_exec line 489
  37. theorem OAI.BinPackingGap.GraphPackingGlobalLoop.stream_eq_finRange line 596
  38. theorem OAI.BinPackingGap.GraphPackingJobs.loop_exec_list line 625
  39. def OAI.BinPackingGap.GraphPackingJobs.loopTimePolynomial line 720
  40. theorem OAI.BinPackingGap.GraphPackingJobs.loop_exec line 723
  41. def OAI.BinPackingGap.GraphPackingPoolRuntime.tallyPolynomial line 762
  42. theorem OAI.BinPackingGap.GraphPackingPoolRuntime.tallyPolynomial_eval line 765
  43. theorem OAI.BinPackingGap.GraphPackingPoolRuntime.tally_le line 770
  44. def OAI.BinPackingGap.GraphPackingPoolRuntime.poolPolynomial line 783
  45. theorem OAI.BinPackingGap.GraphPackingPoolRuntime.poolPolynomial_eval line 789
  46. theorem OAI.BinPackingGap.GraphPackingPoolRuntime.poolBudget_le line 798
  47. def OAI.BinPackingGap.GraphPackingPoolRuntime.poolListPolynomial line 813
  48. theorem OAI.BinPackingGap.GraphPackingPoolRuntime.poolListPolynomial_eval line 817
  49. theorem OAI.BinPackingGap.GraphPackingPoolRuntime.poolListBudget_le line 823
  50. def OAI.BinPackingGap.GraphPackingGlobalSemantics.inventory line 854
  51. def OAI.BinPackingGap.GraphPackingGlobalSemantics.globalOutput line 857
  52. def OAI.BinPackingGap.GraphPackingGlobalSemantics.flagOutput line 864
  53. theorem OAI.BinPackingGap.GraphPackingGlobalSemantics.prepared_output line 868
  54. theorem OAI.BinPackingGap.GraphPackingGlobalSemantics.prepared_globalStock line 876
  55. theorem OAI.BinPackingGap.GraphPackingGlobalSemantics.prepared_flagStock line 885
  56. theorem OAI.BinPackingGap.GraphPackingGlobalSemantics.prepared_radix line 891
  57. theorem OAI.BinPackingGap.GraphPackingGlobalSemantics.prepared_globalCount line 895
  58. theorem OAI.BinPackingGap.GraphPackingGlobalSemantics.unitInput_values line 898
  59. theorem OAI.BinPackingGap.GraphPackingGlobalSemantics.edgeInput_values line 905
  60. theorem OAI.BinPackingGap.GraphPackingGlobalSemantics.flagInput_values line 914
  61. theorem OAI.BinPackingGap.GraphPackingGlobalSemantics.poolWord_global line 920
  62. theorem OAI.BinPackingGap.GraphPackingGlobalSemantics.poolWord_flag line 935
  63. theorem OAI.BinPackingGap.GraphPackingGlobalSemantics.unitPools_word line 949
  64. theorem OAI.BinPackingGap.GraphPackingGlobalSemantics.edgeWord_values line 967
  65. theorem OAI.BinPackingGap.GraphPackingGlobalSemantics.flagPools_word line 979
  66. theorem OAI.BinPackingGap.GraphPackingGlobalSemantics.globalsWord_eq line 991
  67. theorem OAI.BinPackingGap.GraphPackingGlobalSemantics.globalsInput_eq line 1006
  68. theorem OAI.BinPackingGap.GraphPackingGlobalSemantics.flagInput_eq line 1017
  69. theorem OAI.BinPackingGap.GraphPackingGlobalSemantics.flagsWord_eq line 1022
  70. def OAI.BinPackingGap.GraphPackingGlobalRuntime.adjustedWidthPolynomial line 1039
  71. def OAI.BinPackingGap.GraphPackingGlobalRuntime.edgeWidthPolynomial line 1042
  72. def OAI.BinPackingGap.GraphPackingGlobalRuntime.resetPolynomial line 1046
  73. def OAI.BinPackingGap.GraphPackingGlobalRuntime.edgeBodyPolynomial line 1054
  74. def OAI.BinPackingGap.GraphPackingGlobalRuntime.flagsPolynomial line 1062
  75. def OAI.BinPackingGap.GraphPackingGlobalRuntime.globalsPolynomial line 1068
  76. theorem OAI.BinPackingGap.GraphPackingGlobalRuntime.width_le line 1074
  77. theorem OAI.BinPackingGap.GraphPackingGlobalRuntime.adjustedWidth_le line 1080
  78. theorem OAI.BinPackingGap.GraphPackingGlobalRuntime.radixWidth_le line 1086
  79. theorem OAI.BinPackingGap.GraphPackingGlobalRuntime.stockCount_le line 1092
  80. theorem OAI.BinPackingGap.GraphPackingGlobalRuntime.unitCounts_le line 1111
  81. theorem OAI.BinPackingGap.GraphPackingGlobalRuntime.flagCounts_le line 1120
  82. theorem OAI.BinPackingGap.GraphPackingGlobalRuntime.aggregateWidth_le line 1129
  83. theorem OAI.BinPackingGap.GraphPackingGlobalRuntime.resetBudget_le line 1141
  84. theorem OAI.BinPackingGap.GraphPackingGlobalRuntime.bodyBudget_le line 1156
  85. theorem OAI.BinPackingGap.GraphPackingGlobalRuntime.flagsBudget_le line 1174
  86. theorem OAI.BinPackingGap.GraphPackingGlobalRuntime.globalsBudget_le line 1187
  87. theorem OAI.BinPackingGap.GraphPackingGlobalExecution.globals_exec line 1217
  88. theorem OAI.BinPackingGap.GraphPackingGlobalExecution.flags_exec line 1246