OAI/Computability/BinPacking/Computation/MachineExpanderFamilyAffine.lean

GitHub source file

176 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.ExtraTape line 10
2. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.ExtraTape.enumList line 14
3. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.ExtraTape.enumList_getElem?_ctorIdx_eq line 16
4. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.ExtraTape.enumList_nodup line 20
5. instance OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.(instance at line 22) line 22
6. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.Tape line 26
7. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.Alphabet line 28
8. instance OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.alphabetFintype line 32
9. inductive OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.OuterLabel line 35
10. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.OuterLabel.enumList line 39
11. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.OuterLabel.enumList_getElem?_ctorIdx_eq line 42
12. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.OuterLabel.enumList_nodup line 46
13. instance OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.(instance at line 48) line 48
14. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.Label line 52
15. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.Position line 53
16. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.State line 54
17. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.RowStatePrefix line 55
18. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.guardStates line 58
19. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.guardStates_apply line 65
20. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.guardStates_symm_apply line 69
21. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.rowFactor_pos line 72
22. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.zeroPosition line 76
23. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.nextPosition line 79
24. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.positionPair line 82
25. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.caller line 85
26. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.boundaryState line 87
27. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.initialState line 92
28. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.prepareState line 96
29. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.resetState line 100
30. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.clearRegister line 104
31. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.advancePositionState line 107
32. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.resetPositionState line 110
33. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.vertexGuardCore line 113
34. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.outerStatement line 123
35. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.rowReturn line 143
36. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.program line 145
37. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.program_row line 150
38. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.program_outer line 156
39. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.rowExecution line 160
40. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.rowExecution_steps line 172
41. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.rowTapes line 180
42. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.extraTapes line 186
43. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes line 190
44. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.initialTapes line 194
45. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.finalTapes line 200
46. inductive OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.ExtraTape line 211
47. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.ExtraTape.enumList line 215
48. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.ExtraTape.enumList_getElem?_ctorIdx_eq line 218
49. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.ExtraTape.enumList_nodup line 222
50. instance OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.(instance at line 224) line 224
51. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.Tape line 228
52. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.Alphabet line 229
53. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.BoolAlphabet line 231
54. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.alphabet_eq line 233
55. instance OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.alphabetFintype line 239
56. inductive OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.AffinePhase line 243
57. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.AffinePhase.enumList line 247
58. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.AffinePhase.enumList_getElem?_ctorIdx_eq line 249
59. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.AffinePhase.enumList_nodup line 253
60. instance OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.(instance at line 255) line 255
61. inductive OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.AffineLabel line 259
62. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.AffineLabel.enumList line 263
63. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.AffineLabel.enumList_getElem?_ctorIdx_eq line 265
64. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.AffineLabel.enumList_nodup line 269
65. instance OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.(instance at line 271) line 271
66. inductive OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.OuterLabel line 275
67. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.Label line 283
68. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.State line 284
69. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.RegisterAmbient line 285
70. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.registerStates line 288
71. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.registerStates_apply line 295
72. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.registerStates_symm_apply line 299
73. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.caller line 302
74. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.initialState line 305
75. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.normalizeState line 309
76. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.initialEncoding line 313
77. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.initialEncoding_eq_family line 315
78. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.tableTape line 318
79. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.inputVertexTape line 319
80. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.vertexCountTape line 320
81. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.resultTape line 321
82. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.affineSource line 323
83. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.affineDestination line 327
84. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.affineCoefficient line 331
85. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.affineExit line 335
86. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.affineStatement line 339
87. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.drainStatement line 357
88. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.boolOuterStatement line 365
89. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.outerStatement line 394
90. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.tableReturn line 398
91. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.program line 400
92. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.program_table line 405
93. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.program_outer line 412
94. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.boolView line 416
95. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.boolView_outer line 420
96. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.tableExecution line 429
97. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.tableExecution_steps line 441
98. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.tableFrame line 450
99. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.extraFrame line 456
100. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.boundaryTapes line 461
101. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.initialTapes line 465
102. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.familyTapes line 472
103. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.caller_boundaryState line 486
104. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.prepareState_boundaryState line 490
105. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.clearRegister_boundaryState line 495
106. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.caller_prepareState line 500
107. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.caller_resetState line 503
108. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.caller_clearRegister line 506
109. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.caller_advancePositionState line 509
110. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.caller_resetPositionState line 512
111. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.nextPosition_val_of_lt line 515
112. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes_update_count line 519
113. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes_increment_vertex line 529
114. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.initialTapes_initialize line 542
115. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.initializeStep line 556
116. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.initialize_boundaryStep line 565
117. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.vertexGuard_succStep line 580
118. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.vertexGuard_zeroStep line 592
119. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.vertexGuard_boundary_succStep line 603
120. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.vertexGuard_boundary_zeroStep line 616
121. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.prepareRowStep line 626
122. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.afterRow_moreStep line 634
123. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.afterRow_lastStep line 643
124. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.afterRow_last_boundaryStep line 653
125. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.reverseOutput_consStep line 672
126. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.reverseOutput_nilStep line 684
127. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.doneStep line 696
128. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.boolWord line 712
129. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.toBoolWord line 717
130. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.fromBoolTapes line 722
131. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.toBoolTapes line 725
132. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.toBoolWord_boolWord line 728
133. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.boolWord_toBoolWord line 734
134. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.toBool_fromBool line 740
135. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.fromBool_toBool line 745
136. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.transport_tapes_apply line 750
137. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.toBoolTapes_eq_transport line 757
138. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.fromBoolTapes_eq_transport line 765
139. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.fromBoolTapes_update line 773
140. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.toBoolTapes_update line 782
141. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.configuration_fromBool line 792
142. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.configuration_toBool line 798
143. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.controlStatementInverse line 811
144. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.controlTrace line 818
145. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.controlDrainTrace line 842
146. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.controlTransferTrace line 861
147. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.clearRegister line 886
148. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.registerStates_reset line 889
149. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.clearRegister_idempotent line 893
150. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.caller_clearRegister line 896
151. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.clearRegister_position line 899
152. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.clearRegister_register line 902
153. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.boolTraceActual line 907
154. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.drainBoolTrace line 918
155. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.transferBoolTrace line 935
156. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.installedTapes line 958
157. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.cleanedCounterTapes line 965
158. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.installTableBoolTrace line 968
159. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.cleanupCountersBoolTrace line 1027
160. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.installTableTrace line 1045
161. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.cleanupCountersTrace line 1058
162. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.installTableInTime line 1069
163. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.cleanupCountersInTime line 1084
164. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.affine_source_ne_scratch line 1101
165. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.affine_source_ne_destination line 1104
166. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.affine_scratch_ne_destination line 1107
167. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes line 1110
168. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_other line 1117
169. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_source line 1123
170. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_scratch line 1128
171. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_destination line 1133
172. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.affinePhaseBoolTrace line 1141
173. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.affinePhaseTrace line 1186
174. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.affinePhaseInTime line 1201
175. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.copyCountInTime line 1214
176. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.multiplySizeInTime line 1231