OAI/Computability/PerfectCompleteness/Machines/ClashMachineFull.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.rowMap line 17
2. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.Ready line 19
3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.Ready.emitted line 23
4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.ext_slots line 31
5. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.frame line 41
6. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.closurePorts line 44
7. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.CopyContext line 52
8. instance OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.(instance at line 56) line 56
9. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.CopyLabel line 60
10. instance OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.(instance at line 64) line 64
11. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.Label line 68
12. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.copyTarget line 77
13. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.copyExit line 82
14. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.statement line 88
15. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.copySteps line 111
16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.copyTrace line 113
17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.closureTrace line 134
18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.emitted_frame line 161
19. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.bodySteps line 170
20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.bodySteps_eq line 173
21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.bodyTrace line 177
22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.counter_frame line 288
23. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.loopTokens line 296
24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.loopTokens_succ line 299
25. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.loopSteps line 308
26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.loopTrace line 312
27. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.bodyBudget line 341
28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.bodySteps_le line 343
29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.loopSteps_le line 351
30. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.steps line 361
31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.trace line 364
32. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.bodyPolynomial line 449
33. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.timePolynomial line 454
34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.timePolynomial_eval line 458
35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.steps_le_time line 462
36. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.inTime line 468
37. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.machine line 480
38. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClashMachine.Full.machineInTime line 491