OAI/Computability/PerfectCompleteness/Machines/CellsTokensAlignmentLemmas.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsTokensAlignment.cellsInterval_append line 24
2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsTokensAlignment.cellsInterval_full line 33
3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsTokensAlignment.prefix_eq_interval line 37
4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsTokensAlignment.payload_eq_interval line 44
5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsTokensAlignment.cells_eq_streams line 56
6. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssemblyBounds.cellsPolynomial line 90
7. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssemblyBounds.timePolynomial line 98
8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssemblyBounds.capacityPolynomial_eval line 101
9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssemblyBounds.cellsPolynomial_eval line 106
10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssemblyBounds.cells_steps_le line 118
11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssemblyBounds.steps_le line 127
12. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.Tape line 146
13. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.validitySlots line 152
14. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.controlPorts line 159
15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.validityReady line 164
16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.control_emitted_eq line 180
17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.validityReady_control line 184
18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.validitySlots_not_cellWork line 191
19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.controlTrace line 199
20. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.cellsSlots line 219
21. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.CodeLabel line 224
22. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.Label line 230
23. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.placedControl line 234
24. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.cellsLabels line 239
25. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.Ready line 243
26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.Ready.afterEmitted line 252
27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.Ready.cellsReady line 267
28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.Ready.validityReady line 279
29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.capacity_within line 290
30. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.statement line 296
31. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.Agrees line 307
32. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.steps line 311
33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.cellsTokens_eq line 317
34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.trace line 325
35. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.program line 367
36. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.machine line 371
37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.machineTrace line 383
38. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.timePolynomial line 392
39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.steps_le_timePolynomial line 395
40. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.inPolynomialTime line 399
41. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationAssembly.machineInPolynomialTime line 414