OAI/Computability/UniqueGames/Machines/MachineProductSeed.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A finite literal setup sequence. Its list is fixed with the machine; no input word or unbounded address is stored in finite control.

  1. abbrev OAI.UniqueGamesTheorem.Explicit.MachineProductSeed.Command line 19
  2. abbrev OAI.UniqueGamesTheorem.Explicit.MachineProductSeed.LocalLabel line 20
  3. abbrev OAI.UniqueGamesTheorem.Explicit.MachineProductSeed.Label line 21
  4. def OAI.UniqueGamesTheorem.Explicit.MachineProductSeed.entry line 23
  5. def OAI.UniqueGamesTheorem.Explicit.MachineProductSeed.localInstruction line 26
  6. def OAI.UniqueGamesTheorem.Explicit.MachineProductSeed.instruction line 30
  7. def OAI.UniqueGamesTheorem.Explicit.MachineProductSeed.result line 34
  8. def OAI.UniqueGamesTheorem.Explicit.MachineProductSeed.finalTapes line 37
  9. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductSeed.sequence_steps line 40
  10. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductSeed.seedTrace line 49

    Source documentation

    Each literal has an actual one-transition trace in the ambient machine.

    theorem seedTrace (commands : List (Command K)) (labels : Label commands → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (σ × Option Bool))
    (atLabels : ∀ l, program (labels l) = instruction commands labels exit l)
    (base : K → List Bool) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[commands.length]
      (some ⟨entry commands labels exit, (ambient, register), base⟩) =
      some ⟨exit, (ambient, register), finalTapes commands base⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineProductSeed.Command, OAI.UniqueGamesTheorem.Explicit.MachineProductSeed.Label, OAI.UniqueGamesTheorem.Explicit.MachineProductSeed.instruction, OAI.UniqueGamesTheorem.Explicit.MachineProductSeed.entry, OAI.UniqueGamesTheorem.Explicit.MachineProductSeed.finalTapes

  11. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductSeed.finalTapes_frame line 67
  12. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductSeed.finalTapes_field line 77