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

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The same finite TM0 table in the bounded-state presentation used by the rapid-forcing development.

  1. def OAI.ForcedComputation.FiniteMachine.rapidAction line 13
  2. def OAI.ForcedComputation.FiniteMachine.rapidTM0 line 20
  3. def OAI.ForcedComputation.FiniteMachine.eraseRapid line 29
  4. theorem OAI.ForcedComputation.FiniteMachine.val_update line 33
  5. theorem OAI.ForcedComputation.FiniteMachine.eraseRapid_step line 40
  6. theorem OAI.ForcedComputation.FiniteMachine.eraseRapid_initial line 71
  7. theorem OAI.ForcedComputation.FiniteMachine.eraseRapid_run line 86
  8. theorem OAI.ForcedComputation.FiniteMachine.rapidTM0_halts_iff line 96