OAI/Computability/BinPacking/CookLevin/TransitionIterationTime.lean

GitHub source file

116 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.RootLabel line 12
2. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.widthAddress line 17
3. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.rootProgram line 20
4. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.rootSteps line 27
5. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.trace_trans line 32
6. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.rootTrace line 36
7. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.rootSteps_le line 60
8. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.rootEmitter line 72
9. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.closurePorts line 87
10. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.ClosureLabel line 90
11. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.ClosureLabel.enumList line 94
12. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.ClosureLabel.enumList_getElem?_ctorIdx_eq line 97
13. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.ClosureLabel.enumList_nodup line 101
14. instance OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.(instance at line 103) line 103
15. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.closureProgram line 107
16. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.closureSteps line 116
17. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.closureTrace line 119
18. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.closureSteps_le line 157
19. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.closureEmitter line 164
20. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.Valid line 179
21. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.Valid.roots line 182
22. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.Valid.transition line 185
23. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.Valid.withCursor line 192
24. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.widthAddress_eq line 196
25. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.carryTokens line 202
26. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.carryEmitter line 208
27. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.orEmitter line 216
28. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.finishEmitter line 221
29. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.Label line 225
30. instance OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.labelFintype line 235
31. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.program line 242
32. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.machine line 254
33. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.outputTokens line 266
34. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.steps line 271
35. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.fullTrace line 280
36. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.timeConstant line 312
37. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.timePolynomial line 317
38. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.steps_le line 324
39. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.inPolynomialTime line 341
40. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.rootLookup_ofFn line 367
41. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.mismatchForest_ofFn line 371
42. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.verifierInput line 382
43. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.verifierInput_valid line 386
44. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.outputTokens_eq_acceptance line 391
45. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.compile_outputTokens line 401
46. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.outputTokens_length_le line 411
47. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.verifierMachine line 418
48. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceMachine.verifierInPolynomialTime line 421
49. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.EmitLabel line 450
50. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.Label line 453
51. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.entry line 455
52. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.program line 458
53. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.machine line 464
54. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.expressions line 475
55. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.wireValues line 479
56. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.tokens_eq_forest line 482
57. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.finish_termFrame line 489
58. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.prepared line 502
59. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.finish_place_emitTapes line 508
60. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.prepared_eq_lower line 516
61. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.lower_final_eq line 534
62. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.emissionSteps line 562
63. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.loweringSteps line 567
64. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.steps line 574
65. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.chain line 578
66. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.fullTrace line 582
67. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.budget line 621
68. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.steps_le_budget line 631
69. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.inTime line 648
70. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.verifierTrace line 661
71. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.AcceptanceStage.final_root_singleton line 671
72. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.bootstrapPolynomial line 692
73. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.validityPolynomial line 695
74. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.loweringPolynomial line 698
75. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.transitionEmissionPolynomial line 701
76. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.acceptanceEmissionPolynomial line 706
77. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.finishPolynomial line 710
78. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.iterationPolynomial line 713
79. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.knownPhasePolynomial line 717
80. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.producerPolynomial line 722
81. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.bootstrapPolynomial_eval line 725
82. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.validity_steps_le line 729
83. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.front_steps_le line 734
84. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.loweringPolynomial_eval line 739
85. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.transitionEmissionPolynomial_eval line 745
86. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.acceptanceEmissionPolynomial_eval line 752
87. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.forestSteps line 760
88. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.forestSteps_le line 766
89. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.initialForestSteps line 785
90. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.initialForestSteps_le line 789
91. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.transitionForestSteps line 803
92. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.transitionForestSteps_le line 807
93. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.acceptanceForestSteps line 813
94. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.acceptanceForestSteps_le line 818
95. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.frameInput line 834
96. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.frameInput_dataSize_le line 837
97. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.transitionEmissionSteps line 846
98. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.transitionEmissionSteps_le line 850
99. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.acceptanceEmissionSteps line 874
100. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.acceptanceEmissionSteps_le line 878
101. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.finishSteps line 896
102. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.finishSteps_le line 900
103. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.iterationPolynomial_eval line 922
104. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.iterationSteps line 928
105. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.iterationSteps_le line 932
106. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.knownPhaseSteps line 949
107. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.knownPhaseSteps_le line 956
108. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerTime.producerPolynomial_eval line 970
109. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.steps_eq_sum line 988
110. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.tokens_frame_eq_forest line 1002
111. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.lowerSteps_eq_forestSteps line 1018
112. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.stageSteps_verifier line 1041
113. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.verifier_steps_eq line 1048
114. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.verifier_steps_le line 1062
115. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.verifierInPolynomialTime line 1069
116. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionIteration.verifierPlacedInPolynomialTime line 1086