OAI/Computability/PerfectCompleteness/Machines/AcceptanceMachine.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.RootLabel line 13
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.widthAddress line 18
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.rootProgram line 21
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.rootSteps line 28
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.trace_trans line 33
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.rootTrace line 37
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.rootSteps_le line 61
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.rootEmitter line 73
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.closurePorts line 88
  10. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.ClosureLabel line 91
  11. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.ClosureLabel.enumList line 95
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.ClosureLabel.enumList_getElem?_ctorIdx_eq line 98
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.ClosureLabel.enumList_nodup line 102
  14. instance OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.(instance at line 104) line 104
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.closureProgram line 108
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.closureSteps line 117
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.closureTrace line 120
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.closureSteps_le line 158
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.closureEmitter line 165
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.Valid line 180
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.Valid.roots line 183
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.Valid.transition line 186
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.Valid.withCursor line 193
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.widthAddress_eq line 197
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.carryTokens line 203
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.carryEmitter line 209
  27. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.orEmitter line 217
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.finishEmitter line 222
  29. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.Label line 226
  30. instance OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.labelFintype line 236
  31. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.program line 243
  32. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.machine line 255
  33. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.outputTokens line 267
  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.steps line 272
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.fullTrace line 280
  36. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.timeConstant line 312
  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.timePolynomial line 317
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.steps_le line 323
  39. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.inPolynomialTime line 340
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.rootLookup_ofFn line 368
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.mismatchForest_ofFn line 372
  42. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.verifierInput line 383
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.verifierInput_valid line 387
  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.outputTokens_eq_acceptance line 392
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.compile_outputTokens line 402
  46. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.outputTokens_length_le line 412
  47. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.verifierMachine line 419
  48. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceMachine.verifierInPolynomialTime line 422