OAI/Computability/PerfectCompleteness/Machines/ClockPreparation.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.PhasePrivate line 16
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.Private line 18
  3. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.Layout line 22
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.Label line 24
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.Output line 28
  6. instance OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.privateFintype line 32
  7. instance OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.privateDecidableEq line 39
  8. instance OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.labelFintype line 46
  9. instance OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.labelDecidableEq line 53
  10. instance OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.outputFintype line 60
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.controlSlots line 67
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.headLayout line 79
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.tailLayout line 97
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.headSlots line 113
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.tailSlots line 117
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.headSlots_input line 122
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.headSlots_output line 126
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.tailSlots_input line 131
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.head_output_ne_tail line 135
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.Clean line 155
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.head_clean line 159
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.head_coefficients_clean line 165
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.tail_clean_after_head line 170
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.entry line 178
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.statement line 182
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.resultTapes line 192
  27. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.steps line 199
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.timePolynomial line 203
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.steps_le_timePolynomial line 207
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.trace_trans line 218
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.trace line 222
  32. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.outputSlot line 250
  33. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.outputPolynomial line 255
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.outputSlot_private line 260
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.outputSlot_ne_input line 273
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.outputSlot_injective line 280
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.resultTapes_off_outputs line 300
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.resultTapes_input line 312
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.resultTapes_output line 319
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.resultTapes_work_clear line 338
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.resultTapes_ambient line 345
  42. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.ProgramLabel line 352
  43. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.program line 354
  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.programTrace line 360
  45. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.programInTime line 377
  46. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.Tape line 391
  47. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.machineSlots line 393
  48. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.machine line 396
  49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.machine_rawInput_preserved line 407
  50. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.machineInTime line 414
  51. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.Clock line 423
  52. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.Clock.enumList line 428

    Source documentation

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

    protected abbrev Clock.enumList : List Clock := [.witness, .horizon, .capacity, .width,
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.Clock

  53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.Clock.enumList_getElem?_ctorIdx_eq line 431
  54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.Clock.enumList_nodup line 435
  55. instance OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.(instance at line 437) line 437
  56. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.clockPolynomial line 441
  57. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.clockPolynomials line 450
  58. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.clockOutput line 454
  59. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.clockValue line 462
  60. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.outputPolynomial_clockOutput line 470
  61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.clockPolynomial_eval line 474
  62. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.clockResult_output line 480
  63. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ClockPreparation.clocksInTime line 488