OAI/Computability/BinPacking/CookLevin/Completeness.lean

GitHub source file

134 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.loweringSteps_eq_forestSteps line 27
2. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.verifier_steps_eq line 39
3. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.verifier_steps_le line 46
4. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.verifierInPolynomialTime line 54
5. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.verifierPlacedInPolynomialTime line 68
6. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.verifierInitialTapes line 97
7. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.verifierFinalTapes line 101
8. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.verifierInPolynomialTime line 104
9. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.verifierInPolynomialTime_steps line 116
10. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.verifierPlacedInPolynomialTime line 121
11. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.verifierFinal_output line 135
12. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.verifierFinal_clean line 139
13. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.verifierPlaced_output line 143
14. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.verifierPlaced_clean line 149
15. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitFinish.verifierPlaced_other line 154
16. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.Ports line 165
17. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.State line 166
18. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.freeInputs line 168
19. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.initialGates line 171
20. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.preparedLocal line 175
21. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.snapshotLocal line 179
22. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.finishedLocal line 186
23. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.initialCompile line 189
24. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.initialRecords line 202
25. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.finalLocal_eq line 213
26. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.lowerSteps line 233
27. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.Ready line 241
28. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.Prepared line 245
29. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.result line 249
30. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.prepared_emitted line 253
31. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.result_emitted line 271
32. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.lowerTrace line 286
33. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.result_at line 310
34. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.result_other line 316
35. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.lowerTimePolynomial line 321
36. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.lowerSteps_le line 325
37. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.lowerInTime line 360
38. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.FullPorts line 373
39. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.Label line 379
40. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.entry line 381
41. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.emitLabels line 383
42. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.statement line 387
43. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.Agrees line 393
44. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.FullReady line 397
45. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.steps line 402
46. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.trace line 405
47. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.program line 424
48. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.machine line 428
49. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.machineTrace line 440
50. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.timePolynomial line 448
51. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.steps_le_timePolynomial line 451
52. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.verifierPlacedInPolynomialTime line 457
53. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationStage.verifierInPolynomialTime line 470
54. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.localBase line 485
55. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary line 488
56. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.finished line 492
57. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.fill_fill line 496
58. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_view line 509
59. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.finished_view line 515
60. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_other line 521
61. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.finished_other line 526
62. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.fill_boundary line 531
63. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.fill_finished line 537
64. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.iteration_handoff line 543
65. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.acceptance_handoff line 548
66. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_current line 553
67. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_roots line 560
68. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_records line 566
69. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_countdown line 572
70. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.finished_current line 578
71. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.finished_roots line 585
72. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.finished_records line 591
73. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.finished_countdown line 597
74. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_private line 603
75. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.finished_private line 613
76. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.private_finish_outside line 623
77. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.private_validity_outside line 630
78. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.private_cells_outside line 637
79. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.bootstrap_clock line 644
80. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.bootstrap_raw line 650
81. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.bootstrap_work line 656
82. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.bootstrap_extra line 662
83. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_raw line 674
84. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_q line 680
85. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_capacity line 686
86. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.initial_result_view line 692
87. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.initial_result_eq_boundary line 716
88. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.initialization_emitted_fill line 730
89. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.initialization_lowering_handoff line 740
90. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.clock_outside line 752
91. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.freeInputs_outside line 767
92. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.framed_outside line 770
93. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_clock line 783
94. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.finished_clock line 789
95. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_framed line 795
96. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.finished_framed line 802
97. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.finished_freeInputs line 809
98. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.finish_view line 814
99. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.circuitFinish_view line 828
100. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.bootstrap_emitter_ready line 840
101. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerHandoffs.bootstrap_lowerer_ready line 853
102. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTailStage.IterateLabel line 890
103. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTailStage.Label line 892
104. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTailStage.entry line 895
105. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTailStage.statement line 898
106. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTailStage.initial line 909
107. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTailStage.afterIteration line 912
108. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTailStage.afterAcceptance line 915
109. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTailStage.terminal line 918
110. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTailStage.timePolynomial line 922
111. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTailStage.finish_entry line 927
112. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTailStage.inTime line 935
113. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTailStage.program line 972
114. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTailStage.programInTime line 975
115. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTailStage.terminal_output line 982
116. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerMachine.Label line 1007
117. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerMachine.initPorts line 1010
118. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerMachine.initLabels line 1016
119. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerMachine.entry line 1019
120. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerMachine.program line 1021
121. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerMachine.timePolynomial line 1028
122. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerMachine.initializerReady line 1032
123. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerMachine.inTime line 1037
124. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerMachine.rawProgram line 1064
125. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerMachine.initialCfg line 1071
126. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerMachine.terminalRun line 1081
127. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerMachine.cleanupTapes line 1092
128. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerMachine.cleanup_complete line 1095
129. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerMachine.computableInPolyTime line 1099
130. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerMachine.finiteAlphabet line 1105
131. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Completeness.circuitProducerFinite line 1117
132. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.Completeness.verifierReduction line 1123
133. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Completeness.verifierReduction_finiteAlphabet line 1129
134. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Completeness.threeSATReduction line 1134