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

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Flattening the fixed finite interpreter into the alternating-flow input format changes only the storage layout of its transition table.

  1. def OAI.ForcedComputation.FiniteMachine.alternatingTM0 line 13
  2. theorem OAI.ForcedComputation.FiniteMachine.alternatingTM0_instruction line 21
  3. theorem OAI.ForcedComputation.FiniteMachine.alternatingTM0_wellFormed line 42
  4. def OAI.ForcedComputation.FiniteMachine.eraseAlternating line 53
  5. theorem OAI.ForcedComputation.FiniteMachine.alternating_configuration_ext line 57
  6. theorem OAI.ForcedComputation.FiniteMachine.eraseAlternating_step line 67
  7. theorem OAI.ForcedComputation.FiniteMachine.eraseAlternating_initial line 104
  8. theorem OAI.ForcedComputation.FiniteMachine.eraseAlternating_run line 120
  9. theorem OAI.ForcedComputation.FiniteMachine.alternatingTM0_halts_iff line 131