OAI/Computability/BinPacking/Computation/MachineFiniteAlphabet.lean

GitHub source file

121 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.Complexity.MachineControl.configuration line 15
2. def OAI.BinPackingGames.Foundations.Complexity.MachineControl.statement line 21
3. theorem OAI.BinPackingGames.Foundations.Complexity.MachineControl.stepAux_simulation line 36
4. def OAI.BinPackingGames.Foundations.Complexity.MachineControl.program line 63
5. theorem OAI.BinPackingGames.Foundations.Complexity.MachineControl.step_simulation line 66
6. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.statement line 88
7. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.statement_symm_statement line 91
8. def OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.configuration line 97
9. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.configuration_label line 100
10. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.configuration_state line 103
11. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.configuration_tapes line 106
12. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.configuration_symm_configuration line 109
13. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.configuration_configuration_symm line 114
14. def OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.configurationEquiv line 119
15. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.configurationEquiv_apply line 125
16. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.control_configuration line 128
17. def OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.program line 133
18. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.program_symm_program line 136
19. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.statementPushBound line 141
20. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.supportsStmt_iff line 146
21. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.supports_iff line 168
22. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.stepAux_transport line 174
23. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.stepAux_transport_symm line 181
24. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.step_transport line 188
25. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.step_iff line 200
26. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.advance_transport line 212
27. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.iterate_transport line 220
28. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.trace_iff line 231
29. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.trace line 247
30. def OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.execution line 254
31. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.execution_steps line 268
32. def OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.execution_reflect line 273
33. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateEquiv.execution_reflect_steps line 288
34. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineSequential.Tape line 300
35. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineSequential.Symbols line 301
36. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineSequential.Label line 304
37. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineSequential.Register line 305
38. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineSequential.State line 306
39. def OAI.BinPackingGames.Foundations.Complexity.MachineSequential.firstStates line 308
40. def OAI.BinPackingGames.Foundations.Complexity.MachineSequential.secondStates line 315
41. def OAI.BinPackingGames.Foundations.Complexity.MachineSequential.secondLabels line 322
42. def OAI.BinPackingGames.Foundations.Complexity.MachineSequential.bridgeLabel line 328
43. def OAI.BinPackingGames.Foundations.Complexity.MachineSequential.firstStatement line 331
44. def OAI.BinPackingGames.Foundations.Complexity.MachineSequential.secondStatement line 336
45. def OAI.BinPackingGames.Foundations.Complexity.MachineSequential.program line 344
46. def OAI.BinPackingGames.Foundations.Complexity.MachineSequential.machine line 360
47. def OAI.BinPackingGames.Foundations.Complexity.MachineSequential.firstConfiguration line 387
48. def OAI.BinPackingGames.Foundations.Complexity.MachineSequential.secondConfiguration line 393
49. theorem OAI.BinPackingGames.Foundations.Complexity.MachineSequential.firstStep line 402
50. theorem OAI.BinPackingGames.Foundations.Complexity.MachineSequential.secondStep line 432
51. theorem OAI.BinPackingGames.Foundations.Complexity.MachineSequential.firstConfiguration_init line 457
52. theorem OAI.BinPackingGames.Foundations.Complexity.MachineSequential.secondConfiguration_halt line 474
53. def OAI.BinPackingGames.Foundations.Complexity.MachineSequential.temporaryTapes line 492
54. def OAI.BinPackingGames.Foundations.Complexity.MachineSequential.temporaryConfiguration line 498
55. theorem OAI.BinPackingGames.Foundations.Complexity.MachineSequential.firstTransfer_tapes line 503
56. theorem OAI.BinPackingGames.Foundations.Complexity.MachineSequential.secondTransfer_tapes line 522
57. def OAI.BinPackingGames.Foundations.Complexity.MachineSequential.firstTransfer line 545
58. def OAI.BinPackingGames.Foundations.Complexity.MachineSequential.secondTransfer line 566
59. def OAI.BinPackingGames.Foundations.Complexity.MachineSequential.execute line 582
60. def OAI.BinPackingGames.Foundations.Complexity.MachineSequential.compose line 612
61. def OAI.BinPackingGames.Foundations.Complexity.MachineSequential.composeBits line 659
62. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.ExtraTape line 672
63. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.ExtraTape.enumList line 676
64. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.ExtraTape.enumList_getElem?_ctorIdx_eq line 678
65. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.ExtraTape.enumList_nodup line 682
66. instance OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.(instance at line 684) line 684
67. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.Phase line 687
68. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.Phase.enumList line 691
69. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.Phase.enumList_getElem?_ctorIdx_eq line 694
70. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.Phase.enumList_nodup line 698
71. instance OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.(instance at line 700) line 700
72. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.Tape line 704
73. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.Symbols line 705
74. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.Label line 706
75. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.State line 707
76. def OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.extraTapes line 709
77. def OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.auxProgram line 715
78. def OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.program line 736
79. def OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.machine line 740
80. def OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.inputTapes line 758
81. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.inputTapes_input line 761
82. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.inputTapes_counter line 765
83. def OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.inputConfig line 768
84. def OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.embedded line 772
85. def OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.temporaryTapes line 777
86. def OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.temporaryConfig line 780
87. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.inputTapes_update_input line 784
88. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.inputTapes_update_counter line 796
89. def OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.oneStep line 805
90. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.parseStep_true line 813
91. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.parseStep_false line 822
92. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.parseTrace line 831
93. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.guardStep_some line 857
94. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.guardStep_none line 866
95. def OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.bodyExecution line 873
96. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.bodyToTemp_tapes line 883
97. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.tempToBody_tapes line 899
98. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.finalToTemp_tapes line 911
99. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.tempToOutput_tapes line 923
100. def OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.bodyToTemp line 935
101. def OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.tempToBody line 951
102. def OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.finalToTemp line 966
103. def OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.tempToOutput line 978
104. def OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.bodyReturn line 991
105. def OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.finish line 1002
106. def OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.loopBudget line 1014
107. def OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.loopExecution line 1019
108. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.inputConfig_init line 1057
109. def OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.executeSequence line 1069
110. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.loopBudget_eq_sum line 1100
111. def OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.executeSequenceSum line 1111
112. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRepeat.loopBudget_le line 1124
113. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFiniteAlphabet.input_finite line 1150
114. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFiniteAlphabet.of_homogeneous line 1154
115. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFiniteAlphabet.of_bool line 1160
116. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFiniteAlphabet.of_equiv line 1163
117. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFiniteAlphabet.symbols_finite line 1168
118. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFiniteAlphabet.sequential_machine line 1174
119. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFiniteAlphabet.compose line 1185
120. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFiniteAlphabet.composeBits line 1196
121. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFiniteAlphabet.repeat_machine line 1205