OAI/Computability/SolenoidalRecorder/Machines.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Normalized finite machines and bounded work-head displacement.

  1. inductive OAI.Solenoidal.Move line 9
  2. abbrev OAI.Solenoidal.Move.enumList line 13
  3. theorem OAI.Solenoidal.Move.enumList_getElem?_ctorIdx_eq line 15
  4. theorem OAI.Solenoidal.Move.enumList_nodup line 19
  5. instance OAI.Solenoidal.(instance at line 22) line 22
  6. def OAI.Solenoidal.Move.displacement line 27
  7. theorem OAI.Solenoidal.Move.abs_displacement_le line 32
  8. structure OAI.Solenoidal.Machine line 37
  9. abbrev OAI.Solenoidal.Machine.State line 48
  10. abbrev OAI.Solenoidal.Machine.Symbol line 49
  11. structure OAI.Solenoidal.Machine.Config line 51
  12. def OAI.Solenoidal.Machine.step line 58
  13. def OAI.Solenoidal.Machine.inputTape line 64
  14. def OAI.Solenoidal.Machine.initialConfig line 67
  15. def OAI.Solenoidal.Machine.run line 70
  16. def OAI.Solenoidal.Machine.Halts line 73
  17. theorem OAI.Solenoidal.Machine.halts_of_initial line 76
  18. theorem OAI.Solenoidal.Machine.step_head_bound line 81
  19. theorem OAI.Solenoidal.Machine.run_succ line 90
  20. theorem OAI.Solenoidal.Machine.run_head_bound line 95
  21. abbrev OAI.Solenoidal.Machine.Instruction line 104
  22. def OAI.Solenoidal.Machine.Instruction.oldState line 109
  23. def OAI.Solenoidal.Machine.Instruction.read line 110
  24. def OAI.Solenoidal.Machine.Instruction.nextState line 111
  25. def OAI.Solenoidal.Machine.Instruction.write line 112
  26. def OAI.Solenoidal.Machine.Instruction.move line 113