OAI/Computability/BinPacking/Search/SearchUpdateMachine.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.BinPackingGap.SearchUpdateMachine.Tape line 13
  2. abbrev OAI.BinPackingGap.SearchUpdateMachine.Tape.enumList line 17
  3. theorem OAI.BinPackingGap.SearchUpdateMachine.Tape.enumList_getElem?_ctorIdx_eq line 20
  4. theorem OAI.BinPackingGap.SearchUpdateMachine.Tape.enumList_nodup line 24
  5. instance OAI.BinPackingGap.SearchUpdateMachine.(instance at line 26) line 26
  6. inductive OAI.BinPackingGap.SearchUpdateMachine.Label line 30
  7. structure OAI.BinPackingGap.SearchUpdateMachine.Ambient line 41
  8. abbrev OAI.BinPackingGap.SearchUpdateMachine.Register line 47
  9. abbrev OAI.BinPackingGap.SearchUpdateMachine.Tapes line 48
  10. def OAI.BinPackingGap.SearchUpdateMachine.ambient line 50
  11. def OAI.BinPackingGap.SearchUpdateMachine.empty line 57
  12. def OAI.BinPackingGap.SearchUpdateMachine.put line 59
  13. def OAI.BinPackingGap.SearchUpdateMachine.replacePlace line 62
  14. theorem OAI.BinPackingGap.SearchUpdateMachine.replacePlace_injective line 68
  15. def OAI.BinPackingGap.SearchUpdateMachine.go line 71
  16. def OAI.BinPackingGap.SearchUpdateMachine.choose line 74
  17. def OAI.BinPackingGap.SearchUpdateMachine.copyBit line 77
  18. def OAI.BinPackingGap.SearchUpdateMachine.copyDigit line 82
  19. def OAI.BinPackingGap.SearchUpdateMachine.skipUnary line 86
  20. def OAI.BinPackingGap.SearchUpdateMachine.code line 90
  21. def OAI.BinPackingGap.SearchUpdateMachine.program line 145
  22. abbrev OAI.BinPackingGap.SearchUpdateMachine.machine line 152
  23. theorem OAI.BinPackingGap.SearchUpdateMachine.machine_step line 154
  24. def OAI.BinPackingGap.SearchUpdateMachine.cfg line 156
  25. def OAI.BinPackingGap.SearchUpdateMachine.io line 160
  26. theorem OAI.BinPackingGap.SearchUpdateMachine.io_input line 163
  27. theorem OAI.BinPackingGap.SearchUpdateMachine.io_reversed line 166
  28. theorem OAI.BinPackingGap.SearchUpdateMachine.update_io_input line 169
  29. theorem OAI.BinPackingGap.SearchUpdateMachine.update_io_reversed line 173
  30. theorem OAI.BinPackingGap.SearchUpdateMachine.joinTrace line 177
  31. theorem OAI.BinPackingGap.SearchUpdateMachine.oneStepTrace line 181
  32. theorem OAI.BinPackingGap.SearchUpdateMachine.copyBitStep line 185
  33. theorem OAI.BinPackingGap.SearchUpdateMachine.copyDigitStep line 196
  34. theorem OAI.BinPackingGap.SearchUpdateMachine.unaryCopyTrace line 205
  35. theorem OAI.BinPackingGap.SearchUpdateMachine.unarySkipStep line 222
  36. theorem OAI.BinPackingGap.SearchUpdateMachine.unarySkipTrace line 231
  37. theorem OAI.BinPackingGap.SearchUpdateMachine.nameCopyTrace line 247
  38. def OAI.BinPackingGap.SearchUpdateMachine.decrement line 275
  39. def OAI.BinPackingGap.SearchUpdateMachine.counterAfter line 278
  40. def OAI.BinPackingGap.SearchUpdateMachine.countedPhase line 282
  41. theorem OAI.BinPackingGap.SearchUpdateMachine.counterAfter_empty line 285
  42. theorem OAI.BinPackingGap.SearchUpdateMachine.countedPhase_counterAfter line 291
  43. def OAI.BinPackingGap.SearchUpdateMachine.countIO line 301
  44. theorem OAI.BinPackingGap.SearchUpdateMachine.itemsStep_nil line 304
  45. theorem OAI.BinPackingGap.SearchUpdateMachine.itemsStep_cons line 316
  46. theorem OAI.BinPackingGap.SearchUpdateMachine.itemsTrace line 328
  47. def OAI.BinPackingGap.SearchUpdateMachine.work line 370
  48. theorem OAI.BinPackingGap.SearchUpdateMachine.put_work line 380
  49. theorem OAI.BinPackingGap.SearchUpdateMachine.io_work line 393
  50. theorem OAI.BinPackingGap.SearchUpdateMachine.transferTrace line 397
  51. theorem OAI.BinPackingGap.SearchUpdateMachine.finishStep line 411
  52. def OAI.BinPackingGap.SearchUpdateMachine.phaseWord line 419
  53. theorem OAI.BinPackingGap.SearchUpdateMachine.phaseWord_ambient line 421
  54. theorem OAI.BinPackingGap.SearchUpdateMachine.reverseFinishTrace line 424
  55. theorem OAI.BinPackingGap.SearchUpdateMachine.copyRestTrace line 436
  56. def OAI.BinPackingGap.SearchUpdateMachine.bodyBits line 449
  57. theorem OAI.BinPackingGap.SearchUpdateMachine.stateBits_eq line 453
  58. def OAI.BinPackingGap.SearchUpdateMachine.initialTarget line 456
  59. theorem OAI.BinPackingGap.SearchUpdateMachine.startStep line 465
  60. def OAI.BinPackingGap.SearchUpdateMachine.itemWork line 476
  61. theorem OAI.BinPackingGap.SearchUpdateMachine.itemStep_true line 479
  62. theorem OAI.BinPackingGap.SearchUpdateMachine.itemStep_false line 489
  63. theorem OAI.BinPackingGap.SearchUpdateMachine.itemTrace line 501
  64. theorem OAI.BinPackingGap.SearchUpdateMachine.startItemStep line 520
  65. theorem OAI.BinPackingGap.SearchUpdateMachine.convertTrace line 527
  66. theorem OAI.BinPackingGap.SearchUpdateMachine.frameTrace line 544
  67. theorem OAI.BinPackingGap.SearchUpdateMachine.restorePayloadTrace line 555
  68. theorem OAI.BinPackingGap.SearchUpdateMachine.zeroLabelStep line 568
  69. theorem OAI.BinPackingGap.SearchUpdateMachine.replaceTapes_eq line 577
  70. theorem OAI.BinPackingGap.SearchUpdateMachine.replaceTrace line 583
  71. def OAI.BinPackingGap.SearchUpdateMachine.fillHeader line 596
  72. def OAI.BinPackingGap.SearchUpdateMachine.newFixed line 599
  73. def OAI.BinPackingGap.SearchUpdateMachine.fillBody line 601
  74. def OAI.BinPackingGap.SearchUpdateMachine.fillPhase line 604
  75. def OAI.BinPackingGap.SearchUpdateMachine.fillCounter line 606
  76. def OAI.BinPackingGap.SearchUpdateMachine.fillPrefixSteps line 609
  77. theorem OAI.BinPackingGap.SearchUpdateMachine.fillPrefixTrace line 614
  78. def OAI.BinPackingGap.SearchUpdateMachine.fillSteps line 654
  79. theorem OAI.BinPackingGap.SearchUpdateMachine.fillTrace line 658
  80. theorem OAI.BinPackingGap.SearchUpdateMachine.zeroControlsStep line 674
  81. theorem OAI.BinPackingGap.SearchUpdateMachine.incrementLabelStep line 681
  82. def OAI.BinPackingGap.SearchUpdateMachine.findBody line 688
  83. def OAI.BinPackingGap.SearchUpdateMachine.findSteps line 691
  84. theorem OAI.BinPackingGap.SearchUpdateMachine.findTrace line 696
  85. def OAI.BinPackingGap.SearchUpdateMachine.fillNoBody line 718
  86. def OAI.BinPackingGap.SearchUpdateMachine.fillNoSteps line 722
  87. theorem OAI.BinPackingGap.SearchUpdateMachine.fillNoTrace line 727
  88. def OAI.BinPackingGap.SearchUpdateMachine.rawTime line 748
  89. theorem OAI.BinPackingGap.SearchUpdateMachine.bodyBits_length line 750
  90. theorem OAI.BinPackingGap.SearchUpdateMachine.copyBudget_le line 756
  91. theorem OAI.BinPackingGap.SearchUpdateMachine.findBudget_le line 764
  92. theorem OAI.BinPackingGap.SearchUpdateMachine.fillNoBudget_le line 772
  93. theorem OAI.BinPackingGap.SearchUpdateMachine.fillBudget_le line 780
  94. theorem OAI.BinPackingGap.SearchUpdateMachine.init_eq line 796
  95. def OAI.BinPackingGap.SearchUpdateMachine.copyRun line 803
  96. def OAI.BinPackingGap.SearchUpdateMachine.rawRun line 823
  97. def OAI.BinPackingGap.SearchUpdateMachine.cleanupTapes line 897
  98. theorem OAI.BinPackingGap.SearchUpdateMachine.cleanup_complete line 900
  99. def OAI.BinPackingGap.SearchUpdateMachine.computation line 903
  100. theorem OAI.BinPackingGap.SearchUpdateMachine.finiteAlphabet line 910