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

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The executable recorder orbit and its halting equivalence.

  1. def OAI.ForcedComputation.Recorder.nextConfiguration line 11
  2. def OAI.ForcedComputation.Recorder.run line 16
  3. theorem OAI.ForcedComputation.Recorder.run_zero line 19
  4. theorem OAI.ForcedComputation.Recorder.run_succ line 21
  5. theorem OAI.ForcedComputation.Recorder.Step.next_eq line 25
  6. theorem OAI.ForcedComputation.Recorder.Steps.run_eq line 30
  7. theorem OAI.ForcedComputation.Recorder.reachable_has_successor_of_nonhalting line 36
  8. theorem OAI.ForcedComputation.Recorder.run_steps_of_nonhalting line 45
  9. theorem OAI.ForcedComputation.Recorder.run_step_of_nonhalting line 56
  10. theorem OAI.ForcedComputation.Recorder.run_halting_iff line 66