OAI/Computability/BinPacking/Machines/PackingPowerProgram.lean

GitHub source file

117 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.BinPackingGap.FiniteTapeProgram.Data line 17
  2. inductive OAI.BinPackingGap.FiniteTapeProgram.Action line 21
  3. def OAI.BinPackingGap.FiniteTapeProgram.Action.statement line 31
  4. def OAI.BinPackingGap.FiniteTapeProgram.Action.eval line 42
  5. theorem OAI.BinPackingGap.FiniteTapeProgram.Action.stepAux_statement line 51
  6. inductive OAI.BinPackingGap.FiniteTapeProgram.Code line 71
  7. def OAI.BinPackingGap.FiniteTapeProgram.Code.Label line 79
  8. instance OAI.BinPackingGap.FiniteTapeProgram.Code.labelFintype line 86
  9. def OAI.BinPackingGap.FiniteTapeProgram.Code.entry line 101
  10. def OAI.BinPackingGap.FiniteTapeProgram.jump line 108
  11. theorem OAI.BinPackingGap.FiniteTapeProgram.stepAux_jump line 113
  12. def OAI.BinPackingGap.FiniteTapeProgram.Code.instruction line 117
  13. inductive OAI.BinPackingGap.FiniteTapeProgram.Exec line 138
  14. theorem OAI.BinPackingGap.FiniteTapeProgram.Exec.trace line 155
  15. def OAI.BinPackingGap.FiniteTapeProgram.Runs line 210
  16. theorem OAI.BinPackingGap.FiniteTapeProgram.Exec.runs line 213
  17. theorem OAI.BinPackingGap.FiniteTapeProgram.Runs.mono line 216
  18. theorem OAI.BinPackingGap.FiniteTapeProgram.Runs.seq line 221
  19. def OAI.BinPackingGap.FiniteTapeProgram.Code.machine line 229
  20. theorem OAI.BinPackingGap.FiniteTapeProgram.Code.machine_finiteAlphabet line 240
  21. def OAI.BinPackingGap.FiniteTapeProgram.Code.outputsInTime line 247
  22. theorem OAI.BinPackingGap.FiniteTapeProgram.Exec.stack_length_le line 288
  23. theorem OAI.BinPackingGap.FiniteTapeProgram.Runs.stack_length_le line 308
  24. abbrev OAI.BinPackingGap.BooleanTapeCode.State line 326
  25. abbrev OAI.BinPackingGap.BooleanTapeCode.Program line 327
  26. def OAI.BinPackingGap.BooleanTapeCode.clean line 329
  27. def OAI.BinPackingGap.BooleanTapeCode.transfer line 331
  28. theorem OAI.BinPackingGap.BooleanTapeCode.transfer_exec line 335
  29. def OAI.BinPackingGap.BooleanTapeCode.copyProgram line 352
  30. def OAI.BinPackingGap.BooleanTapeCode.copy line 357
  31. theorem OAI.BinPackingGap.BooleanTapeCode.copy_exec line 360
  32. def OAI.BinPackingGap.BooleanTapeCode.drain line 369
  33. theorem OAI.BinPackingGap.BooleanTapeCode.drain_exec line 372
  34. def OAI.BinPackingGap.BooleanTapeCode.convert line 380
  35. theorem OAI.BinPackingGap.BooleanTapeCode.convert_exec line 384
  36. inductive OAI.BinPackingGap.BooleanTapeCode.FrameLabel line 398
  37. def OAI.BinPackingGap.BooleanTapeCode.frameProgram line 402
  38. def OAI.BinPackingGap.BooleanTapeCode.framePayload line 410
  39. theorem OAI.BinPackingGap.BooleanTapeCode.framePayload_output line 413
  40. theorem OAI.BinPackingGap.BooleanTapeCode.framePayload_exec line 420
  41. def OAI.BinPackingGap.BooleanTapeCode.frame line 434
  42. theorem OAI.BinPackingGap.BooleanTapeCode.frame_eq line 438
  43. theorem OAI.BinPackingGap.BooleanTapeCode.frame_exec line 444
  44. def OAI.BinPackingGap.BooleanTapeCode.increment line 458
  45. theorem OAI.BinPackingGap.BooleanTapeCode.increment_exec line 463
  46. abbrev OAI.BinPackingGap.LiteralSlotGraphMachine.NonemptyFormula line 504
  47. def OAI.BinPackingGap.LiteralSlotGraphMachine.inputBits line 506
  48. def OAI.BinPackingGap.LiteralSlotGraphMachine.graphInput line 508
  49. inductive OAI.BinPackingGap.LiteralSlotGraphMachine.Tape line 514
  50. abbrev OAI.BinPackingGap.LiteralSlotGraphMachine.Tape.enumList line 519
  51. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.Tape.enumList_getElem?_ctorIdx_eq line 523
  52. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.Tape.enumList_nodup line 527
  53. instance OAI.BinPackingGap.LiteralSlotGraphMachine.(instance at line 529) line 529
  54. structure OAI.BinPackingGap.LiteralSlotGraphMachine.Control line 533
  55. def OAI.BinPackingGap.LiteralSlotGraphMachine.initialControl line 542
  56. abbrev OAI.BinPackingGap.LiteralSlotGraphMachine.State line 544
  57. abbrev OAI.BinPackingGap.LiteralSlotGraphMachine.Program line 545
  58. def OAI.BinPackingGap.LiteralSlotGraphMachine.initialState line 547
  59. def OAI.BinPackingGap.LiteralSlotGraphMachine.saveHead line 549
  60. def OAI.BinPackingGap.LiteralSlotGraphMachine.mapControl line 550
  61. def OAI.BinPackingGap.LiteralSlotGraphMachine.resetHead line 551
  62. def OAI.BinPackingGap.LiteralSlotGraphMachine.skip line 553
  63. def OAI.BinPackingGap.LiteralSlotGraphMachine.sequence line 555
  64. def OAI.BinPackingGap.LiteralSlotGraphMachine.pushBit line 559
  65. def OAI.BinPackingGap.LiteralSlotGraphMachine.changeControl line 560
  66. def OAI.BinPackingGap.LiteralSlotGraphMachine.transfer line 562
  67. def OAI.BinPackingGap.LiteralSlotGraphMachine.copy line 564
  68. def OAI.BinPackingGap.LiteralSlotGraphMachine.drain line 566
  69. def OAI.BinPackingGap.LiteralSlotGraphMachine.frame line 567
  70. def OAI.BinPackingGap.LiteralSlotGraphMachine.increment line 569
  71. def OAI.BinPackingGap.LiteralSlotGraphMachine.readVariable line 572
  72. def OAI.BinPackingGap.LiteralSlotGraphMachine.skipField line 577
  73. def OAI.BinPackingGap.LiteralSlotGraphMachine.readSign line 580
  74. def OAI.BinPackingGap.LiteralSlotGraphMachine.countHeader line 587
  75. def OAI.BinPackingGap.LiteralSlotGraphMachine.vertexBody line 593
  76. def OAI.BinPackingGap.LiteralSlotGraphMachine.vertices line 598
  77. def OAI.BinPackingGap.LiteralSlotGraphMachine.compareGuard line 601
  78. def OAI.BinPackingGap.LiteralSlotGraphMachine.compareVariables line 607
  79. def OAI.BinPackingGap.LiteralSlotGraphMachine.emitPair line 611
  80. def OAI.BinPackingGap.LiteralSlotGraphMachine.isEdge line 616
  81. def OAI.BinPackingGap.LiteralSlotGraphMachine.nextRemaining line 620
  82. def OAI.BinPackingGap.LiteralSlotGraphMachine.innerBody line 623
  83. def OAI.BinPackingGap.LiteralSlotGraphMachine.innerLoop line 632
  84. def OAI.BinPackingGap.LiteralSlotGraphMachine.startRow line 635
  85. def OAI.BinPackingGap.LiteralSlotGraphMachine.nextSlot line 638
  86. def OAI.BinPackingGap.LiteralSlotGraphMachine.outerBody line 641
  87. def OAI.BinPackingGap.LiteralSlotGraphMachine.outerLoop line 654
  88. def OAI.BinPackingGap.LiteralSlotGraphMachine.program line 657
  89. def OAI.BinPackingGap.LiteralSlotGraphMachine.machine line 674
  90. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.machine_finiteAlphabet line 676
  91. abbrev OAI.BinPackingGap.PackingFieldDecodeMachine.State line 686
  92. def OAI.BinPackingGap.PackingFieldDecodeMachine.decoderSlots line 690
  93. theorem OAI.BinPackingGap.PackingFieldDecodeMachine.decoderSlots_zero line 695
  94. theorem OAI.BinPackingGap.PackingFieldDecodeMachine.decoderSlots_one line 701
  95. theorem OAI.BinPackingGap.PackingFieldDecodeMachine.decoderSlots_two line 707
  96. def OAI.BinPackingGap.PackingFieldDecodeMachine.code line 712
  97. def OAI.BinPackingGap.PackingFieldDecodeMachine.decodedTapes line 716
  98. theorem OAI.BinPackingGap.PackingFieldDecodeMachine.decodedTapes_source line 721
  99. theorem OAI.BinPackingGap.PackingFieldDecodeMachine.decodedTapes_scratch line 725
  100. theorem OAI.BinPackingGap.PackingFieldDecodeMachine.decodedTapes_destination line 730
  101. theorem OAI.BinPackingGap.PackingFieldDecodeMachine.decodedTapes_other line 735
  102. theorem OAI.BinPackingGap.PackingFieldDecodeMachine.decodeNat_exec line 739
  103. theorem OAI.BinPackingGap.PackingFieldDecodeMachine.decodeNat_steps line 752
  104. def OAI.BinPackingGap.PackingFieldDecodeMachine.decodeNatInTime line 756
  105. def OAI.BinPackingGap.PackingFieldDecodeMachine.machine line 776
  106. theorem OAI.BinPackingGap.PackingFieldDecodeMachine.machine_finiteAlphabet line 779
  107. structure OAI.BinPackingGap.PackingPowerProgram.Ready line 793
  108. def OAI.BinPackingGap.PackingPowerProgram.resultTapes line 799
  109. theorem OAI.BinPackingGap.PackingPowerProgram.resultTapes_output line 802
  110. theorem OAI.BinPackingGap.PackingPowerProgram.resultTapes_tally line 806
  111. theorem OAI.BinPackingGap.PackingPowerProgram.resultTapes_other line 811
  112. theorem OAI.BinPackingGap.PackingPowerProgram.resultTapes_base line 816
  113. theorem OAI.BinPackingGap.PackingPowerProgram.resultTapes_workspace line 821
  114. def OAI.BinPackingGap.PackingPowerProgram.budget line 836
  115. def OAI.BinPackingGap.PackingPowerProgram.code line 839
  116. def OAI.BinPackingGap.PackingPowerProgram.runInTime line 842
  117. theorem OAI.BinPackingGap.PackingPowerProgram.exec line 854