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

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

A genuinely finite recorder alphabet and control set for a well-formed machine. The extra state is the normalized missing-instruction halt state.

  1. abbrev OAI.ForcedComputation.Recorder.State line 12
  2. abbrev OAI.ForcedComputation.Recorder.Alphabet line 13
  3. def OAI.ForcedComputation.Recorder.finiteMachine line 15
  4. def OAI.ForcedComputation.Recorder.forgetWork line 28
  5. theorem OAI.ForcedComputation.Recorder.forgetWork_next line 32
  6. def OAI.ForcedComputation.Recorder.initialState line 42
  7. def OAI.ForcedComputation.Recorder.initialAlphabet line 44
  8. theorem OAI.ForcedComputation.Recorder.finite_workAt line 49
  9. def OAI.ForcedComputation.Recorder.finiteInitializedRecorder line 58
  10. theorem OAI.ForcedComputation.Recorder.finite_recorder_halts_iff line 62
  11. def OAI.ForcedComputation.Recorder.allControls line 76
  12. def OAI.ForcedComputation.Recorder.allHistories line 83
  13. def OAI.ForcedComputation.Recorder.allSymbols line 87
  14. theorem OAI.ForcedComputation.Recorder.mem_allControls line 91
  15. theorem OAI.ForcedComputation.Recorder.mem_allHistories line 100
  16. theorem OAI.ForcedComputation.Recorder.mem_allSymbols line 107
  17. def OAI.ForcedComputation.Recorder.instructionTable line 117

    Source documentation

    Enumerate all control/read-symbol pairs by finite loops and execute the seven-row local interpreter. This is the finite table used by the geometry.

    def instructionTable (M : Alternating.Machine) (hM : M.WellFormed) :
    List ((Control (State M) (Alphabet M) × Symbol (State M) (Alphabet M)) ×
      (Control (State M) (Alphabet M) × Symbol (State M) (Alphabet M) × ℤ)) :=
…

    Mentions: OAI.Alternating.Machine, OAI.ForcedComputation.Recorder.Control, OAI.ForcedComputation.Recorder.State, OAI.ForcedComputation.Recorder.Alphabet, OAI.ForcedComputation.Recorder.Symbol

  18. theorem OAI.ForcedComputation.Recorder.evalLocal_sound line 123
  19. theorem OAI.ForcedComputation.Recorder.localStep_mem_instructionTable line 209
  20. theorem OAI.ForcedComputation.Recorder.mem_instructionTable_iff line 218