OAI/Computability/SpaceSimulation/Stack/Lift.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Renamings / framing extra stacks, and presence of extra RO arguments.

  1. def OAI.Fifths.StChange.pad line 10
  2. def OAI.Fifths.Store.pad line 15
  3. theorem OAI.Fifths.Store.pad_st line 18
  4. theorem OAI.Fifths.Store.pad_st' line 21
  5. theorem OAI.Fifths.Store.pad_perform line 25
  6. theorem OAI.Fifths.Store.pad_ok line 38
  7. def OAI.Fifths.SM.pad line 52
  8. def OAI.Fifths.SM.padCfg line 60
  9. theorem OAI.Fifths.SM.pad_step line 63
  10. theorem OAI.Fifths.SM.pad_run line 77
  11. theorem OAI.Fifths.SM.pad_exec line 84
  12. def OAI.Fifths.SM.withArgs line 95

    Source documentation

    Preserve a program that never reads any arg tapes.

    def withArgs (J : Type) : SM X J K Y where
…

    Mentions: OAI.Fifths.SM

  13. def OAI.Fifths.SM.storeArgs line 103
  14. def OAI.Fifths.SM.argsCfg line 106
  15. theorem OAI.Fifths.SM.args_step line 109
  16. theorem OAI.Fifths.SM.args_exec line 124