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

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The full guarded recorder is injective on integer-stack configurations. Incoming direction is recovered from the target control; the new stacks then reveal the written symbol, and the seven-row inverse reveals the read symbol. No invariant of the selected computation is assumed.

  1. def OAI.ForcedComputation.ExpandingDetector.moveCode line 14
  2. def OAI.ForcedComputation.ExpandingDetector.IntegerStep line 16
  3. def OAI.ForcedComputation.ExpandingDetector.integerNext line 26
  4. theorem OAI.ForcedComputation.ExpandingDetector.IntegerStep.compiled line 32
  5. theorem OAI.ForcedComputation.ExpandingDetector.IntegerStep.successor_unique line 42
  6. theorem OAI.ForcedComputation.ExpandingDetector.IntegerStep.predecessor_unique line 54
  7. theorem OAI.ForcedComputation.ExpandingDetector.IntegerStep.target_bounds line 75