OAI/Computability/UniqueGames/Reduction/MachineRhsLoad.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Reduction.MachineRhsLoad.State line 14
  2. abbrev OAI.UniqueGamesTheorem.Reduction.MachineRhsLoad.Alphabet line 15
  3. def OAI.UniqueGamesTheorem.Reduction.MachineRhsLoad.rhs line 17
  4. def OAI.UniqueGamesTheorem.Reduction.MachineRhsLoad.setRhs line 19
  5. theorem OAI.UniqueGamesTheorem.Reduction.MachineRhsLoad.rhs_setRhs line 22
  6. theorem OAI.UniqueGamesTheorem.Reduction.MachineRhsLoad.setRhs_setRhs line 25
  7. theorem OAI.UniqueGamesTheorem.Reduction.MachineRhsLoad.setRhs_same line 28
  8. def OAI.UniqueGamesTheorem.Reduction.MachineRhsLoad.fill line 30
  9. theorem OAI.UniqueGamesTheorem.Reduction.MachineRhsLoad.fill_apply line 33
  10. theorem OAI.UniqueGamesTheorem.Reduction.MachineRhsLoad.fill_all line 46
  11. def OAI.UniqueGamesTheorem.Reduction.MachineRhsLoad.finish line 56
  12. def OAI.UniqueGamesTheorem.Reduction.MachineRhsLoad.peekChain line 61
  13. def OAI.UniqueGamesTheorem.Reduction.MachineRhsLoad.statement line 69
  14. def OAI.UniqueGamesTheorem.Reduction.MachineRhsLoad.readRhs line 72
  15. theorem OAI.UniqueGamesTheorem.Reduction.MachineRhsLoad.stepAux_peekChain line 75
  16. theorem OAI.UniqueGamesTheorem.Reduction.MachineRhsLoad.stepAux_statement line 86
  17. theorem OAI.UniqueGamesTheorem.Reduction.MachineRhsLoad.readRhs_of_unary line 93
  18. theorem OAI.UniqueGamesTheorem.Reduction.MachineRhsLoad.loadStep line 103

    Source documentation

    One actual transition loads every RHS register while preserving all tapes, caller registers, and the existing optional head register.

    theorem loadStep (field : Fin k → K) (entry : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State k σ))
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineRhsLoad.Alphabet, OAI.UniqueGamesTheorem.Reduction.MachineRhsLoad.State

  19. def OAI.UniqueGamesTheorem.Reduction.MachineRhsLoad.loadInTime line 114
  20. theorem OAI.UniqueGamesTheorem.Reduction.MachineRhsLoad.peekChain_pushBound line 130
  21. theorem OAI.UniqueGamesTheorem.Reduction.MachineRhsLoad.statement_pushBound line 137