OAI/Computability/PerfectCompleteness/Machines/InputFrame.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.Tape line 14
2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.Label line 15
3. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.State line 16
4. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.Alphabet line 17
5. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.scan line 19
6. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.program line 26
7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.machine line 33
8. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.tapes line 44
9. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.cfg line 47
10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.tapes_zero line 51
11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.tapes_one line 54
12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.tapes_two line 57
13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.update_zero line 60
14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.update_one line 66
15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.update_two line 72
16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.scanStep_nil line 78
17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.scanStep_cons line 85
18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.scanTrace line 93
19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.startStep line 111
20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.restoreTrace line 120
21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.reverseCounterTrace line 136
22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.prependTrace line 152
23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.stopped_eq_haltList line 168
24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.frameTrace line 175
25. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputFrame.computableInPolyTime line 201