OAI/Computability/BinPacking/CookLevin/ForestStage.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestPlacement.Tapes line 13
2. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestPlacement.fill line 15
3. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestPlacement.fill_at line 18
4. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestPlacement.fill_other line 22
5. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestPlacement.fill_self line 26
6. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestPlacement.fill_update line 35
7. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestPlacement.fill_comp line 51
8. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestPlacement.placedLabel line 78
9. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestPlacement.configuration line 82
10. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestPlacement.statement line 89
11. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestPlacement.stepAux_simulation line 104
12. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestPlacement.step_simulation line 130
13. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestPlacement.trace line 149
14. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestPlacement.execution line 163
15. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.RootRefresh.Alphabet line 185
16. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.RootRefresh.guard line 187
17. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.RootRefresh.guardStep_nil line 195
18. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.RootRefresh.guardStep_nonempty line 206
19. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.RootRefresh.fieldTapes_overwrite line 219
20. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.RootRefresh.steps line 233
21. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.RootRefresh.steps_nil line 235
22. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.RootRefresh.steps_cons line 237
23. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.RootRefresh.steps_le_length line 242
24. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.RootRefresh.refreshTrace line 248
25. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.RootRefresh.refreshInTime line 304
26. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.RootRefresh.refresh_other line 326
27. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.RootRefresh.Label line 332
28. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.RootRefresh.Label.enumList line 336
29. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.RootRefresh.Label.enumList_getElem?_ctorIdx_eq line 338
30. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.RootRefresh.Label.enumList_nodup line 342
31. instance OAI.BinPackingGames.Foundations.Complexity.CookLevin.RootRefresh.(instance at line 344) line 344
32. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.RootRefresh.program line 348
33. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.RootRefresh.machine line 354
34. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.RootRefresh.machineTrace line 365
35. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.RootRefresh.computableInPolyTime line 383
36. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.Tape line 406
37. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.Ports line 411
38. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.Alphabet line 412
39. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.State line 413
40. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.Label line 415
41. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.lowerPorts line 421
42. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.initialLocal line 426
43. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.finalLocal line 435
44. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.coreBase line 443
45. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.coreInitial line 447
46. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.coreFinal line 450
47. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.chain line 454
48. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.coreTrace line 458
49. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.stateEquiv line 487
50. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.framedStatement line 493
51. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.framedProgram line 498
52. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.framedCfg line 502
53. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.framed_step line 507
54. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.framed_coreTrace line 524
55. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.steps line 534
56. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.forest_length_le_cost line 540
57. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.forest_rootsBits_length_le line 549
58. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.forest_rootRefresh_le line 562
59. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.forest_cost_quadratic line 568
60. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.timePolynomial line 595
61. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.forest_steps_le line 598
62. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.localLowerPorts line 615
63. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.lowerFill line 618
64. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.fill_lower_eq line 623
65. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.program line 632
66. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.extras line 647
67. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.afterRecords line 652
68. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.localTrace line 660
69. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.statement line 776
70. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.traceAt line 780
71. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.forestTraceAt line 794
72. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.forestInPolynomialTime line 809
73. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.preparedSize line 829
74. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.preparedSize_initial line 835
75. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.forestInPreparedTime line 844
76. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.final_other line 869
77. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.final_counter line 875
78. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.final_lower_clean line 878
79. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.final_forest_roots line 883
80. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.machine line 891
81. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ForestStage.machine_alphabet_finite line 902