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

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The incoming row of the fresh checkpoint is unreachable. Removing this row leaves every actual recorder transition intact and frees a loader target.

  1. theorem OAI.ForcedComputation.freshMachine_normalized_nonzero line 12
  2. def OAI.ForcedComputation.Recorder.FreshControl line 28
  3. theorem OAI.ForcedComputation.Recorder.LocalStep.freshControl line 31
  4. theorem OAI.ForcedComputation.Recorder.LocalStep.not_fresh_checkpoint line 37
  5. theorem OAI.ForcedComputation.Recorder.Step.freshControl line 42
  6. theorem OAI.ForcedComputation.Recorder.Steps.freshControl line 49
  7. theorem OAI.ForcedComputation.Recorder.fresh_finiteMachine_next line 57
  8. theorem OAI.ForcedComputation.Recorder.fresh_recorder_never_returns line 65