OAI/Computability/BinPacking/Search/SearchInitialItemsMachine.lean

GitHub source file

120 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.BinPackingGap.ExtensionMachineRegisters.Lens line 12
  2. def OAI.BinPackingGap.ExtensionMachineRegisters.Lens.identity line 23
  3. def OAI.BinPackingGap.ExtensionMachineRegisters.Lens.ofEquiv line 30
  4. def OAI.BinPackingGap.ExtensionMachineRegisters.Lens.first line 37
  5. def OAI.BinPackingGap.ExtensionMachineRegisters.Lens.second line 44
  6. def OAI.BinPackingGap.ExtensionMachineRegisters.Lens.compose line 51
  7. def OAI.BinPackingGap.ExtensionMachineRegisters.statement line 62
  8. theorem OAI.BinPackingGap.ExtensionMachineRegisters.statement_identity line 74
  9. theorem OAI.BinPackingGap.ExtensionMachineRegisters.statement_compose line 78
  10. theorem OAI.BinPackingGap.ExtensionMachineRegisters.statement_ofEquiv_symm line 83
  11. def OAI.BinPackingGap.ExtensionMachineRegisters.equivConfiguration line 87
  12. def OAI.BinPackingGap.ExtensionMachineRegisters.configuration line 90
  13. def OAI.BinPackingGap.ExtensionMachineRegisters.project line 93
  14. theorem OAI.BinPackingGap.ExtensionMachineRegisters.configuration_ofEquiv line 96
  15. theorem OAI.BinPackingGap.ExtensionMachineRegisters.equivConfiguration_symm line 100
  16. theorem OAI.BinPackingGap.ExtensionMachineRegisters.project_configuration line 105
  17. theorem OAI.BinPackingGap.ExtensionMachineRegisters.configuration_project line 110
  18. theorem OAI.BinPackingGap.ExtensionMachineRegisters.stepAux_transport line 117
  19. theorem OAI.BinPackingGap.ExtensionMachineRegisters.stepAux_transport_project line 144
  20. def OAI.BinPackingGap.ExtensionMachineRegisters.program line 151
  21. theorem OAI.BinPackingGap.ExtensionMachineRegisters.program_identity line 155
  22. theorem OAI.BinPackingGap.ExtensionMachineRegisters.program_ofEquiv_symm line 161
  23. theorem OAI.BinPackingGap.ExtensionMachineRegisters.step_transport line 167
  24. theorem OAI.BinPackingGap.ExtensionMachineRegisters.advance_transport line 180
  25. theorem OAI.BinPackingGap.ExtensionMachineRegisters.iterate_transport line 188
  26. theorem OAI.BinPackingGap.ExtensionMachineRegisters.trace line 199
  27. def OAI.BinPackingGap.ExtensionMachineRegisters.execution line 209
  28. def OAI.BinPackingGap.ExtensionMachineRegisters.equivExecution line 224
  29. theorem OAI.BinPackingGap.ExtensionMachineRegisters.equivTrace line 238
  30. theorem OAI.BinPackingGap.ExtensionMachineRegisters.observer_configuration line 249
  31. def OAI.BinPackingGap.ExtensionMachinePlacement.tapes line 263
  32. def OAI.BinPackingGap.ExtensionMachinePlacement.label line 269
  33. def OAI.BinPackingGap.ExtensionMachinePlacement.configuration line 273
  34. def OAI.BinPackingGap.ExtensionMachinePlacement.statement line 279
  35. theorem OAI.BinPackingGap.ExtensionMachinePlacement.tapes_apply line 297
  36. theorem OAI.BinPackingGap.ExtensionMachinePlacement.tapes_unmapped line 303
  37. theorem OAI.BinPackingGap.ExtensionMachinePlacement.tapes_restrict line 308
  38. theorem OAI.BinPackingGap.ExtensionMachinePlacement.tapes_update line 318
  39. theorem OAI.BinPackingGap.ExtensionMachinePlacement.stepAux_simulation line 337
  40. theorem OAI.BinPackingGap.ExtensionMachinePlacement.step_simulation line 373
  41. theorem OAI.BinPackingGap.ExtensionMachinePlacement.trace line 397
  42. def OAI.BinPackingGap.ExtensionMachinePlacement.execution line 414
  43. theorem OAI.BinPackingGap.ExtensionMachinePlacement.configuration_observer line 431
  44. abbrev OAI.BinPackingGap.ExtensionNatMachine.State line 447
  45. abbrev OAI.BinPackingGap.ExtensionNatMachine.Alphabet line 448
  46. inductive OAI.BinPackingGap.ExtensionNatMachine.Label line 450
  47. abbrev OAI.BinPackingGap.ExtensionNatMachine.Label.enumList line 454
  48. theorem OAI.BinPackingGap.ExtensionNatMachine.Label.enumList_getElem?_ctorIdx_eq line 456
  49. theorem OAI.BinPackingGap.ExtensionNatMachine.Label.enumList_nodup line 460
  50. instance OAI.BinPackingGap.ExtensionNatMachine.(instance at line 462) line 462
  51. def OAI.BinPackingGap.ExtensionNatMachine.scannerEquiv line 466
  52. def OAI.BinPackingGap.ExtensionNatMachine.statement line 474
  53. def OAI.BinPackingGap.ExtensionNatMachine.resultTapes line 483
  54. theorem OAI.BinPackingGap.ExtensionNatMachine.natTrace line 487
  55. def OAI.BinPackingGap.ExtensionNatMachine.natInTime line 557
  56. def OAI.BinPackingGap.ExtensionNatMachine.orderEquiv line 572
  57. def OAI.BinPackingGap.ExtensionNatMachine.orderStatement line 580
  58. def OAI.BinPackingGap.ExtensionNatMachine.preservingOrderInTime line 587
  59. inductive OAI.BinPackingGap.SearchInitialItemsMachine.Number line 624
  60. abbrev OAI.BinPackingGap.SearchInitialItemsMachine.Number.enumList line 628
  61. theorem OAI.BinPackingGap.SearchInitialItemsMachine.Number.enumList_getElem?_ctorIdx_eq line 630
  62. theorem OAI.BinPackingGap.SearchInitialItemsMachine.Number.enumList_nodup line 634
  63. instance OAI.BinPackingGap.SearchInitialItemsMachine.(instance at line 636) line 636
  64. inductive OAI.BinPackingGap.SearchInitialItemsMachine.Control line 640
  65. abbrev OAI.BinPackingGap.SearchInitialItemsMachine.Control.enumList line 646
  66. theorem OAI.BinPackingGap.SearchInitialItemsMachine.Control.enumList_getElem?_ctorIdx_eq line 650
  67. theorem OAI.BinPackingGap.SearchInitialItemsMachine.Control.enumList_nodup line 654
  68. instance OAI.BinPackingGap.SearchInitialItemsMachine.(instance at line 656) line 656
  69. inductive OAI.BinPackingGap.SearchInitialItemsMachine.Label line 660
  70. abbrev OAI.BinPackingGap.SearchInitialItemsMachine.Tape line 666
  71. abbrev OAI.BinPackingGap.SearchInitialItemsMachine.Alphabet line 667
  72. abbrev OAI.BinPackingGap.SearchInitialItemsMachine.State line 668
  73. def OAI.BinPackingGap.SearchInitialItemsMachine.clean line 670
  74. def OAI.BinPackingGap.SearchInitialItemsMachine.validity line 672
  75. def OAI.BinPackingGap.SearchInitialItemsMachine.jump line 674
  76. def OAI.BinPackingGap.SearchInitialItemsMachine.scanTape line 677
  77. def OAI.BinPackingGap.SearchInitialItemsMachine.scanPorts line 682
  78. def OAI.BinPackingGap.SearchInitialItemsMachine.orderTape line 687
  79. def OAI.BinPackingGap.SearchInitialItemsMachine.orderPorts line 694
  80. def OAI.BinPackingGap.SearchInitialItemsMachine.scanSuccess line 697
  81. def OAI.BinPackingGap.SearchInitialItemsMachine.orderExit line 701
  82. def OAI.BinPackingGap.SearchInitialItemsMachine.instruction line 705
  83. def OAI.BinPackingGap.SearchInitialItemsMachine.program line 734
  84. abbrev OAI.BinPackingGap.SearchInitialItemsMachine.machine line 741
  85. def OAI.BinPackingGap.SearchInitialItemsMachine.tapes line 752
  86. def OAI.BinPackingGap.SearchInitialItemsMachine.cfg line 761
  87. theorem OAI.BinPackingGap.SearchInitialItemsMachine.update_raw line 764
  88. theorem OAI.BinPackingGap.SearchInitialItemsMachine.update_stream line 768
  89. theorem OAI.BinPackingGap.SearchInitialItemsMachine.update_scratch line 772
  90. theorem OAI.BinPackingGap.SearchInitialItemsMachine.update_numerator line 776
  91. theorem OAI.BinPackingGap.SearchInitialItemsMachine.update_denominator line 780
  92. theorem OAI.BinPackingGap.SearchInitialItemsMachine.update_count line 784
  93. def OAI.BinPackingGap.SearchInitialItemsMachine.oneStep line 788
  94. def OAI.BinPackingGap.SearchInitialItemsMachine.join line 796
  95. def OAI.BinPackingGap.SearchInitialItemsMachine.enlarge line 803
  96. theorem OAI.BinPackingGap.SearchInitialItemsMachine.entryStep line 809
  97. theorem OAI.BinPackingGap.SearchInitialItemsMachine.markerStep line 819
  98. theorem OAI.BinPackingGap.SearchInitialItemsMachine.positiveStep line 830
  99. def OAI.BinPackingGap.SearchInitialItemsMachine.numeratorInTime line 841
  100. def OAI.BinPackingGap.SearchInitialItemsMachine.denominatorInTime line 864
  101. theorem OAI.BinPackingGap.SearchInitialItemsMachine.bits_eq_nil_iff line 887
  102. def OAI.BinPackingGap.SearchInitialItemsMachine.comparisonInTime line 895
  103. def OAI.BinPackingGap.SearchInitialItemsMachine.clearInTime line 920
  104. def OAI.BinPackingGap.SearchInitialItemsMachine.rowTime line 945
  105. def OAI.BinPackingGap.SearchInitialItemsMachine.loopTime line 947
  106. theorem OAI.BinPackingGap.SearchInitialItemsMachine.validItems_cons line 951
  107. def OAI.BinPackingGap.SearchInitialItemsMachine.itemsInTime line 956
  108. theorem OAI.BinPackingGap.SearchInitialItemsMachine.loopTime_le line 1008
  109. def OAI.BinPackingGap.SearchInitialItemsMachine.copyInTime line 1024
  110. theorem OAI.BinPackingGap.SearchInitialItemsMachine.seedStep line 1040
  111. def OAI.BinPackingGap.SearchInitialItemsMachine.countInTime line 1049
  112. theorem OAI.BinPackingGap.SearchInitialItemsMachine.finishStep line 1079
  113. theorem OAI.BinPackingGap.SearchInitialItemsMachine.initList_eq line 1088
  114. theorem OAI.BinPackingGap.SearchInitialItemsMachine.haltList_eq line 1094
  115. theorem OAI.BinPackingGap.SearchInitialItemsMachine.item_count_le line 1100
  116. def OAI.BinPackingGap.SearchInitialItemsMachine.encodedInTime line 1110
  117. def OAI.BinPackingGap.SearchInitialItemsMachine.malformedInTime line 1136
  118. def OAI.BinPackingGap.SearchInitialItemsMachine.outputsInTime line 1158
  119. def OAI.BinPackingGap.SearchInitialItemsMachine.computation line 1171
  120. theorem OAI.BinPackingGap.SearchInitialItemsMachine.finiteAlphabet line 1183