OAI/Computability/DirectedFeedback/CookLevin/PolynomialMachine.lean

GitHub source file

136 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.coefficientPolynomial line 9
2. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.coefficientPolynomial_eval line 13
3. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.coefficientPolynomial_eval_reverse line 19
4. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.coefficients line 24
5. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.highCoefficients line 44
6. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.width line 47
7. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.digit line 49
8. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.digitBound line 52
9. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.le_sum_of_mem line 54
10. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.digit_le_bound line 64
11. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.highCoefficients_foldl line 70
12. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.range_map_digit line 77
13. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.prependFields line 91
14. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.prependFieldsTapes line 97
15. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.stepAux_prependFields line 103
16. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.prependFieldsTapes_apply line 113
17. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.popN line 127
18. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.stepAux_popN line 132
19. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.clearFields line 143
20. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.clearFieldsTapes line 148
21. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.stepAux_clearFields line 153
22. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.clearFieldsTapes_apply line 163
23. abbrev OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.Layout line 181
24. abbrev OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.Label line 182
25. abbrev OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.State line 183
26. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.fieldWord line 185
27. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.fieldIndices line 189
28. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.fieldIndices_nodup line 192
29. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.inl_not_mem_fields line 195
30. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.inr_mem_fields line 198
31. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.initialTapes line 201
32. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.preparedTapes line 204
33. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.preparedTapes_inl line 207
34. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.preparedTapes_inr line 212
35. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.slots line 217
36. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.preparedTapes_clean line 219
37. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.innerLabels line 223
38. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.program line 226
39. abbrev OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.machine line 236
40. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.afterHornerTapes line 247
41. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.afterInputTapes line 250
42. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.finalTapes line 253
43. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.clearFields_final line 256
44. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.initList_eq line 267
45. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.haltList_eq line 273
46. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.initializationTrace line 279
47. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.cleanupTrace line 289
48. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.prefixValuePolynomial line 306
49. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.prefixCostPolynomial line 310
50. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.prefixValuePolynomial_eval line 316
51. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.prefixCostPolynomial_eval line 322
52. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.timePolynomial line 332
53. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.timePolynomial_eval line 336
54. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.hornerValue_eq_eval line 343
55. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.hornerStageTrace line 349
56. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.outputsInTime line 363
57. def OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialMachine.computableInPolyTime line 382
58. abbrev OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Eval.Label line 416
59. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Eval.start line 418
60. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Eval.inner line 419
61. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Eval.finish line 420
62. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Eval.word line 422
63. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Eval.indices line 425
64. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Eval.indices_nodup line 429
65. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Eval.word_slot line 433
66. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Eval.control_not_mem line 438
67. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Eval.digit_mem line 444
68. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Eval.prepared line 449
69. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Eval.prepared_control line 453
70. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Eval.prepared_digit line 459
71. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Eval.clear_result line 466
72. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Eval.statement line 485
73. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Eval.steps line 495
74. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Eval.trace line 498
75. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Eval.inTime line 540
76. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.leftValue line 558
77. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.rightValue line 559
78. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.dummyValue line 560
79. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.bitValue line 561
80. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.occurrenceValue line 562
81. inductive OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Kind line 565
82. instance OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.(instance at line 568) line 568
83. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.polynomial line 572
84. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.polynomial_left_eval line 578
85. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.polynomial_right_eval line 580
86. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.polynomial_occurrences_eval line 582
87. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.bitValue_eq_nBits line 586
88. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.occurrenceValue_eq_length line 591
89. inductive OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Control line 602
90. instance OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.(instance at line 607) line 607
91. abbrev OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Coefficients line 612
92. abbrev OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Layout line 617
93. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.coefficientBlock line 619
94. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.inputControl line 626
95. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.outputControl line 629
96. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.controlSlots line 632
97. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.localSlots line 640
98. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.control line 659
99. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.evalSlots line 661
100. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_radix line 665
101. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_accA line 667
102. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_accB line 669
103. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_destination line 671
104. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_counter line 673
105. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_scratch line 675
106. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_digit line 677
107. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.control_eq_iff line 681
108. structure OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Clean line 685
109. inductive OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Label line 697
110. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.evalStart line 703
111. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.afterEval line 705
112. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.statement line 710
113. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.resultTapes line 731
114. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.steps line 738
115. structure OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.WorkClean line 743
116. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.Clean.work line 751
117. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.WorkClean.update_output line 755
118. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.evalPhaseTrace line 765
119. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.trace_trans_inline_SourceHeaderCounts line 786
120. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.trace line 790
121. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.timePolynomial line 894
122. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.steps_le_timePolynomial line 901
123. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.inTime line 922
124. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.inPolynomialTime line 937
125. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.formulaInTime line 953
126. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.result_frame line 968
127. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.result_left line 974
128. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.result_occurrences line 977
129. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.result_dummy line 980
130. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.result_bits line 983
131. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.result_variableCount line 986
132. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.result_clauseCount line 989
133. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.result_source_headers line 993
134. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.program line 1002
135. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.machine line 1006
136. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderCounts.afterInitializationInTime line 1017