OAI/Computability/PerfectCompleteness/Machines/AcceptanceStage.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.EmitLabel line 24
2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.Label line 27
3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.entry line 29
4. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.program line 32
5. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.machine line 38
6. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.expressions line 49
7. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.wireValues line 53
8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.tokens_eq_forest line 56
9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.finish_termFrame line 63
10. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.prepared line 75
11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.finish_place_emitTapes line 81
12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.prepared_eq_lower line 90
13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.lower_final_eq line 108
14. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.emissionSteps line 136
15. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.loweringSteps line 141
16. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.steps line 148
17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.chain line 152
18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.fullTrace line 156
19. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.budget line 195
20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.steps_le_budget line 205
21. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.inTime line 222
22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.verifierTrace line 235
23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.final_root_singleton line 245