OAI/Computability/UniqueGames/Machines/MachineTransducerCopy.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTransducerCopy.Alphabet line 15
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTransducerCopy.State line 16
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTransducerCopy.scanLoop line 18
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTransducerCopy.emitter line 27
  5. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTransducerCopy.tapes line 33
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTransducerCopy.update_source line 37
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTransducerCopy.update_scratch line 52
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTransducerCopy.update_output line 64
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTransducerCopy.scanStep_empty line 70
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTransducerCopy.scanStep_cons line 88
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTransducerCopy.emitterStep line 106
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTransducerCopy.twoSteps_cons line 127
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTransducerCopy.scanTrace line 153
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTransducerCopy.restoreTapes line 187
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTransducerCopy.transduceCopyTrace line 206
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTransducerCopy.transduceCopyInTime line 252
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTransducerCopy.scanLoop_pushBound line 278
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTransducerCopy.emitter_pushBound line 284