OAI/Computability/UniqueGames/Reduction/MachineReverse.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Reduction.MachineReverse.loop line 9
2. def OAI.UniqueGamesTheorem.Reduction.MachineReverse.machine line 15
3. def OAI.UniqueGamesTheorem.Reduction.MachineReverse.tapeStacks line 26
4. def OAI.UniqueGamesTheorem.Reduction.MachineReverse.running line 29
5. def OAI.UniqueGamesTheorem.Reduction.MachineReverse.halted line 32
6. theorem OAI.UniqueGamesTheorem.Reduction.MachineReverse.update_input line 35
7. theorem OAI.UniqueGamesTheorem.Reduction.MachineReverse.update_output line 40
8. theorem OAI.UniqueGamesTheorem.Reduction.MachineReverse.step_empty line 46

   Source documentation

   Popping an empty input resets the internal state to none before halting.

   theorem step_empty (output : List Bool) (state : Option Bool) :
       machine.step (running [] output state) = some (halted output) := by
   …

   Mentions: OAI.UniqueGamesTheorem.Reduction.MachineReverse.running, OAI.UniqueGamesTheorem.Reduction.MachineReverse.halted

9. theorem OAI.UniqueGamesTheorem.Reduction.MachineReverse.step_cons line 54

   Source documentation

   One transition moves the head symbol from the input onto the output.

   theorem step_cons (head : Bool) (input output : List Bool) (state : Option Bool) :
       machine.step (running (head :: input) output state) =
         some (running input (head :: output) (some head)) := by
   …

   Mentions: OAI.UniqueGamesTheorem.Reduction.MachineReverse.running

10. def OAI.UniqueGamesTheorem.Reduction.MachineReverse.next line 62
11. theorem OAI.UniqueGamesTheorem.Reduction.MachineReverse.reverse_steps line 66

    Source documentation

    An exact transition trace, with arbitrary initial accumulator and state.

    theorem reverse_steps (input output : List Bool) (state : Option Bool) :
        next^[input.length + 1] (some (running input output state)) =
          some (halted (input.reverse ++ output)) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineReverse.next, OAI.UniqueGamesTheorem.Reduction.MachineReverse.running, OAI.UniqueGamesTheorem.Reduction.MachineReverse.halted

12. theorem OAI.UniqueGamesTheorem.Reduction.MachineReverse.initList_eq line 80
13. theorem OAI.UniqueGamesTheorem.Reduction.MachineReverse.haltList_eq line 87
14. theorem OAI.UniqueGamesTheorem.Reduction.MachineReverse.reverse_init_steps line 92

    Source documentation

    The exact trace starts and ends at the standard encoded TM2 configurations.

    theorem reverse_init_steps (input : List Bool) :
        next^[input.length + 1] (some (initList machine input)) =
          some (haltList machine input.reverse) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineReverse.next, OAI.UniqueGamesTheorem.Reduction.MachineReverse.machine

15. def OAI.UniqueGamesTheorem.Reduction.MachineReverse.outputsInTime line 98
16. theorem OAI.UniqueGamesTheorem.Reduction.MachineReverse.outputsInTime_steps line 104
17. def OAI.UniqueGamesTheorem.Reduction.MachineReverse.computableInPolyTime line 108

    Source documentation

    Actual finite-machine polynomial-time computability, with identity encodings.

    noncomputable def computableInPolyTime :
        TM2ComputableInPolyTime (id : List Bool → List Bool) id List.reverse where
    …