OAI/Computability/BinPacking/Search/ExtensionVerifierPipeline.lean

GitHub source file

133 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BinPackingGap.ExtensionCapacityMachine.workBound line 17
2. theorem OAI.BinPackingGap.ExtensionCapacityMachine.scan_overfull line 26
3. structure OAI.BinPackingGap.ExtensionCapacityMachine.CoreRun line 30
4. def OAI.BinPackingGap.ExtensionCapacityMachine.coreRun line 39
5. def OAI.BinPackingGap.ExtensionCapacityMachine.innerInPolynomialTime line 205
6. abbrev OAI.BinPackingGap.ExtensionCapacityOuterMachine.Tape line 275
7. abbrev OAI.BinPackingGap.ExtensionCapacityOuterMachine.State line 276
8. abbrev OAI.BinPackingGap.ExtensionCapacityOuterMachine.Alphabet line 277
9. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.allTapes line 279
10. inductive OAI.BinPackingGap.ExtensionCapacityOuterMachine.CopyKind line 281
11. abbrev OAI.BinPackingGap.ExtensionCapacityOuterMachine.CopyKind.enumList line 285
12. theorem OAI.BinPackingGap.ExtensionCapacityOuterMachine.CopyKind.enumList_getElem?_ctorIdx_eq line 287
13. theorem OAI.BinPackingGap.ExtensionCapacityOuterMachine.CopyKind.enumList_nodup line 291
14. instance OAI.BinPackingGap.ExtensionCapacityOuterMachine.(instance at line 293) line 293
15. inductive OAI.BinPackingGap.ExtensionCapacityOuterMachine.Label line 297
16. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.clean line 308
17. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.innerTape line 310
18. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.innerView line 313
19. theorem OAI.BinPackingGap.ExtensionCapacityOuterMachine.innerView_left line 316
20. theorem OAI.BinPackingGap.ExtensionCapacityOuterMachine.innerView_right line 321
21. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.numberTapes line 330
22. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.copySource line 332
23. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.copyDestination line 337
24. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.afterCopy line 342
25. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.cleanupEntry line 347
26. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.jump line 350
27. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.finish line 353
28. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.program line 358
29. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.machine line 386
30. theorem OAI.BinPackingGap.ExtensionCapacityOuterMachine.machine_finiteAlphabet line 397
31. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.join line 401
32. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.stageTapes line 408
33. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.initialTapes line 415
34. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.resultTapes line 418
35. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.configuration line 421
36. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.initialCfg line 424
37. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.finalCfg line 427
38. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.inputLength line 429
39. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.scanResult line 432
40. theorem OAI.BinPackingGap.ExtensionCapacityOuterMachine.scanResult_eq_capacityChecks line 435
41. theorem OAI.BinPackingGap.ExtensionCapacityOuterMachine.selected_size_le_encoding line 446
42. theorem OAI.BinPackingGap.ExtensionCapacityOuterMachine.suffix_encoding_length_le line 463
43. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.roundBudget line 477
44. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.timePolynomial line 480
45. theorem OAI.BinPackingGap.ExtensionCapacityOuterMachine.totalBudget_le line 483
46. theorem OAI.BinPackingGap.ExtensionCapacityOuterMachine.guardStep line 504
47. theorem OAI.BinPackingGap.ExtensionCapacityOuterMachine.afterInnerStep line 514
48. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.copyInTime line 523
49. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.initialCopyInTime line 544
50. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.selectedInTime line 564
51. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.readyTapes line 582
52. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.prepareSelectedInTime line 588
53. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.innerExecution line 659
54. theorem OAI.BinPackingGap.ExtensionCapacityOuterMachine.inner_initial_configuration line 672
55. theorem OAI.BinPackingGap.ExtensionCapacityOuterMachine.inner_final_configuration line 681
56. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.afterInnerInTime line 695
57. theorem OAI.BinPackingGap.ExtensionCapacityOuterMachine.stage_lengthSum line 719
58. theorem OAI.BinPackingGap.ExtensionCapacityOuterMachine.ended_lengthSum line 726
59. theorem OAI.BinPackingGap.ExtensionCapacityOuterMachine.cleanup_tapes line 733
60. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.cleanupInTime line 739
61. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.emptyInTime line 773
62. abbrev OAI.BinPackingGap.ExtensionCapacityOuterMachine.InnerRuns line 803
63. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.roundFromInner line 811
64. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.loopBudget line 848
65. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.loopFromInner line 854
66. def OAI.BinPackingGap.ExtensionCapacityOuterMachine.outerInPolynomialTime line 921
67. inductive OAI.BinPackingGap.ExtensionVerifierMachine.Helper line 957
68. abbrev OAI.BinPackingGap.ExtensionVerifierMachine.Helper.enumList line 961
69. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Helper.enumList_getElem?_ctorIdx_eq line 964
70. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Helper.enumList_nodup line 968
71. instance OAI.BinPackingGap.ExtensionVerifierMachine.(instance at line 970) line 970
72. abbrev OAI.BinPackingGap.ExtensionVerifierMachine.LocalTape line 974
73. abbrev OAI.BinPackingGap.ExtensionVerifierMachine.LocalLabel line 981
74. abbrev OAI.BinPackingGap.ExtensionVerifierMachine.LocalState line 989
75. instance OAI.BinPackingGap.ExtensionVerifierMachine.(instance at line 997) line 997
76. instance OAI.BinPackingGap.ExtensionVerifierMachine.(instance at line 998) line 998
77. instance OAI.BinPackingGap.ExtensionVerifierMachine.(instance at line 999) line 999
78. instance OAI.BinPackingGap.ExtensionVerifierMachine.(instance at line 1000) line 1000
79. instance OAI.BinPackingGap.ExtensionVerifierMachine.(instance at line 1001) line 1001
80. instance OAI.BinPackingGap.ExtensionVerifierMachine.(instance at line 1002) line 1002
81. def OAI.BinPackingGap.ExtensionVerifierMachine.localInitial line 1004
82. def OAI.BinPackingGap.ExtensionVerifierMachine.localMain line 1013
83. def OAI.BinPackingGap.ExtensionVerifierMachine.localProgram line 1022
84. abbrev OAI.BinPackingGap.ExtensionVerifierMachine.Tape line 1032
85. abbrev OAI.BinPackingGap.ExtensionVerifierMachine.Registers line 1033
86. abbrev OAI.BinPackingGap.ExtensionVerifierMachine.State line 1034
87. abbrev OAI.BinPackingGap.ExtensionVerifierMachine.Alphabet line 1035
88. def OAI.BinPackingGap.ExtensionVerifierMachine.clean line 1037
89. def OAI.BinPackingGap.ExtensionVerifierMachine.register line 1039
90. theorem OAI.BinPackingGap.ExtensionVerifierMachine.register_clean line 1046
91. def OAI.BinPackingGap.ExtensionVerifierMachine.slot line 1050
92. def OAI.BinPackingGap.ExtensionVerifierMachine.view line 1059
93. theorem OAI.BinPackingGap.ExtensionVerifierMachine.view_slot line 1129
94. theorem OAI.BinPackingGap.ExtensionVerifierMachine.slot_view line 1132
95. def OAI.BinPackingGap.ExtensionVerifierMachine.put line 1142
96. theorem OAI.BinPackingGap.ExtensionVerifierMachine.put_slot line 1145
97. theorem OAI.BinPackingGap.ExtensionVerifierMachine.put_restrict line 1150
98. inductive OAI.BinPackingGap.ExtensionVerifierMachine.Gate line 1154
99. abbrev OAI.BinPackingGap.ExtensionVerifierMachine.Gate.enumList line 1158
100. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Gate.enumList_getElem?_ctorIdx_eq line 1161
101. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Gate.enumList_nodup line 1165
102. instance OAI.BinPackingGap.ExtensionVerifierMachine.(instance at line 1167) line 1167
103. inductive OAI.BinPackingGap.ExtensionVerifierMachine.Copy line 1171
104. abbrev OAI.BinPackingGap.ExtensionVerifierMachine.Copy.enumList line 1175
105. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Copy.enumList_getElem?_ctorIdx_eq line 1178
106. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Copy.enumList_nodup line 1182
107. instance OAI.BinPackingGap.ExtensionVerifierMachine.(instance at line 1184) line 1184
108. def OAI.BinPackingGap.ExtensionVerifierMachine.allTapes line 1188
109. inductive OAI.BinPackingGap.ExtensionVerifierMachine.Label line 1190
110. def OAI.BinPackingGap.ExtensionVerifierMachine.entry line 1199
111. def OAI.BinPackingGap.ExtensionVerifierMachine.cleanupEntry line 1201
112. def OAI.BinPackingGap.ExtensionVerifierMachine.afterHelper line 1204
113. def OAI.BinPackingGap.ExtensionVerifierMachine.gateTape line 1213
114. def OAI.BinPackingGap.ExtensionVerifierMachine.afterGate line 1220
115. def OAI.BinPackingGap.ExtensionVerifierMachine.copySource line 1227
116. def OAI.BinPackingGap.ExtensionVerifierMachine.copyDestination line 1231
117. def OAI.BinPackingGap.ExtensionVerifierMachine.afterCopy line 1235
118. def OAI.BinPackingGap.ExtensionVerifierMachine.jump line 1240
119. def OAI.BinPackingGap.ExtensionVerifierMachine.program line 1245
120. def OAI.BinPackingGap.ExtensionVerifierMachine.machine line 1263
121. theorem OAI.BinPackingGap.ExtensionVerifierMachine.machine_finiteAlphabet line 1274
122. def OAI.BinPackingGap.ExtensionVerifierMachine.cfg line 1278
123. def OAI.BinPackingGap.ExtensionVerifierMachine.stagedTapes line 1281
124. def OAI.BinPackingGap.ExtensionVerifierMachine.fieldInput line 1287
125. def OAI.BinPackingGap.ExtensionVerifierMachine.oneStep line 1290
126. def OAI.BinPackingGap.ExtensionVerifierMachine.join line 1296
127. def OAI.BinPackingGap.ExtensionVerifierMachine.enlarge line 1304
128. def OAI.BinPackingGap.ExtensionVerifierMachine.callInTime line 1311
129. theorem OAI.BinPackingGap.ExtensionVerifierMachine.gateStep line 1335
130. def OAI.BinPackingGap.ExtensionVerifierMachine.copyInTime line 1343
131. theorem OAI.BinPackingGap.ExtensionVerifierMachine.cleanup_tapes line 1355
132. def OAI.BinPackingGap.ExtensionVerifierMachine.resultTapes line 1361
133. def OAI.BinPackingGap.ExtensionVerifierMachine.cleanupInTime line 1364