OAI/Computability/DirectedFeedback/Machines/DummySelectSteps.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.dummySelectSteps line 55
  2. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.dummySelectSteps_eq line 59
  3. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectDummyTrace line 64
  4. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectionSteps line 123
  5. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectionTrace line 131
  6. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectionSteps_le line 163
  7. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectorMachine line 184
  8. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectionInTime line 195
  9. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorTapes line 215
  10. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreFinishTapes line 217
  11. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectTape line 219
  12. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectView line 237
  13. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectView_left line 246
  14. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectView_right line 254
  15. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreCleanupTape line 259
  16. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorStateEquiv line 261
  17. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectStateEquiv line 270
  18. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreAfterCleanup line 277
  19. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreInstruction line 281
  20. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreInitialState line 295
  21. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreMachine line 299
  22. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreMemory line 310
  23. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreMemory_update_output line 316
  24. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorTapes_injective line 324
  25. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreFinishTapes_injective line 328
  26. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreCleaned line 332
  27. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreCleanupSteps line 337
  28. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreCleanupTrace line 342
  29. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreCleaned_memory line 419
  30. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreCleanupSteps_memory line 427
  31. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorFinalFrame line 439
  32. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorTrace line 455
  33. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectFrame line 501
  34. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectionTrace line 510
  35. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreFinishTrace line 545
  36. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreInputTapes line 577
  37. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreSteps line 587
  38. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreTrace line 601
  39. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectedIndex_le line 648
  40. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.encodedDrop_length_le line 659
  41. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.rotorSize_le_encodedLength line 666
  42. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreTimeBound line 674
  43. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreSteps_le line 678
  44. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreMachineInTime line 742
  45. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalClean.Tape line 771
  46. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalClean.Alphabet line 772
  47. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalClean.State line 773
  48. inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalClean.Label line 775
  49. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalClean.instruction line 780
  50. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupTapes line 790
  51. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupSteps line 794
  52. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalClean.join_trace_inline_MachineRegularOriginalClean line 798
  53. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupTraceAt line 802
  54. structure OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalClean.Input line 836
  55. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalClean.cleanup_frame line 841
  56. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalClean.suffix_length_le line 855
  57. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupSteps_eq line 865
  58. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupSteps_le line 909
  59. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalClean.steps line 923
  60. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalClean.timeBound line 927
  61. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalClean.steps_le line 930
  62. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalClean.traceAt line 938
  63. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalClean.machine line 957
  64. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalClean.machineInTime line 968