OAI/Computability/BinPacking/Computation/MachineRegularInternalRow.lean

GitHub source file

145 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.Alphabet line 15
  2. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.equalityBits line 17
  3. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.equalityBits_length_le line 20
  4. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.emittedBits line 23
  5. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.emittedBits_length line 26
  6. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.emittedBits_eq_row line 31
  7. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selected_rotation line 45
  8. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selected_rotation_div line 52
  9. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selected_rotation_mod line 60
  10. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.rotationLookupTrace line 68
  11. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.FinishLabel line 91
  12. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.finishFields line 97
  13. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.finishFields_zero line 101
  14. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.finishFields_one line 103
  15. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.finishFields_two line 105
  16. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.finishInstruction line 107
  17. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.finishSteps line 126
  18. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.finishSteps_le line 131
  19. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.joinTrace line 138
  20. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.finishTrace line 142
  21. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.RotorLabel line 257
  22. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.rotorLookupTapes line 262
  23. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.rotorLookupTapes_injective line 266
  24. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.rotorLookupTapes_outside line 274
  25. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.rotorInstruction line 281
  26. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.rotorFinalTapes line 292
  27. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.rotorSteps line 302
  28. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.rotorTrace line 307
  29. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.rotorSteps_le line 386
  30. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.SelectExtraTape line 396
  31. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.SelectExtraTape.enumList line 401
  32. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.SelectExtraTape.enumList_getElem?_ctorIdx_eq line 404
  33. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.SelectExtraTape.enumList_nodup line 408
  34. instance OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.(instance at line 410) line 410
  35. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.SelectTape line 414
  36. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.RawSelectAlphabet line 415
  37. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.SelectAlphabet line 417
  38. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectAlphabet_eq line 419
  39. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectToBoolWord line 425
  40. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectToBoolTapes line 430
  41. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.alphabet_tapes_apply line 433
  42. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectToBoolTapes_eq line 440
  43. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.SelectState line 448
  44. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectStateEquiv line 450
  45. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectScratch line 456
  46. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectQuery line 457
  47. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectOutput line 458
  48. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.compareSlots line 460
  49. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.subtractSlots line 464
  50. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.SelectCopy line 468
  51. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.SelectCopy.enumList line 472
  52. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.SelectCopy.enumList_getElem?_ctorIdx_eq line 475
  53. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.SelectCopy.enumList_nodup line 479
  54. instance OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.(instance at line 481) line 481
  55. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.SelectAdd line 485
  56. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.SelectAdd.enumList line 489
  57. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.SelectAdd.enumList_getElem?_ctorIdx_eq line 491
  58. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.SelectAdd.enumList_nodup line 495
  59. instance OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.(instance at line 497) line 497
  60. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.SelectAddStage line 501
  61. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.SelectAddStage.enumList line 505
  62. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.SelectAddStage.enumList_getElem?_ctorIdx_eq line 507
  63. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.SelectAddStage.enumList_nodup line 511
  64. instance OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.(instance at line 513) line 513
  65. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.SelectControl line 517
  66. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.SelectLabel line 526
  67. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.copySource line 528
  68. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.copyDestination line 534
  69. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.afterCopy line 540
  70. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.addSource line 547
  71. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.afterAdd line 551
  72. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.cleanupTape line 555
  73. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.afterCleanup line 558
  74. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectControl line 561
  75. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.rawSelectProgram line 583
  76. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectProgram line 589
  77. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectProgram_control line 592
  78. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectCleanState line 604
  79. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectComparisonTrace line 607
  80. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectCopyTrace line 628
  81. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectAddTrace line 647
  82. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.CoreTape line 673
  83. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.CoreState line 674
  84. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.CoreLabel line 678
  85. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreEntry line 685
  86. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectCloudTrace line 687
  87. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectExtraMemory line 719
  88. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory line 732
  89. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory_query line 739
  90. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory_output line 743
  91. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory_scratch line 747
  92. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory_extra line 751
  93. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_query line 756
  94. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_output line 768
  95. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_local line 780
  96. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_size line 792
  97. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_left line 804
  98. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_right line 816
  99. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectCleanupTrace line 828
  100. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.oldSelectSteps line 871
  101. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectOldTrace line 876
  102. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.dummySelectSteps line 920
  103. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.dummySelectSteps_eq line 924
  104. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectDummyTrace line 929
  105. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectionSteps line 988
  106. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectionTrace line 996
  107. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectionSteps_le line 1028
  108. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectorMachine line 1049
  109. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectionInTime line 1060
  110. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorTapes line 1080
  111. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreFinishTapes line 1082
  112. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectTape line 1084
  113. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectView line 1102
  114. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectView_left line 1111
  115. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectView_right line 1119
  116. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreCleanupTape line 1124
  117. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorStateEquiv line 1126
  118. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectStateEquiv line 1135
  119. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreAfterCleanup line 1142
  120. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreInstruction line 1146
  121. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreInitialState line 1160
  122. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreMachine line 1164
  123. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreMemory line 1175
  124. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreMemory_update_output line 1181
  125. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorTapes_injective line 1189
  126. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreFinishTapes_injective line 1193
  127. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreCleaned line 1197
  128. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreCleanupSteps line 1202
  129. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreCleanupTrace line 1207
  130. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreCleaned_memory line 1284
  131. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreCleanupSteps_memory line 1292
  132. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorFinalFrame line 1304
  133. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorTrace line 1320
  134. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectFrame line 1366
  135. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectionTrace line 1375
  136. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreFinishTrace line 1410
  137. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreInputTapes line 1442
  138. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreSteps line 1452
  139. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreTrace line 1466
  140. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.selectedIndex_le line 1513
  141. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.encodedDrop_length_le line 1524
  142. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.rotorSize_le_encodedLength line 1531
  143. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreTimeBound line 1539
  144. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreSteps_le line 1543
  145. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularInternalRow.coreMachineInTime line 1607