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

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The seven-row recorder applied to finite machine tables.

  1. def OAI.ForcedComputation.Recorder.ofMachine line 10
  2. def OAI.ForcedComputation.Recorder.originalConfiguration line 20
  3. theorem OAI.ForcedComputation.Recorder.originalConfiguration_step line 23
  4. theorem OAI.ForcedComputation.Recorder.workAt_ofMachine line 29
  5. def OAI.ForcedComputation.Recorder.initializedRecorder line 37
  6. theorem OAI.ForcedComputation.Recorder.recorder_halts_iff line 42

    Source documentation

    The recorder's finite initialized run has exactly the original machine's halting event, including a machine initially in a halting state.

    theorem recorder_halts_iff (I : Alternating.MachineInput) :
    (∃ m C q, Steps (ofMachine I.1) m (initializedRecorder I) C ∧
      C.control = Control.checkpoint q ∧ I.1.isHalting q = true) ↔ Alternating.Halts I := by
…

    Mentions: OAI.Alternating.MachineInput, OAI.ForcedComputation.Recorder.Steps, OAI.ForcedComputation.Recorder.ofMachine, OAI.ForcedComputation.Recorder.initializedRecorder, OAI.Alternating.Halts