OAI/Computability/PerfectCompleteness/Machines/ValidityComposition.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Full.nonemptyMap line 15
2. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Full.Label line 17
3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Full.statement line 23
4. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Full.steps line 32
5. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Full.timePolynomial line 34
6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Full.timePolynomial_eval line 38
7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Full.steps_le_time line 42
8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Full.chain line 47
9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Full.trace line 51
10. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Full.inTime line 86
11. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Full.machine line 104
12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Full.machineTrace line 116
13. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ValidityMachine.Full.machineInTime line 123