OAI/Computability/BinPacking/CookLevin/ProducerFrontStage.lean

GitHub source file

163 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerBootstrap.Ports line 16
2. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerBootstrap.Label line 18
3. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerBootstrap.Label.enumList line 22
4. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerBootstrap.Label.enumList_getElem?_ctorIdx_eq line 24
5. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerBootstrap.Label.enumList_nodup line 28
6. instance OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerBootstrap.(instance at line 30) line 30
7. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerBootstrap.State line 34
8. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerBootstrap.Ready line 36
9. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerBootstrap.copied line 43
10. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerBootstrap.prepared line 46
11. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerBootstrap.statement line 50
12. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerBootstrap.prepared_current line 59
13. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerBootstrap.prepared_source line 63
14. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerBootstrap.prepared_count line 67
15. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerBootstrap.prepared_cursor line 71
16. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerBootstrap.prepared_scratch line 75
17. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerBootstrap.prepared_other line 79
18. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerBootstrap.seedTrace line 83
19. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerBootstrap.trace line 96
20. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerBootstrap.inTime line 117
21. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.Ports line 141
22. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.Alphabet line 142
23. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.prefixMap line 144
24. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.loopMap line 145
25. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.paddingMap line 146
26. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.prefixPorts line 148
27. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.loopPorts line 149
28. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.paddingPorts line 150
29. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.WorkEmpty line 152
30. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.Ready line 155
31. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.workEmpty_emitted line 161
32. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.frame line 168
33. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.ext_ports line 171
34. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.frame_emitted line 180
35. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.update_emitted_capacity line 185
36. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.frame_seed line 194
37. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.seed_ready line 202
38. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.Label line 222
39. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.prefixLabels line 229
40. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.payloadLabels line 232
41. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.statement line 235
42. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.Agrees line 253
43. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.prefixTrace line 265
44. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.preparePayloadTrace line 296
45. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.payloadTrace line 329
46. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.paddingTrace line 346
47. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.cleanupTrace line 379
48. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.tokens line 407
49. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.steps line 413
50. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.trace line 417
51. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsMachine.steps_le line 449
52. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssemblyBounds.cellsPolynomial line 466
53. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssemblyBounds.timePolynomial line 474
54. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssemblyBounds.capacityPolynomial_eval line 477
55. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssemblyBounds.cellsPolynomial_eval line 482
56. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssemblyBounds.cells_steps_le line 494
57. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssemblyBounds.steps_le line 503
58. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.Tape line 518
59. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.validitySlots line 524
60. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.validitySlots_apply line 531
61. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.controlPorts line 539
62. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.validityReady line 544
63. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.control_emitted_eq line 553
64. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.validityReady_control line 557
65. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.validitySlots_not_cellWork line 564
66. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.controlTrace line 568
67. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.cellsSlots line 586
68. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.CodeLabel line 591
69. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.Label line 597
70. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.placedControl line 601
71. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.cellsLabels line 606
72. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.Ready line 610
73. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.Ready.afterEmitted line 619
74. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.Ready.cellsReady line 634
75. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.Ready.validityReady line 646
76. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.capacity_within line 655
77. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.statement line 661
78. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.Agrees line 672
79. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.steps line 676
80. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.cellsTokens_eq line 682
81. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.trace line 690
82. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.program line 732
83. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.machine line 736
84. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.machineTrace line 748
85. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.timePolynomial line 757
86. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.steps_le_timePolynomial line 760
87. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.inPolynomialTime line 764
88. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationAssembly.machineInPolynomialTime line 779
89. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.Work line 795
90. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.Tape line 803
91. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.Alphabet line 804
92. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.State line 805
93. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.initialState line 806
94. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.frontPorts line 808
95. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.raw line 811
96. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.framed line 812
97. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.clock line 813
98. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.q line 815
99. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.capacity line 816
100. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.countdown line 817
101. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.freeInputs line 818
102. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.shared line 820
103. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.current line 822
104. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.roots line 823
105. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.records line 824
106. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.tokens line 825
107. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.count line 826
108. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.cursor line 827
109. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.output line 828
110. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.clock_injective line 830
111. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.clock_eq_iff line 836
112. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.clock_ne_raw line 839
113. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.raw_ne_clock line 843
114. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.clock_ne_framed line 846
115. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.framed_ne_clock line 850
116. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.raw_ne_framed line 853
117. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.transitionTape line 856
118. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.transitionPorts line 863
119. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.transitionPorts_apply line 886
120. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.forestPorts line 889
121. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.termPorts line 892
122. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.initializationTape line 895
123. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.initializationPorts line 905
124. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.initializationPorts_apply line 918
125. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.finishTape line 921
126. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.finishPorts line 930
127. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.finishPorts_apply line 937
128. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.bootstrapPorts line 940
129. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.bootstrap_source line 947
130. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.bootstrap_current line 948
131. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.bootstrap_scratch line 949
132. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.bootstrap_count line 951
133. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.bootstrap_cursor line 952
134. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.empty line 954
135. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.frontTapes line 956
136. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.frontTapes_at line 961
137. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.frontTapes_work line 965
138. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.front_fill line 969
139. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.initialTapes line 978
140. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.initialTapes_eq line 981
141. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.frontendPrepared line 992
142. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.frontendPrepared_raw line 995
143. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.frontendPrepared_framed line 998
144. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.frontendPrepared_clock line 1002
145. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.frontendPrepared_work line 1007
146. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.bootstrapReady line 1010
147. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.bootstrapPrepared line 1015
148. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.bootstrapPrepared_front line 1018
149. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.bootstrapPrepared_current line 1024
150. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.bootstrapPrepared_count line 1030
151. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.bootstrapPrepared_cursor line 1035
152. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.bootstrapPrepared_other line 1040
153. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.initializationBase line 1045
154. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.bootstrap_initialization_view line 1054
155. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerArena.initializationValidityReady line 1066
156. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerFrontStage.Label line 1079
157. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerFrontStage.entry line 1081
158. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerFrontStage.statement line 1083
159. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerFrontStage.timePolynomial line 1089
160. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerFrontStage.timePolynomial_eval line 1093
161. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerFrontStage.inTime line 1098
162. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerFrontStage.program line 1124
163. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerFrontStage.programInTime line 1127