OAI/Computability/BinPacking/Machines/PackingJobLoop.lean

GitHub source file

102 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.NatExpressionCompiler.substitute line 15
  2. theorem OAI.BinPackingGap.NatExpressionCompiler.eval_substitute line 22
  3. def OAI.BinPackingGap.NatExpressionCompiler.rename line 26
  4. theorem OAI.BinPackingGap.NatExpressionCompiler.eval_rename line 28
  5. inductive OAI.BinPackingGap.PackingItemExpression.Variable line 39
  6. instance OAI.BinPackingGap.PackingItemExpression.(instance at line 43) line 43
  7. def OAI.BinPackingGap.PackingItemExpression.coordinateVariable line 47
  8. def OAI.BinPackingGap.PackingItemExpression.scalarReplacement line 53
  9. def OAI.BinPackingGap.PackingItemExpression.numerator line 61
  10. def OAI.BinPackingGap.PackingItemExpression.denominator line 65
  11. def OAI.BinPackingGap.PackingItemExpression.values line 69
  12. theorem OAI.BinPackingGap.PackingItemExpression.values_coordinateVariable line 77
  13. def OAI.BinPackingGap.PackingItemExpression.itemCoordinate line 82
  14. theorem OAI.BinPackingGap.PackingItemExpression.replacement_values line 86
  15. theorem OAI.BinPackingGap.PackingItemExpression.eval_item_numerator line 102
  16. theorem OAI.BinPackingGap.PackingItemExpression.eval_item_denominator line 108
  17. def OAI.BinPackingGap.PackingItemBlockMachine.code line 123
  18. def OAI.BinPackingGap.PackingItemBlockMachine.record line 131
  19. def OAI.BinPackingGap.PackingItemBlockMachine.outputTapes line 134
  20. def OAI.BinPackingGap.PackingItemBlockMachine.widthPolynomial line 137
  21. theorem OAI.BinPackingGap.PackingItemBlockMachine.widthPolynomial_eval line 142
  22. def OAI.BinPackingGap.PackingItemBlockMachine.timePolynomial line 147
  23. theorem OAI.BinPackingGap.PackingItemBlockMachine.timePolynomial_eval line 153
  24. theorem OAI.BinPackingGap.PackingItemBlockMachine.consumed_width line 161
  25. theorem OAI.BinPackingGap.PackingItemBlockMachine.exec line 171
  26. theorem OAI.BinPackingGap.PackingItemBlockMachine.exec_item line 249
  27. def OAI.BinPackingGap.PackingChunkMachine.code line 283
  28. def OAI.BinPackingGap.PackingChunkMachine.records line 292
  29. theorem OAI.BinPackingGap.PackingChunkMachine.records_nil line 298
  30. theorem OAI.BinPackingGap.PackingChunkMachine.records_cons line 302
  31. def OAI.BinPackingGap.PackingChunkMachine.timePolynomial line 309
  32. theorem OAI.BinPackingGap.PackingChunkMachine.timePolynomial_eq_sum line 317
  33. theorem OAI.BinPackingGap.PackingChunkMachine.outputTapes_nil line 332
  34. theorem OAI.BinPackingGap.PackingChunkMachine.outputTapes_append line 336
  35. theorem OAI.BinPackingGap.PackingChunkMachine.shape_after_output line 342
  36. theorem OAI.BinPackingGap.PackingChunkMachine.exec_one line 351
  37. theorem OAI.BinPackingGap.PackingChunkMachine.exec line 367
  38. theorem OAI.BinPackingGap.PackingChunkMachine.final_output line 419
  39. theorem OAI.BinPackingGap.PackingChunkMachine.final_frame line 423
  40. def OAI.BinPackingGap.PackingDescriptorExpression.instantiate line 434
  41. theorem OAI.BinPackingGap.PackingDescriptorExpression.vertexDescriptors_instantiate line 437
  42. theorem OAI.BinPackingGap.PackingDescriptorExpression.jobDescriptors_instantiate line 466
  43. def OAI.BinPackingGap.PackingDescriptorExpression.numerator line 470
  44. theorem OAI.BinPackingGap.PackingDescriptorExpression.numerator_instantiate line 475
  45. def OAI.BinPackingGap.PackingDescriptorExpression.values line 479
  46. theorem OAI.BinPackingGap.PackingDescriptorExpression.coordinate_values line 488
  47. theorem OAI.BinPackingGap.PackingDescriptorExpression.replacement_values line 494
  48. theorem OAI.BinPackingGap.PackingDescriptorExpression.eval_numerator line 514
  49. theorem OAI.BinPackingGap.PackingDescriptorExpression.eval_denominator line 522
  50. def OAI.BinPackingGap.PackingDescriptorExpression.rawRecord line 526
  51. def OAI.BinPackingGap.PackingDescriptorExpression.rawRecords line 529
  52. theorem OAI.BinPackingGap.PackingDescriptorExpression.record_eq line 531
  53. theorem OAI.BinPackingGap.PackingDescriptorExpression.chunk_records line 538
  54. theorem OAI.BinPackingGap.PackingDescriptorExpression.rawInstanceBits_eq line 545
  55. theorem OAI.BinPackingGap.PackingDescriptorExpression.reductionOutputBits_eq line 555
  56. def OAI.BinPackingGap.PackingVertexLoop.vertexInput line 568
  57. theorem OAI.BinPackingGap.PackingVertexLoop.vertexInput_power line 571
  58. theorem OAI.BinPackingGap.PackingVertexLoop.vertexInput_other line 575
  59. theorem OAI.BinPackingGap.PackingVertexLoop.vertexInput_update line 579
  60. theorem OAI.BinPackingGap.PackingVertexLoop.pow3_size_le line 588
  61. def OAI.BinPackingGap.PackingVertexLoop.aggregateWidth line 594
  62. theorem OAI.BinPackingGap.PackingVertexLoop.vertexInput_size_le line 597
  63. def OAI.BinPackingGap.PackingVertexLoop.stream line 613
  64. theorem OAI.BinPackingGap.PackingVertexLoop.stream_zero line 621
  65. theorem OAI.BinPackingGap.PackingVertexLoop.stream_succ line 625
  66. def OAI.BinPackingGap.PackingJobBody.nextInput line 643
  67. theorem OAI.BinPackingGap.PackingJobBody.nextInput_repetition line 646
  68. theorem OAI.BinPackingGap.PackingJobBody.nextInput_power line 651
  69. def OAI.BinPackingGap.PackingJobBody.pairRecords line 656
  70. def OAI.BinPackingGap.PackingJobBody.body line 663
  71. def OAI.BinPackingGap.PackingJobBody.bodyTimePolynomial line 676
  72. theorem OAI.BinPackingGap.PackingJobBody.bodyTimePolynomial_eval line 684
  73. theorem OAI.BinPackingGap.PackingJobBody.update_size_le line 693
  74. theorem OAI.BinPackingGap.PackingJobBody.layout_external_update line 702
  75. theorem OAI.BinPackingGap.PackingJobBody.layout_output line 711
  76. theorem OAI.BinPackingGap.PackingJobBody.chunk_exec line 719
  77. theorem OAI.BinPackingGap.PackingJobBody.body_exec line 740
  78. theorem OAI.BinPackingGap.PackingVertexRecords.finRange_cons line 811
  79. theorem OAI.BinPackingGap.PackingVertexRecords.stream_eq_finRange line 816
  80. theorem OAI.BinPackingGap.PackingVertexRecords.values_vertexInput line 834
  81. theorem OAI.BinPackingGap.PackingVertexRecords.rawRecords_flatMap line 843
  82. theorem OAI.BinPackingGap.PackingVertexRecords.stream_eq_vertexStream line 848
  83. def OAI.BinPackingGap.PackingJobLoop.iterationInput line 870
  84. theorem OAI.BinPackingGap.PackingJobLoop.iterationInput_zero line 876
  85. theorem OAI.BinPackingGap.PackingJobLoop.iterationInput_rep line 879
  86. theorem OAI.BinPackingGap.PackingJobLoop.iterationInput_power line 884
  87. theorem OAI.BinPackingGap.PackingJobLoop.iterationInput_other line 891
  88. theorem OAI.BinPackingGap.PackingJobLoop.iterationInput_succ line 896
  89. theorem OAI.BinPackingGap.PackingJobLoop.nextInput_iterationInput line 914
  90. def OAI.BinPackingGap.PackingJobLoop.aggregateWidth line 931
  91. theorem OAI.BinPackingGap.PackingJobLoop.size_le_succ line 934
  92. theorem OAI.BinPackingGap.PackingJobLoop.iterationInput_size_le line 943
  93. def OAI.BinPackingGap.PackingJobLoop.stream line 977
  94. theorem OAI.BinPackingGap.PackingJobLoop.stream_zero line 984
  95. theorem OAI.BinPackingGap.PackingJobLoop.stream_succ line 988
  96. def OAI.BinPackingGap.PackingJobLoop.code line 1006
  97. theorem OAI.BinPackingGap.PackingJobLoop.layout_counter line 1015
  98. theorem OAI.BinPackingGap.PackingJobLoop.output_counter line 1024
  99. theorem OAI.BinPackingGap.PackingJobLoop.exec_bounded line 1038
  100. theorem OAI.BinPackingGap.PackingJobLoop.exec line 1113
  101. def OAI.BinPackingGap.PackingJobLoop.timePolynomial line 1144
  102. theorem OAI.BinPackingGap.PackingJobLoop.exec_polynomial line 1148