OAI/Computability/BinPacking/Computation/PoweringMachineRowBody.lean

GitHub source file

117 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineEqualityField.Alphabet line 17
2. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineEqualityField.Tape line 18
3. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineEqualityField.State line 19
4. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineEqualityField.Label line 20
5. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineEqualityField.entry line 23
6. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineEqualityField.instruction line 25
7. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineEqualityField.endpoint line 41
8. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineEqualityField.resultBit line 45
9. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineEqualityField.wordTapes line 49
10. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineEqualityField.finalTapes line 55
11. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineEqualityField.steps line 65
12. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineEqualityField.steps_le line 72
13. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineEqualityField.wordTapes_other line 88
14. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineEqualityField.wordTapes_role line 108
15. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineEqualityField.finalTapes_other line 129
16. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineEqualityField.finalTapes_role line 144
17. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineEqualityField.finalTapes_output line 155
18. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineEqualityField.joinTrace line 168
19. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineEqualityField.fieldTrace line 172
20. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineEqualityField.fieldInTime line 274
21. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineEqualityField.machine line 297
22. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement line 320
23. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_injective line 323
24. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_table line 327
25. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_query line 331
26. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_scan line 335
27. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_reverse line 339
28. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_scratch line 343
29. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_output line 347
30. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_start line 351
31. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_succ line 355
32. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowHeaders.Label line 359
33. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowHeaders.entry line 362
34. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowHeaders.tailEntry line 364
35. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowHeaders.affineInstruction line 367
36. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowHeaders.instruction line 374
37. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowHeaders.afterReverse line 387
38. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowHeaders.finalTapes line 392
39. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowHeaders.steps line 401
40. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowHeaders.headerTrace line 407
41. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowHeaders.finalTapes_other line 479
42. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowHeaders.finalTapes_shared line 502
43. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowHeaders.steps_le line 516
44. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowHeaders.machine line 532
45. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineField.Tape line 551
46. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineField.State line 552
47. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineField.Label line 554
48. instance OAI.BinPackingGames.Foundations.Complexity.PoweringMachineField.labelFintype line 558
49. instance OAI.BinPackingGames.Foundations.Complexity.PoweringMachineField.labelDecidableEq line 561
50. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineField.entry line 564
51. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineField.instruction line 568
52. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineField.finalTapes line 577
53. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineField.steps line 587
54. structure OAI.BinPackingGames.Foundations.Complexity.PoweringMachineField.Ready line 591
55. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineField.finalTapes_role line 599
56. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineField.ready_finalTapes line 614
57. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineField.finalTapes_other line 631
58. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineField.fieldTrace line 644
59. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineField.finalTapes_output line 666
60. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachinePlan.Command line 698
61. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachinePlan.LocalLabel line 699
62. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachinePlan.Label line 700
63. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachinePlan.entry line 702
64. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachinePlan.instruction line 706
65. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachinePlan.result line 713
66. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachinePlan.finalTapes line 717
67. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachinePlan.steps line 721
68. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachinePlan.planTrace line 726
69. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachinePlan.ready_finalTapes line 752
70. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachinePlan.finalTapes_output line 765
71. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachinePlan.boundedRowPlan line 786
72. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachinePlan.boundedRowPlan_values line 793
73. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachinePlan.rowPlan_output line 798
74. def OAI.BinPackingGames.Foundations.Complexity.PoweringPlanBudget.fieldBudget line 820
75. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringPlanBudget.field_steps_le line 823
76. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringPlanBudget.plan_steps_le line 848
77. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringPlanBudget.boundedRowPlan_length line 865
78. def OAI.BinPackingGames.Foundations.Complexity.PoweringPlanBudget.rowBudget line 871
79. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringPlanBudget.rowPlan_steps_le line 875
80. def OAI.BinPackingGames.Foundations.Complexity.PoweringPlanBudget.planInTime line 888
81. def OAI.BinPackingGames.Foundations.Complexity.PoweringPlanBudget.rowPlanInTime line 907
82. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.capacity line 942
83. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.bufferSize line 943
84. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.State line 944
85. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.commands line 946
86. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.Label line 949
87. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.planMain line 953
88. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.plan_entry_eq line 960
89. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.entry line 967
90. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement line 970
91. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_output line 975
92. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_other line 980
93. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_injective line 986
94. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_excludes_data line 1002
95. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.instruction line 1014
96. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.afterPlan line 1025
97. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.rowRelation line 1029
98. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.rowWords line 1034
99. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.afterEmit line 1039
100. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes line 1046
101. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.planSteps line 1054
102. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.planSteps_eq line 1059
103. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.steps line 1072
104. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.Ready line 1077
105. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.plan_other line 1082
106. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.afterEmit_data line 1095
107. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.afterEmit_role line 1102
108. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.afterEmit_ready line 1112
109. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes_data line 1134
110. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes_ready line 1147
111. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes_other line 1172
112. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.rowBlock_eq_rowRelation line 1191
113. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes_output line 1207
114. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.rowTrace line 1236
115. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.budget line 1288
116. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.steps_le line 1292
117. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRowBody.rowInTime line 1303