OAI/Computability/PerfectCompleteness/Machines/InitializationMachineAt.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.Ports line 16
2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.Alphabet line 17
3. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.State line 18
4. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.initialState line 20
5. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.frame line 22
6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.frame_at line 28
7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.frame_other line 32
8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.update_frame line 36
9. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.contents line 49
10. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.tapes line 58
11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.tapes_at line 61
12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.tapes_other line 66
13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.update_remaining line 70
14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.update_current line 79
15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.update_threshold line 88
16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.update_reversed line 97
17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.update_count line 106
18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.push_current line 115
19. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.statement line 123
20. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.Agrees line 139
21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.chain line 143
22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.inputTagStep line 147
23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.identity_output line 157
24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.indexTrace line 164
25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.thresholdStep line 181
26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.resultStep line 200
27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.bodyTrace line 210
28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.guardStep_zero line 248
29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.guardStep_succ line 257
30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.prepend_three line 272
31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.selectorTrace line 278
32. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.selectorInTime line 311
33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.increment_count line 324
34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.standalone_agrees line 331
35. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.machine line 337
36. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.closurePorts line 348
37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.presenceTrace line 356
38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.presenceSteps_le line 403
39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachineAt.presence_count line 412