OAI/Computability/DirectedFeedback/Machines/MachineSubstitution.lean

GitHub source file

91 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Reduction.MachineSubstitution.pushWord line 18
  2. theorem OAI.DFVSGames.Reduction.MachineSubstitution.stepAux_pushWord line 23
  3. theorem OAI.DFVSGames.Reduction.MachineSubstitution.statementPushBound_pushWord line 37
  4. def OAI.DFVSGames.Reduction.MachineSubstitution.loop line 49
  5. def OAI.DFVSGames.Reduction.MachineSubstitution.program line 55
  6. def OAI.DFVSGames.Reduction.MachineSubstitution.machine line 60
  7. def OAI.DFVSGames.Reduction.MachineSubstitution.maxEmission line 71
  8. theorem OAI.DFVSGames.Reduction.MachineSubstitution.statementPushBound_le line 74
  9. theorem OAI.DFVSGames.Reduction.MachineSubstitution.programPushBound_le line 84
  10. def OAI.DFVSGames.Reduction.MachineSubstitution.tapeStacks line 94
  11. def OAI.DFVSGames.Reduction.MachineSubstitution.running line 97
  12. def OAI.DFVSGames.Reduction.MachineSubstitution.emitting line 101
  13. def OAI.DFVSGames.Reduction.MachineSubstitution.halted line 105
  14. theorem OAI.DFVSGames.Reduction.MachineSubstitution.update_input_inline_MachineSubstitution line 108
  15. theorem OAI.DFVSGames.Reduction.MachineSubstitution.update_output_inline_MachineSubstitution line 113
  16. theorem OAI.DFVSGames.Reduction.MachineSubstitution.step_empty line 118
  17. theorem OAI.DFVSGames.Reduction.MachineSubstitution.step_cons line 125
  18. theorem OAI.DFVSGames.Reduction.MachineSubstitution.step_emit line 134
  19. def OAI.DFVSGames.Reduction.MachineSubstitution.next line 148
  20. theorem OAI.DFVSGames.Reduction.MachineSubstitution.two_steps_cons line 152
  21. theorem OAI.DFVSGames.Reduction.MachineSubstitution.substitution_steps line 161
  22. theorem OAI.DFVSGames.Reduction.MachineSubstitution.initList_eq line 176
  23. theorem OAI.DFVSGames.Reduction.MachineSubstitution.haltList_eq line 183
  24. theorem OAI.DFVSGames.Reduction.MachineSubstitution.substitution_init_steps line 188
  25. def OAI.DFVSGames.Reduction.MachineSubstitution.outputsInTime line 194
  26. theorem OAI.DFVSGames.Reduction.MachineSubstitution.outputsInTime_steps line 201
  27. def OAI.DFVSGames.Reduction.MachineSubstitution.computableInPolyTime line 204
  28. def OAI.DFVSGames.Reduction.MachineReverse.loop line 228
  29. def OAI.DFVSGames.Reduction.MachineReverse.machine line 234
  30. def OAI.DFVSGames.Reduction.MachineReverse.tapeStacks line 245
  31. def OAI.DFVSGames.Reduction.MachineReverse.running line 248
  32. def OAI.DFVSGames.Reduction.MachineReverse.halted line 251
  33. theorem OAI.DFVSGames.Reduction.MachineReverse.update_input_inline_MachineReverse line 254
  34. theorem OAI.DFVSGames.Reduction.MachineReverse.update_output_inline_MachineReverse line 259
  35. theorem OAI.DFVSGames.Reduction.MachineReverse.step_empty line 264
  36. theorem OAI.DFVSGames.Reduction.MachineReverse.step_cons line 271
  37. def OAI.DFVSGames.Reduction.MachineReverse.next line 279
  38. theorem OAI.DFVSGames.Reduction.MachineReverse.reverse_steps line 282
  39. theorem OAI.DFVSGames.Reduction.MachineReverse.initList_eq line 296
  40. theorem OAI.DFVSGames.Reduction.MachineReverse.haltList_eq line 303
  41. theorem OAI.DFVSGames.Reduction.MachineReverse.reverse_init_steps line 307
  42. def OAI.DFVSGames.Reduction.MachineReverse.outputsInTime line 313
  43. theorem OAI.DFVSGames.Reduction.MachineReverse.outputsInTime_steps line 319
  44. def OAI.DFVSGames.Reduction.MachineReverse.computableInPolyTime line 322
  45. def OAI.DFVSGames.Foundations.Complexity.MachineControl.configuration line 346
  46. def OAI.DFVSGames.Foundations.Complexity.MachineControl.statement line 352
  47. theorem OAI.DFVSGames.Foundations.Complexity.MachineControl.stepAux_simulation line 367
  48. def OAI.DFVSGames.Foundations.Complexity.MachineControl.program line 394
  49. theorem OAI.DFVSGames.Foundations.Complexity.MachineControl.step_simulation line 397
  50. abbrev OAI.DFVSGames.Foundations.Complexity.MachineStackSwap.Alphabet line 421
  51. def OAI.DFVSGames.Foundations.Complexity.MachineStackSwap.tapes line 424
  52. theorem OAI.DFVSGames.Foundations.Complexity.MachineStackSwap.tapes_first line 430
  53. theorem OAI.DFVSGames.Foundations.Complexity.MachineStackSwap.tapes_second line 432
  54. theorem OAI.DFVSGames.Foundations.Complexity.MachineStackSwap.tapes_third line 434
  55. theorem OAI.DFVSGames.Foundations.Complexity.MachineStackSwap.tapes_involutive line 437
  56. def OAI.DFVSGames.Foundations.Complexity.MachineStackSwap.configuration line 442
  57. def OAI.DFVSGames.Foundations.Complexity.MachineStackSwap.statement line 448
  58. theorem OAI.DFVSGames.Foundations.Complexity.MachineStackSwap.tapes_update_first line 465
  59. theorem OAI.DFVSGames.Foundations.Complexity.MachineStackSwap.tapes_update_second line 477
  60. theorem OAI.DFVSGames.Foundations.Complexity.MachineStackSwap.tapes_update_third line 489
  61. theorem OAI.DFVSGames.Foundations.Complexity.MachineStackSwap.stepAux_simulation line 501
  62. def OAI.DFVSGames.Foundations.Complexity.MachineStackSwap.program line 549
  63. theorem OAI.DFVSGames.Foundations.Complexity.MachineStackSwap.step_simulation line 552
  64. abbrev OAI.DFVSGames.Foundations.Complexity.MachineSequential.Tape line 571
  65. abbrev OAI.DFVSGames.Foundations.Complexity.MachineSequential.Symbols line 572
  66. abbrev OAI.DFVSGames.Foundations.Complexity.MachineSequential.Label line 575
  67. abbrev OAI.DFVSGames.Foundations.Complexity.MachineSequential.Register line 576
  68. abbrev OAI.DFVSGames.Foundations.Complexity.MachineSequential.State line 577
  69. def OAI.DFVSGames.Foundations.Complexity.MachineSequential.firstStates line 579
  70. def OAI.DFVSGames.Foundations.Complexity.MachineSequential.secondStates line 586
  71. def OAI.DFVSGames.Foundations.Complexity.MachineSequential.secondLabels line 593
  72. def OAI.DFVSGames.Foundations.Complexity.MachineSequential.bridgeLabel line 599
  73. def OAI.DFVSGames.Foundations.Complexity.MachineSequential.firstStatement line 602
  74. def OAI.DFVSGames.Foundations.Complexity.MachineSequential.secondStatement line 607
  75. def OAI.DFVSGames.Foundations.Complexity.MachineSequential.program line 615
  76. def OAI.DFVSGames.Foundations.Complexity.MachineSequential.machine line 631
  77. def OAI.DFVSGames.Foundations.Complexity.MachineSequential.firstConfiguration line 658
  78. def OAI.DFVSGames.Foundations.Complexity.MachineSequential.secondConfiguration line 664
  79. theorem OAI.DFVSGames.Foundations.Complexity.MachineSequential.firstStep line 673
  80. theorem OAI.DFVSGames.Foundations.Complexity.MachineSequential.secondStep line 703
  81. theorem OAI.DFVSGames.Foundations.Complexity.MachineSequential.firstConfiguration_init line 728
  82. theorem OAI.DFVSGames.Foundations.Complexity.MachineSequential.secondConfiguration_halt line 745
  83. def OAI.DFVSGames.Foundations.Complexity.MachineSequential.temporaryTapes line 763
  84. def OAI.DFVSGames.Foundations.Complexity.MachineSequential.temporaryConfiguration line 769
  85. theorem OAI.DFVSGames.Foundations.Complexity.MachineSequential.firstTransfer_tapes line 774
  86. theorem OAI.DFVSGames.Foundations.Complexity.MachineSequential.secondTransfer_tapes line 793
  87. def OAI.DFVSGames.Foundations.Complexity.MachineSequential.firstTransfer line 816
  88. def OAI.DFVSGames.Foundations.Complexity.MachineSequential.secondTransfer line 837
  89. def OAI.DFVSGames.Foundations.Complexity.MachineSequential.execute line 853
  90. def OAI.DFVSGames.Foundations.Complexity.MachineSequential.compose line 883
  91. def OAI.DFVSGames.Foundations.Complexity.MachineSequential.composeBits line 930