OAI/Computability/PerfectCompleteness/Machines/ProducerArenaLemmas.lean

GitHub source file

123 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.Work line 17
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.Tape line 25
  3. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.Alphabet line 26
  4. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.State line 27
  5. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.initialState line 28
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.frontPorts line 30
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.raw line 33
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.framed line 34
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.clock line 35
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.q line 37
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.capacity line 38
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.countdown line 39
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.freeInputs line 40
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.shared line 42
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.current line 44
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.roots line 45
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.records line 46
  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.tokens line 47
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.count line 48
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.cursor line 49
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.output line 50
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.clock_injective line 52
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.clock_eq_iff line 58
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.clock_ne_raw line 61
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.raw_ne_clock line 65
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.clock_ne_framed line 68
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.framed_ne_clock line 72
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.raw_ne_framed line 75
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.transitionTape line 78
  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.transitionPorts line 85
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.transitionPorts_apply line 108
  32. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.forestPorts line 111
  33. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.termPorts line 114
  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.initializationTape line 117
  35. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.initializationPorts line 127
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.initializationPorts_apply line 140
  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.finishTape line 143
  38. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.finishPorts line 152
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.finishPorts_apply line 159
  40. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.bootstrapPorts line 162
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.bootstrap_source line 169
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.bootstrap_current line 170
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.bootstrap_scratch line 171
  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.bootstrap_count line 173
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.bootstrap_cursor line 174
  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.empty line 176
  47. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.frontTapes line 178
  48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.frontTapes_at line 183
  49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.frontTapes_work line 187
  50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.front_fill line 191
  51. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.initialTapes line 200
  52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.initialTapes_eq line 203
  53. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.frontendPrepared line 214
  54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.frontendPrepared_raw line 217
  55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.frontendPrepared_framed line 220
  56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.frontendPrepared_clock line 224
  57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.frontendPrepared_work line 229
  58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.bootstrapReady line 232
  59. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.bootstrapPrepared line 237
  60. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.bootstrapPrepared_front line 240
  61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.bootstrapPrepared_current line 246
  62. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.bootstrapPrepared_count line 252
  63. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.bootstrapPrepared_cursor line 257
  64. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.bootstrapPrepared_other line 262
  65. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.initializationBase line 267
  66. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.bootstrap_initialization_view line 276
  67. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerArena.initializationValidityReady line 288
  68. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerFrontStage.Label line 302
  69. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerFrontStage.entry line 304
  70. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerFrontStage.statement line 306
  71. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerFrontStage.timePolynomial line 312
  72. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerFrontStage.timePolynomial_eval line 316
  73. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerFrontStage.inTime line 321
  74. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerFrontStage.program line 347
  75. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerFrontStage.programInTime line 350
  76. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.localBase line 365
  77. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary line 368
  78. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.finished line 372
  79. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.fill_fill line 376
  80. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_view line 389
  81. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.finished_view line 395
  82. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_other line 401
  83. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.finished_other line 406
  84. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.fill_boundary line 411
  85. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.fill_finished line 417
  86. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.iteration_handoff line 423
  87. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.acceptance_handoff line 428
  88. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_current line 433
  89. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_roots line 440
  90. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_records line 446
  91. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_countdown line 452
  92. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.finished_current line 458
  93. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.finished_roots line 465
  94. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.finished_records line 471
  95. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.finished_countdown line 477
  96. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_private line 483
  97. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.finished_private line 493
  98. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.private_finish_outside line 503
  99. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.private_validity_outside line 510
  100. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.private_cells_outside line 517
  101. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.bootstrap_clock line 524
  102. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.bootstrap_raw line 530
  103. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.bootstrap_work line 536
  104. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.bootstrap_extra line 542
  105. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_raw line 554
  106. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_q line 560
  107. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_capacity line 566
  108. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.initial_result_view line 572
  109. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.initial_result_eq_boundary line 596
  110. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.initialization_emitted_fill line 610
  111. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.initialization_lowering_handoff line 620
  112. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.clock_outside line 632
  113. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.freeInputs_outside line 647
  114. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.framed_outside line 650
  115. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_clock line 663
  116. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.finished_clock line 669
  117. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.boundary_framed line 675
  118. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.finished_framed line 682
  119. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.finished_freeInputs line 689
  120. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.finish_view line 694
  121. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.circuitFinish_view line 708
  122. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.bootstrap_emitter_ready line 720
  123. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerHandoffs.bootstrap_lowerer_ready line 733