OAI/Computability/PerfectCompleteness/Machines/BoundedExecution.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.absorbingNext line 12
2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.absorbingNext_of_none line 14
3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.absorbingNext_of_some line 17
4. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.advance line 20
5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.advance_iterate_none line 22
6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.absorbing_of_successfulTrace line 25
7. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.executionToAbsorbing line 43
8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.absorbing_eq_of_execution line 65
9. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.stickyNext line 78
10. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.run line 80
11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.run_zero line 83
12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.run_succ line 86
13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.step_none_iff line 90
14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.stickyNext_live line 97
15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.run_eq_halt_of_outputs line 106
16. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.outputs_of_run_eq_halt line 112
17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.outputs_iff_run_eq_halt line 123
18. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.IsStickyTrace line 130
19. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.boundedTrace line 133
20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.boundedTrace_isSticky line 136
21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.trace_eq_run line 141
22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.outputs_iff_trace line 157
23. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.stackCapacity line 172
24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.run_stack_bound line 176
25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.run_stack_le line 184
26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.statement_budget line 190
27. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.StackBound line 204
28. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.StatementSafe line 207
29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.StatementSafe.stackBound line 220
30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.StatementSafe.push_room line 225
31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.StatementSafe.mono line 229
32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.StatementSafe.resultBound line 250
33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.stackBound_of_budget line 270
34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.statementSafe_of_budget line 277
35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.run_statement_safe line 337
36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.trace_stack_le line 343
37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.BoundedExecution.trace_statement_safe line 350