OAI/Computability/SpaceSimulation/OneTape/Wander.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Local/global correspondence for a visit. Work in addresses [0,2T]. Arithmetic for neighboring positions saturates on raw calls, though it won't clamp an in-budget move on the represented trajectory. Run locally through the cap when halted too (advancing only tick).

  1. def OAI.Fifths.Single.capture line 16
  2. def OAI.Fifths.Single.glimpse line 19
  3. def OAI.Fifths.Single.stored line 21
  4. def OAI.Fifths.Single.view line 24
  5. def OAI.Fifths.Single.refresh line 28
  6. def OAI.Fifths.Single.localTable line 31
  7. def OAI.Fifths.Single.traceCtrl line 35
  8. def OAI.Fifths.Single.localStep line 40
  9. def OAI.Fifths.Single.chooseBlock line 48
  10. def OAI.Fifths.Single.sweep line 51
  11. def OAI.Fifths.Single.tour line 55
  12. theorem OAI.Fifths.Single.sym_lt line 67
  13. theorem OAI.Fifths.Single.stored_lt line 69
  14. theorem OAI.Fifths.Single.refresh_lt line 72
  15. theorem OAI.Fifths.Single.sweep_bounded line 80
  16. theorem OAI.Fifths.Single.tour_bounded line 91
  17. theorem OAI.Fifths.Single.rep_sym line 96

    Source comment

    Write correctness
    theorem rep_sym (W : Site) (f : ℤ → M.A) (p : Square W.T) :
    get (M.radix W.T) (M.stored W f (W.home p)) (W.slot p) =
      code (f (disp p)) := by
…

    Mentions: OAI.Fifths.Site, OAI.Fifths.Square

  18. theorem OAI.Fifths.Single.rep_write line 102
  19. def OAI.Fifths.Single.seenPos line 134
  20. def OAI.Fifths.Single.place line 136
  21. theorem OAI.Fifths.Single.so_select line 138
  22. theorem OAI.Fifths.Single.seenBack line 141
  23. theorem OAI.Fifths.Single.realize line 150

    Source documentation

    Single capped step from the representation, selected block in work space.

    theorem realize (x : List X) (W : Site) (n i : ℕ) (l : n < W.T)
    (h : M.place x W n = i) :
    M.localStep x W i ((M.view x W n).ctrl,(M.view x W n).cells i) =
       ((M.view x W (n+1)).ctrl,(M.view x W (n+1)).cells i)
    ∧ ∀ j, j ≠ i → (M.view x W n).cells j = (M.view x W (n+1)).cells j := by
…

    Mentions: OAI.Fifths.Site