OAI/Computability/BinPacking/Machines/PackingPoolMachine.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.BinPackingGap.MachineFieldTemplate.Token line 14
  2. def OAI.BinPackingGap.MachineFieldTemplate.tokenOutput line 21
  3. def OAI.BinPackingGap.MachineFieldTemplate.templateOutput line 25
  4. def OAI.BinPackingGap.MachineFieldTemplate.tokenSteps line 28
  5. def OAI.BinPackingGap.MachineFieldTemplate.workSteps line 32
  6. def OAI.BinPackingGap.MachineFieldTemplate.templateSteps line 35
  7. def OAI.BinPackingGap.MachineFieldTemplate.copiedLength line 38
  8. inductive OAI.BinPackingGap.MachineFieldTemplate.Label line 41
  9. abbrev OAI.BinPackingGap.MachineFieldTemplate.State line 49
  10. abbrev OAI.BinPackingGap.MachineFieldTemplate.Alphabet line 50
  11. def OAI.BinPackingGap.MachineFieldTemplate.reset line 52
  12. theorem OAI.BinPackingGap.MachineFieldTemplate.reset_reset line 54
  13. def OAI.BinPackingGap.MachineFieldTemplate.startAt line 56
  14. def OAI.BinPackingGap.MachineFieldTemplate.jump line 59
  15. def OAI.BinPackingGap.MachineFieldTemplate.identityEmit line 64
  16. def OAI.BinPackingGap.MachineFieldTemplate.instruction line 66
  17. def OAI.BinPackingGap.MachineFieldTemplate.program line 85
  18. def OAI.BinPackingGap.MachineFieldTemplate.outputTapes line 92
  19. theorem OAI.BinPackingGap.MachineFieldTemplate.outputTapes_self line 95
  20. theorem OAI.BinPackingGap.MachineFieldTemplate.outputTapes_output line 98
  21. theorem OAI.BinPackingGap.MachineFieldTemplate.outputTapes_other line 101
  22. theorem OAI.BinPackingGap.MachineFieldTemplate.outputTapes_append line 105
  23. theorem OAI.BinPackingGap.MachineFieldTemplate.fieldValues_outputTapes line 110
  24. theorem OAI.BinPackingGap.MachineFieldTemplate.identity_output line 116
  25. theorem OAI.BinPackingGap.MachineFieldTemplate.chain line 122
  26. theorem OAI.BinPackingGap.MachineFieldTemplate.doneStep line 138
  27. theorem OAI.BinPackingGap.MachineFieldTemplate.literalStep line 145
  28. theorem OAI.BinPackingGap.MachineFieldTemplate.copySetupStep line 156
  29. theorem OAI.BinPackingGap.MachineFieldTemplate.copyTrace line 166
  30. theorem OAI.BinPackingGap.MachineFieldTemplate.tokenTrace line 189
  31. theorem OAI.BinPackingGap.MachineFieldTemplate.suffixTrace line 206
  32. theorem OAI.BinPackingGap.MachineFieldTemplate.phaseTrace line 250
  33. theorem OAI.BinPackingGap.MachineFieldTemplate.programTrace line 262
  34. theorem OAI.BinPackingGap.MachineFieldTemplate.templateSteps_le line 274
  35. def OAI.BinPackingGap.MachineFieldTemplate.phaseInTime line 287
  36. def OAI.BinPackingGap.PackingOutputEmission.itemTokens line 312
  37. def OAI.BinPackingGap.PackingOutputEmission.headerTokens line 314
  38. def OAI.BinPackingGap.PackingOutputEmission.terminatorTokens line 316
  39. theorem OAI.BinPackingGap.PackingOutputEmission.itemTokens_length line 318
  40. theorem OAI.BinPackingGap.PackingOutputEmission.headerTokens_length line 320
  41. theorem OAI.BinPackingGap.PackingOutputEmission.terminatorTokens_length line 322
  42. theorem OAI.BinPackingGap.PackingOutputEmission.item_template_output line 324
  43. theorem OAI.BinPackingGap.PackingOutputEmission.item_template_steps line 328
  44. theorem OAI.BinPackingGap.PackingOutputEmission.item_copied_length line 333
  45. theorem OAI.BinPackingGap.PackingOutputEmission.header_template_output line 337
  46. theorem OAI.BinPackingGap.PackingOutputEmission.header_template_steps line 341
  47. theorem OAI.BinPackingGap.PackingOutputEmission.terminator_template_output line 345
  48. theorem OAI.BinPackingGap.PackingOutputEmission.terminator_template_steps line 349
  49. theorem OAI.BinPackingGap.PackingOutputEmission.item_output_eq_binary_cons line 353
  50. def OAI.BinPackingGap.PackingOutputEmission.itemProgram line 362
  51. def OAI.BinPackingGap.PackingOutputEmission.headerProgram line 366
  52. def OAI.BinPackingGap.PackingOutputEmission.terminatorProgram line 370
  53. theorem OAI.BinPackingGap.PackingOutputEmission.itemPhaseTrace line 374
  54. def OAI.BinPackingGap.PackingOutputEmission.itemPhaseInTime line 391
  55. def OAI.BinPackingGap.PackingOutputEmission.itemPhaseInTimeCoarse line 409
  56. theorem OAI.BinPackingGap.PackingOutputEmission.itemProgramTrace line 428
  57. theorem OAI.BinPackingGap.PackingOutputEmission.item_fields_preserved line 442
  58. theorem OAI.BinPackingGap.PackingOutputEmission.item_scratch_restored line 448
  59. theorem OAI.BinPackingGap.PackingOutputEmission.item_accumulator line 453
  60. theorem OAI.BinPackingGap.PackingOutputEmission.framed_item_steps line 458
  61. theorem OAI.BinPackingGap.PackingOutputEmission.headerPhaseTrace line 465
  62. theorem OAI.BinPackingGap.PackingOutputEmission.headerProgramTrace line 480
  63. theorem OAI.BinPackingGap.PackingOutputEmission.terminatorPhaseTrace line 493
  64. theorem OAI.BinPackingGap.PackingOutputEmission.terminatorProgramTrace line 506
  65. inductive OAI.BinPackingGap.PackingPoolMachine.Label line 526
  66. def OAI.BinPackingGap.PackingPoolMachine.finish line 534
  67. def OAI.BinPackingGap.PackingPoolMachine.instruction line 539
  68. def OAI.BinPackingGap.PackingPoolMachine.repeatWord line 549
  69. theorem OAI.BinPackingGap.PackingPoolMachine.repeatWord_zero line 553
  70. theorem OAI.BinPackingGap.PackingPoolMachine.repeatWord_succ line 555
  71. theorem OAI.BinPackingGap.PackingPoolMachine.repeatWord_length line 558
  72. def OAI.BinPackingGap.PackingPoolMachine.record line 564
  73. def OAI.BinPackingGap.PackingPoolMachine.bodySteps line 567
  74. def OAI.BinPackingGap.PackingPoolMachine.steps line 570
  75. theorem OAI.BinPackingGap.PackingPoolMachine.joinTrace line 573
  76. theorem OAI.BinPackingGap.PackingPoolMachine.poolTrace line 577
  77. def OAI.BinPackingGap.PackingPoolMachine.poolInTime line 662