OAI/Computability/PerfectCompleteness/Machines/SourceCoordinateMachine.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.SourceCoordinateMachine.Alphabet line 15
  2. abbrev OAI.PerfectCompleteness.SourceCoordinateMachine.State line 16
  3. abbrev OAI.PerfectCompleteness.SourceCoordinateMachine.Signs line 17
  4. def OAI.PerfectCompleteness.SourceCoordinateMachine.lookupMap line 19
  5. def OAI.PerfectCompleteness.SourceCoordinateMachine.readerMap line 20
  6. def OAI.PerfectCompleteness.SourceCoordinateMachine.lookupTapes line 22
  7. def OAI.PerfectCompleteness.SourceCoordinateMachine.readerTapes line 23
  8. theorem OAI.PerfectCompleteness.SourceCoordinateMachine.lookupTapes_injective line 26
  9. theorem OAI.PerfectCompleteness.SourceCoordinateMachine.readerTapes_injective line 33
  10. inductive OAI.PerfectCompleteness.SourceCoordinateMachine.Label line 41
  11. def OAI.PerfectCompleteness.SourceCoordinateMachine.main line 47
  12. def OAI.PerfectCompleteness.SourceCoordinateMachine.instruction line 49
  13. def OAI.PerfectCompleteness.SourceCoordinateMachine.resultTapes line 59
  14. theorem OAI.PerfectCompleteness.SourceCoordinateMachine.result_variable line 64
  15. theorem OAI.PerfectCompleteness.SourceCoordinateMachine.result_original line 71
  16. def OAI.PerfectCompleteness.SourceCoordinateMachine.steps line 80
  17. theorem OAI.PerfectCompleteness.SourceCoordinateMachine.steps_le line 85
  18. theorem OAI.PerfectCompleteness.SourceCoordinateMachine.joinTrace line 98
  19. theorem OAI.PerfectCompleteness.SourceCoordinateMachine.coordinateTrace line 111
  20. def OAI.PerfectCompleteness.SourceCoordinateMachine.coordinateInTime line 192