OAI/Computability/BinPacking/Computation/MachineLazyRows.lean

GitHub source file

119 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedIndex line 11
2. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow line 16
3. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_eq line 21
4. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_tail line 29
5. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_reverse line 34
6. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_relation line 47
7. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_words line 60
8. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.prefixWords line 67
9. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.suffixWords line 70
10. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.prefixWords_length line 73
11. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.tableWords_at_row line 78
12. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.tableWords_drop_row line 90
13. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.selected_reverse line 96
14. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.remaining_relation line 103
15. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.Tape line 110
16. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.Buffer line 111
17. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.State line 112
18. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.Alphabet line 113
19. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.zeroBuffer line 115
20. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.lookupTape line 117
21. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.lookupTape_injective line 119
22. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.source_outside line 126
23. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.fields line 132
24. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.fields_zero line 134
25. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.fields_one line 135
26. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.fields_two line 136
27. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.fields_separate line 138
28. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.copyStateEquiv line 141
29. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.Label line 147
30. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.relationCopyAt line 153
31. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.instruction line 158
32. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.machine line 170
33. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.looked line 181
34. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.copied line 185
35. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.affined line 190
36. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.looked_other line 195
37. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.looked_reverse line 200
38. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.looked_relation line 204
39. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.vectorBits_eq_encodedBlock line 214
40. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.relationBits_eq_encodedBlock line 226
41. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.relationCopy_step line 230
42. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.relationCopy_pushBound line 259
43. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.copied_other line 264
44. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.copied_reverse line 270
45. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.copied_relation line 275
46. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.affined_other line 279
47. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.affined_reverse line 284
48. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.affined_relation line 288
49. structure OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.Input line 292
50. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.emittedWords line 301
51. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.affined_fields line 304
52. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.rowSteps line 314
53. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.steps line 317
54. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.finalTapes line 321
55. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.join_trace line 329
56. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.lookupTrace line 333
57. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.copyTrace line 347
58. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.affineTrace line 362
59. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.emitTrace line 383
60. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.traceAt line 409
61. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.timeBound line 425
62. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.steps_le line 428
63. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalRow.machineInTime line 445
64. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.Label line 470
65. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.State line 471
66. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.addressIndex line 473
67. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.addressIndex_injective line 475
68. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.fields line 479
69. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.reindexInstruction line 481
70. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.instruction line 490
71. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.reindexRowBits line 495
72. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.reindexMappedTapes line 499
73. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.reindexResultTapes line 503
74. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.reindexSteps line 508
75. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.rowBits line 512
76. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.mappedTapes line 515
77. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.resultTapes line 518
78. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.steps line 523
79. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.reindexRowTrace line 526
80. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.rowTrace line 589
81. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.rowBits_eq_moveRow line 610
82. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.machine line 618
83. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.Buffer line 629
84. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.StreamState line 630
85. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.streamClean line 632
86. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.relationStateEquiv line 635
87. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.streamRelationCopy line 642
88. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.streamRelationCopy_step line 647
89. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.bodyIndex line 672
90. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.bodyIndex_injective line 674
91. inductive OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.StreamLabel line 679
92. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.streamInstruction line 685
93. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.inputRowBits line 703
94. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.streamRowSteps line 706
95. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.streamResultTapes line 711
96. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.joinTrace line 716
97. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.streamRowTrace line 720
98. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.VertexLabel line 908
99. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.vertexInstruction line 910
100. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.recordsInput line 920
101. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.recordsOutput line 923
102. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.streamFrame line 926
103. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.vertexSteps line 931
104. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.recordsInput_eq_codec line 937
105. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.streamFrame_afterRow line 946
106. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.vertexSuffixTrace line 963
107. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.vertexTrace line 1047
108. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.encodeWords_flatMap line 1063
109. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.recordsOutput_lazy line 1069
110. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.valueBound line 1084
111. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.rowSizeBound line 1085
112. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.rowCostBound line 1086
113. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.reindexValue_le line 1089
114. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.reindexRowBits_length_le line 1098
115. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.streamRowSteps_le line 1108
116. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.vertexSteps_le_capacity line 1120
117. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.vertexSteps_le line 1145
118. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.vertexInTime line 1151
119. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyRows.vertexMachine line 1172