OAI/Computability/BinPacking/Machines/PackingCountedProgram.lean

GitHub source file

116 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.BinPackingGap.GraphFieldMachine.Field line 17
  2. instance OAI.BinPackingGap.GraphFieldMachine.(instance at line 22) line 22
  3. def OAI.BinPackingGap.GraphFieldMachine.keepsName line 26
  4. def OAI.BinPackingGap.GraphFieldMachine.emit line 32
  5. def OAI.BinPackingGap.GraphFieldMachine.scanOutput line 42
  6. theorem OAI.BinPackingGap.GraphFieldMachine.scanOutput_nil line 45
  7. theorem OAI.BinPackingGap.GraphFieldMachine.scanOutput_cons line 48
  8. theorem OAI.BinPackingGap.GraphFieldMachine.scanOutput_done line 52
  9. theorem OAI.BinPackingGap.GraphFieldMachine.scanOutput_frame line 59
  10. theorem OAI.BinPackingGap.GraphFieldMachine.scanOutput_natBits line 71
  11. theorem OAI.BinPackingGap.GraphFieldMachine.scanOutput_pairBits line 77
  12. theorem OAI.BinPackingGap.GraphFieldMachine.scanOutput_vertices line 84
  13. theorem OAI.BinPackingGap.GraphFieldMachine.scanOutput_endpoints line 94
  14. def OAI.BinPackingGap.GraphFieldMachine.fieldsOutput line 106
  15. def OAI.BinPackingGap.GraphFieldMachine.fieldBits line 110
  16. theorem OAI.BinPackingGap.GraphFieldMachine.thresholdBits line 113
  17. theorem OAI.BinPackingGap.GraphFieldMachine.endpointsBits line 116
  18. theorem OAI.BinPackingGap.GraphFieldMachine.output_graphFields line 120
  19. theorem OAI.BinPackingGap.GraphFieldMachine.output_graphBits line 128
  20. theorem OAI.BinPackingGap.GraphFieldMachine.emit_length_le line 132
  21. theorem OAI.BinPackingGap.GraphFieldMachine.scanOutput_length_le line 141
  22. theorem OAI.BinPackingGap.GraphFieldMachine.fieldBits_length_le line 151
  23. abbrev OAI.BinPackingGap.GraphFieldMachine.State line 158
  24. def OAI.BinPackingGap.GraphFieldMachine.clean line 160
  25. def OAI.BinPackingGap.GraphFieldMachine.fieldCopyInTime line 162
  26. inductive OAI.BinPackingGap.GraphFieldMachine.Label line 192
  27. def OAI.BinPackingGap.GraphFieldMachine.instruction line 197
  28. def OAI.BinPackingGap.GraphFieldMachine.resultTapes line 208
  29. def OAI.BinPackingGap.GraphFieldMachine.steps line 212
  30. theorem OAI.BinPackingGap.GraphFieldMachine.steps_le line 215
  31. theorem OAI.BinPackingGap.GraphFieldMachine.extractTrace line 221
  32. def OAI.BinPackingGap.GraphFieldMachine.extractInTime line 278
  33. inductive OAI.BinPackingGap.GraphTokenMachine.Field line 305
  34. instance OAI.BinPackingGap.GraphTokenMachine.(instance at line 310) line 310
  35. def OAI.BinPackingGap.GraphTokenMachine.emit line 314
  36. def OAI.BinPackingGap.GraphTokenMachine.scanOutput line 319
  37. theorem OAI.BinPackingGap.GraphTokenMachine.scanOutput_nil line 322
  38. theorem OAI.BinPackingGap.GraphTokenMachine.scanOutput_cons line 325
  39. theorem OAI.BinPackingGap.GraphTokenMachine.scanOutput_done line 329
  40. theorem OAI.BinPackingGap.GraphTokenMachine.scanOutput_frame line 336
  41. theorem OAI.BinPackingGap.GraphTokenMachine.scanOutput_natBits line 347
  42. theorem OAI.BinPackingGap.GraphTokenMachine.scanOutput_pairBits line 352
  43. theorem OAI.BinPackingGap.GraphTokenMachine.scanOutput_vertices line 357
  44. theorem OAI.BinPackingGap.GraphTokenMachine.scanOutput_endpoints line 368
  45. def OAI.BinPackingGap.GraphTokenMachine.fieldsCount line 380
  46. def OAI.BinPackingGap.GraphTokenMachine.count line 384
  47. def OAI.BinPackingGap.GraphTokenMachine.tokenBits line 388
  48. theorem OAI.BinPackingGap.GraphTokenMachine.count_vertex line 391
  49. theorem OAI.BinPackingGap.GraphTokenMachine.count_edge line 394
  50. theorem OAI.BinPackingGap.GraphTokenMachine.tokenBits_length line 397
  51. theorem OAI.BinPackingGap.GraphTokenMachine.tokenBits_reverse line 400
  52. theorem OAI.BinPackingGap.GraphTokenMachine.output_graphFields line 403
  53. theorem OAI.BinPackingGap.GraphTokenMachine.fieldsCount_fields line 411
  54. theorem OAI.BinPackingGap.GraphTokenMachine.output_graphBits line 415
  55. theorem OAI.BinPackingGap.GraphTokenMachine.count_le_bits line 420
  56. theorem OAI.BinPackingGap.GraphTokenMachine.emit_length_le line 426
  57. abbrev OAI.BinPackingGap.GraphTokenMachine.State line 432
  58. def OAI.BinPackingGap.GraphTokenMachine.clean line 434
  59. inductive OAI.BinPackingGap.GraphTokenMachine.Label line 436
  60. def OAI.BinPackingGap.GraphTokenMachine.instruction line 442
  61. def OAI.BinPackingGap.GraphTokenMachine.resultTapes line 451
  62. theorem OAI.BinPackingGap.GraphTokenMachine.resultTapes_other line 455
  63. theorem OAI.BinPackingGap.GraphTokenMachine.resultTapes_destination line 459
  64. theorem OAI.BinPackingGap.GraphTokenMachine.tokensTrace line 464
  65. def OAI.BinPackingGap.GraphTokenMachine.tokensInTime line 488
  66. theorem OAI.BinPackingGap.GraphTokenMachine.resultTapes_counter line 504
  67. def OAI.BinPackingGap.GraphTokenMachine.counterInTime line 511
  68. abbrev OAI.BinPackingGap.GraphPreparationMachine.State line 535
  69. inductive OAI.BinPackingGap.GraphPreparationMachine.Label line 537
  70. def OAI.BinPackingGap.GraphPreparationMachine.fieldIndices line 544
  71. def OAI.BinPackingGap.GraphPreparationMachine.tokenIndices line 548
  72. def OAI.BinPackingGap.GraphPreparationMachine.fieldSlots line 554
  73. def OAI.BinPackingGap.GraphPreparationMachine.tokenSlots line 557
  74. theorem OAI.BinPackingGap.GraphPreparationMachine.fieldSlots_zero line 561
  75. theorem OAI.BinPackingGap.GraphPreparationMachine.fieldSlots_one line 565
  76. theorem OAI.BinPackingGap.GraphPreparationMachine.fieldSlots_two line 569
  77. theorem OAI.BinPackingGap.GraphPreparationMachine.fieldSlots_three line 573
  78. theorem OAI.BinPackingGap.GraphPreparationMachine.tokenSlots_zero line 577
  79. theorem OAI.BinPackingGap.GraphPreparationMachine.tokenSlots_one line 581
  80. theorem OAI.BinPackingGap.GraphPreparationMachine.tokenSlots_two line 585
  81. def OAI.BinPackingGap.GraphPreparationMachine.instruction line 588
  82. def OAI.BinPackingGap.GraphPreparationMachine.preparedTapes line 599
  83. def OAI.BinPackingGap.GraphPreparationMachine.steps line 607
  84. theorem OAI.BinPackingGap.GraphPreparationMachine.preparedTapes_register line 611
  85. theorem OAI.BinPackingGap.GraphPreparationMachine.preparedTapes_other line 624
  86. theorem OAI.BinPackingGap.GraphPreparationMachine.steps_le line 631
  87. theorem OAI.BinPackingGap.GraphPreparationMachine.joinTrace line 638
  88. theorem OAI.BinPackingGap.GraphPreparationMachine.preparationTrace line 642
  89. def OAI.BinPackingGap.GraphPreparationMachine.preparationInTime line 688
  90. inductive OAI.BinPackingGap.PackingMachineBlocks.State line 712
  91. def OAI.BinPackingGap.PackingMachineBlocks.graphControl line 718
  92. def OAI.BinPackingGap.PackingMachineBlocks.arithmeticControl line 725
  93. def OAI.BinPackingGap.PackingMachineBlocks.emissionControl line 732
  94. def OAI.BinPackingGap.PackingMachineBlocks.invoke line 741
  95. theorem OAI.BinPackingGap.PackingMachineBlocks.invokeExec line 748
  96. theorem OAI.BinPackingGap.PackingMachineBlocks.invokeExecInTime line 767
  97. def OAI.BinPackingGap.PackingMachineBlocks.prepareGraph line 781
  98. theorem OAI.BinPackingGap.PackingMachineBlocks.prepareGraph_exec line 785
  99. theorem OAI.BinPackingGap.PackingMachineBlocks.prepareGraph_cost line 796
  100. def OAI.BinPackingGap.PackingMachineBlocks.emitPool line 801
  101. theorem OAI.BinPackingGap.PackingMachineBlocks.emitPool_exec line 806
  102. def OAI.BinPackingGap.PackingArithmeticProgram.code line 842
  103. theorem OAI.BinPackingGap.PackingArithmeticProgram.exec line 847
  104. theorem OAI.BinPackingGap.PackingArithmeticProgram.exec_in_time line 857
  105. def OAI.BinPackingGap.PackingCountedProgram.guardState line 875
  106. def OAI.BinPackingGap.PackingCountedProgram.guard line 878
  107. def OAI.BinPackingGap.PackingCountedProgram.more line 881
  108. def OAI.BinPackingGap.PackingCountedProgram.loop line 885
  109. def OAI.BinPackingGap.PackingCountedProgram.counterTapes line 888
  110. theorem OAI.BinPackingGap.PackingCountedProgram.guard_succ line 891
  111. theorem OAI.BinPackingGap.PackingCountedProgram.guard_zero line 896
  112. def OAI.BinPackingGap.PackingCountedProgram.totalBudget line 901
  113. theorem OAI.BinPackingGap.PackingCountedProgram.totalBudget_zero line 904
  114. theorem OAI.BinPackingGap.PackingCountedProgram.totalBudget_succ line 907
  115. theorem OAI.BinPackingGap.PackingCountedProgram.exec line 912
  116. theorem OAI.BinPackingGap.PackingCountedProgram.totalBudget_le line 949