OAI/Computability/UniqueGames/Machines/MachinePortReindex.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.Alphabet line 14
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.State line 15
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.clean line 17
  4. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.Label line 20
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.exitAt line 26
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.emit line 32

    Source documentation

    A residue-indexed literal instruction; its length is bounded by d+b.

    def emit (d : Nat) (positive : 0 < d) (output : K) (b : Nat)
    (r : Fin d) (next : Λ) : TM2.Stmt (Alphabet (K := K)) Λ (State A d) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.State

  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.instruction line 37
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.steps line 58
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.steps_le line 60
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.steps_le_encodedLength line 65
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.value line 71
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.frame line 73
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.joinTrace line 77
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.reindexTrace line 84

    Source documentation

    Exact execution in any caller containing these finite instructions. The only changed caller tape is the output; the input field and all three initially empty work tapes are preserved exactly.

    theorem reindexTrace (d : Nat) (positive : 0 < d) (c b : Nat)
    (tape : Fin 5 → K) (distinct : Function.Injective tape)
    (labels : Label d → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State A d))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.State

  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.reindexInTime line 240
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.machine line 259
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.machineInTime line 270
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.lazy_value line 284