OAI/Computability/DirectedFeedback/Machines/MachineTransducer.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Reduction.MachineTransducer.tapeStacks line 13
  2. theorem OAI.DFVSGames.Reduction.MachineTransducer.update_input_inline_MachineTransducer line 16
  3. theorem OAI.DFVSGames.Reduction.MachineTransducer.update_output_inline_MachineTransducer line 21
  4. def OAI.DFVSGames.Reduction.MachineTransducer.output line 28
  5. def OAI.DFVSGames.Reduction.MachineTransducer.loop line 34
  6. def OAI.DFVSGames.Reduction.MachineTransducer.program line 41
  7. def OAI.DFVSGames.Reduction.MachineTransducer.machine line 49
  8. def OAI.DFVSGames.Reduction.MachineTransducer.maxEmission line 61
  9. theorem OAI.DFVSGames.Reduction.MachineTransducer.emission_le line 64
  10. theorem OAI.DFVSGames.Reduction.MachineTransducer.statementPushBound_le line 69
  11. theorem OAI.DFVSGames.Reduction.MachineTransducer.programPushBound_le line 78
  12. def OAI.DFVSGames.Reduction.MachineTransducer.running line 89
  13. def OAI.DFVSGames.Reduction.MachineTransducer.emitting line 94
  14. def OAI.DFVSGames.Reduction.MachineTransducer.halted line 99
  15. theorem OAI.DFVSGames.Reduction.MachineTransducer.step_empty line 103
  16. theorem OAI.DFVSGames.Reduction.MachineTransducer.step_cons line 114
  17. theorem OAI.DFVSGames.Reduction.MachineTransducer.step_emit line 126
  18. def OAI.DFVSGames.Reduction.MachineTransducer.next line 144
  19. theorem OAI.DFVSGames.Reduction.MachineTransducer.two_steps_cons line 149
  20. theorem OAI.DFVSGames.Reduction.MachineTransducer.transduce_steps line 162
  21. theorem OAI.DFVSGames.Reduction.MachineTransducer.initList_eq line 179
  22. theorem OAI.DFVSGames.Reduction.MachineTransducer.haltList_eq line 188
  23. theorem OAI.DFVSGames.Reduction.MachineTransducer.transduce_init_steps line 195
  24. def OAI.DFVSGames.Reduction.MachineTransducer.outputsInTime line 203
  25. theorem OAI.DFVSGames.Reduction.MachineTransducer.outputsInTime_steps line 211
  26. def OAI.DFVSGames.Reduction.MachineTransducer.reversedComputableInPolyTime line 215
  27. def OAI.DFVSGames.Reduction.MachineTransducer.computableInPolyTime line 235
  28. abbrev OAI.DFVSGames.Foundations.Complexity.MachineTransducerCopy.Alphabet line 253
  29. abbrev OAI.DFVSGames.Foundations.Complexity.MachineTransducerCopy.State line 254
  30. def OAI.DFVSGames.Foundations.Complexity.MachineTransducerCopy.scanLoop line 256
  31. def OAI.DFVSGames.Foundations.Complexity.MachineTransducerCopy.emitter line 265
  32. abbrev OAI.DFVSGames.Foundations.Complexity.MachineTransducerCopy.tapes line 271
  33. theorem OAI.DFVSGames.Foundations.Complexity.MachineTransducerCopy.update_source_inline_MachineTransducerCopy line 275
  34. theorem OAI.DFVSGames.Foundations.Complexity.MachineTransducerCopy.update_scratch_inline_MachineTransducerCopy line 290
  35. theorem OAI.DFVSGames.Foundations.Complexity.MachineTransducerCopy.update_output_inline_MachineTransducerCopy line 302
  36. theorem OAI.DFVSGames.Foundations.Complexity.MachineTransducerCopy.scanStep_empty line 308
  37. theorem OAI.DFVSGames.Foundations.Complexity.MachineTransducerCopy.scanStep_cons line 326
  38. theorem OAI.DFVSGames.Foundations.Complexity.MachineTransducerCopy.emitterStep line 344
  39. theorem OAI.DFVSGames.Foundations.Complexity.MachineTransducerCopy.twoSteps_cons line 365
  40. theorem OAI.DFVSGames.Foundations.Complexity.MachineTransducerCopy.scanTrace line 391
  41. theorem OAI.DFVSGames.Foundations.Complexity.MachineTransducerCopy.restoreTapes line 425
  42. theorem OAI.DFVSGames.Foundations.Complexity.MachineTransducerCopy.transduceCopyTrace line 444
  43. def OAI.DFVSGames.Foundations.Complexity.MachineTransducerCopy.transduceCopyInTime line 490
  44. theorem OAI.DFVSGames.Foundations.Complexity.MachineTransducerCopy.scanLoop_pushBound line 516
  45. theorem OAI.DFVSGames.Foundations.Complexity.MachineTransducerCopy.emitter_pushBound line 522
  46. inductive OAI.DFVSGames.Reduction.MachineFieldTemplate.Token line 537
  47. def OAI.DFVSGames.Reduction.MachineFieldTemplate.tokenOutput line 544
  48. def OAI.DFVSGames.Reduction.MachineFieldTemplate.templateOutput line 548
  49. def OAI.DFVSGames.Reduction.MachineFieldTemplate.tokenSteps line 551
  50. def OAI.DFVSGames.Reduction.MachineFieldTemplate.workSteps line 555
  51. def OAI.DFVSGames.Reduction.MachineFieldTemplate.templateSteps line 558
  52. def OAI.DFVSGames.Reduction.MachineFieldTemplate.copiedLength line 561
  53. inductive OAI.DFVSGames.Reduction.MachineFieldTemplate.Label line 564
  54. abbrev OAI.DFVSGames.Reduction.MachineFieldTemplate.State line 572
  55. abbrev OAI.DFVSGames.Reduction.MachineFieldTemplate.Alphabet line 573
  56. def OAI.DFVSGames.Reduction.MachineFieldTemplate.reset line 575
  57. theorem OAI.DFVSGames.Reduction.MachineFieldTemplate.reset_reset line 577
  58. def OAI.DFVSGames.Reduction.MachineFieldTemplate.startAt line 579
  59. def OAI.DFVSGames.Reduction.MachineFieldTemplate.jump line 582
  60. def OAI.DFVSGames.Reduction.MachineFieldTemplate.identityEmit line 587
  61. def OAI.DFVSGames.Reduction.MachineFieldTemplate.instruction line 589
  62. def OAI.DFVSGames.Reduction.MachineFieldTemplate.program line 608
  63. def OAI.DFVSGames.Reduction.MachineFieldTemplate.outputTapes line 615
  64. theorem OAI.DFVSGames.Reduction.MachineFieldTemplate.outputTapes_self line 618
  65. theorem OAI.DFVSGames.Reduction.MachineFieldTemplate.outputTapes_output line 621
  66. theorem OAI.DFVSGames.Reduction.MachineFieldTemplate.outputTapes_other line 624
  67. theorem OAI.DFVSGames.Reduction.MachineFieldTemplate.outputTapes_append line 628
  68. theorem OAI.DFVSGames.Reduction.MachineFieldTemplate.fieldValues_outputTapes line 633
  69. theorem OAI.DFVSGames.Reduction.MachineFieldTemplate.identity_output line 639
  70. theorem OAI.DFVSGames.Reduction.MachineFieldTemplate.chain_inline_MachineFieldTemplate line 645
  71. theorem OAI.DFVSGames.Reduction.MachineFieldTemplate.doneStep line 661
  72. theorem OAI.DFVSGames.Reduction.MachineFieldTemplate.literalStep line 668
  73. theorem OAI.DFVSGames.Reduction.MachineFieldTemplate.copySetupStep line 679
  74. theorem OAI.DFVSGames.Reduction.MachineFieldTemplate.copyTrace line 689
  75. theorem OAI.DFVSGames.Reduction.MachineFieldTemplate.tokenTrace line 712
  76. theorem OAI.DFVSGames.Reduction.MachineFieldTemplate.suffixTrace_inline_MachineFieldTemplate line 729
  77. theorem OAI.DFVSGames.Reduction.MachineFieldTemplate.phaseTrace line 773
  78. theorem OAI.DFVSGames.Reduction.MachineFieldTemplate.programTrace line 785
  79. theorem OAI.DFVSGames.Reduction.MachineFieldTemplate.templateSteps_le line 797
  80. def OAI.DFVSGames.Reduction.MachineFieldTemplate.phaseInTime line 810