OAI/Computability/SpaceSimulation/Epoch/Theorem.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Fifths.Tour.visits line 10
2. theorem OAI.Fifths.Tour.finalDigit line 12
3. theorem OAI.Fifths.Tour.follows line 23

   Source documentation

   Epoch application. No simulation-specific assumptions beyond bounded words, uniform interface, and appropriate amount of space.

   theorem follows {I X : Type} {D : I → Tour} {x : I → List X} {S cp}
       (q : Runnable D x S cp) (g : ∀ i, (D i).FiniteWords)
       (h : Scaled S (fun i => (D i).E * (D i).per)) :
       Comp x S cp (fun i => ((D i).story (D i).visits).ctrl) := by
   …

   Mentions: OAI.Fifths.Tour, OAI.Fifths.Tour.Runnable, OAI.Fifths.Tour.FiniteWords, OAI.Fifths.Scaled, OAI.Fifths.Tour.E, OAI.Fifths.Tour.per, OAI.Fifths.Comp, OAI.Fifths.Tour.story, OAI.Fifths.Tour.visits