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

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite support is sufficient for a fixed TM0 program to have a genuine finite table. Only the input word varies in this conversion.

  1. theorem OAI.ForcedComputation.FiniteMachine.exists_pointed_fin_equiv line 12
  2. theorem OAI.ForcedComputation.FiniteMachine.map_eval_dom line 20
  3. theorem OAI.ForcedComputation.FiniteMachine.finite_supported_TM0 line 34