OAI/Computability/PerfectCompleteness/Machines/VerifierFront.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.Tape line 17
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.ExtraLabel line 18
  3. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.Label line 19
  4. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.State line 20
  5. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.EmbeddedAlphabet line 21
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.raw line 24
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.stream line 25
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.scratch line 26
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.clockSlots line 27
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.lengthTape line 29
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.clockTape line 30
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.phase line 32
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.clockLabel line 33
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.frameStates line 36
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.clockStates line 42
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.alphabet_eq line 48
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.extraProgram line 54
  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.innerExtra line 65
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.embeddedProgram line 70
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.program line 74
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.program_extra line 78
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.frameTapes line 88
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.framedTapes line 92
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.copiedTapes line 95
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.seedTapes line 98
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.preparedTapes line 102
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.alphabet_tapes_apply line 106
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.uniform_frame_tapes line 113
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.frameInTime line 122
  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.copyInTime line 150
  31. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.fieldInTime line 166
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.seed_input line 180
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.seed_clean line 184
  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.clocksInTime line 189
  35. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.timePolynomial line 206
  36. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.prepareInTime line 209
  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.callerInTime line 229
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.prepared_raw line 240
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.prepared_stream line 247
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.prepared_length line 254
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.prepared_clock line 261
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.clockOutput_surjective line 267
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.prepared_work_clear line 279
  44. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.machine line 294
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.initial_configuration line 305
  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.machineInTime line 319
  47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierFront.finite_work_alphabets line 326