OAI/Computability/PerfectCompleteness/Machines/InitializationMachine.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.Tape line 15
2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.Tape.enumList line 20
3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.Tape.enumList_getElem?_ctorIdx_eq line 23
4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.Tape.enumList_nodup line 27
5. instance OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.(instance at line 29) line 29
6. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.Label line 33
7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.Alphabet line 38
8. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.State line 39
9. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.initialState line 41
10. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.program line 43
11. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.machine line 55
12. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.tapes line 66
13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.tapes_current line 75
14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.tapes_reversed line 78
15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.update_reversed line 81
16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.push_current line 88
17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.counterTapes_remaining line 94
18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.counterTapes_threshold line 101
19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.chain line 108
20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.inputTagStep line 112
21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.identity_output line 122
22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.indexTrace line 129
23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.thresholdStep line 142
24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.resultStep line 157
25. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.termTokens line 166
26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.termTokens_bits line 169
27. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.bodySteps line 175
28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.bodyTrace line 177
29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.guardStep_succ line 210
30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.guardStep_zero line 217
31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.tokens_append_bits line 224
32. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.selectorSteps line 228
33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.selectorTrace line 232
34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.selectorSteps_le line 260
35. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.selectorInTime line 274
36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.tapes_rawInput line 284
37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.tapes_witnessBound line 287
38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.tapes_capacity line 290
39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationMachine.tapes_closure line 293