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

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The integer address of the actual reversible recorder configuration. The finite prefix is enlarged by one at every local instruction, and its integer update agrees with the full guarded table.

  1. def OAI.ForcedComputation.ExpandingDetector.codedTape line 14
  2. theorem OAI.ForcedComputation.ExpandingDetector.codedTape_left line 19
  3. theorem OAI.ForcedComputation.ExpandingDetector.codedTape_stay line 31
  4. theorem OAI.ForcedComputation.ExpandingDetector.codedTape_right line 41
  5. def OAI.ForcedComputation.ExpandingDetector.configurationStacks line 51
  6. theorem OAI.ForcedComputation.ExpandingDetector.configurationStacks_bounds line 56
  7. theorem OAI.ForcedComputation.ExpandingDetector.configurationStacks_read line 66
  8. theorem OAI.ForcedComputation.ExpandingDetector.configurationStacks_update line 77
  9. theorem OAI.ForcedComputation.ExpandingDetector.recorder_step_integer line 102