OAI/Computability/MinUncut/Machines/MachineSubstitution.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Reduction.MachineSubstitution.pushWord line 17
  2. theorem OAI.MinUncutGames.Reduction.MachineSubstitution.stepAux_pushWord line 22
  3. theorem OAI.MinUncutGames.Reduction.MachineSubstitution.statementPushBound_pushWord line 36
  4. def OAI.MinUncutGames.Reduction.MachineSubstitution.loop line 48
  5. def OAI.MinUncutGames.Reduction.MachineSubstitution.program line 54
  6. def OAI.MinUncutGames.Reduction.MachineSubstitution.machine line 59
  7. def OAI.MinUncutGames.Reduction.MachineSubstitution.maxEmission line 70
  8. theorem OAI.MinUncutGames.Reduction.MachineSubstitution.statementPushBound_le line 73
  9. theorem OAI.MinUncutGames.Reduction.MachineSubstitution.programPushBound_le line 83
  10. def OAI.MinUncutGames.Reduction.MachineSubstitution.tapeStacks line 93
  11. def OAI.MinUncutGames.Reduction.MachineSubstitution.running line 96
  12. def OAI.MinUncutGames.Reduction.MachineSubstitution.emitting line 100
  13. def OAI.MinUncutGames.Reduction.MachineSubstitution.halted line 104
  14. theorem OAI.MinUncutGames.Reduction.MachineSubstitution.update_input line 107
  15. theorem OAI.MinUncutGames.Reduction.MachineSubstitution.update_output line 112
  16. theorem OAI.MinUncutGames.Reduction.MachineSubstitution.step_empty line 117
  17. theorem OAI.MinUncutGames.Reduction.MachineSubstitution.step_cons line 124
  18. theorem OAI.MinUncutGames.Reduction.MachineSubstitution.step_emit line 133
  19. def OAI.MinUncutGames.Reduction.MachineSubstitution.next line 148
  20. theorem OAI.MinUncutGames.Reduction.MachineSubstitution.two_steps_cons line 152
  21. theorem OAI.MinUncutGames.Reduction.MachineSubstitution.substitution_steps line 161
  22. theorem OAI.MinUncutGames.Reduction.MachineSubstitution.initList_eq line 176
  23. theorem OAI.MinUncutGames.Reduction.MachineSubstitution.haltList_eq line 183
  24. theorem OAI.MinUncutGames.Reduction.MachineSubstitution.substitution_init_steps line 188
  25. def OAI.MinUncutGames.Reduction.MachineSubstitution.outputsInTime line 194
  26. theorem OAI.MinUncutGames.Reduction.MachineSubstitution.outputsInTime_steps line 201
  27. def OAI.MinUncutGames.Reduction.MachineSubstitution.computableInPolyTime line 204
  28. def OAI.MinUncutGames.Reduction.MachineReverse.loop line 229
  29. def OAI.MinUncutGames.Reduction.MachineReverse.machine line 235
  30. def OAI.MinUncutGames.Reduction.MachineReverse.tapeStacks line 246
  31. def OAI.MinUncutGames.Reduction.MachineReverse.running line 249
  32. def OAI.MinUncutGames.Reduction.MachineReverse.halted line 252
  33. theorem OAI.MinUncutGames.Reduction.MachineReverse.update_input line 255
  34. theorem OAI.MinUncutGames.Reduction.MachineReverse.update_output line 260
  35. theorem OAI.MinUncutGames.Reduction.MachineReverse.step_empty line 265
  36. theorem OAI.MinUncutGames.Reduction.MachineReverse.step_cons line 272
  37. def OAI.MinUncutGames.Reduction.MachineReverse.next line 280
  38. theorem OAI.MinUncutGames.Reduction.MachineReverse.reverse_steps line 283
  39. theorem OAI.MinUncutGames.Reduction.MachineReverse.initList_eq line 297
  40. theorem OAI.MinUncutGames.Reduction.MachineReverse.haltList_eq line 304
  41. theorem OAI.MinUncutGames.Reduction.MachineReverse.reverse_init_steps line 308
  42. def OAI.MinUncutGames.Reduction.MachineReverse.outputsInTime line 314
  43. theorem OAI.MinUncutGames.Reduction.MachineReverse.outputsInTime_steps line 320
  44. def OAI.MinUncutGames.Reduction.MachineReverse.computableInPolyTime line 323
  45. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineStackSwap.Alphabet line 349
  46. def OAI.MinUncutGames.Foundations.Complexity.MachineStackSwap.tapes line 352
  47. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStackSwap.tapes_first line 358
  48. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStackSwap.tapes_second line 360
  49. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStackSwap.tapes_third line 362
  50. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStackSwap.tapes_involutive line 365
  51. def OAI.MinUncutGames.Foundations.Complexity.MachineStackSwap.configuration line 370
  52. def OAI.MinUncutGames.Foundations.Complexity.MachineStackSwap.statement line 376
  53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStackSwap.tapes_update_first line 393
  54. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStackSwap.tapes_update_second line 405
  55. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStackSwap.tapes_update_third line 417
  56. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStackSwap.stepAux_simulation line 429
  57. def OAI.MinUncutGames.Foundations.Complexity.MachineStackSwap.program line 477
  58. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStackSwap.step_simulation line 480
  59. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineSequential.Tape line 500
  60. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineSequential.Symbols line 501
  61. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineSequential.Label line 504
  62. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineSequential.Register line 505
  63. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineSequential.State line 506
  64. def OAI.MinUncutGames.Foundations.Complexity.MachineSequential.firstStates line 508
  65. def OAI.MinUncutGames.Foundations.Complexity.MachineSequential.secondStates line 515
  66. def OAI.MinUncutGames.Foundations.Complexity.MachineSequential.secondLabels line 522
  67. def OAI.MinUncutGames.Foundations.Complexity.MachineSequential.bridgeLabel line 528
  68. def OAI.MinUncutGames.Foundations.Complexity.MachineSequential.firstStatement line 531
  69. def OAI.MinUncutGames.Foundations.Complexity.MachineSequential.secondStatement line 536
  70. def OAI.MinUncutGames.Foundations.Complexity.MachineSequential.program line 544
  71. def OAI.MinUncutGames.Foundations.Complexity.MachineSequential.machine line 560
  72. def OAI.MinUncutGames.Foundations.Complexity.MachineSequential.firstConfiguration line 587
  73. def OAI.MinUncutGames.Foundations.Complexity.MachineSequential.secondConfiguration line 593
  74. theorem OAI.MinUncutGames.Foundations.Complexity.MachineSequential.firstStep line 602
  75. theorem OAI.MinUncutGames.Foundations.Complexity.MachineSequential.secondStep line 632
  76. theorem OAI.MinUncutGames.Foundations.Complexity.MachineSequential.firstConfiguration_init line 657
  77. theorem OAI.MinUncutGames.Foundations.Complexity.MachineSequential.secondConfiguration_halt line 674
  78. def OAI.MinUncutGames.Foundations.Complexity.MachineSequential.temporaryTapes line 692
  79. def OAI.MinUncutGames.Foundations.Complexity.MachineSequential.temporaryConfiguration line 698
  80. theorem OAI.MinUncutGames.Foundations.Complexity.MachineSequential.firstTransfer_tapes line 703
  81. theorem OAI.MinUncutGames.Foundations.Complexity.MachineSequential.secondTransfer_tapes line 722
  82. def OAI.MinUncutGames.Foundations.Complexity.MachineSequential.firstTransfer line 745
  83. def OAI.MinUncutGames.Foundations.Complexity.MachineSequential.secondTransfer line 766
  84. def OAI.MinUncutGames.Foundations.Complexity.MachineSequential.execute line 782
  85. def OAI.MinUncutGames.Foundations.Complexity.MachineSequential.compose line 812
  86. def OAI.MinUncutGames.Foundations.Complexity.MachineSequential.composeBits line 859