OAI/Computability/PerfectCompleteness/Machines/PostfixBounds.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixBounds.RootsBounded line 14
2. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixBounds.TokenBounded line 16
3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixBounds.fieldSteps_le line 20
4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixBounds.recordSteps_le line 25
5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixBounds.gateRecord_slot_le line 33
6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixBounds.operandSteps_le line 42
7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixBounds.operandFields_length_le line 48
8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixBounds.tokenSteps_le line 54
9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixBounds.takeGate_bounds line 64
10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixBounds.tokensSteps_le line 110
11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixBounds.exprTokens_bounded line 138
12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixBounds.forestTokens_bounded line 164
13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixBounds.forest_tokensSteps_le line 170
14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixBounds.forest_recordsBits_length_le line 180
15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixBounds.forest_phases_le line 191
16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixBounds.forest_header_le_input_length line 207
17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixBounds.forest_phases_le_input_quadratic line 214