OAI/Computability/DirectedFeedback/Machines/MachineBinaryRenameMachine.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.BinaryRenameMachine.Tape line 58
  2. abbrev OAI.DFVSGames.BinaryRenameMachine.Alphabet line 59
  3. abbrev OAI.DFVSGames.BinaryRenameMachine.State line 60
  4. inductive OAI.DFVSGames.BinaryRenameMachine.Label line 62
  5. def OAI.DFVSGames.BinaryRenameMachine.loopTapes line 69
  6. theorem OAI.DFVSGames.BinaryRenameMachine.loopTapes_injective line 71
  7. def OAI.DFVSGames.BinaryRenameMachine.program line 76
  8. abbrev OAI.DFVSGames.BinaryRenameMachine.machine line 89
  9. def OAI.DFVSGames.BinaryRenameMachine.tapes line 100
  10. def OAI.DFVSGames.BinaryRenameMachine.cfg line 110
  11. theorem OAI.DFVSGames.BinaryRenameMachine.initList_eq line 115
  12. theorem OAI.DFVSGames.BinaryRenameMachine.haltList_eq line 122
  13. theorem OAI.DFVSGames.BinaryRenameMachine.copyTrace line 129
  14. theorem OAI.DFVSGames.BinaryRenameMachine.restoreTrace line 146
  15. theorem OAI.DFVSGames.BinaryRenameMachine.headerTrace line 167
  16. theorem OAI.DFVSGames.BinaryRenameMachine.cleanupTrace line 191
  17. theorem OAI.DFVSGames.BinaryRenameMachine.outputBody_eq line 209
  18. theorem OAI.DFVSGames.BinaryRenameMachine.loopTrace line 224
  19. theorem OAI.DFVSGames.BinaryRenameMachine.joinTrace_inline_MachineBinaryRenameMachine line 267
  20. def OAI.DFVSGames.BinaryRenameMachine.steps line 271
  21. theorem OAI.DFVSGames.BinaryRenameMachine.renameTrace line 278
  22. theorem OAI.DFVSGames.BinaryRenameMachine.clause_count_le_stream line 297
  23. theorem OAI.DFVSGames.BinaryRenameMachine.body_length_le line 302
  24. def OAI.DFVSGames.BinaryRenameMachine.timePolynomial line 313
  25. theorem OAI.DFVSGames.BinaryRenameMachine.steps_le line 317
  26. def OAI.DFVSGames.BinaryRenameMachine.outputsInTime line 337
  27. def OAI.DFVSGames.BinaryRenameMachine.tokenComputation line 345
  28. def OAI.DFVSGames.BinaryRenameMachine.preprocessing line 358
  29. def OAI.DFVSGames.BinaryRenameMachine.computableInPolyTime line 368
  30. theorem OAI.DFVSGames.BinaryRenameMachine.machine_finiteAlphabet line 373
  31. theorem OAI.DFVSGames.BinaryRenameMachine.computation_finiteAlphabet line 377
  32. def OAI.DFVSGames.Foundations.Complexity.CookLevin.pairBits line 389
  33. def OAI.DFVSGames.Foundations.Complexity.CookLevin.decodePairAux line 392
  34. def OAI.DFVSGames.Foundations.Complexity.CookLevin.decodePair line 398
  35. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.decodePairAux_frame line 401
  36. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.decodePair_pairBits line 411
  37. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.pairBits_injective line 417
  38. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.pairBits_length line 422
  39. def OAI.DFVSGames.Foundations.Complexity.CookLevin.pairEncoding line 427
  40. structure OAI.DFVSGames.Foundations.Complexity.CookLevin.NPVerifier line 432
  41. def OAI.DFVSGames.Foundations.Complexity.CookLevin.NPVerifier.Accepts line 438
  42. def OAI.DFVSGames.Foundations.Complexity.CookLevin.InNP line 443
  43. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.NPVerifier.acceptedLanguage_inNP line 446
  44. structure OAI.DFVSGames.Foundations.Complexity.CookLevin.PolynomialThreeSATReduction line 449
  45. def OAI.DFVSGames.Foundations.Complexity.CookLevin.NPVerifier.horizon line 454
  46. theorem OAI.DFVSGames.Foundations.Complexity.CookLevin.NPVerifier.input_time_le_horizon line 458
  47. def OAI.DFVSGames.Foundations.Complexity.CookLevin.NPVerifier.runWithinHorizon line 467
  48. def OAI.DFVSGames.BinaryInputReduction.computation line 488
  49. theorem OAI.DFVSGames.BinaryInputReduction.computation_finiteAlphabet line 495
  50. def OAI.DFVSGames.BinaryInputReduction.reduction line 501
  51. theorem OAI.DFVSGames.BinaryInputReduction.reduction_finiteAlphabet line 506
  52. def OAI.DFVSGames.Outer.BinaryParityReduction.output line 523
  53. def OAI.DFVSGames.Outer.BinaryParityReduction.formulaMachine line 527
  54. theorem OAI.DFVSGames.Outer.BinaryParityReduction.formulaMachine_finite line 535
  55. def OAI.DFVSGames.Outer.BinaryParityReduction.computation line 543
  56. theorem OAI.DFVSGames.Outer.BinaryParityReduction.computation_finite line 550
  57. theorem OAI.DFVSGames.Outer.BinaryParityReduction.complete line 557
  58. theorem OAI.DFVSGames.Outer.BinaryParityReduction.sound line 569
  59. structure OAI.DFVSGames.Outer.BinaryParityReduction.Reduction line 581
  60. theorem OAI.DFVSGames.Outer.BinaryParityReduction.exists_reduction line 592
  61. theorem OAI.DFVSGames.Outer.BinaryParityReduction.failure_completeness line 600
  62. theorem OAI.DFVSGames.Outer.BinaryParityReduction.parity_soundness line 609
  63. theorem OAI.DFVSGames.Outer.BinaryParityReduction.ordinaryGame_soundness line 623
  64. inductive OAI.DFVSGames.Explicit.MachineSingleOrbitProgram.Tape line 645
  65. instance OAI.DFVSGames.Explicit.MachineSingleOrbitProgram.(instance at line 649) line 649
  66. abbrev OAI.DFVSGames.Explicit.MachineSingleOrbitProgram.State line 653
  67. def OAI.DFVSGames.Explicit.MachineSingleOrbitProgram.initialState line 655
  68. def OAI.DFVSGames.Explicit.MachineSingleOrbitProgram.clearKeys line 657
  69. inductive OAI.DFVSGames.Explicit.MachineSingleOrbitProgram.Label line 659
  70. def OAI.DFVSGames.Explicit.MachineSingleOrbitProgram.copyField line 667
  71. def OAI.DFVSGames.Explicit.MachineSingleOrbitProgram.program line 675
  72. def OAI.DFVSGames.Explicit.MachineSingleOrbitProgram.machine line 711
  73. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitProgram.finite_workAlphabet line 722
  74. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitProgram.accumulator_not_mem_clearKeys line 727
  75. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitProgram.output_not_mem_clearKeys line 728
  76. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitProgram.clearKeys_covers line 730
  77. def OAI.DFVSGames.Explicit.MachineSingleOrbitStreams.tapes line 744
  78. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitStreams.tapes_input line 752
  79. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitStreams.tapes_capacity line 753
  80. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitStreams.tapes_saved line 754
  81. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitStreams.tapes_remaining line 755
  82. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitStreams.tapes_accumulator line 756
  83. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitStreams.tapes_output line 757
  84. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitStreams.update_tapes line 759
  85. def OAI.DFVSGames.Explicit.MachineSingleOrbitStreams.cfg line 766
  86. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitStreams.copyStep_true line 770
  87. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitStreams.copyStep_false line 779
  88. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitStreams.copyFieldTrace line 788
  89. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitStreams.tableTrace line 805