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

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Compile finite TM0 tables into the finite table presentation used by the fluid theorems. A move writes back the symbol that was read; a write uses the stationary move.

  1. def OAI.ForcedComputation.FiniteMachine.encodeAction line 15
  2. def OAI.ForcedComputation.FiniteMachine.compileTM0 line 21
  3. theorem OAI.ForcedComputation.FiniteMachine.compileTM0_stateCount line 24
  4. theorem OAI.ForcedComputation.FiniteMachine.compileTM0_symbolCount line 28
  5. theorem OAI.ForcedComputation.FiniteMachine.encodeAction_bounds line 32
  6. theorem OAI.ForcedComputation.FiniteMachine.compileTM0_wellFormed line 40
  7. theorem OAI.ForcedComputation.FiniteMachine.compileTM0_instruction line 53
  8. theorem OAI.ForcedComputation.FiniteMachine.compileTM0_not_halting line 63
  9. def OAI.ForcedComputation.FiniteMachine.compileTM0Input line 70
  10. theorem OAI.ForcedComputation.FiniteMachine.compileTM0Input_valid line 75