OAI/Computability/SpaceSimulation/Register/External.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

TM access interface inside indexed register computations. Charge the arguments too. Tolerance of a scaled bound containing their lengths lets us go both directions.

  1. def OAI.Fifths.Bin.tuple line 15
  2. theorem OAI.Fifths.Bin.tuple_fits line 18
  3. def OAI.Fifths.SM.scatter line 34
  4. def OAI.Fifths.SM.spread line 38
  5. theorem OAI.Fifths.SM.spread_nil line 41
  6. theorem OAI.Fifths.SM.spread_cons line 42
  7. theorem OAI.Fifths.SM.spread_ro line 44
  8. theorem OAI.Fifths.SM.spread_outside line 48
  9. theorem OAI.Fifths.SM.spread_inside line 56
  10. theorem OAI.Fifths.SM.exec_scatter line 71
  11. theorem OAI.Fifths.Comp.tuple line 106
  12. theorem OAI.Fifths.Comp.call line 116

    Source documentation

    A standard binary-argument TM can take part in a computation. Input word remains the one bounded-read-only-head interface. This is used for calls to any fixed accessor.

    theorem call [Fintype J] [Fintype Y] (M : TM X J Y) (code : Y → ℕ)
    (p : Fits S a) {f : I → J → ℕ} (h : ∀ j, Comp x S a (fun i => f i j))
    {y : I → Y} (d : ℕ)
    (r : ∀ i, M.Within (binaryIn (x i) (f i)) (y i) (d*(S i+1))) :
    Comp x S a (fun i => code (y i)) := by
…

    Mentions: OAI.Fifths.TM, OAI.Fifths.Fits, OAI.Fifths.Comp