OAI/Computability/SpaceSimulation/Stack/ToTM.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Compilation of stack space-bounded algorithms to Turing machines.

  1. def OAI.Fifths.Tape.packStack line 9
  2. theorem OAI.Fifths.Tape.packStack_see line 15
  3. theorem OAI.Fifths.Tape.packStack_pos line 17
  4. theorem OAI.Fifths.Tape.packStack_over line 19
  5. abbrev OAI.Fifths.StOp.Cell line 31
  6. def OAI.Fifths.StOp.first line 34

    Source documentation

    Empty has its head on a blank. All other heads read the top.

    def first (o : StOp) (r : Cell) : WriteMove Cell := match o with
…

    Mentions: OAI.Fifths.StOp, OAI.Fifths.StOp.Cell, OAI.Fifths.WriteMove

  7. def OAI.Fifths.StOp.second line 39
  8. def OAI.Fifths.StOp.middle line 42
  9. theorem OAI.Fifths.StOp.middle_pos line 45
  10. theorem OAI.Fifths.StOp.second_middle line 50
  11. def OAI.Fifths.SM.toTM line 84
  12. def OAI.Fifths.SM.encoded line 99
  13. def OAI.Fifths.SM.midCfg line 102
  14. def OAI.Fifths.SM.window line 106
  15. theorem OAI.Fifths.SM.toTM_step line 109
  16. theorem OAI.Fifths.SM.toTM_mid line 124
  17. theorem OAI.Fifths.SM.encoded_ok line 130
  18. theorem OAI.Fifths.SM.mid_ok line 135
  19. theorem OAI.Fifths.SM.toTM_run line 145
  20. def OAI.Fifths.SM.multiplier line 165
  21. theorem OAI.Fifths.SM.window_bits line 168
  22. theorem OAI.Fifths.SM.toTM_within line 170