OAI/Computability/BinPacking/CookLevin/PaddingCellsMachine.lean

GitHub source file

123 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.Ports line 14
2. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.Alphabet line 15
3. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.tapes line 17
4. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.tapes_input line 21
5. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.tapes_output line 26
6. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.tapes_count line 30
7. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.tapes_other line 34
8. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.update_input line 39
9. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.update_output line 50
10. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.update_count line 61
11. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.TruthTable line 67
12. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.tableAt line 69
13. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.rowFrom line 72
14. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.rowTokens line 75
15. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.streamTokens line 77
16. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.rowFrom_succ line 80
17. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.rowFrom_length line 89
18. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.streamTokens_length line 95
19. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.streamTokens_eq_rows line 105
20. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.tokenBits_cons line 111
21. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.tokenBits_append line 115
22. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.Label line 119
23. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.statement line 124
24. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.Agrees line 139
25. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.EmitAgrees line 143
26. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.scanStep_nil line 147
27. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.scanStep_cons line 157
28. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.emitStep line 168
29. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.finishRowStep line 183
30. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.rowTrace line 194
31. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.streamTrace line 222
32. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.streamInTime line 260
33. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.copyAndStreamTrace line 274
34. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.program line 307
35. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.machine line 311
36. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.machineInTime line 322
37. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.symbolTruth line 338
38. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.prefixTruth line 345
39. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.symbolTruth_eq_initialCellTokens line 348
40. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.prefixTruth_eq_initialCellTokens line 360
41. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.prefixRow_eq_initialCellTokens line 368
42. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsMachine.prefixStream_eq_initialCells line 382
43. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationControl.tokens line 409
44. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationControl.tokens_length line 415
45. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationControl.cells line 419
46. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationControl.configurationTokens_eq line 425
47. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationControl.flatten_singletons line 434
48. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationControl.initializationTokens_eq_blocks line 440
49. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationControl.Ports line 450
50. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationControl.emitted line 455
51. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationControl.emitted_reversed line 460
52. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationControl.emitted_count line 464
53. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationControl.emitted_other line 468
54. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationControl.exitStatement line 472
55. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationControl.literalStatement line 477
56. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationControl.literalStep line 482
57. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationControl.literalTrace line 490
58. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationControl.statement line 500
59. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationControl.trace line 503
60. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsCapacity.Ports line 520
61. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsCapacity.corePorts line 522
62. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsCapacity.capacity_distinct line 529
63. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsCapacity.tapes line 535
64. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsCapacity.tapes_input line 540
65. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsCapacity.tapes_output line 544
66. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsCapacity.tapes_count line 548
67. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsCapacity.tapes_capacity line 552
68. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsCapacity.tapes_other line 558
69. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsCapacity.update_input line 564
70. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsCapacity.update_capacity line 570
71. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsCapacity.statement line 583
72. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsCapacity.Agrees line 595
73. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsCapacity.emitAgrees line 601
74. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsCapacity.scanStep_nil line 609
75. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsCapacity.scanStep_cons line 621
76. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsCapacity.streamTrace_add line 635
77. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsCapacity.streamTrace line 683
78. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InputCellsCapacity.copyAndStreamTrace line 699
79. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsPrefixStage.Ports line 740
80. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsPrefixStage.capacityPorts line 742
81. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsPrefixStage.saved_distinct line 750
82. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsPrefixStage.scratch_distinct line 755
83. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsPrefixStage.prepared_eq line 759
84. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsPrefixStage.Label line 773
85. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsPrefixStage.streamLabels line 778
86. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsPrefixStage.statement line 784
87. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsPrefixStage.Agrees line 797
88. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsPrefixStage.stream_agrees line 802
89. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsPrefixStage.trace line 810
90. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsPrefixStage.inTime line 838
91. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.Ports line 866
92. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.corePorts line 868
93. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.literalPorts line 876
94. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.frame line 879
95. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.frame_remaining line 883
96. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.frame_output line 888
97. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.frame_count line 893
98. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.frame_other line 898
99. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.frame_input line 904
100. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.update_remaining line 909
101. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.literal_emitted line 915
102. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.repeatedRows line 927
103. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.repeatedRows_zero line 930
104. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.repeatedRows_succ line 932
105. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.repeatedRows_length line 936
106. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.statement line 942
107. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.step_zero line 952
108. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.step_succ line 961
109. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.trace line 971
110. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.frame_eq_capacityTapes line 1002
111. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.capacityTrace line 1015
112. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.inTime line 1030
113. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.blankRow line 1053
114. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.blankRow_length line 1058
115. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.initialCellTokens_padding line 1061
116. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.cellRow_padding line 1072
117. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.cellsInterval line 1080
118. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.cellsInterval_padding line 1087
119. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.verifierStatement line 1102
120. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.verifierTrace line 1106
121. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.paddingCellsTrace line 1120
122. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.machine line 1142
123. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PaddingCellsMachine.machineTrace line 1154