OAI/Computability/SpaceSimulation/Stack/Edit.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Some elementary SM programs and their space bounds. We move by popping into empty scratch stacks or onto stacks already in use; as long as the end stacks of such a drain fit, the intermediate writes fit. All lemmas here bound maximum height, not time.

  1. theorem OAI.Fifths.Store.ext' line 13
  2. def OAI.Fifths.Store.atX line 16
  3. def OAI.Fifths.Store.pre line 19
  4. theorem OAI.Fifths.Store.pre_nil line 22
  5. theorem OAI.Fifths.Store.pre_pre line 25
  6. def OAI.Fifths.Store.set line 32
  7. theorem OAI.Fifths.Store.set_ro line 35
  8. theorem OAI.Fifths.Store.set_same line 36
  9. theorem OAI.Fifths.Store.set_other line 37
  10. theorem OAI.Fifths.Store.set_set line 40
  11. theorem OAI.Fifths.Store.set_self line 42
  12. theorem OAI.Fifths.Store.set_swap line 43
  13. theorem OAI.Fifths.Store.set_ok line 53
  14. def OAI.Fifths.Store.drained line 60
  15. def OAI.Fifths.SM.editOne line 71
  16. theorem OAI.Fifths.SM.perform_one line 74
  17. def OAI.Fifths.SM.pop line 82

    Source documentation

    Destructively peek (return none on empty).

    def pop (k : K) : SM X J K (Option Bool) :=
…

    Mentions: OAI.Fifths.SM

  18. theorem OAI.Fifths.SM.exec_pop line 85
  19. def OAI.Fifths.SM.racks line 100

    Source documentation

    Push a fixed (top-first) string onto each selected stack.

    def racks (d : K → Bool) (b : Bool) : StChange J K :=
…

    Mentions: OAI.Fifths.StChange

  20. theorem OAI.Fifths.SM.racks_perform line 103
  21. def OAI.Fifths.SM.broadcast line 108
  22. theorem OAI.Fifths.SM.exec_broadcast line 112
  23. def OAI.Fifths.SM.onto line 132
  24. theorem OAI.Fifths.SM.pre_onto line 134
  25. def OAI.Fifths.SM.prepend line 138
  26. theorem OAI.Fifths.SM.exec_prepend line 139
  27. def OAI.Fifths.SM.drainBody line 148

    Source documentation

    All symbols of one source stack flow to a number of destinations (possibly zero), with each popped bit mapped to its own fixed code.

    def drainBody (k : K) (d : K → Bool) (code : Bool → List Bool) :
    SM X J K (Option Unit) :=
…

    Mentions: OAI.Fifths.SM

  28. def OAI.Fifths.SM.drain line 154
  29. theorem OAI.Fifths.SM.exec_drain line 158
  30. def OAI.Fifths.SM.clear line 211
  31. theorem OAI.Fifths.SM.exec_clear line 213
  32. def OAI.Fifths.SM.spill line 220
  33. theorem OAI.Fifths.SM.exec_spill line 221
  34. def OAI.Fifths.SM.rewind line 235

    Source documentation

    Rewind only the public head. Does not need a position counter.

    def rewind : SM X J K Unit :=
…

    Mentions: OAI.Fifths.SM

  35. theorem OAI.Fifths.SM.exec_rewind line 241