OAI/Computability/PerfectCompleteness/Machines/PostfixMachine.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.Tape line 18
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.Tape.enumList line 22
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.Tape.enumList_getElem?_ctorIdx_eq line 25
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.Tape.enumList_nodup line 29
  5. instance OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.(instance at line 31) line 31
  6. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.Alphabet line 35
  7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.State line 36
  8. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.Label line 38
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.initialState line 49
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.headerTape line 51
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.binary line 53
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.readSource line 55
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.readDestination line 57
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.readNext line 60
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.prepare line 63
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.gateTag line 66
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.fieldSource line 68
  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.fieldUnused line 72
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.fieldNext line 75
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.resetGoto line 78
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.tagDecoder line 81
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.program line 88
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.machine line 116
  24. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.advance line 127
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.outputTapes line 129
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.outputTapes_reversed line 132
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.outputTapes_other line 135
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.outputTapes_twice line 139
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.trace_trans line 146
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.readSource_ne_destination line 150
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.fieldSource_ne_scratch line 155
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.fieldSource_ne_reversed line 160
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.decodeTrace line 165
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.readTrace line 173
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.emitTagTrace line 191
  36. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.FieldReady line 198
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.FieldReady.output line 202
  38. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.fieldSteps line 210
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.fieldTrace line 213
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.rootPushTrace line 249
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.incrementTrace line 261
  42. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.recordSteps line 270
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.recordTrace line 273
  44. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.clearTapes line 312
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.clearTrace line 315
  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.finishTapes line 335
  47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.finishNodeTrace line 340
  48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.emitPreparedTrace line 359
  49. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.boundaryTapes line 384
  50. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.preparedTapes line 392
  51. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.operandFields line 402
  52. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.operandSteps line 409
  53. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.tokenSteps line 416
  54. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.tokensSteps line 421
  55. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.argumentBits line 428
  56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.token_bits line 432
  57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.prepareInputTrace line 437
  58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.prepareUnaryTrace line 455
  59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.prepareBinaryTrace line 473
  60. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.prepareTrace line 504
  61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.preparedReady line 556
  62. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.tokenTrace line 615
  63. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.tokenBits_cons line 647
  64. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.boundary_remaining line 651
  65. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.guardPositiveTrace line 658
  66. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.tokensTrace line 666
  67. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.initialTapes line 733
  68. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.headersTrace line 740
  69. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.reversedTapes line 780
  70. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.reverseTrace line 784
  71. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.finalTapes line 814
  72. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.compileTrace line 822
  73. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixMachine.compileInTime line 851