OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/ConfigurationTapes.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact two-stream coordinates of a one-head tape update.

  1. def OAI.ForcedComputation.Recorder.tapeAt line 12
  2. theorem OAI.ForcedComputation.Recorder.tapeAt_right line 15
  3. theorem OAI.ForcedComputation.Recorder.tapeAt_stay line 33
  4. theorem OAI.ForcedComputation.Recorder.tapeAt_left line 47