OAI/Computability/UniqueGames/Machines/MachineUnaryAffineAt.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.Alphabet line 15
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.finish line 17
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.scan line 20
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.seed line 30
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.tapes line 34
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.tapes_source line 38
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.tapes_scratch line 44
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.tapes_destination line 49
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.update_source line 54
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.update_scratch line 68
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.update_destination line 79
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.prepend_replicate_word line 85
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.scan_step_succ line 90
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.scan_step_zero line 110
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.scanTrace line 127
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.restoreTapes line 157
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.affineTrace line 176
  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.affineInTime line 212
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.seededAffineTrace line 234

    Source documentation

    Include the literal offset prefix. The caller supplies an arbitrary output suffix, not a precomputed address; all runtime arithmetic occurs on the tapes.

    theorem seededAffineTrace (source scratch destination : K)
    (hs : source ≠ scratch) (hd : source ≠ destination) (hsd : scratch ≠ destination)
    (coefficient offset : Nat) (seedLabel scanLabel restoreLabel : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.Alphabet

  20. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.Label line 268
  21. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.Label.enumList line 272
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.Label.enumList_getElem?_ctorIdx_eq line 274
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.Label.enumList_nodup line 278
  24. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.(instance at line 280) line 280
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.program line 284
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.machine line 290