OAI/Computability/UniqueGames/Machines/MachineCopy.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.Alphabet line 14
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.forkLoop line 17

    Source documentation

    Drain one tape into two reverse-order accumulators.

    def forkLoop (source left right : K) (fallback : β) (loopLabel : Λ) (exit : Option Λ) :
    TM2.Stmt (Alphabet (K := K) β) Λ (σ × Option β) :=
…

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

  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.forkTapes line 25
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.forkTapes_source line 30
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.forkTapes_left line 36
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.forkTapes_right line 41
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.forkTapes_self line 46
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.update_fork_source line 50
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.update_fork_left line 64
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.update_fork_right line 75
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.forkStep_empty line 81
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.forkStep_cons line 97
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.forkTrace line 116

    Source documentation

    Each symbol and the final empty test take one actual transition.

    theorem forkTrace (source left right : K)
    (sourceLeft : source ≠ left) (sourceRight : source ≠ right) (leftRight : left ≠ right)
    (fallback : β) (loopLabel : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K) β) Λ (σ × Option β))
…

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

  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.forkInTime line 143
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.drainedTapes line 163
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.restoredTapes line 166
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.copyTrace line 184
  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.copyInTime line 226

    Source documentation

    A timed witness whose stored step count is the exact two-loop trace length.

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

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