OAI/Computability/PerfectCompleteness/Machines/UnaryRepresentationMachine.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.UnaryRepresentationMachine.Alphabet line 14
  2. abbrev OAI.PerfectCompleteness.UnaryRepresentationMachine.State line 15
  3. inductive OAI.PerfectCompleteness.UnaryRepresentationMachine.RawLabel line 17
  4. abbrev OAI.PerfectCompleteness.UnaryRepresentationMachine.RawLabel.enumList line 21
  5. theorem OAI.PerfectCompleteness.UnaryRepresentationMachine.RawLabel.enumList_getElem?_ctorIdx_eq line 23
  6. theorem OAI.PerfectCompleteness.UnaryRepresentationMachine.RawLabel.enumList_nodup line 27
  7. instance OAI.PerfectCompleteness.UnaryRepresentationMachine.(instance at line 29) line 29
  8. inductive OAI.PerfectCompleteness.UnaryRepresentationMachine.EncodedLabel line 33
  9. abbrev OAI.PerfectCompleteness.UnaryRepresentationMachine.EncodedLabel.enumList line 37
  10. theorem OAI.PerfectCompleteness.UnaryRepresentationMachine.EncodedLabel.enumList_getElem?_ctorIdx_eq line 39
  11. theorem OAI.PerfectCompleteness.UnaryRepresentationMachine.EncodedLabel.enumList_nodup line 43
  12. instance OAI.PerfectCompleteness.UnaryRepresentationMachine.(instance at line 45) line 45
  13. def OAI.PerfectCompleteness.UnaryRepresentationMachine.encodedToRawMain line 49
  14. def OAI.PerfectCompleteness.UnaryRepresentationMachine.rawToEncodedMain line 50
  15. def OAI.PerfectCompleteness.UnaryRepresentationMachine.encodedToRawInstruction line 54
  16. def OAI.PerfectCompleteness.UnaryRepresentationMachine.rawToEncodedInstruction line 60
  17. theorem OAI.PerfectCompleteness.UnaryRepresentationMachine.encodedToRaw_pushBound line 68
  18. theorem OAI.PerfectCompleteness.UnaryRepresentationMachine.rawToEncoded_pushBound line 79
  19. theorem OAI.PerfectCompleteness.UnaryRepresentationMachine.encodedToRawTrace line 86
  20. def OAI.PerfectCompleteness.UnaryRepresentationMachine.encodedToRawInTime line 105
  21. theorem OAI.PerfectCompleteness.UnaryRepresentationMachine.seedStep line 120
  22. theorem OAI.PerfectCompleteness.UnaryRepresentationMachine.joinTrace line 130
  23. theorem OAI.PerfectCompleteness.UnaryRepresentationMachine.rawToEncodedTrace line 134
  24. def OAI.PerfectCompleteness.UnaryRepresentationMachine.rawToEncodedInTime line 164
  25. theorem OAI.PerfectCompleteness.UnaryRepresentationMachine.finiteState line 179
  26. theorem OAI.PerfectCompleteness.UnaryRepresentationMachine.finiteAlphabet line 182