OAI/Computability/UniqueGames/Machines/MachineControlLemmas.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Static renaming of labels and finite internal states. This does not execute a data-copying phase and preserves every actual transition exactly.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineControl.configuration line 17
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineControl.statement line 23
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineControl.stepAux_simulation line 38
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineControl.program line 65
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineControl.step_simulation line 70

    Source documentation

    The renamed program is conjugate to the original transition function, including the halted configuration.

    theorem step_simulation (labels : Λ ≃ Λ') (states : σ ≃ σ')
    (source : Λ → Stmt Γ Λ σ) (c : Cfg Γ Λ σ) :
    step (program labels states source) (configuration labels states c) =
      (step source c).map (configuration labels states) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineControl.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineControl.configuration

  6. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineEmbedding.Alphabet line 100
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineEmbedding.tapes line 104
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineEmbedding.tapes_inl line 109
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineEmbedding.tapes_inr line 112
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineEmbedding.label line 115
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineEmbedding.configuration line 119
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineEmbedding.statement line 126
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineEmbedding.tapes_update line 143
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineEmbedding.stepAux_simulation line 158

    Source documentation

    One finite statement executes identically on the original stacks and state. The entire statement is simulated in exactly one TM2 transition.

    theorem stepAux_simulation (haltTarget : Option (Λ ⊕ Λextra))
    (extraState : τ) (extraTapes : ∀ e, List (Δ e))
    (q : Stmt Γ Λ σ) (state : σ) (source : ∀ k, List (Γ k)) :
    stepAux (statement haltTarget q) (state, extraState) (tapes source extraTapes) =
      configuration haltTarget extraState extraTapes (stepAux q state source) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineEmbedding.statement, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineEmbedding.tapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineEmbedding.configuration

  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineEmbedding.stepAux_preserves_extra_state line 184
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineEmbedding.stepAux_preserves_extra_tape line 192
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineEmbedding.program line 200
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineEmbedding.step_running line 206
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineEmbedding.step_simulation line 219
  20. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStackSwap.Alphabet line 253
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStackSwap.tapes line 256
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStackSwap.tapes_first line 262
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStackSwap.tapes_second line 264
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStackSwap.tapes_third line 266
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStackSwap.tapes_involutive line 269
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStackSwap.configuration line 274
  27. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStackSwap.statement line 280
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStackSwap.tapes_update_first line 297
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStackSwap.tapes_update_second line 309
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStackSwap.tapes_update_third line 321
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStackSwap.stepAux_simulation line 333
  32. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStackSwap.program line 381
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStackSwap.step_simulation line 384