OAI/Computability/PerfectCompleteness/Machines/TransitionMachine.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.Template line 16
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.listTokens line 18
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.compileList line 22
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.prefixTokens line 29
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.compilePrefix line 35
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.withCursor line 44
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.cursorTapes line 46
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.withCursor_cursor line 49
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.withCursor_capacity line 52
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.withCursor_roots line 55
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.withCursor_withCursor line 58
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.Frame.cursor line 61
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.cursorTapes_same line 71
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.cursorTapes_twice line 75
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.emitTapes_cursor line 79
  16. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.Plan line 84
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.Valid line 89
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.Valid.roots line 95
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.Valid.withCursor line 104
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.finalValid line 109
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.finalTokens line 113
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.finalEmitter line 119
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.guard line 142
  24. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.Label line 144
  25. instance OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.labelFintype line 157
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.program line 164
  27. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.machine line 181
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.cellTokens line 198
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.remainingTokens line 202
  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.loopSteps line 208
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.trace_trans line 216
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.guardTrace line 222
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.dispatchTrace line 236
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.incrementTrace line 246
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.resetTrace line 260
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.loopTrace line 280
  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.outputTokens line 328
  38. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.steps line 333
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.fullTrace line 340
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.traceAt line 359
  41. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.loopConstant line 374
  42. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.dataSize line 379
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.loopSteps_le line 383
  44. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.timeConstant line 426
  45. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.timePolynomial line 430
  46. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.steps_le line 436
  47. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.inPolynomialTime line 456
  48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.remainingTokens_eq_range line 473
  49. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.carriedTokens line 484
  50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.finalTokens_at_capacity line 490
  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.outputTokens_eq_blocks line 498
  52. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.transitionPrefixKinds line 509
  53. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.transitionCellKinds line 513
  54. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.transitionPlan line 516
  55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.transition_outputTokens line 522
  56. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionMachine.transitionInPolynomialTime line 534