OAI/Computability/DirectedFeedback/Machines/MachineEmbedding.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Foundations.Complexity.MachineEmbedding.Alphabet line 12
  2. def OAI.DFVSGames.Foundations.Complexity.MachineEmbedding.tapes line 16
  3. theorem OAI.DFVSGames.Foundations.Complexity.MachineEmbedding.tapes_inl line 21
  4. theorem OAI.DFVSGames.Foundations.Complexity.MachineEmbedding.tapes_inr line 24
  5. def OAI.DFVSGames.Foundations.Complexity.MachineEmbedding.label line 27
  6. def OAI.DFVSGames.Foundations.Complexity.MachineEmbedding.configuration line 31
  7. def OAI.DFVSGames.Foundations.Complexity.MachineEmbedding.statement line 38
  8. theorem OAI.DFVSGames.Foundations.Complexity.MachineEmbedding.tapes_update line 55
  9. theorem OAI.DFVSGames.Foundations.Complexity.MachineEmbedding.stepAux_simulation line 68
  10. theorem OAI.DFVSGames.Foundations.Complexity.MachineEmbedding.stepAux_preserves_extra_state line 94
  11. theorem OAI.DFVSGames.Foundations.Complexity.MachineEmbedding.stepAux_preserves_extra_tape line 102
  12. def OAI.DFVSGames.Foundations.Complexity.MachineEmbedding.program line 110
  13. theorem OAI.DFVSGames.Foundations.Complexity.MachineEmbedding.step_running line 116
  14. theorem OAI.DFVSGames.Foundations.Complexity.MachineEmbedding.step_simulation line 129
  15. def OAI.DFVSGames.Foundations.Complexity.MachineComposition.advance line 151
  16. theorem OAI.DFVSGames.Foundations.Complexity.MachineComposition.advance_none line 154
  17. theorem OAI.DFVSGames.Foundations.Complexity.MachineComposition.advance_some line 157
  18. theorem OAI.DFVSGames.Foundations.Complexity.MachineComposition.advance_iterate_none line 160
  19. theorem OAI.DFVSGames.Foundations.Complexity.MachineComposition.liftSuccessfulTrace line 166
  20. def OAI.DFVSGames.Foundations.Complexity.MachineComposition.liftExecutionInTime line 190
  21. theorem OAI.DFVSGames.Foundations.Complexity.MachineComposition.liftExecutionInTime_steps line 204
  22. def OAI.DFVSGames.Foundations.Complexity.MachineComposition.embeddedExecution line 211
  23. theorem OAI.DFVSGames.Foundations.Complexity.MachineComposition.natPolynomial_eval_mono line 229
  24. def OAI.DFVSGames.Foundations.Complexity.MachineComposition.compositionPolynomial line 238
  25. theorem OAI.DFVSGames.Foundations.Complexity.MachineComposition.compositionBudget_le line 241
  26. def OAI.DFVSGames.Foundations.Complexity.MachineComposition.fourPhaseExecution line 252
  27. abbrev OAI.DFVSGames.Reduction.MachineTransfer.alphabet line 286
  28. def OAI.DFVSGames.Reduction.MachineTransfer.loop line 292
  29. def OAI.DFVSGames.Reduction.MachineTransfer.machine line 299
  30. def OAI.DFVSGames.Reduction.MachineTransfer.tapeStacks line 311
  31. def OAI.DFVSGames.Reduction.MachineTransfer.running line 316
  32. def OAI.DFVSGames.Reduction.MachineTransfer.halted line 320
  33. theorem OAI.DFVSGames.Reduction.MachineTransfer.update_input_inline_MachineTransfer line 324
  34. theorem OAI.DFVSGames.Reduction.MachineTransfer.update_output_inline_MachineTransfer line 330
  35. theorem OAI.DFVSGames.Reduction.MachineTransfer.step_empty line 335
  36. theorem OAI.DFVSGames.Reduction.MachineTransfer.step_cons line 343
  37. def OAI.DFVSGames.Reduction.MachineTransfer.next line 352
  38. theorem OAI.DFVSGames.Reduction.MachineTransfer.transfer_steps line 355
  39. theorem OAI.DFVSGames.Reduction.MachineTransfer.initList_eq line 372
  40. theorem OAI.DFVSGames.Reduction.MachineTransfer.haltList_eq line 379
  41. theorem OAI.DFVSGames.Reduction.MachineTransfer.transfer_init_steps line 386
  42. def OAI.DFVSGames.Reduction.MachineTransfer.outputsInTime line 397
  43. theorem OAI.DFVSGames.Reduction.MachineTransfer.outputsInTime_steps line 404
  44. def OAI.DFVSGames.Reduction.MachineTransfer.computableInPolyTime line 407
  45. def OAI.DFVSGames.Reduction.MachineTransfer.exitAt line 424
  46. def OAI.DFVSGames.Reduction.MachineTransfer.loopAt line 429
  47. def OAI.DFVSGames.Reduction.MachineTransfer.tapesAt line 436
  48. theorem OAI.DFVSGames.Reduction.MachineTransfer.tapesAt_src line 440
  49. theorem OAI.DFVSGames.Reduction.MachineTransfer.tapesAt_dst line 445
  50. theorem OAI.DFVSGames.Reduction.MachineTransfer.tapesAt_other line 450
  51. theorem OAI.DFVSGames.Reduction.MachineTransfer.tapesAt_self line 455
  52. theorem OAI.DFVSGames.Reduction.MachineTransfer.update_tapesAt_src_inline_MachineTransfer line 459
  53. theorem OAI.DFVSGames.Reduction.MachineTransfer.update_tapesAt_dst_inline_MachineTransfer line 473
  54. def OAI.DFVSGames.Reduction.MachineTransfer.nextAt line 484
  55. theorem OAI.DFVSGames.Reduction.MachineTransfer.stepAt_empty line 489
  56. theorem OAI.DFVSGames.Reduction.MachineTransfer.stepAt_cons line 503
  57. theorem OAI.DFVSGames.Reduction.MachineTransfer.transferAt_steps line 519
  58. theorem OAI.DFVSGames.Reduction.MachineTransfer.transferAt_fromTapes line 543
  59. def OAI.DFVSGames.Reduction.MachineTransfer.transferAtInTime line 556
  60. abbrev OAI.DFVSGames.Foundations.Complexity.MachineCopy.Alphabet line 581
  61. def OAI.DFVSGames.Foundations.Complexity.MachineCopy.forkLoop line 583
  62. def OAI.DFVSGames.Foundations.Complexity.MachineCopy.forkTapes line 591
  63. theorem OAI.DFVSGames.Foundations.Complexity.MachineCopy.forkTapes_source line 596
  64. theorem OAI.DFVSGames.Foundations.Complexity.MachineCopy.forkTapes_left line 602
  65. theorem OAI.DFVSGames.Foundations.Complexity.MachineCopy.forkTapes_right line 607
  66. theorem OAI.DFVSGames.Foundations.Complexity.MachineCopy.forkTapes_self line 612
  67. theorem OAI.DFVSGames.Foundations.Complexity.MachineCopy.update_fork_source_inline_MachineCopy line 616
  68. theorem OAI.DFVSGames.Foundations.Complexity.MachineCopy.update_fork_left_inline_MachineCopy line 630
  69. theorem OAI.DFVSGames.Foundations.Complexity.MachineCopy.update_fork_right_inline_MachineCopy line 641
  70. theorem OAI.DFVSGames.Foundations.Complexity.MachineCopy.forkStep_empty line 647
  71. theorem OAI.DFVSGames.Foundations.Complexity.MachineCopy.forkStep_cons line 663
  72. theorem OAI.DFVSGames.Foundations.Complexity.MachineCopy.forkTrace line 681
  73. def OAI.DFVSGames.Foundations.Complexity.MachineCopy.forkInTime line 708
  74. def OAI.DFVSGames.Foundations.Complexity.MachineCopy.drainedTapes line 728
  75. theorem OAI.DFVSGames.Foundations.Complexity.MachineCopy.restoredTapes line 731
  76. theorem OAI.DFVSGames.Foundations.Complexity.MachineCopy.copyTrace line 749
  77. def OAI.DFVSGames.Foundations.Complexity.MachineCopy.copyInTime line 790