OAI/Computability/PerfectCompleteness/Machines/InitializationControl.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationControl.tokens line 21
2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationControl.tokens_length line 27
3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationControl.cells line 31
4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationControl.configurationTokens_eq line 37
5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationControl.flatten_singletons line 46
6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationControl.initializationTokens_eq_blocks line 52
7. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationControl.Ports line 63
8. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationControl.emitted line 68
9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationControl.emitted_reversed line 73
10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationControl.emitted_count line 77
11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationControl.emitted_other line 81
12. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationControl.exitStatement line 85
13. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationControl.literalStatement line 90
14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationControl.literalStep line 95
15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationControl.literalTrace line 103
16. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationControl.statement line 113
17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationControl.trace line 116