OAI/Computability/Interspersed/Machines.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Finite transition tables and two-sided machine executions.

  1. inductive OAI.PrefixFlows.Move line 10
  2. def OAI.PrefixFlows.Move.displacement line 14
  3. def OAI.PrefixFlows.Move.code line 19
  4. structure OAI.PrefixFlows.Instruction line 24
  5. structure OAI.PrefixFlows.Machine line 32
  6. def OAI.PrefixFlows.Machine.WellFormed line 42
  7. def OAI.PrefixFlows.Machine.ValidInput line 50
  8. def OAI.PrefixFlows.Machine.code line 54
  9. def OAI.PrefixFlows.Machine.instruction line 59
  10. structure OAI.PrefixFlows.Machine.Configuration line 62
  11. def OAI.PrefixFlows.Machine.initial line 69
  12. def OAI.PrefixFlows.Machine.step line 74
  13. def OAI.PrefixFlows.Machine.run line 81
  14. def OAI.PrefixFlows.Machine.Halts line 86