OAI/Computability/PerfectCompleteness/Machines/BinaryLiteralMachine.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.BinaryLiteralMachine.Alphabet line 20
  2. abbrev OAI.PerfectCompleteness.BinaryLiteralMachine.State line 21
  3. abbrev OAI.PerfectCompleteness.BinaryLiteralMachine.clean line 22
  4. inductive OAI.PerfectCompleteness.BinaryLiteralMachine.Label line 25
  5. def OAI.PerfectCompleteness.BinaryLiteralMachine.searchTapes line 31
  6. theorem OAI.PerfectCompleteness.BinaryLiteralMachine.searchTapes_injective line 40
  7. def OAI.PerfectCompleteness.BinaryLiteralMachine.finish line 46
  8. def OAI.PerfectCompleteness.BinaryLiteralMachine.readSign line 52
  9. def OAI.PerfectCompleteness.BinaryLiteralMachine.emitSign line 60
  10. def OAI.PerfectCompleteness.BinaryLiteralMachine.instruction line 66
  11. def OAI.PerfectCompleteness.BinaryLiteralMachine.signWord line 86
  12. def OAI.PerfectCompleteness.BinaryLiteralMachine.index line 88
  13. def OAI.PerfectCompleteness.BinaryLiteralMachine.outputWord line 91
  14. def OAI.PerfectCompleteness.BinaryLiteralMachine.steps line 94
  15. theorem OAI.PerfectCompleteness.BinaryLiteralMachine.afterMatch_length_le line 100
  16. theorem OAI.PerfectCompleteness.BinaryLiteralMachine.steps_le line 109
  17. theorem OAI.PerfectCompleteness.BinaryLiteralMachine.stepAux_finish line 125
  18. theorem OAI.PerfectCompleteness.BinaryLiteralMachine.joinTrace line 129
  19. theorem OAI.PerfectCompleteness.BinaryLiteralMachine.literalTrace line 133
  20. def OAI.PerfectCompleteness.BinaryLiteralMachine.literalInTime line 303