OAI/Computability/MaxCut/Machines/MachinePortReindex.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.Alphabet line 13
  2. abbrev OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.State line 14
  3. def OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.clean line 16
  4. inductive OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.Label line 19
  5. def OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.exitAt line 25
  6. def OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.emit line 31

    Source documentation

    A residue-indexed literal instruction; its length is bounded by d+b.

    def emit (d : Nat) (positive : 0 < d) (output : K) (b : Nat)
    (r : Fin d) (next : Λ) : TM2.Stmt (Alphabet (K := K)) Λ (State A d) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.State

  7. def OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.instruction line 36
  8. def OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.steps line 57
  9. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.steps_le line 59
  10. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.steps_le_encodedLength line 64
  11. def OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.value line 70
  12. def OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.frame_inline_MachinePortReindex line 72
  13. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.joinTrace_inline_MachinePortReindex line 76
  14. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.reindexTrace line 83

    Source documentation

    Exact execution in any caller containing these finite instructions. The only changed caller tape is the output; the input field and all three initially empty work tapes are preserved exactly.

    theorem reindexTrace (d : Nat) (positive : 0 < d) (c b : Nat)
    (tape : Fin 5 → K) (distinct : Function.Injective tape)
    (labels : Label d → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State A d))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.Label, OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.State

  15. def OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.reindexInTime line 239
  16. def OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.machine line 258
  17. def OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.machineInTime line 269
  18. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePortReindex.lazy_value line 283