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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

One fixed finite interpreter and a computable input encoding. Arbitrary partial-recursive programs enter as input data, not as varying machine tables.

  1. theorem OAI.ForcedComputation.FiniteMachine.exists_universal_list_code line 14
  2. theorem OAI.ForcedComputation.FiniteMachine.fixed_list_TM0 line 24
  3. theorem OAI.ForcedComputation.FiniteMachine.exists_fixed_universal_TM0 line 73
  4. theorem OAI.ForcedComputation.FiniteMachine.exists_fixed_universal_machine line 83