OAI/Computability/PerfectCompleteness/Machines/PaddingCellsMachine.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.Ports line 16
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.corePorts line 18
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.literalPorts line 26
  4. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.frame line 29
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.frame_remaining line 33
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.frame_output line 38
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.frame_count line 43
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.frame_other line 48
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.frame_input line 54
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.update_remaining line 59
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.literal_emitted line 65
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.repeatedRows line 77
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.repeatedRows_zero line 80
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.repeatedRows_succ line 82
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.repeatedRows_length line 86
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.statement line 92
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.step_zero line 102
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.step_succ line 111
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.trace line 121
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.frame_eq_capacityTapes line 152
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.capacityTrace line 165
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.inTime line 180
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.blankRow line 203
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.blankRow_length line 208
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.initialCellTokens_padding line 211
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.cellRow_padding line 222
  27. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.cellsInterval line 230
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.cellsInterval_padding line 237
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.verifierStatement line 252
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.verifierTrace line 256
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.paddingCellsTrace line 270
  32. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.machine line 292
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PaddingCellsMachine.machineTrace line 304