OAI/Computability/UniqueGames/Machines/MachineAppendAt.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAppendAt.Alphabet line 14
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAppendAt.appendTapes line 16
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAppendAt.appendTapes_source line 20
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAppendAt.appendTapes_destination line 25
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAppendAt.appendTapes_other line 29
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAppendAt.appendTapes_scratch line 34
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAppendAt.firstTapes line 41
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAppendAt.secondTapes line 44
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAppendAt.finalTapes_eq line 48
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAppendAt.appendTrace line 70
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAppendAt.appendInTime line 141

    Source documentation

    The timed witness stores the exact three-loop transition count.

    def appendInTime (source destination scratch : K)
    (sourceDestination : source ≠ destination) (sourceScratch : source ≠ scratch)
    (destinationScratch : destination ≠ scratch)
    (fallback : β) (firstLabel secondLabel thirdLabel : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K) β) Λ (σ × Option β))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAppendAt.Alphabet