OAI/Computability/SpaceSimulation/OneTape/Caps.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Fifths.Single.choiceSite line 10
2. theorem OAI.Fifths.Single.choice_at line 15
3. theorem OAI.Fifths.Single.cappedRegister line 22

   Source documentation

   Capped evaluator. All offsets, workspace reused.

   theorem cappedRegister (A : M.Sym) (d : ℕ)
       {x : I → List X} {S T a : I → ℕ}
       (q : Comp x S a T) (h : Scaled S (fun i => Cost.bound d (T i)))
       (l : ∃ B, ∀ i, M.Gives A (x i) (T i) (B*(S i+1))) :
       Tells x S a (fun i => M.outcome (x i) (T i)) := by
   …

   Mentions: OAI.Fifths.Single.q, OAI.Fifths.Comp, OAI.Fifths.Scaled, OAI.Fifths.Cost.bound

4. theorem OAI.Fifths.Single.capFits line 61
5. theorem OAI.Fifths.Single.stable line 66
6. theorem OAI.Fifths.Single.noCapRegister line 81

   Source documentation

   Unknown-time branch. Keep predicate is computed by a fully charged invocation; n below is a proof index for the represented call trajectory, not a program input.

   theorem noCapRegister (A : M.Sym) (d c : ℕ)
       {x : I → List X} {t : I → ℕ}
       (h : ∀ i, (M.outcome (x i) (t i)).2 = true)
       (p : ∀ i T, T ≥ 2 → M.Gives A (x i) T (c*(Cost.bound d T+1))) :
       Tells x (fun i => Cost.bound d (t i+2)) (fun _ => 0)
         (fun i => M.outcome (x i) (t i)) := by
   …

   Mentions: OAI.Fifths.Single.c, OAI.Fifths.Cost.bound