OAI/Computability/PerfectCompleteness/Machines/BinaryNameMachine.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.BinaryNameMachine.frame line 15
  2. def OAI.PerfectCompleteness.BinaryNameMachine.finalDigit line 19
  3. def OAI.PerfectCompleteness.BinaryNameMachine.canonical line 23
  4. structure OAI.PerfectCompleteness.BinaryNameMachine.Result line 25
  5. def OAI.PerfectCompleteness.BinaryNameMachine.scanSpec line 31
  6. def OAI.PerfectCompleteness.BinaryNameMachine.steps line 37
  7. theorem OAI.PerfectCompleteness.BinaryNameMachine.steps_le line 41
  8. theorem OAI.PerfectCompleteness.BinaryNameMachine.frame_length line 50
  9. theorem OAI.PerfectCompleteness.BinaryNameMachine.scanSpec_frame line 56
  10. theorem OAI.PerfectCompleteness.BinaryNameMachine.steps_frame line 65
  11. abbrev OAI.PerfectCompleteness.BinaryNameMachine.Alphabet line 75
  12. abbrev OAI.PerfectCompleteness.BinaryNameMachine.State line 76
  13. def OAI.PerfectCompleteness.BinaryNameMachine.clean line 78
  14. def OAI.PerfectCompleteness.BinaryNameMachine.exitAt line 80
  15. def OAI.PerfectCompleteness.BinaryNameMachine.finish line 85
  16. def OAI.PerfectCompleteness.BinaryNameMachine.scan line 88
  17. theorem OAI.PerfectCompleteness.BinaryNameMachine.stepAux_finish line 103
  18. theorem OAI.PerfectCompleteness.BinaryNameMachine.update_source line 108
  19. theorem OAI.PerfectCompleteness.BinaryNameMachine.update_destination line 119
  20. theorem OAI.PerfectCompleteness.BinaryNameMachine.step_empty line 133
  21. theorem OAI.PerfectCompleteness.BinaryNameMachine.step_end line 141
  22. theorem OAI.PerfectCompleteness.BinaryNameMachine.step_truncated line 152
  23. theorem OAI.PerfectCompleteness.BinaryNameMachine.step_digit line 160
  24. theorem OAI.PerfectCompleteness.BinaryNameMachine.scanTrace line 170
  25. def OAI.PerfectCompleteness.BinaryNameMachine.scanInTime line 204
  26. theorem OAI.PerfectCompleteness.BinaryNameMachine.framedTrace line 216
  27. def OAI.PerfectCompleteness.BinaryNameMachine.machine line 229
  28. theorem OAI.PerfectCompleteness.BinaryNameMachine.machine_finiteAlphabet line 240
  29. def OAI.PerfectCompleteness.BinaryNameMachine.machineInTime line 244