OAI/Computability/PerfectCompleteness/Machines/InputCellsMachineLemmas.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.Ports line 16
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.Alphabet line 17
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.tapes line 19
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.tapes_input line 23
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.tapes_output line 28
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.tapes_count line 32
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.tapes_other line 36
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.update_input line 41
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.update_output line 52
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.update_count line 63
  11. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.TruthTable line 69
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.tableAt line 71
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.rowFrom line 74
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.rowTokens line 77
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.streamTokens line 79
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.rowFrom_succ line 82
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.rowFrom_length line 91
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.streamTokens_length line 97
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.streamTokens_eq_rows line 107
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.tokenBits_cons line 113
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.tokenBits_append line 117
  22. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.Label line 121
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.statement line 126
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.Agrees line 141
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.EmitAgrees line 145
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.scanStep_nil line 149
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.scanStep_cons line 159
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.emitStep line 170
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.finishRowStep line 185
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.rowTrace line 196
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.streamTrace line 224
  32. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.streamInTime line 262
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.copyAndStreamTrace line 276
  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.program line 309
  35. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.machine line 313
  36. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.machineInTime line 324
  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.symbolTruth line 342
  38. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.prefixTruth line 349
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.symbolTruth_eq_initialCellTokens line 352
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.prefixTruth_eq_initialCellTokens line 364
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.prefixRow_eq_initialCellTokens line 372
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsMachine.prefixStream_eq_initialCells line 386
  43. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsCapacity.Ports line 413
  44. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsCapacity.corePorts line 415
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsCapacity.capacity_distinct line 422
  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsCapacity.tapes line 428
  47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsCapacity.tapes_input line 433
  48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsCapacity.tapes_output line 437
  49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsCapacity.tapes_count line 441
  50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsCapacity.tapes_capacity line 445
  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsCapacity.tapes_other line 451
  52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsCapacity.update_input line 457
  53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsCapacity.update_capacity line 463
  54. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsCapacity.statement line 475
  55. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsCapacity.Agrees line 487
  56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsCapacity.emitAgrees line 493
  57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsCapacity.scanStep_nil line 501
  58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsCapacity.scanStep_cons line 513
  59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsCapacity.streamTrace_add line 527
  60. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsCapacity.streamTrace line 575
  61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InputCellsCapacity.copyAndStreamTrace line 591
  62. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsPrefixStage.Ports line 634
  63. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsPrefixStage.capacityPorts line 636
  64. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsPrefixStage.saved_distinct line 644
  65. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsPrefixStage.scratch_distinct line 649
  66. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsPrefixStage.prepared_eq line 653
  67. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsPrefixStage.Label line 676
  68. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsPrefixStage.streamLabels line 681
  69. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsPrefixStage.statement line 687
  70. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsPrefixStage.Agrees line 700
  71. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsPrefixStage.stream_agrees line 705
  72. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsPrefixStage.trace line 713
  73. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsPrefixStage.inTime line 741