OAI/Computability/PerfectCompleteness/Machines/CellsMachine.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.Ports line 17
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.Alphabet line 18
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.prefixMap line 20
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.loopMap line 21
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.paddingMap line 22
  6. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.prefixPorts line 24
  7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.loopPorts line 25
  8. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.paddingPorts line 26
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.WorkEmpty line 28
  10. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.Ready line 31
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.workEmpty_emitted line 37
  12. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.frame line 44
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.ext_ports line 47
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.frame_emitted line 56
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.update_emitted_capacity line 61
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.frame_seed line 70
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.seed_ready line 78
  18. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.Label line 97
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.prefixLabels line 104
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.payloadLabels line 107
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.statement line 110
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.Agrees line 128
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.prefixTrace line 140
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.preparePayloadTrace line 180
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.payloadTrace line 213
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.paddingTrace line 230
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.cleanupTrace line 263
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.tokens line 291
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.steps line 297
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.trace line 301
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CellsMachine.steps_le line 333