OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/ExpandingRecorderSupport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Finite tape windows grow by one cell per recorder instruction. The actual recorder step therefore appears in the finite stage graph.

  1. def OAI.ForcedComputation.ExpandingDetector.CenteredBlank line 14
  2. theorem OAI.ForcedComputation.ExpandingDetector.CenteredBlank.step line 18
  3. theorem OAI.ForcedComputation.ExpandingDetector.CenteredBlank.steps line 37
  4. theorem OAI.ForcedComputation.ExpandingDetector.CenteredBlank.coded_tails line 46
  5. def OAI.ForcedComputation.ExpandingDetector.configurationAddress line 59
  6. theorem OAI.ForcedComputation.ExpandingDetector.configurationAddress_step line 67
  7. theorem OAI.ForcedComputation.ExpandingDetector.initial_centeredBlank line 77
  8. theorem OAI.ForcedComputation.ExpandingDetector.initialized_steps_centeredBlank line 90