OAI/Computability/BinPacking/Computation/MachineVertexPadding.lean

GitHub source file

138 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.tapes line 11
2. def OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.statement line 13
3. def OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.configuration line 15
4. def OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.program line 17
5. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.castStatement line 20
6. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.castConfiguration line 21
7. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.castProgram line 22
8. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.tapes_rfl line 24
9. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.statement_rfl line 25
10. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.configuration_rfl line 26
11. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.program_rfl line 27
12. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.program_apply line 29
13. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.statement_roundtrip line 32
14. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.statement_symm_roundtrip line 35
15. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.configuration_roundtrip line 38
16. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.configuration_symm_roundtrip line 41
17. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.program_roundtrip line 44
18. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.program_symm_roundtrip line 47
19. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.tapes_roundtrip line 50
20. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.tapes_symm_roundtrip line 53
21. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.configuration_label line 56
22. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.configuration_state line 59
23. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.configuration_tapes line 62
24. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.configuration_mk line 65
25. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.map_configuration_rfl line 69
26. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.stepAux_simulation line 74
27. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.step_simulation line 79
28. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.trace_transport line 85
29. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.successfulTrace line 93
30. def OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.executionInTime line 101
31. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.executionInTime_steps line 113
32. def OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.successfulExecutionInTime line 118
33. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAlphabetTransport.successfulExecutionInTime_steps line 124
34. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.Tape line 135
35. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.State line 136
36. inductive OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.Label line 138
37. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.Label.enumList line 142
38. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.Label.enumList_getElem?_ctorIdx_eq line 145
39. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.Label.enumList_nodup line 149
40. instance OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.(instance at line 151) line 151
41. def OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.tapes line 155
42. def OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.initialTapes line 159
43. def OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.resultTapes line 161
44. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.resultTapes_original line 164
45. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.resultTapes_work line 168
46. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.resultTapes_scratch line 171
47. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.resultTapes_vertices line 174
48. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.resultTapes_darts line 177
49. def OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.program line 180
50. def OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.exactSteps line 188
51. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.splitTrace line 191
52. def OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.timePolynomial line 261
53. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.timePolynomial_eval line 263
54. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.exactSteps_le line 266
55. def OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.splitInTime line 273
56. def OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.machine line 283
57. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.initial_configuration line 294
58. def OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.rowsBits line 301
59. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.tableBits_header_rows line 304
60. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.tableTrace line 308
61. def OAI.BinPackingGames.Foundations.Complexity.MachineTableSplit.initializedTableInTime line 316
62. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddingTable.initialOutput line 329
63. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddingTable.execution line 332
64. inductive OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.Tape line 365
65. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.Tape.enumList line 370
66. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.Tape.enumList_getElem?_ctorIdx_eq line 373
67. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.Tape.enumList_nodup line 377
68. instance OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.(instance at line 379) line 379
69. inductive OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.Label line 383
70. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.Alphabet line 392
71. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.State line 393
72. def OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.memory line 395
73. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.update_output line 406
74. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.update_vertex line 409
75. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.update_edge line 412
76. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.update_power line 415
77. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.update_fuel line 418
78. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.update_relation line 421
79. def OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.splitTape line 425
80. def OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.splitView line 426
81. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.splitView_left line 434
82. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.splitView_right line 436
83. def OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.powerTape line 440
84. def OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.powerView line 449
85. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.powerView_left line 460
86. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.powerView_right line 462
87. def OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.subtractTape line 466
88. def OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.subtractView line 477
89. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.subtractView_left line 490
90. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.subtractView_right line 492
91. def OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.rowTape line 496
92. def OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.rowView line 499
93. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.rowView_left line 509
94. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.rowView_right line 513
95. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.rowAlphabet_eq line 519
96. def OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.rowStateEquiv line 522
97. def OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.rowProgram line 528
98. def OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.program line 535
99. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.appendTrace line 561
100. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.tableBits_split line 565
101. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.splitInitialTapes line 571
102. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.splitResultTapes line 577
103. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.splitTrace line 583
104. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.powerTapes line 600
105. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.powerTrace line 605
106. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.affineTapes line 619
107. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.affineOutputTrace line 626
108. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.headersTrace line 668
109. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.copyPowerTrace line 684
110. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.subtractTapes line 698
111. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.subtractTrace line 705
112. def OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.rowBoolTapes line 720
113. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.transport_tapes_apply line 725
114. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.rowCastTapes line 732
115. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.rowInitialTapes line 738
116. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.rowFinalTapes line 745
117. def OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.rowTime line 753
118. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.frameTrace line 756
119. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.rowsTrace line 765
120. def OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.cleanupTime line 799
121. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.cleanupTrace line 801
122. def OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.otherTime line 836
123. def OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.totalTime line 843
124. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.vertexPaddingTrace line 846
125. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.rows_length_le line 882
126. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.darts_length_le line 887
127. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.power_length_bound line 891
128. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.initialOutput_length line 896
129. def OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.intermediateCoefficient line 903
130. def OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.intermediatePolynomial line 905
131. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.intermediate_bound line 908
132. def OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.otherPolynomial line 923
133. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.otherTime_le line 927
134. def OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.timePolynomial line 943
135. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.totalTime_le line 946
136. def OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.vertexPaddingInTime line 957
137. def OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.machine line 971
138. theorem OAI.BinPackingGames.Foundations.Complexity.MachineVertexPadding.alphabet_finite line 982