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

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The bounded rapid-machine presentation embeds into a ragged lattice table by turning absent instructions into explicit transfers to a final empty row. Thus its terminal-state test is exactly the lattice stop test.

  1. def OAI.ForcedComputation.FiniteMachine.latticeAction line 12
  2. def OAI.ForcedComputation.FiniteMachine.latticeMachine line 18
  3. theorem OAI.ForcedComputation.FiniteMachine.latticeAction_bounds line 27
  4. theorem OAI.ForcedComputation.FiniteMachine.latticeMachine_lookup line 38
  5. theorem OAI.ForcedComputation.FiniteMachine.latticeMachine_terminal line 48
  6. theorem OAI.ForcedComputation.FiniteMachine.latticeMachine_wellFormed line 58
  7. def OAI.ForcedComputation.FiniteMachine.eraseLattice line 76
  8. theorem OAI.ForcedComputation.FiniteMachine.eraseLattice_step line 80
  9. theorem OAI.ForcedComputation.FiniteMachine.eraseLattice_initial line 109
  10. theorem OAI.ForcedComputation.FiniteMachine.eraseLattice_run line 120
  11. theorem OAI.ForcedComputation.FiniteMachine.latticeMachine_halts_iff line 131