OAI/Computability/PerfectCompleteness/Machines/CircuitProducerStagesLemmas.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerStages.drainStep_cons line 17
  2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerStages.drainStep_nil line 29
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerStages.drainTrace line 40
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerStages.drainTrace_base line 59
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerStages.drainInTime line 68
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerStages.tagStep line 79
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerStages.tagInTime line 88
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerStages.clearFields line 98
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerStages.clearFields_field line 102
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerStages.clearFields_other line 106
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerStages.cleanupSteps line 110
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerStages.cleanupTrace line 114
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerStages.cleanupInTime line 136
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerStages.finishTapes line 146
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerStages.counterStep line 151
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerStages.finishTrace line 156
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerStages.finishInTime line 186
  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerHeaders.parsedTapes line 205
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerHeaders.resultTapes line 213
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerHeaders.parsedTapes_eq line 222
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerHeaders.headersTrace line 233
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerHeaders.headersInTime line 304
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerLoop.recordsInput line 326
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerLoop.recordsOutput line 327
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerLoop.tapes line 329
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerLoop.parsedFields line 338
  27. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerLoop.decodedFields line 339
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerLoop.update_reversed line 342
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerLoop.counterTapes_eq line 349
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerLoop.fourTapes_eq line 357
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerLoop.decodeTapes_eq line 372
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerLoop.clearFields_eq line 381
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerLoop.cleanupSteps_eq line 390
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerLoop.recordBits_length line 397
  35. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerLoop.bodyCost line 402
  36. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerLoop.bodyInTime line 406
  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerLoop.loopCost line 448
  38. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerLoop.loopInTime line 452
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerLoop.bodyCost_le line 484
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerLoop.loopCost_le line 490
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerLoop.recordOutput_length_le line 500
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerLoop.recordsOutput_length_le line 505
  43. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerRuntime.Input line 524
  44. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerRuntime.inputBits line 529
  45. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerRuntime.outputHeaders line 532
  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerRuntime.producedBits line 535
  47. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerRuntime.inputTapes line 538
  48. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerRuntime.retainedTapes line 541
  49. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerRuntime.guardTapes line 544
  50. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerRuntime.afterLoopTapes line 548
  51. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerRuntime.beforeFinishTapes line 552
  52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerRuntime.initList_eq line 555
  53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerRuntime.headers_result_eq line 565
  54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerRuntime.output_result_eq line 572
  55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerRuntime.finish_eq line 579
  56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerRuntime.inputBits_length line 589
  57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerRuntime.producedBits_length_le line 595
  58. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerRuntime.fullRunInTime line 603
  59. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerRuntime.computableInPolyTime line 644
  60. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducer.asInput line 672
  61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducer.recordsInput_eq line 675
  62. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducer.recordsOutput_eq line 684
  63. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducer.inputBits_asInput line 693
  64. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducer.producedBits_asInput line 698
  65. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducer.fullRunInTime line 704
  66. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducer.computableInPolyTime line 710
  67. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestPlacement.Tapes line 739
  68. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestPlacement.fill line 741
  69. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestPlacement.fill_at line 744
  70. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestPlacement.fill_other line 748
  71. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestPlacement.fill_self line 752
  72. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestPlacement.fill_update line 761
  73. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestPlacement.fill_comp line 777
  74. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestPlacement.placedLabel line 804
  75. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestPlacement.configuration line 808
  76. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestPlacement.statement line 815
  77. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestPlacement.stepAux_simulation line 830
  78. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestPlacement.step_simulation line 856
  79. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestPlacement.trace line 875
  80. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestPlacement.execution line 889