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

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The fixed observer for the program which includes its loader in every period. The fresh initial machine state makes every later loading row inert.

  1. theorem OAI.ForcedComputation.Recorder.periodic_flow_halting_iff line 12