OAI/Computability/BinPacking/CookLevin/TransitionIteration.lean

GitHub source file

102 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceTemplate.headMask line 17
2. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceTemplate.accepting_label line 24
3. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceTemplate.accepting_state line 27
4. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceTemplate.accepting_cell line 31
5. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceTemplate.targetBit line 43
6. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceTemplate.mismatchTokens line 46
7. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceTemplate.tokens line 49
8. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceTemplate.mismatchTokens_eq line 56
9. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceTemplate.tokens_eq line 65
10. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceTemplate.compile_tokens line 72
11. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceTemplate.tokens_length_le line 81
12. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.Template line 97
13. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.listTokens line 99
14. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.compileList line 103
15. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.prefixTokens line 110
16. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.compilePrefix line 116
17. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.withCursor line 125
18. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.cursorTapes line 127
19. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.withCursor_cursor line 130
20. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.withCursor_capacity line 133
21. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.withCursor_roots line 136
22. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.withCursor_withCursor line 139
23. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.Frame.cursor line 142
24. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.cursorTapes_same line 152
25. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.cursorTapes_twice line 156
26. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.emitTapes_cursor line 160
27. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.Plan line 165
28. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.Valid line 170
29. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.Valid.roots line 176
30. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.Valid.withCursor line 185
31. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.finalValid line 190
32. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.finalTokens line 194
33. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.finalEmitter line 200
34. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.guard line 223
35. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.Label line 225
36. instance OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.labelFintype line 238
37. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.program line 245
38. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.machine line 262
39. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.cellTokens line 279
40. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.remainingTokens line 283
41. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.loopSteps line 289
42. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.trace_trans line 297
43. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.guardTrace line 303
44. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.dispatchTrace line 317
45. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.incrementTrace line 327
46. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.resetTrace line 341
47. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.loopTrace line 361
48. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.outputTokens line 409
49. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.steps line 414
50. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.fullTrace line 421
51. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.traceAt line 440
52. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.loopConstant line 455
53. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.dataSize line 460
54. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.loopSteps_le line 464
55. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.timeConstant line 507
56. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.timePolynomial line 511
57. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.steps_le line 517
58. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.inPolynomialTime line 537
59. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.remainingTokens_eq_range line 554
60. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.carriedTokens line 565
61. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.finalTokens_at_capacity line 571
62. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.outputTokens_eq_blocks line 579
63. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.transitionPrefixKinds line 590
64. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.transitionCellKinds line 594
65. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.transitionPlan line 597
66. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.transition_outputTokens line 603
67. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionMachine.transitionInPolynomialTime line 615
68. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptancePlan.negateIf line 646
69. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptancePlan.stateTemplate line 649
70. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptancePlan.cellTemplate line 653
71. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptancePlan.plan line 661
72. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptancePlan.mismatchForest line 675
73. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptancePlan.label_tokens line 680
74. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptancePlan.state_tokens line 691
75. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptancePlan.cell_tokens line 701
76. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptancePlan.outputTokens_eq line 718
77. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptancePlan.mismatchForest_circuit line 744
78. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptancePlan.fullTokens_eq line 752
79. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.tokens line 773
80. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.emitSteps line 778
81. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.emitTraceAt line 784
82. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.Label line 814
83. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.entry line 819
84. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.emitLabel line 822
85. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.lowerLabel line 827
86. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.emitEntry line 831
87. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.countdownStatement line 836
88. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.program line 842
89. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.machine line 852
90. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.guardZero line 864
91. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.guardSucc line 874
92. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.stageGates line 894
93. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.lowerSteps line 900
94. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.stageSteps line 909
95. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.steps line 915
96. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.chain line 923
97. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.place_forest_initial line 927
98. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.place_forest_final line 943
99. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.stageTrace line 967
100. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.repeatTrace line 1007
101. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.repeatInTime line 1023
102. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.repeatTraceAt line 1036