OAI/Computability/BinPacking/Machines/GraphPackingJobList.lean

GitHub source file

107 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.GraphPackingPreparation.initialTapes line 13
  2. def OAI.BinPackingGap.GraphPackingPreparation.baseTapes line 17
  3. def OAI.BinPackingGap.GraphPackingPreparation.parsedOther line 24
  4. def OAI.BinPackingGap.GraphPackingPreparation.parsedTapes line 29
  5. def OAI.BinPackingGap.GraphPackingPreparation.setupOther line 33
  6. def OAI.BinPackingGap.GraphPackingPreparation.repetitions line 41
  7. def OAI.BinPackingGap.GraphPackingPreparation.geometryFactor line 44
  8. def OAI.BinPackingGap.GraphPackingPreparation.preparedInputs line 47
  9. def OAI.BinPackingGap.GraphPackingPreparation.preparedWork line 54
  10. def OAI.BinPackingGap.GraphPackingPreparation.preparedOther line 58
  11. def OAI.BinPackingGap.GraphPackingPreparation.binBound line 61
  12. def OAI.BinPackingGap.GraphPackingPreparation.preparedTapes line 65
  13. def OAI.BinPackingGap.GraphPackingJobStream.endpointPower line 76
  14. theorem OAI.BinPackingGap.GraphPackingJobStream.values_update_label line 79
  15. theorem OAI.BinPackingGap.GraphPackingJobStream.nextInput_values line 86
  16. def OAI.BinPackingGap.GraphPackingJobStream.rawPair line 96
  17. theorem OAI.BinPackingGap.GraphPackingJobStream.pairRecords_eq line 101
  18. theorem OAI.BinPackingGap.GraphPackingJobStream.stream_eq line 113
  19. theorem OAI.BinPackingGap.GraphPackingJobStream.stream_edge_eq line 137
  20. theorem OAI.BinPackingGap.GraphPackingJobStream.all_edges_eq line 147
  21. theorem OAI.BinPackingGap.GraphPackingJobStream.stream_edge_instantiate_eq line 156
  22. def OAI.BinPackingGap.GraphPackingWidths.treeScale line 183
  23. def OAI.BinPackingGap.GraphPackingWidths.setupPolynomial line 185
  24. theorem OAI.BinPackingGap.GraphPackingWidths.setupPolynomial_eval line 190
  25. def OAI.BinPackingGap.GraphPackingWidths.geometryCoefficient line 196
  26. def OAI.BinPackingGap.GraphPackingWidths.polynomial line 200
  27. theorem OAI.BinPackingGap.GraphPackingWidths.polynomial_eval line 207
  28. def OAI.BinPackingGap.GraphPackingWidths.width line 215
  29. theorem OAI.BinPackingGap.GraphPackingWidths.setup_width line 217
  30. theorem OAI.BinPackingGap.GraphPackingWidths.geometry_width line 246
  31. theorem OAI.BinPackingGap.GraphPackingWidths.edge_power_width line 264
  32. theorem OAI.BinPackingGap.GraphPackingWidths.vertex_power_width line 277
  33. theorem OAI.BinPackingGap.GraphPackingWidths.preparedInputs_width line 289
  34. theorem OAI.BinPackingGap.GraphPackingWidths.preparedWork_width line 300
  35. theorem OAI.BinPackingGap.GraphPackingWidths.preparedOther_width line 306
  36. theorem OAI.BinPackingGap.GraphPackingWidths.partial_inputs_width line 313
  37. theorem OAI.BinPackingGap.GraphPackingWidths.repetitions_width line 319
  38. theorem OAI.BinPackingGap.GraphPackingWidths.small_constant_width line 329
  39. theorem OAI.BinPackingGap.GraphPackingWidths.input_length_le_width line 334
  40. theorem OAI.BinPackingGap.GraphPackingWidths.update_width line 341
  41. def OAI.BinPackingGap.GraphPackingJobs.inventory line 358
  42. def OAI.BinPackingGap.GraphPackingJobs.inputs line 362
  43. theorem OAI.BinPackingGap.GraphPackingJobs.inputs_label line 366
  44. theorem OAI.BinPackingGap.GraphPackingJobs.inputs_repetition line 369
  45. theorem OAI.BinPackingGap.GraphPackingJobs.inputs_edge line 372
  46. theorem OAI.BinPackingGap.GraphPackingJobs.inputs_eq_values line 377
  47. def OAI.BinPackingGap.GraphPackingJobs.endpointWork line 386
  48. def OAI.BinPackingGap.GraphPackingJobs.powerWork line 387
  49. def OAI.BinPackingGap.GraphPackingJobs.loadEndpoint line 389
  50. def OAI.BinPackingGap.GraphPackingJobs.loadedOther line 393
  51. theorem OAI.BinPackingGap.GraphPackingJobs.loaded_left line 396
  52. theorem OAI.BinPackingGap.GraphPackingJobs.loaded_right line 400
  53. theorem OAI.BinPackingGap.GraphPackingJobs.inputs_width line 404
  54. theorem OAI.BinPackingGap.GraphPackingJobs.loadEndpoint_width line 410
  55. theorem OAI.BinPackingGap.GraphPackingJobs.loadedOther_width line 422
  56. theorem OAI.BinPackingGap.GraphPackingJobs.loaded_setup line 429
  57. theorem OAI.BinPackingGap.GraphPackingJobs.loaded_helper_zero line 434
  58. def OAI.BinPackingGap.GraphPackingJobs.completedInputs line 441
  59. theorem OAI.BinPackingGap.GraphPackingJobs.completedInputs_width line 445
  60. def OAI.BinPackingGap.GraphPackingJobs.clearedOther line 453
  61. theorem OAI.BinPackingGap.GraphPackingJobs.clearedOther_eq line 458
  62. theorem OAI.BinPackingGap.GraphPackingJobs.clearedInputs_eq line 467
  63. def OAI.BinPackingGap.GraphPackingStockBounds.inventory line 483
  64. def OAI.BinPackingGap.GraphPackingStockBounds.stockCoefficient line 487
  65. def OAI.BinPackingGap.GraphPackingStockBounds.stockPolynomial line 490
  66. theorem OAI.BinPackingGap.GraphPackingStockBounds.stockPolynomial_eval line 493
  67. theorem OAI.BinPackingGap.GraphPackingStockBounds.binCount_le line 497
  68. theorem OAI.BinPackingGap.GraphPackingStockBounds.globalStock_le line 504
  69. theorem OAI.BinPackingGap.GraphPackingStockBounds.flagStock_le line 515
  70. theorem OAI.BinPackingGap.GraphPackingStockBounds.globalStock_le_polynomial line 526
  71. theorem OAI.BinPackingGap.GraphPackingStockBounds.flagStock_le_polynomial line 533
  72. def OAI.BinPackingGap.GraphPackingStockBounds.setupCoefficient line 539
  73. def OAI.BinPackingGap.GraphPackingStockBounds.widthCoefficient line 544
  74. def OAI.BinPackingGap.GraphPackingStockBounds.widthPolynomial line 549
  75. theorem OAI.BinPackingGap.GraphPackingStockBounds.widthPolynomial_eval line 552
  76. theorem OAI.BinPackingGap.GraphPackingStockBounds.setupPolynomial_le line 556
  77. theorem OAI.BinPackingGap.GraphPackingStockBounds.preparationPolynomial_le line 572
  78. theorem OAI.BinPackingGap.GraphPackingStockBounds.preparationWidth_le line 584
  79. theorem OAI.BinPackingGap.GraphPackingStockBounds.values_width line 589
  80. theorem OAI.BinPackingGap.GraphPackingStockBounds.values_size_le line 610
  81. theorem OAI.BinPackingGap.GraphPackingStockBounds.values_size_le_polynomial line 616
  82. theorem OAI.BinPackingGap.GraphPackingStockBounds.preparedOther_size_le line 623
  83. theorem OAI.BinPackingGap.GraphPackingStockBounds.preparedOther_size_le_polynomial line 630
  84. def OAI.BinPackingGap.GraphPackingJobs.repeatInputs line 648
  85. def OAI.BinPackingGap.GraphPackingJobs.repeatFinalInputs line 651
  86. def OAI.BinPackingGap.GraphPackingJobs.edgeWord line 654
  87. theorem OAI.BinPackingGap.GraphPackingJobs.repeatInputs_repetition line 661
  88. theorem OAI.BinPackingGap.GraphPackingJobs.repeatInputs_eq_values line 665
  89. theorem OAI.BinPackingGap.GraphPackingJobs.repeatInputs_width line 672
  90. theorem OAI.BinPackingGap.GraphPackingJobs.repeatFinalInputs_width line 681
  91. theorem OAI.BinPackingGap.GraphPackingJobs.loaded_one line 686
  92. theorem OAI.BinPackingGap.GraphPackingJobs.loaded_repetitions line 692
  93. theorem OAI.BinPackingGap.GraphPackingJobs.repeatStream_eq line 699
  94. theorem OAI.BinPackingGap.GraphPackingJobs.repeatIteration_eq line 712
  95. def OAI.BinPackingGap.GraphPackingJobs.edgeFields line 733
  96. def OAI.BinPackingGap.GraphPackingJobs.edgeWords line 736
  97. theorem OAI.BinPackingGap.GraphPackingJobs.edgeFields_nil line 740
  98. theorem OAI.BinPackingGap.GraphPackingJobs.edgeFields_cons line 743
  99. theorem OAI.BinPackingGap.GraphPackingJobs.edgeWords_nil line 750
  100. theorem OAI.BinPackingGap.GraphPackingJobs.edgeWords_cons line 753
  101. theorem OAI.BinPackingGap.GraphPackingJobs.listBits_map line 758
  102. theorem OAI.BinPackingGap.GraphPackingJobs.edgeFields_finRange line 765
  103. theorem OAI.BinPackingGap.GraphPackingJobs.edgeWords_finRange line 780
  104. theorem OAI.BinPackingGap.GraphPackingJobs.finRange_add_map line 789
  105. theorem OAI.BinPackingGap.GraphPackingJobs.finRange_val_map line 799
  106. theorem OAI.BinPackingGap.GraphPackingJobs.contiguous_finRange line 803
  107. theorem OAI.BinPackingGap.GraphPackingJobs.contiguous_cons line 807