OAI/Computability/PerfectCompleteness/Machines/ValidityMachine.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Alphabet line 18
2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.chain line 20
3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.inputMap line 26
4. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.Label line 28
5. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.statement line 32
6. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.frame line 39
7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.frame_current line 42
8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.frame_remaining line 45
9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.counter_frame line 48
10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.emitted_frame line 56
11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.increment_frame line 70
12. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.tokens line 75
13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.tokens_zero line 78
14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.tokens_succ line 80
15. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.steps line 89
16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.trace line 93
17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.steps_le line 139
18. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.loopMap line 155
19. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.closurePorts line 157
20. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.Label line 165
21. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.copyStatement line 173
22. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.statement line 180
23. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.steps line 195
24. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.Ready line 199
25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.emitted_update line 206
26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.frame_updates line 222
27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.tokens_nonempty line 226
28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.closed_frame line 230
29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.trace line 241
30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.steps_le line 377
31. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.inTime line 383
32. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.machine line 400
33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.machineTrace line 412