OAI/Computability/UniqueGames/Machines/MachineExpanderTableReverse.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.clearRegister_position line 13
  2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.clearRegister_register line 16
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.clearRegister_idempotent line 19
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.boundaryTapes_reverse_update line 22
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.reverseOutputTrace line 40

    Source documentation

    Exact execution of the entire final reverse loop, including its empty test. No reversal-execution hypothesis is assumed.

    theorem reverseOutputTrace (positive : 0 < d) (H : Table (cloudSize d) d)
    (vertex remaining : Nat) (oldTable output countSuffix result : List Bool)
    (state : State ρ d) :
    (advance (TM2.step (program positive H)))^[output.length + 1]
      (some ⟨some (.inr .reverseOutput), state,
        boundaryTapes vertex remaining oldTable output countSuffix result⟩) =
      some ⟨some (.inr .done), clearRegister state,
        boundaryTapes vertex remaining oldTable [] countSuffix (output.reverse ++ result)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.boundaryTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.clearRegister

  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.reverseOutputHaltTrace line 73

    Source documentation

    The actual done statement halts one transition after reversal completes.

    theorem reverseOutputHaltTrace (positive : 0 < d) (H : Table (cloudSize d) d)
    (vertex remaining : Nat) (oldTable output countSuffix result : List Bool)
    (state : State ρ d) :
    (advance (TM2.step (program positive H)))^[output.length + 2]
      (some ⟨some (.inr .reverseOutput), state,
        boundaryTapes vertex remaining oldTable output countSuffix result⟩) =
      some ⟨none, clearRegister state,
        boundaryTapes vertex remaining oldTable [] countSuffix (output.reverse ++ result)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.boundaryTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.clearRegister

  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.reverseOutputInTime line 88
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.reverseOutputHaltInTime line 101