OAI/Computability/BinPacking/Search/SearchPrepareMachine.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.BinPackingGap.SearchPrepareMachine.Tape line 13
  2. abbrev OAI.BinPackingGap.SearchPrepareMachine.Tape.enumList line 17
  3. theorem OAI.BinPackingGap.SearchPrepareMachine.Tape.enumList_getElem?_ctorIdx_eq line 20
  4. theorem OAI.BinPackingGap.SearchPrepareMachine.Tape.enumList_nodup line 24
  5. instance OAI.BinPackingGap.SearchPrepareMachine.(instance at line 26) line 26
  6. inductive OAI.BinPackingGap.SearchPrepareMachine.Label line 30
  7. abbrev OAI.BinPackingGap.SearchPrepareMachine.Register line 42
  8. def OAI.BinPackingGap.SearchPrepareMachine.tapes line 44
  9. theorem OAI.BinPackingGap.SearchPrepareMachine.tapes_input line 53
  10. theorem OAI.BinPackingGap.SearchPrepareMachine.update_input line 56
  11. theorem OAI.BinPackingGap.SearchPrepareMachine.tapes_binary line 61
  12. theorem OAI.BinPackingGap.SearchPrepareMachine.update_binary line 64
  13. theorem OAI.BinPackingGap.SearchPrepareMachine.tapes_scratch line 69
  14. theorem OAI.BinPackingGap.SearchPrepareMachine.update_scratch line 72
  15. theorem OAI.BinPackingGap.SearchPrepareMachine.tapes_index line 77
  16. theorem OAI.BinPackingGap.SearchPrepareMachine.update_index line 80
  17. theorem OAI.BinPackingGap.SearchPrepareMachine.tapes_payload line 85
  18. theorem OAI.BinPackingGap.SearchPrepareMachine.update_payload line 88
  19. theorem OAI.BinPackingGap.SearchPrepareMachine.tapes_reversed line 93
  20. theorem OAI.BinPackingGap.SearchPrepareMachine.update_reversed line 96
  21. theorem OAI.BinPackingGap.SearchPrepareMachine.tapes_output line 101
  22. theorem OAI.BinPackingGap.SearchPrepareMachine.update_output line 104
  23. def OAI.BinPackingGap.SearchPrepareMachine.go line 109
  24. def OAI.BinPackingGap.SearchPrepareMachine.replacePlace line 112
  25. theorem OAI.BinPackingGap.SearchPrepareMachine.replacePlace_injective line 118
  26. def OAI.BinPackingGap.SearchPrepareMachine.copyFlag line 122
  27. def OAI.BinPackingGap.SearchPrepareMachine.copyDigit line 127
  28. def OAI.BinPackingGap.SearchPrepareMachine.code line 131
  29. def OAI.BinPackingGap.SearchPrepareMachine.program line 164
  30. abbrev OAI.BinPackingGap.SearchPrepareMachine.machine line 171
  31. def OAI.BinPackingGap.SearchPrepareMachine.cfg line 173
  32. theorem OAI.BinPackingGap.SearchPrepareMachine.oneStepTrace line 178
  33. theorem OAI.BinPackingGap.SearchPrepareMachine.actualStep line 182
  34. theorem OAI.BinPackingGap.SearchPrepareMachine.transferNext line 184
  35. theorem OAI.BinPackingGap.SearchPrepareMachine.joinTrace line 188
  36. theorem OAI.BinPackingGap.SearchPrepareMachine.saveTrace line 192
  37. theorem OAI.BinPackingGap.SearchPrepareMachine.frameSavedTrace line 202
  38. theorem OAI.BinPackingGap.SearchPrepareMachine.phaseActive line 212
  39. theorem OAI.BinPackingGap.SearchPrepareMachine.phaseInactive line 219
  40. theorem OAI.BinPackingGap.SearchPrepareMachine.convertBinsTrace line 226
  41. theorem OAI.BinPackingGap.SearchPrepareMachine.emitBinsTrace line 238
  42. theorem OAI.BinPackingGap.SearchPrepareMachine.seedIndexStep line 249
  43. theorem OAI.BinPackingGap.SearchPrepareMachine.indexStep line 256
  44. theorem OAI.BinPackingGap.SearchPrepareMachine.indexTrace line 264
  45. theorem OAI.BinPackingGap.SearchPrepareMachine.convertLabelTrace line 283
  46. theorem OAI.BinPackingGap.SearchPrepareMachine.emitLabelTrace line 295
  47. theorem OAI.BinPackingGap.SearchPrepareMachine.restoreLabelTrace line 305
  48. theorem OAI.BinPackingGap.SearchPrepareMachine.copyFlagStep line 316
  49. theorem OAI.BinPackingGap.SearchPrepareMachine.copyDigitStep line 326
  50. theorem OAI.BinPackingGap.SearchPrepareMachine.copyNameTrace line 335
  51. theorem OAI.BinPackingGap.SearchPrepareMachine.copyItemsTrace line 364
  52. theorem OAI.BinPackingGap.SearchPrepareMachine.dispatchStep line 398
  53. theorem OAI.BinPackingGap.SearchPrepareMachine.copyFixedTrace line 406
  54. theorem OAI.BinPackingGap.SearchPrepareMachine.replaceTapes_eq line 416
  55. theorem OAI.BinPackingGap.SearchPrepareMachine.replaceFixedTrace line 423
  56. theorem OAI.BinPackingGap.SearchPrepareMachine.reverseTrace line 437
  57. def OAI.BinPackingGap.SearchPrepareMachine.bodyBits line 446
  58. def OAI.BinPackingGap.SearchPrepareMachine.selectedFixed line 450
  59. def OAI.BinPackingGap.SearchPrepareMachine.queryBits line 453
  60. def OAI.BinPackingGap.SearchPrepareMachine.prefixSteps line 456
  61. theorem OAI.BinPackingGap.SearchPrepareMachine.prefixTrace line 461
  62. def OAI.BinPackingGap.SearchPrepareMachine.suffixSteps line 487
  63. theorem OAI.BinPackingGap.SearchPrepareMachine.suffixTrace line 491
  64. def OAI.BinPackingGap.SearchPrepareMachine.activeBits line 515
  65. def OAI.BinPackingGap.SearchPrepareMachine.activeSteps line 518
  66. theorem OAI.BinPackingGap.SearchPrepareMachine.activeTrace line 521
  67. def OAI.BinPackingGap.SearchPrepareMachine.initialSteps line 541
  68. theorem OAI.BinPackingGap.SearchPrepareMachine.initialTrace line 543
  69. def OAI.BinPackingGap.SearchPrepareMachine.rawTime line 550
  70. theorem OAI.BinPackingGap.SearchPrepareMachine.activeSteps_le line 552
  71. theorem OAI.BinPackingGap.SearchPrepareMachine.inactiveSteps_le line 578
  72. theorem OAI.BinPackingGap.SearchPrepareMachine.init_eq line 586
  73. theorem OAI.BinPackingGap.SearchPrepareMachine.savedFrame_eq line 593
  74. def OAI.BinPackingGap.SearchPrepareMachine.activeRun line 600
  75. def OAI.BinPackingGap.SearchPrepareMachine.inactiveRun line 633
  76. def OAI.BinPackingGap.SearchPrepareMachine.rawRun line 669
  77. def OAI.BinPackingGap.SearchPrepareMachine.cleanupTapes line 683
  78. theorem OAI.BinPackingGap.SearchPrepareMachine.cleanup_complete line 685
  79. def OAI.BinPackingGap.SearchPrepareMachine.computation line 688
  80. theorem OAI.BinPackingGap.SearchPrepareMachine.finiteAlphabet line 693