OAI/Computability/BinPacking/Search/SearchStageMachines.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingGap.SearchInitialEmitMachine.Tape line 18
  2. abbrev OAI.BinPackingGap.SearchInitialEmitMachine.Alphabet line 19
  3. abbrev OAI.BinPackingGap.SearchInitialEmitMachine.Flags line 20
  4. abbrev OAI.BinPackingGap.SearchInitialEmitMachine.Register line 21
  5. inductive OAI.BinPackingGap.SearchInitialEmitMachine.Label line 23
  6. def OAI.BinPackingGap.SearchInitialEmitMachine.clean line 28
  7. def OAI.BinPackingGap.SearchInitialEmitMachine.mulTape line 30
  8. def OAI.BinPackingGap.SearchInitialEmitMachine.mulSlots line 37
  9. theorem OAI.BinPackingGap.SearchInitialEmitMachine.mulSlots_apply line 40
  10. def OAI.BinPackingGap.SearchInitialEmitMachine.dispatch line 44
  11. def OAI.BinPackingGap.SearchInitialEmitMachine.finishLabel line 46
  12. def OAI.BinPackingGap.SearchInitialEmitMachine.header line 49
  13. def OAI.BinPackingGap.SearchInitialEmitMachine.code line 55
  14. def OAI.BinPackingGap.SearchInitialEmitMachine.program line 93
  15. abbrev OAI.BinPackingGap.SearchInitialEmitMachine.machine line 100
  16. def OAI.BinPackingGap.SearchInitialEmitMachine.tapes line 102
  17. def OAI.BinPackingGap.SearchInitialEmitMachine.cfg line 111
  18. theorem OAI.BinPackingGap.SearchInitialEmitMachine.tapes_input line 115
  19. theorem OAI.BinPackingGap.SearchInitialEmitMachine.update_input line 118
  20. theorem OAI.BinPackingGap.SearchInitialEmitMachine.tapes_output line 123
  21. theorem OAI.BinPackingGap.SearchInitialEmitMachine.update_output line 126
  22. theorem OAI.BinPackingGap.SearchInitialEmitMachine.tapes_left line 131
  23. theorem OAI.BinPackingGap.SearchInitialEmitMachine.update_left line 134
  24. theorem OAI.BinPackingGap.SearchInitialEmitMachine.tapes_right line 139
  25. theorem OAI.BinPackingGap.SearchInitialEmitMachine.update_right line 142
  26. theorem OAI.BinPackingGap.SearchInitialEmitMachine.tapes_scratch line 147
  27. theorem OAI.BinPackingGap.SearchInitialEmitMachine.update_scratch line 150
  28. theorem OAI.BinPackingGap.SearchInitialEmitMachine.tapes_fixed line 155
  29. theorem OAI.BinPackingGap.SearchInitialEmitMachine.update_fixed line 158
  30. theorem OAI.BinPackingGap.SearchInitialEmitMachine.tapes_counter line 163
  31. theorem OAI.BinPackingGap.SearchInitialEmitMachine.update_counter line 166
  32. def OAI.BinPackingGap.SearchInitialEmitMachine.oneStep line 171
  33. def OAI.BinPackingGap.SearchInitialEmitMachine.join line 180
  34. def OAI.BinPackingGap.SearchInitialEmitMachine.enlarge line 188
  35. def OAI.BinPackingGap.SearchInitialEmitMachine.observed line 195
  36. theorem OAI.BinPackingGap.SearchInitialEmitMachine.observed_zero line 197
  37. theorem OAI.BinPackingGap.SearchInitialEmitMachine.observed_succ line 199
  38. theorem OAI.BinPackingGap.SearchInitialEmitMachine.observed_true line 202
  39. def OAI.BinPackingGap.SearchInitialEmitMachine.initialFlags line 205
  40. def OAI.BinPackingGap.SearchInitialEmitMachine.fixedWord line 207
  41. theorem OAI.BinPackingGap.SearchInitialEmitMachine.fixedWord_zero line 209
  42. theorem OAI.BinPackingGap.SearchInitialEmitMachine.fixedWord_succ line 211
  43. theorem OAI.BinPackingGap.SearchInitialEmitMachine.startStep line 214
  44. theorem OAI.BinPackingGap.SearchInitialEmitMachine.countStep_true line 221
  45. theorem OAI.BinPackingGap.SearchInitialEmitMachine.countStep_false line 230
  46. theorem OAI.BinPackingGap.SearchInitialEmitMachine.countTrace line 239
  47. def OAI.BinPackingGap.SearchInitialEmitMachine.countInTime line 258
  48. theorem OAI.BinPackingGap.SearchInitialEmitMachine.fixedStep_true line 269
  49. theorem OAI.BinPackingGap.SearchInitialEmitMachine.fixedStep_zero line 278
  50. theorem OAI.BinPackingGap.SearchInitialEmitMachine.fixedTrace line 286
  51. def OAI.BinPackingGap.SearchInitialEmitMachine.fixedInTime line 301
  52. def OAI.BinPackingGap.SearchInitialEmitMachine.selectedFixed line 310
  53. def OAI.BinPackingGap.SearchInitialEmitMachine.residualFixed line 313
  54. def OAI.BinPackingGap.SearchInitialEmitMachine.prepareInTime line 316
  55. def OAI.BinPackingGap.SearchInitialEmitMachine.prependRawInTime line 340
  56. theorem OAI.BinPackingGap.SearchInitialEmitMachine.headerStep line 373
  57. theorem OAI.BinPackingGap.SearchInitialEmitMachine.zeroFuelStep line 382
  58. def OAI.BinPackingGap.SearchInitialEmitMachine.fuelValue line 389
  59. def OAI.BinPackingGap.SearchInitialEmitMachine.fuelTime line 391
  60. def OAI.BinPackingGap.SearchInitialEmitMachine.fuelInTime line 394
  61. def OAI.BinPackingGap.SearchInitialEmitMachine.bodyWord line 421
  62. def OAI.BinPackingGap.SearchInitialEmitMachine.outputWord line 424
  63. def OAI.BinPackingGap.SearchInitialEmitMachine.finishTapes line 427
  64. def OAI.BinPackingGap.SearchInitialEmitMachine.rawSteps line 431
  65. def OAI.BinPackingGap.SearchInitialEmitMachine.emitInTime line 434
  66. theorem OAI.BinPackingGap.SearchInitialEmitMachine.bodyWord_eq line 450
  67. theorem OAI.BinPackingGap.SearchInitialEmitMachine.outputWord_eq line 469
  68. theorem OAI.BinPackingGap.SearchInitialEmitMachine.init_eq line 475
  69. def OAI.BinPackingGap.SearchInitialEmitMachine.rawTime line 483
  70. theorem OAI.BinPackingGap.SearchInitialEmitMachine.rawSteps_le line 485
  71. def OAI.BinPackingGap.SearchInitialEmitMachine.rawRun line 506
  72. def OAI.BinPackingGap.SearchInitialEmitMachine.cleanupTapes line 521
  73. theorem OAI.BinPackingGap.SearchInitialEmitMachine.cleanup_complete line 523
  74. def OAI.BinPackingGap.SearchInitialEmitMachine.computation line 526
  75. theorem OAI.BinPackingGap.SearchInitialEmitMachine.finiteAlphabet line 532
  76. def OAI.BinPackingGap.SearchInitializeMachine.shapeComputation line 544
  77. theorem OAI.BinPackingGap.SearchInitializeMachine.shapeFinite line 559
  78. def OAI.BinPackingGap.SearchInitializeMachine.composed line 562
  79. def OAI.BinPackingGap.SearchInitializeMachine.computation line 572
  80. theorem OAI.BinPackingGap.SearchInitializeMachine.finiteAlphabet line 583
  81. def OAI.BinPackingGap.SearchStageMachines.stages line 597