OAI/Computability/BinPacking/PCP/PCPSourceHardness.lean

GitHub source file

113 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.inputBits line 23
2. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.prefixWords line 26
3. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits line 31
4. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.cursorWords line 34
5. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.cursorBits line 37
6. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.prefixWords_zero line 40
7. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits_zero line 46
8. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.prefixWords_succ line 52
9. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits_succ line 65
10. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits_reverse_succ line 72
11. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.prefixWords_full line 79
12. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits_full line 88
13. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.cursorBits_zero line 93
14. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.cursorWords_succ line 98
15. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.cursorBits_succ line 109
16. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.cursorBits_full line 117
17. structure OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.Ready line 125
18. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.Ready.of_agree line 143
19. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.Ready.update_scan line 163
20. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.Ready.update_indexScan line 170
21. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.Ready.counter_succ line 177
22. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.Ready.counter_at_end line 184
23. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.Ready.cursor_at_end line 189
24. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopState.Ready.reversed_at_end line 193
25. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Finish.afterReversal line 207
26. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Finish.afterReversal_output line 210
27. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Finish.afterReversal_reversed line 214
28. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Finish.finishBudget line 218
29. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Finish.reverseInTime line 221
30. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Finish.cleared_eq_haltList line 235
31. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Finish.cleanupInTime line 242
32. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Finish.finishInTime line 258
33. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Finish.afterReversal_selected_length_le line 279
34. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Finish.stackLength_after_prefix line 286
35. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Finish.finishBudget_le_of_prefix line 298
36. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Finish.completedPolynomial line 320
37. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Finish.finishAfterPrefix line 325
38. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Finish.finishAfterPolynomialPrefix line 341
39. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Body.bodyTime line 365
40. structure OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Body.RowStepResult line 368
41. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Body.guardTapes line 378
42. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Body.parsedTapes line 382
43. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Body.workingTapes line 387
44. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Body.emittedTapes line 391
45. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Body.clearFieldsTapes line 396
46. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Body.resultTapes line 399
47. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Body.workingTapes_other line 404
48. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Body.workingTapes_counter line 414
49. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Body.workingTapes_cursor line 420
50. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Body.workingTapes_tail line 426
51. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Body.workingTapes_reverse line 432
52. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Body.workingTapes_head line 438
53. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Body.clearFieldsInTime line 445
54. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Body.incrementInTime line 467
55. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Body.emitterView_at line 482
56. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Body.context_rowState line 492
57. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Body.emitInTime line 501
58. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Body.result_ready line 539
59. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Body.workingOperands line 550
60. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Body.rowStep line 560
61. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.LoopInitialization.initialization_ready line 681
62. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Loop.zeroGuardInTime line 715
63. structure OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Loop.LoopResult line 729
64. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Loop.runRemaining line 741
65. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Loop.prefixTime line 773
66. structure OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Loop.PrefixResult line 789
67. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Loop.runPrefix line 799
68. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Loop.PrefixResult.reversed line 822
69. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Loop.PrefixResult.output line 826
70. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Runtime.prefixPolynomial line 837
71. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Runtime.prefixPolynomial_eval line 843
72. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Runtime.time line 850
73. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Runtime.tableOutputsInTime line 853
74. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Runtime.tablePolynomialTime line 869
75. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Driver.finiteAlphabet line 893
76. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Runtime.finiteAlphabet line 899
77. abbrev OAI.BinPackingGames.Foundations.PCP.RoundComputation.PreprocessingCertificate line 910
78. abbrev OAI.BinPackingGames.Foundations.PCP.RoundComputation.PoweringCertificate line 915
79. theorem OAI.BinPackingGames.Foundations.PCP.RoundComputation.powered_eq_transform line 921
80. def OAI.BinPackingGames.Foundations.PCP.RoundComputation.poweredPolynomialTimeOfCertificates line 926
81. def OAI.BinPackingGames.Foundations.PCP.RoundComputation.tablePolynomialTimeOfCertificates line 936
82. theorem OAI.BinPackingGames.Foundations.PCP.RoundComputation.powered_finiteAlphabet line 946
83. theorem OAI.BinPackingGames.Foundations.PCP.RoundComputation.finiteAlphabet line 954
84. def OAI.BinPackingGames.Foundations.PCP.RoundComputation.tablePolynomialTime line 966
85. theorem OAI.BinPackingGames.Foundations.PCP.RoundComputation.tablePolynomialTime_finite_alphabet line 974
86. def OAI.BinPackingGames.Foundations.PCP.PreprocessingFinishRuntime.finish line 992
87. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingFinishRuntime.output_eq_finish line 997
88. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingFinishRuntime.finish_degree_positive line 1001
89. def OAI.BinPackingGames.Foundations.PCP.PreprocessingFinishRuntime.computableInPolyTime line 1004
90. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingFinishRuntime.finite_alphabet line 1015
91. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRuntime.tablePolynomialTime line 1031
92. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRuntime.finiteAlphabet line 1044
93. def OAI.BinPackingCompleteness.PreprocessingMachine.preprocessing line 1061
94. theorem OAI.BinPackingCompleteness.PreprocessingMachine.preprocessing_finite_alphabet line 1064
95. def OAI.BinPackingCompleteness.PreprocessingMachine.round line 1068
96. theorem OAI.BinPackingCompleteness.PreprocessingMachine.round_finite_alphabet line 1073
97. def OAI.BinPackingCompleteness.PreprocessingMachine.computableInPolyTime line 1077
98. theorem OAI.BinPackingCompleteness.PreprocessingMachine.finite_alphabet line 1081
99. def OAI.BinPackingCompleteness.PCPSourceMachine.normalizedComputation line 1091
100. theorem OAI.BinPackingCompleteness.PCPSourceMachine.normalized_finiteAlphabet line 1098
101. def OAI.BinPackingCompleteness.PCPSourceMachine.rawSource line 1104
102. def OAI.BinPackingCompleteness.PCPSourceMachine.rawComputation line 1107
103. theorem OAI.BinPackingCompleteness.PCPSourceMachine.raw_finiteAlphabet line 1112
104. theorem OAI.BinPackingCompleteness.PCPSourceMachine.rawSource_nonempty line 1116
105. theorem OAI.BinPackingCompleteness.PCPSourceMachine.rawSource_satisfiable_iff line 1119
106. theorem OAI.BinPackingCompleteness.PCPSourceMachine.rawSource_distinct line 1124
107. theorem OAI.BinPackingCompleteness.PCPSourceMachine.rawSource_clauseGap line 1129
108. theorem OAI.BinPackingCompleteness.PCPSourceMachine.amplifiedSource_complete line 1135
109. theorem OAI.BinPackingCompleteness.PCPSourceMachine.amplifiedSource_sound line 1141
110. def OAI.BinPackingCompleteness.PCPSourceHardness.formula line 1153
111. def OAI.BinPackingCompleteness.PCPSourceHardness.computation line 1157
112. theorem OAI.BinPackingCompleteness.PCPSourceHardness.computation_finiteAlphabet line 1164
113. theorem OAI.BinPackingCompleteness.PCPSourceHardness.normalizedSource line 1171