OAI/Computability/PerfectCompleteness/Machines/InitializationStageLemmas.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.Ports line 17
2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.State line 18
3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.freeInputs line 20
4. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.initialGates line 23
5. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.preparedLocal line 27
6. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.snapshotLocal line 31
7. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.finishedLocal line 38
8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.initialCompile line 41
9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.initialRecords line 54
10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.finalLocal_eq line 65
11. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.lowerSteps line 85
12. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.Ready line 93
13. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.Prepared line 97
14. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.result line 101
15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.prepared_emitted line 105
16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.result_emitted line 123
17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.lowerTrace line 138
18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.result_at line 162
19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.result_other line 168
20. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.lowerTimePolynomial line 173
21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.lowerSteps_le line 177
22. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.lowerInTime line 212
23. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.FullPorts line 225
24. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.Label line 231
25. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.entry line 233
26. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.emitLabels line 235
27. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.statement line 239
28. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.Agrees line 245
29. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.FullReady line 249
30. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.steps line 254
31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.trace line 257
32. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.program line 276
33. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.machine line 280
34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.machineTrace line 292
35. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.timePolynomial line 300
36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.steps_le_timePolynomial line 303
37. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.verifierPlacedInPolynomialTime line 309
38. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationStage.verifierInPolynomialTime line 322
39. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.Extra line 341
40. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.Extra.enumList line 347

    Source documentation

    A list enumerating every element of the type, which are all zero-argument constructors. (Generated by the Fintype deriving handler.)

    protected abbrev Extra.enumList : List Extra := [.cursor, .capacity, .position, .address, .value,
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.Extra

41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.Extra.enumList_getElem?_ctorIdx_eq line 350
42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.Extra.enumList_nodup line 354
43. instance OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.(instance at line 356) line 356
44. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.Tape line 360
45. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.Alphabet line 361
46. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.State line 362
47. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.forestPorts line 364
48. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.termTape line 367
49. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.termPorts line 381
50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.termPorts_apply line 385
51. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.termInput line 387
52. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.tapes line 390
53. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.finishTapes line 405
54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.tapes_q line 409
55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.tapes_raw line 413
56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.tapes_capacity line 417
57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.termFrame line 421
58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.tapes_countdown_tail line 429
59. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.preparedTapes line 444
60. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.place_emitTapes line 451
61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionArena.fill_forest line 459