OAI/Computability/PerfectCompleteness/Machines/BinaryNameCompare.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.BinaryNameCompare.Alphabet line 17
  2. abbrev OAI.PerfectCompleteness.BinaryNameCompare.State line 18
  3. def OAI.PerfectCompleteness.BinaryNameCompare.clean line 20
  4. def OAI.PerfectCompleteness.BinaryNameCompare.scanStateEquiv line 22
  5. def OAI.PerfectCompleteness.BinaryNameCompare.compareStateEquiv line 28
  6. inductive OAI.PerfectCompleteness.BinaryNameCompare.Label line 34
  7. abbrev OAI.PerfectCompleteness.BinaryNameCompare.Label.enumList line 38
  8. theorem OAI.PerfectCompleteness.BinaryNameCompare.Label.enumList_getElem?_ctorIdx_eq line 40
  9. theorem OAI.PerfectCompleteness.BinaryNameCompare.Label.enumList_nodup line 44
  10. instance OAI.PerfectCompleteness.BinaryNameCompare.(instance at line 46) line 46
  11. def OAI.PerfectCompleteness.BinaryNameCompare.instruction line 50
  12. def OAI.PerfectCompleteness.BinaryNameCompare.steps line 63
  13. theorem OAI.PerfectCompleteness.BinaryNameCompare.steps_le line 66
  14. theorem OAI.PerfectCompleteness.BinaryNameCompare.joinTrace line 71
  15. theorem OAI.PerfectCompleteness.BinaryNameCompare.compareTrace line 75
  16. def OAI.PerfectCompleteness.BinaryNameCompare.compareInTime line 179
  17. def OAI.PerfectCompleteness.BinaryNameCompare.machine line 201
  18. theorem OAI.PerfectCompleteness.BinaryNameCompare.machine_finiteAlphabet line 214