OAI/Computability/MinUncut/Machines/Runtime.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.Complexity.Runtime.statementPushBound line 9
  2. def OAI.MinUncutGames.Foundations.Complexity.Runtime.maxLabelPushes line 19
  3. theorem OAI.MinUncutGames.Foundations.Complexity.Runtime.maxLabelPushes_ge line 24
  4. def OAI.MinUncutGames.Foundations.Complexity.Runtime.programPushBound line 36
  5. theorem OAI.MinUncutGames.Foundations.Complexity.Runtime.statement_le_programPushBound line 39
  6. theorem OAI.MinUncutGames.Foundations.Complexity.Runtime.stepAuxStackLength line 44
  7. theorem OAI.MinUncutGames.Foundations.Complexity.Runtime.iterateSizeBound line 87
  8. theorem OAI.MinUncutGames.Foundations.Complexity.Runtime.executionSizeBound line 99
  9. theorem OAI.MinUncutGames.Foundations.Complexity.Runtime.stepStackLength line 122
  10. theorem OAI.MinUncutGames.Foundations.Complexity.Runtime.initialStackLength line 135
  11. theorem OAI.MinUncutGames.Foundations.Complexity.Runtime.haltedOutputLength line 142
  12. theorem OAI.MinUncutGames.Foundations.Complexity.Runtime.outputLength_le line 146
  13. theorem OAI.MinUncutGames.Foundations.Complexity.Runtime.encodedOutputLength line 158
  14. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineEmbedding.Alphabet line 176
  15. def OAI.MinUncutGames.Foundations.Complexity.MachineEmbedding.tapes line 180
  16. theorem OAI.MinUncutGames.Foundations.Complexity.MachineEmbedding.tapes_inl line 185
  17. theorem OAI.MinUncutGames.Foundations.Complexity.MachineEmbedding.tapes_inr line 188
  18. def OAI.MinUncutGames.Foundations.Complexity.MachineEmbedding.label line 191
  19. def OAI.MinUncutGames.Foundations.Complexity.MachineEmbedding.configuration line 195
  20. def OAI.MinUncutGames.Foundations.Complexity.MachineEmbedding.statement line 202
  21. theorem OAI.MinUncutGames.Foundations.Complexity.MachineEmbedding.tapes_update line 219
  22. theorem OAI.MinUncutGames.Foundations.Complexity.MachineEmbedding.stepAux_simulation line 232
  23. theorem OAI.MinUncutGames.Foundations.Complexity.MachineEmbedding.stepAux_preserves_extra_state line 258
  24. theorem OAI.MinUncutGames.Foundations.Complexity.MachineEmbedding.stepAux_preserves_extra_tape line 266
  25. def OAI.MinUncutGames.Foundations.Complexity.MachineEmbedding.program line 274
  26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineEmbedding.step_running line 280
  27. theorem OAI.MinUncutGames.Foundations.Complexity.MachineEmbedding.step_simulation line 293
  28. def OAI.MinUncutGames.Foundations.Complexity.MachineComposition.advance line 314
  29. theorem OAI.MinUncutGames.Foundations.Complexity.MachineComposition.advance_none line 317
  30. theorem OAI.MinUncutGames.Foundations.Complexity.MachineComposition.advance_some line 320
  31. theorem OAI.MinUncutGames.Foundations.Complexity.MachineComposition.advance_iterate_none line 323
  32. theorem OAI.MinUncutGames.Foundations.Complexity.MachineComposition.liftSuccessfulTrace line 329
  33. def OAI.MinUncutGames.Foundations.Complexity.MachineComposition.liftExecutionInTime line 353
  34. theorem OAI.MinUncutGames.Foundations.Complexity.MachineComposition.liftExecutionInTime_steps line 367
  35. def OAI.MinUncutGames.Foundations.Complexity.MachineComposition.embeddedExecution line 374
  36. theorem OAI.MinUncutGames.Foundations.Complexity.MachineComposition.natPolynomial_eval_mono line 392
  37. def OAI.MinUncutGames.Foundations.Complexity.MachineComposition.compositionPolynomial line 401
  38. theorem OAI.MinUncutGames.Foundations.Complexity.MachineComposition.compositionBudget_le line 404
  39. def OAI.MinUncutGames.Foundations.Complexity.MachineComposition.fourPhaseExecution line 415
  40. abbrev OAI.MinUncutGames.Reduction.MachineTransfer.alphabet line 448
  41. def OAI.MinUncutGames.Reduction.MachineTransfer.loop line 454
  42. def OAI.MinUncutGames.Reduction.MachineTransfer.machine line 461
  43. def OAI.MinUncutGames.Reduction.MachineTransfer.tapeStacks line 473
  44. def OAI.MinUncutGames.Reduction.MachineTransfer.running line 478
  45. def OAI.MinUncutGames.Reduction.MachineTransfer.halted line 482
  46. theorem OAI.MinUncutGames.Reduction.MachineTransfer.update_input line 486
  47. theorem OAI.MinUncutGames.Reduction.MachineTransfer.update_output line 492
  48. theorem OAI.MinUncutGames.Reduction.MachineTransfer.step_empty line 497
  49. theorem OAI.MinUncutGames.Reduction.MachineTransfer.step_cons line 505
  50. def OAI.MinUncutGames.Reduction.MachineTransfer.next line 514
  51. theorem OAI.MinUncutGames.Reduction.MachineTransfer.transfer_steps line 517
  52. theorem OAI.MinUncutGames.Reduction.MachineTransfer.initList_eq line 534
  53. theorem OAI.MinUncutGames.Reduction.MachineTransfer.haltList_eq line 541
  54. theorem OAI.MinUncutGames.Reduction.MachineTransfer.transfer_init_steps line 548
  55. def OAI.MinUncutGames.Reduction.MachineTransfer.outputsInTime line 557
  56. theorem OAI.MinUncutGames.Reduction.MachineTransfer.outputsInTime_steps line 564
  57. def OAI.MinUncutGames.Reduction.MachineTransfer.computableInPolyTime line 567
  58. def OAI.MinUncutGames.Reduction.MachineTransfer.exitAt line 586
  59. def OAI.MinUncutGames.Reduction.MachineTransfer.loopAt line 591
  60. def OAI.MinUncutGames.Reduction.MachineTransfer.tapesAt line 598
  61. theorem OAI.MinUncutGames.Reduction.MachineTransfer.tapesAt_src line 602
  62. theorem OAI.MinUncutGames.Reduction.MachineTransfer.tapesAt_dst line 607
  63. theorem OAI.MinUncutGames.Reduction.MachineTransfer.tapesAt_other line 612
  64. theorem OAI.MinUncutGames.Reduction.MachineTransfer.tapesAt_self line 617
  65. theorem OAI.MinUncutGames.Reduction.MachineTransfer.update_tapesAt_src line 621
  66. theorem OAI.MinUncutGames.Reduction.MachineTransfer.update_tapesAt_dst line 635
  67. def OAI.MinUncutGames.Reduction.MachineTransfer.nextAt line 646
  68. theorem OAI.MinUncutGames.Reduction.MachineTransfer.stepAt_empty line 651
  69. theorem OAI.MinUncutGames.Reduction.MachineTransfer.stepAt_cons line 665
  70. theorem OAI.MinUncutGames.Reduction.MachineTransfer.transferAt_steps line 681
  71. theorem OAI.MinUncutGames.Reduction.MachineTransfer.transferAt_fromTapes line 705
  72. def OAI.MinUncutGames.Reduction.MachineTransfer.transferAtInTime line 718